f_equiv optimizations

This makes f_equiv a lot faster.

The first commit is inspired by looking at this line in Perennial: the very first f_equiv there takes 30s. 20s of that are spent in simple apply (_ : Proper (R ==> R) f), where f is bi_and <some complicated term> -- basically is tries to treat bi_and as a unary function and takes forever to realize that will not work. There is no TC trace for this, so this must be all unification time. By changing the pattern for this arm from ?R (?f _) _ to ?R (?f _) (?f _) we avoid entering it unless things match syntactically. This seeds up the first f_equiv from 30s to 10s.

The second commit is born from looking at that same line more, and also looking at the equivalent line in Iris itself: according to the ltac profiler, almost all time is spent in try simple apply reflexivity -- again, unification of inequal terms being very slow. So we now do entirely syntactic unification before even trying this. This speeds up the do 23 (f_contractive || f_equiv) in Iris from 1.3s to 0.6s, and it speeds up the do 22 (f_contractive || f_equiv) in Perennial to 0.75s from originally 42s (22s after the previous commit) -- a whopping 50x overall improvement!

Later commits slightly relax this to fix compatibility, so the fallback cases now do perform unification to match up the functions on the left-hand and right-hand side -- but this barely slows down the benchmarks mentioned above since they do not usually hit those cases. In fact, both in the Iris and Perennial case, 66% of the time is now spent in f_contractive.

theories/tactics.v

@@ -374,46 +374,60 @@ Ltac f_equiv :=
     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 *)
-  | |- ?R (?f _) _ => simple apply (_ : Proper (R ==> R) f)
-  | |- ?R (?f _ _) _ => simple apply (_ : Proper (R ==> R ==> R) f)
-  | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
-  | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
-  | |- ?R (?f _ _ _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R ==> R) f)
+  (* 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 _) _ => 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 _ ==> R _ ==> _) f)
-  | |- (?R _ _) (?f _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> _) f)
-  | |- (?R _ _ _) (?f _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> _) f)
-  | |- (?R _) (?f _ _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> _) f)
-  | |- (?R _ _) (?f _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> _) f)
-  | |- (?R _ _ _) (?f _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ R _ _ _ ==> _) f)
-  | |- (?R _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> _) f)
-  | |- (?R _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
-  | |- (?R _ _ _) (?f _ _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> _) f)
-  | |- (?R _) (?f _ _ _ _ _) _ => simple apply (_ : Proper (R _ ==> R _ ==> R _ ==> R _ ==> R _ ==> _) f)
-  | |- (?R _ _) (?f _ _ _ _ _) _ => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> R _ _ ==> _) f)
-  | |- (?R _ _ _) (?f _ _ _ _ _) _ => simple apply (_ : Proper (R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> R _ _ _ ==> _) f)
-  (* Next, try to infer the relation. Unfortunately, very often, it will turn
-     the goal into a Leibniz equality so we get stuck. *)
-  (* TODO: Can we exclude that instance? *)
+  | |- (?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)
-  (* In case the function symbol differs, but the arguments are the same,
-     maybe we have a relation about those functions in our context. *)
-  (* TODO: If only some of the arguments are the same, we could also
-     query for such relations. But that leads to a combinatorial
-     explosion about which arguments are and which are not the same. *)
-  | 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]
   end;
-  try simple apply reflexivity.
+  (* Only try reflexivity if the terms are syntactically equal. This avoids
+     very expensive failing unification. *)
+  try match goal with  |- _ ?x ?x => simple apply reflexivity end.
 Tactic Notation "f_equiv" "/=" := csimpl in *; f_equiv.
 
 (** The tactic [solve_proper_unfold] unfolds the first head symbol, so that