Jason Gross (Oct 19 2022 at 18:04): Jason Gross (Oct 19 2022 at 18:04):Following up on https://coq.zulipchat.com/#narrow/stream/237656-Coq-devs-.26-plugin-devs/topic/8.2E16.20regression.20in.20ssreflect.20apply/near/304985848
@Pierre-Marie Pédrot Is evarsolve aliasing the thing that makes instantiate (1:=t); reflexivity 4x faster than refine (@eq_refl T t) on page 34 of https://jasongross.github.io/presentations/coq-workshop-2022/superlinear-slowness.pdf? (/ https://jasongross.github.io/#superlinear-slowness) (code at https://github.com/mit-plv/bedrock2/releases/tag/2022-08-CoqWorkshop-011-LtacProf, look at the tip commit, which changes only bedrock2/src/bedrock2Examples/chacha20.v, to see the code resulting in the times reported on that slide -- the times in the commit message are 10x the times in the slide because I prefixed all the tactics being timed with do 10)
(You could plausibly extract a more-or-less small example out of this file for stressing evarsolve, though there are 97 goals with a couple-hundred binders in the context, so the example might not be that small.)
Jason Gross (Oct 19 2022 at 18:06):As for why evarsolve aliasing exists: do substitutions know about let binders? If not, do you need some form of aliasing to prevent superlinear blowup if there's an enormous number of let binders in the context, like
x1 : nat
x2 := x1 + x1
x3 := x2 + x2
...
x100 := x99 + x99
---------------
?e = x100
And you want ?e instantiated with x100 and not an enormous term?
Pierre-Marie Pédrot (Oct 19 2022 at 20:33):Substitutions do contain the let-binders. Aliasing is about finding the "best" representative in the class of equivalences of names up to variable unfolding.
Pierre-Marie Pédrot (Oct 19 2022 at 20:34):In particular, it doesn't do anything specific on your example.
Pierre-Marie Pédrot (Oct 19 2022 at 20:35):It triggers when you have chains of the form x₀ := x₁; x₁ := x₂; ...; xₙ-₁ := xₙ
Jason Gross (Oct 20 2022 at 00:49):@Pierre-Marie Pédrot Does it do anything specific on my example if ?e contains in its context x1 ... x95, but not x96 .. x100?
Or does it do refolding, like if I have ?e = x99 + x99 (and x100 is present in the context of ?e), will it choose x100?
Or what's an example where it does do something? (And how is "best" decided?)
Jason Gross (Oct 20 2022 at 08:13):I guess evarsolve aliasing is what makes this fast?
Goal nat -> True.
intro x.
do 100 let x' := fresh x in rename x into x'; pose (x' + x') as x.
pose x as y.
epose ?[e].
assert (?e = x).
instantiate (1:=ltac:(clearbody y)).
instantiate (1:=ltac:(do 50 match goal with x := _ |- _ => clear x end)).
Time reflexivity.
Last updated: May 31 2023 at 16:01 UTC