@Pierre-Marie Pédrot : I see that you do a lot of useful enhancements to Ltac2. Did you also think about a way to change a constr term with another constr term (not a pattern with a term)?
After the discussion about slow Qed I might remove a lot of change, but still this is something I miss in Ltac2.
P.S.: replace seems to be missing as well.
it's not hard to expose such a function, but there are way too many different semantics for term equality for it to be really general
Ltac1 implements constr-in-patterns as a horrendous hack
quite miraculously, it mangles the result enough to seem to be working on the average case
(typical issue that need to be pondered: how do you handle sorts?)
So looking at the recommendation of Jason regarding framing/casting computation to avoid slow Qed in (https://github.com/coq/coq/wiki/Troubleshooting#conversion-not-recorded-in-the-proof-trace): how would you do it in Ltac2?
I typically have either a term and an evaluated term and want to replace one with the other.
This use-case is much simpler, since you don't want to replace subterms, only change the whole goal.
This is very different because you don't have to rely on an equality function, you just use conversion.
Well I typically evaluate only subterms of the goal, but I could construct a term matching the complete goal.
The issue with just exact is, as Jason explained, that the Kernel might not be able to make sense out of it later during Qed in practically finite time. I currently have a case where I do a few (<10) rather innocent "change"s - say with a few minor changes in a list of length 10, and the kernel takes forever to type check the term in Qed (I aborted after 11 hours).
What Jason recommends is to use replace instead of change in order to factorize the type checking problem during Qed time.
But you can implement replace by rewriting over equality then.
Yes, true. Would it make a difference performance wise?
Probably not, replace is essentially a rewrite internally.
Or would it be faster if a construct an exact term based on "f_equalX"?
I have to check that pattern selection is performed the same way, but apart from that...
f_equal is probably going to help conversion
OK, then I build up a fine grain equality chain using f_equal or f_equal like lemmas. Should I try to get an exact in the end, or would a rewrite of the complete term be OK?
The complete term is largish.
my educated guess is that exact is going to be faster
since you won't have to do the work twice, you defer everything to conversion
pattern selection is a real hell
you need to be at the same time fast and intuitive
if you can get away without relying on pattern selection, you'll be faster always
I see. I will do a few experiments and let you know. The top level tactic is easy to change. The main complicatedness is in constructing the equality.
please do. I wouldn't be surprised that a handcrafted tactic can outperform rewrite-based solutions by orders of magnitude in degenerate cases
I guess for Qed it won't make a difference.
indeed, but it might for tactics
this kind of situation is precisely the raison d'être of low-level apis exported by Ltac2
Yes, I guess so. I would think that I can get the time VST currently takes for a medium complex C function down to a few seconds (currently it is minutes).
But then I have a case here of below average complexity where VST uses 20502 Ltac1 tactics (according to debug trace) for a single C instruction. It is rather a miracle that this takes only 2 seconds.
Last updated: Jan 31 2023 at 09:01 UTC