Michael Soegtrop (Mar 25 2021 at 09:57): Michael Soegtrop (Mar 25 2021 at 09:57):@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.
Michael Soegtrop (Mar 26 2021 at 08:58):P.S.: replace seems to be missing as well.
Pierre-Marie Pédrot (Mar 26 2021 at 08:59):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
Pierre-Marie Pédrot (Mar 26 2021 at 09:00):Ltac1 implements constr-in-patterns as a horrendous hack
Pierre-Marie Pédrot (Mar 26 2021 at 09:00):quite miraculously, it mangles the result enough to seem to be working on the average case
Pierre-Marie Pédrot (Mar 26 2021 at 09:01):(typical issue that need to be pondered: how do you handle sorts?)
Michael Soegtrop (Mar 26 2021 at 09:33):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.
Pierre-Marie Pédrot (Mar 26 2021 at 09:39):This use-case is much simpler, since you don't want to replace subterms, only change the whole goal.
Pierre-Marie Pédrot (Mar 26 2021 at 09:40):This is very different because you don't have to rely on an equality function, you just use conversion.
Michael Soegtrop (Mar 26 2021 at 09:45):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.
Pierre-Marie Pédrot (Mar 26 2021 at 09:46):But you can implement replace by rewriting over equality then.
Michael Soegtrop (Mar 26 2021 at 09:46):Yes, true. Would it make a difference performance wise?
Pierre-Marie Pédrot (Mar 26 2021 at 09:47):Probably not, replace is essentially a rewrite internally.
Michael Soegtrop (Mar 26 2021 at 09:47):Or would it be faster if a construct an exact term based on "f_equalX"?
Pierre-Marie Pédrot (Mar 26 2021 at 09:47):I have to check that pattern selection is performed the same way, but apart from that...
Pierre-Marie Pédrot (Mar 26 2021 at 09:47):f_equal is probably going to help conversion
Michael Soegtrop (Mar 26 2021 at 09:48):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?
Michael Soegtrop (Mar 26 2021 at 09:49):The complete term is largish.
Pierre-Marie Pédrot (Mar 26 2021 at 09:50):my educated guess is that exact is going to be faster
Pierre-Marie Pédrot (Mar 26 2021 at 09:50):since you won't have to do the work twice, you defer everything to conversion
Pierre-Marie Pédrot (Mar 26 2021 at 09:50):pattern selection is a real hell
Pierre-Marie Pédrot (Mar 26 2021 at 09:50):you need to be at the same time fast and intuitive
Pierre-Marie Pédrot (Mar 26 2021 at 09:51):if you can get away without relying on pattern selection, you'll be faster always
Michael Soegtrop (Mar 26 2021 at 09:51):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.
Pierre-Marie Pédrot (Mar 26 2021 at 09:52):please do. I wouldn't be surprised that a handcrafted tactic can outperform rewrite-based solutions by orders of magnitude in degenerate cases
Michael Soegtrop (Mar 26 2021 at 09:52):I guess for Qed it won't make a difference.
Pierre-Marie Pédrot (Mar 26 2021 at 09:52):indeed, but it might for tactics
Pierre-Marie Pédrot (Mar 26 2021 at 09:53):this kind of situation is precisely the raison d'être of low-level apis exported by Ltac2
Michael Soegtrop (Mar 26 2021 at 09:54):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).
Michael Soegtrop (Mar 26 2021 at 09:56):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: Oct 12 2024 at 12:01 UTC