Automatically fetch guess from local context
I have a proof script with a section that looks like this:
- destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence. - destruct (IHx1 _ _ H6). congruence. - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence. - destruct (IHx1 _ _ H6). congruence. - destruct (IHx _ _ H2). congruence. - destruct (IHx _ _ H5). congruence. - destruct (IHx _ _ H2). congruence. - destruct (IHx _ _ H8). congruence. - destruct (IHx _ _ H8). congruence. - destruct (IHx _ _ H8). congruence. - destruct (IHx _ _ H8). congruence. - destruct (IHx _ _ H7). congruence. - destruct (IHx _ _ H4). congruence. - destruct (IHx1 _ _ H8). congruence. - destruct (IHx1 _ _ H5). subst. destruct (IHx2 _ _ H9).
It looks like it would be a candidate of choice to use ;
to solve purely, unfortunately, hypotheses all over the place. How can I roll different sub-proofs together?
source to share
In cases where we only have one induction guess, we can solve it using the following piece of Ltac (see manual, chapter 9 ):
match goal with
IH : forall st2 s2, ?c / ?st \\ s2 / st2 -> _,
H : ?c / ?st \\ _ / _
|- _ => now destruct (IH _ _ H)
end
Where are the variables prefixed with question marks, for example. ?c
, ?st
etc. are meta-parameters that match patterns, individual hypotheses, and the turnstile symbol ( |-
) separates hypotheses from target. Here we are looking for an induction hypothesis IH
and a compatible hypothesis H
, so we can apply IH
to H
. The part ?c / ?st
provides compatibility IH
and H
.
Subgoals with two induction hypotheses can be solved in the same way:
match goal with
IH1 : forall st2 s2, ?c1 / ?st \\ s2 / st2 -> _,
IH2 : forall st2 s2, ?c2 / _ \\ s2 / st2 -> _,
H1 : ?c1 / ?st \\ _ / ?st'',
H2 : ?c2 / ?st'' \\ _ / st2
|- _ => now destruct (IH1 _ _ H1); subst; destruct (IH2 _ _ H2)
end
Of course, if you want to be able to bind names to these custom tactics, use tactics with them, and so on:
Ltac solve1 :=
try match goal with
IH : forall st2 s2, ?c / ?st || s2 / st2 -> _,
H : ?c / ?st || _ / _
|- _ => now destruct (IH _ _ H)
end.
source to share