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.

changed the description

I think both the improvement in expressiveness (first commit) and performance (second and third commit) make a lot of sense.

• As you already suggested, it would be good to split up this MR into two parts.
• I think that for the uses cases in solve_proper the syntactic matching will be fine (i.e., cause no breakage).
• In other cases, I think this will break stuff. It's a bit weird that if you have a goal f ... = f ... where the implicit parameters of f are slightly different (which happens often with TC and CS), f_equiv no longer works.
• As mentioned on Mattermost, I once tried something similar to increase expressiveness. Your solution seems much simpler, but do the test cases in d16ab1aa also pass?

Yeah, I will add those testcases. However, Iris also fails to build with this, so I am not sure if the optimizations are feasible. Still it would be really nice to avoid all those expensive calls to unification... (partially because unification is probably the least debuggable performance issue in Coq^^).

added 1 commit

• c3468e6e - f_equiv: for consistency also match target relation in parametric case

Compare with previous version

added 3 commits

• 526924fe - f_equiv: do more syntactic matching before handing off to unification
• 26e00ff3 - f_equiv: do syntactic matching before attemtping reflexivity
• db316896 - f_equiv: for consistency also match target relation in parametric case

Compare with previous version

The first Iris failure was a stupid typo...

@@ -383,7 +383,7 @@ Ltac f_equiv :=
   (* 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 _ _ _ _) f)
 
   | |- (?R _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _) f)

added 1 commit

• 6da369d5 - f_equiv: for consistency also match target relation in parametric case

Compare with previous version

Argh, and more stupid typos...

--- a/theories/tactics.v
+++ b/theories/tactics.v
@@ -384,7 +384,7 @@ Ltac f_equiv :=
   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 _ _ _) f)
 
   | |- (?R _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ ==> R _ ==> R _) f)
   | |- (?R _ _) (?f _ _) (?f _ _) => simple apply (_ : Proper (R _ _ ==> R _ _ ==> R _ _) f)

This is so fragile^^

Okay now I think we are onto something; here is the Iris diff required for the current state of this MR: iris@2a13c733.

So, as you expected, some cases where f_equiv previous worked due to unification reasoning, but now stopped working.

And furthermore, auto became smarter in that iris/bi/internal_eq.v proof... and I have no idea why.^^

I will split the first commit into its own MR, so we can keep talking about the larger changes here. EDIT: That would be !326 (merged).

added 8 commits

• 6da369d5...7d5f3593 - 4 commits from branch master
• 875dacf5 - f_equiv: do more syntactic matching before handing off to unification
• 72bb9beb - f_equiv: do syntactic matching before attemtping reflexivity
• 1bab53e6 - f_equiv: for consistency also match target relation in parametric case
• d8024911 - reorder fallback cases, put them at the end, and update comments

Compare with previous version

added 1 commit

• a4ba9288 - try fallback cases last, and update comments

Compare with previous version

changed title from f_equiv improvements to f_equiv optimizations

changed the description

Okay I think I found a reasonable middle-ground in terms of where to call unification. The fallback cases (where the relation is inferred by TC search) now still 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. For Perennial:

total time:      0.930s

 tactic                                   local  total   calls       max 
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─f_contractive -------------------------   3.6%  66.1%      22    0.178s
─f_equiv -------------------------------  12.5%  33.9%      22    0.036s
─simple apply (_ : Proper (dist_later _   25.8%  29.7%      12    0.095s
─simple apply (_ : Proper (_ ==> dist_la  16.0%  19.0%      13    0.080s
─simple apply (_ : Proper (dist_later _   11.6%  13.8%      13    0.052s
─simple apply (_ : Proper (R ==> R) f) -  10.3%  11.7%      12    0.035s
─partial_application_tactic ------------   0.5%   9.0%       0    0.005s
─params --------------------------------   1.6%   7.6%      82    0.004s
─assert (H : Params m' v) by (subst m';    0.4%   5.7%      28    0.003s
─typeclasses eauto (nat_or_var_opt) ----   5.2%   5.2%      28    0.003s
─simple apply (_ : Proper (_ ==> R) f) -   4.0%   4.0%       8    0.006s

 tactic                                   local  total   calls       max 
────────────────────────────────────────┴──────┴──────┴───────┴─────────┘
─f_contractive -------------------------   3.6%  66.1%      22    0.178s
 ├─simple apply (_ : Proper (dist_later   25.8%  29.7%      12    0.095s
 │└partial_application_tactic ----------   0.2%   3.4%       0    0.004s
 │└params ------------------------------   0.7%   2.8%      12    0.003s
 │└assert (H : Params m' v) by (subst m'   0.2%   2.0%      12    0.003s
 ├─simple apply (_ : Proper (_ ==> dist_  16.0%  19.0%      13    0.080s
 │└partial_application_tactic ----------   0.1%   2.5%       0    0.004s
 └─simple apply (_ : Proper (dist_later   11.6%  13.8%      13    0.052s
─f_equiv -------------------------------  12.5%  33.9%      22    0.036s
 ├─simple apply (_ : Proper (R ==> R) f)  10.3%  11.7%      12    0.035s
 └─simple apply (_ : Proper (_ ==> R) f)   4.0%   4.0%       8    0.006s

The required patch in Iris is pretty reasonable now: iris@4f836b8e. That simpl turns some □?false l ↦{q} v into l ↦{q} v, which seems acceptable to me.

So, I think we can land this.

In lambda-rust we have a case where even with the new fallback cases, things still go wrong:

  Cinr (to_agree κ', (q1 + q2)%Qp) ≡ Cinr ((to_agree κ', q1) ⋅ (to_agree κ', q2))

The implicit parameter of Cinr is different, and in the fallback case it seems to not even consider Cinr_proper, probably because it is searching for @Proper (agree lft * Qp → ghosttoken_stR) and here agree lft * Qp is not an ofe (i.e. the instance only applies with a bit of cleverness):

Debug: 1.1: simple apply @Cinr_proper on
(@Proper (agree lft * Qp → ghosttoken_stR) (?R ==> @equiv ghosttoken_stR (ofe_equiv ghosttoken_stR))
   (@Cinr (exclR unitO) (agree lft * Qp))) failed with: Cannot unify (@Ofe 
                                                                       (?M13958 * ?M13959)
                                                                       (@prod_equiv 
                                                                       ?M13958 
                                                                       (ofe_equiv ?M13958) 
                                                                       ?M13959 
                                                                       (ofe_equiv ?M13959))
                                                                       (@prod_dist ?M13958 ?M13959)
                                                                       (@prod_ofe_mixin 
                                                                       ?M13958 
                                                                       ?M13959)) and 
(@Ofe ?M13953 (cmra_equiv ?M13953) (cmra_dist ?M13953) (cmra_ofe_mixin ?M13953))

I suspect apply: would work. Since this is a problem we have in many places, I am tempted to work around it locally rather than trying to tweak f_equiv.