destruct shorthand doesn't work with
orb_true_iff. Use the long way:
apply <TERM> in <HYPOTHESIS>. destruct <HYPOTHESIS> as ...
Jiahong Lee has marked this topic as resolved.
there is a different shorthand here:
Example lemma_application_ex2 : forall b : bool, false || b = true -> b = true. Proof. now intros b [[=]|H]%orb_true_iff. Qed.
For a slightly less compact proof:
Proof. intros b [Hcontra|Hb]%orb_true_iff. - discriminate Hcontra. - apply Hb. Qed.
Thanks! It is indeed what I'm looking for, although not by using
After digging around, docs about the notation can be found here.
To explain a bit, the notation
intros H%orb_true_iff will introduce the hypothesis
H after applying
H is a disjunction, you can use the
or intropattern to decompose it:
intros [H | H]%orb_true_iff. Proof:
Proof. intros b [H | H]%orb_true_iff. - discriminate H. - apply H. Qed.
Then for the first
H, instead of solving with
discriminate H, you can solve it directly with the
[=] intro pattern. Proof:
Proof. intros b [[=]| H]%orb_true_iff. apply H. Qed.
Takeway: You can destruct the application of an iff theorem with the
intros ...%<THEOREM> pattern.
Last updated: Jan 29 2023 at 01:02 UTC