(* stdpp/tactics.v *)
(* f_equiv works on goals of the form [f _ = f _], for any relation and any
number of arguments. It looks for an appropriate [Proper] instance, and applies
it. The tactic is somewhat limited, since it cannot be used to backtrack on
the Proper instances that has been found. To that end, we try to avoid the
trivial instance in which the resulting goals have an [eq]. More generally,
we try to "maintain" the relation of the current goal. For example,
when having [Proper (equiv ==> dist) f] and [Proper (dist ==> dist) f], it will
favor the second because the relation (dist) stays the same. *)
Ltac f_equiv
:=
  (* Simplify away [flip], they would get in the way later. *)
  clean_flip;
  (* Find out what kind of goal we have, and try to make progress. *)
  match goal with
  (* Similar to [f_equal] also handle the reflexivity case. *)
  | |- _ ?x ?x => fast_reflexivity
  (* Making progress on [pointwise_relation] is as simple as introducing the variable. *)
  | |- pointwise_relation _ _ _ _ => intros ?
  (* We support matches on both sides, *if* they concern the same variable, or
     terms in some relation. *)
  | |- ?R (match ?x with _ => _ end) (match ?x with _ => _ end) =>
    destruct x
  | H : ?R ?x ?y |- ?R2 (match ?x with _ => _ end) (match ?y with _ => _ end) =>
     destruct H
  (* First assume that the arguments need the same relation as the result. We
  check the most restrictive pattern first: [(?f _) (?f _)] requires all but the
  last argument to be syntactically equal. *)
  | |- ?R (?f _) (?f _) => simple apply (_ : Proper (R ==> R) f)
  | |- ?R (?f _ _) (?f _ _) => simple apply (_ : Proper (R ==> R ==> R) f)
  | |- ?R (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
  | |- ?R (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
  | |- ?R (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R ==> R) f)
  (* For the case in which R is polymorphic, or an operational type class,
  like equiv. *)
  | |- (?R _) (?f _) (?f _) => simple apply (_ : Proper (R _ ==> R _) f)
  | |- (?R _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ ==> R _ _) f)
  | |- (?R _ _ _) (?f _) (?f _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _) f)

  | |- (?R _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _) f)
  | |- (?R _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _) f)
  | |- (?R _ _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _) f)

  | |- (?R _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _) f)
  | |- (?R _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
  | |- (?R _ _ _) (?f _ _ _) (?f _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)

  | |- (?R _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _) f)
  | |- (?R _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
  | |- (?R _ _ _) (?f _ _ _ _) (?f _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)

  | |- (?R _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _ ==> R _) f)
  | |- (?R _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _) f)
  | |- (?R _ _ _) (?f _ _ _ _ _) (?f _ _ _ _ _) => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _) f)
  (* In case the function symbol differs, but the arguments are the same, maybe
     we have a relation about those functions in our context that we can simply
     apply. (The case where the arguments differ is a lot more complicated; with
     the way we typically define the relations on function spaces it further
     requires [Proper]ness of [f] or [g]). *)
  | H : _ ?f ?g |- ?R (?f ?x) (?g ?x) => solve [simple apply H]
  | H : _ ?f ?g |- ?R (?f ?x ?y) (?g ?x ?y) => solve [simple apply H]

  (* Fallback case: try to infer the relation, and allow the function to not be
     syntactically the same on both sides. Unfortunately, very often, it will
     turn the goal into a Leibniz equality so we get stuck. Furthermore, looking
     for instances in this order will mean that Coq will try to unify the
     remaining arguments that we have not explicitly generalized, which can be
     very slow -- but if we go for the opposite order, we will hit the Leibniz
     equality fallback instance even more often. *)
  (* TODO: Can we exclude that Leibniz equality instance? *)
  | |- ?R (?f _) _ => simple apply (_ : Proper (_ ==> R) f)
  | |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)
  | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
  | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
  | |- ?R (?f _ _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> _ ==> R) f)
  end;
  (* Similar to [f_equal] immediately solve trivial goals *)
  try fast_reflexivity.