Takeaway: the 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 destruct
.
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 orb_true_iff
. Since 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