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?
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.
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.
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).
You can use
change without a pattern to change the whole conclusion of your goal, is that what you're looking for?
simple apply (id Goal') generate a very similar proof term in size, but the former one is more idiomatic IMO.
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)`?
refine (_ : new_goal) should work too
Creative! I will have a look at the proof term of the different variants and see which I like best.
That is the proof term
change should generate, refine is kind of the most primitive tactic
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
Thanks, that is interesting! Is there a good reason why change explicitly removes the cast? @Jason Gross opened an issue declaring this as bug.
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.
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)
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.
I'm coming in late on this one, but I wonder why you just don't use
suff, etc...) closing the trivial subgoal by
exact (fun x => x) or ssr
Last updated: Jan 31 2023 at 13:02 UTC