Stream: Ltac2

Topic: change term1 with term2


view this post on Zulip 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.

view this post on Zulip Michael Soegtrop (Mar 26 2021 at 08:58):

P.S.: replace seems to be missing as well.

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:00):

Ltac1 implements constr-in-patterns as a horrendous hack

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:01):

(typical issue that need to be pondered: how do you handle sorts?)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:46):

But you can implement replace by rewriting over equality then.

view this post on Zulip Michael Soegtrop (Mar 26 2021 at 09:46):

Yes, true. Would it make a difference performance wise?

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:47):

Probably not, replace is essentially a rewrite internally.

view this post on Zulip Michael Soegtrop (Mar 26 2021 at 09:47):

Or would it be faster if a construct an exact term based on "f_equalX"?

view this post on Zulip 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...

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:47):

f_equal is probably going to help conversion

view this post on Zulip 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?

view this post on Zulip Michael Soegtrop (Mar 26 2021 at 09:49):

The complete term is largish.

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:50):

my educated guess is that exact is going to be faster

view this post on Zulip 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

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:50):

pattern selection is a real hell

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:50):

you need to be at the same time fast and intuitive

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Michael Soegtrop (Mar 26 2021 at 09:52):

I guess for Qed it won't make a difference.

view this post on Zulip Pierre-Marie Pédrot (Mar 26 2021 at 09:52):

indeed, but it might for tactics

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip 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: Jan 31 2023 at 09:01 UTC