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
(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.)
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?
Substitutions do contain the let-binders. Aliasing is about finding the "best" representative in the class of equivalences of names up to variable unfolding.
In particular, it doesn't do anything specific on your example.
It triggers when you have chains of the form
x₀ := x₁; x₁ := x₂; ...; xₙ-₁ := xₙ
@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?)
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: Feb 06 2023 at 20:02 UTC