Michael Soegtrop (Mar 30 2021 at 07:59): Michael Soegtrop (Mar 30 2021 at 07:59):I wonder what is the best way to change a lengthy goal with a convertible goal. I know I can use change to change parts of a goal, but it uses patterns und needs to search for what to replace. If I want to e.g. replace the right hand side of a lengthy equation, I guess this is not terribly efficient e.g. for tree structures, where the comparison can go quite deep before it fails in many places of the left hand side term. Also as discussed in the "Slow Qed" thread, complex change can lead to long Qed time. I am currently doing a "simple apply" or apply (in ltac2) of a lemma "forall P : Prop, P -> P" where I give the P explicitly. Is there a better way?
Enrico Tassi (Mar 30 2021 at 08:05):If you use ssr rewrite you can localize all rewritings, including a change, with a context pattern. In ssr's lingo, rewrite -[T in RHS]/(T') with first match _ = X against the goal (quick), then look for T inside X. Note: only terms which have the head constant of T verbatim are considered.
Enrico Tassi (Mar 30 2021 at 08:07):Of course, if you do it behind the scenes, a compact user syntax is not really needed. But I guess the idea of using a sequence of patterns with one named hole can still be used to make the code more flexible. RHS is just a notation for X in _ = X (X is a binder for a hole). I don't know ltac2 well enough to suggest how to represent that pattern, but there must be a way.
Michael Soegtrop (Mar 30 2021 at 09:28):The main question is: what is the best way to do this avoiding patterns all together. It is trivial to construct the complete modified goal, so why should I take it apart to math parts of it against the goal? I would think that replacing the complete goal should be both faster and safer (deep inside of automation).
Matthieu Sozeau (Mar 30 2021 at 09:47):You can use change without a pattern to change the whole conclusion of your goal, is that what you're looking for?
Enrico Tassi (Mar 30 2021 at 09:51):I see. change and simple apply (id Goal') generate a very similar proof term in size, but the former one is more idiomatic IMO.
Michael Soegtrop (Mar 30 2021 at 10:07):Ah thanks, I didn't know that change can be called without pattern.
Change has a downside, though: as Jason explained in the slow Qed thread, it doesn't leave an explicit cast in the proof term, which can lead to very long Qed times if the algorithm used to find the converted term is far away from what the kernel does (I have cases where Qed doesn't finish in 11 hours, although it took only seconds to construct the proof term).
So I guess I stick with "simple apply (id new_goal)`?
Gaëtan Gilbert (Mar 30 2021 at 10:09):refine (_ : new_goal) should work too
Michael Soegtrop (Mar 30 2021 at 10:17):Creative! I will have a look at the proof term of the different variants and see which I like best.
Enrico Tassi (Mar 30 2021 at 10:23):That is the proof term change should generate, refine is kind of the most primitive tactic
Gaëtan Gilbert (Mar 30 2021 at 10:27):change is more like let g := open_constr:(_ : new_goal) in let g := eval cbv in g in refine g or some such cast-removing operation
Michael Soegtrop (Mar 30 2021 at 10:38):Thanks, that is interesting! Is there a good reason why change explicitly removes the cast? @Jason Gross opened an issue declaring this as bug.
Jason Gross (Mar 30 2021 at 11:09):This is not how change is implemented under the hood, it's just the closest approximation in Ltac. It's not that change explicitly removes the cast, merely that it neglects to insert it in the first place.
Jason Gross (Mar 30 2021 at 11:14):Btw, yet another option is cbv beta; change new_goal (or if you have beta redexes, pick some dummy identifier not in your goal and go cbv delta [dummy]; change new_goal. This way cbv will record the goal for you and change will change it. If this doesn't speed things up in the way you want, you could try moving the cbv after the change (and this will record the new goal rather than the old one in the cast node)
Michael Soegtrop (Mar 30 2021 at 12:19):Thanks - using a dummy computation to insert a cast into the proof term is an interesting idea!
I didn't get much further as yet. I used the admit trick to nail it down to one VST tactic which increases the Qed time dramatically but this tactic does a few 100 changes - partly in hypothesis - and it takes a bit to remove / update / ... them all.
Cyril Cohen (Apr 01 2021 at 13:03):I'm coming in late on this one, but I wonder why you just don't use assert (or cut, have, suff, etc...) closing the trivial subgoal byexact (fun x => x) or ssr exact
Last updated: Oct 03 2023 at 02:34 UTC