## Stream: Coq users

### Topic: ✔ Destruct the application of an iff theorem directly?

#### Jiahong Lee (Jun 22 2022 at 00:27):

Takeaway: the `destruct` shorthand doesn't work with `orb_true_iff`. Use the long way: `apply <TERM> in <HYPOTHESIS>. destruct <HYPOTHESIS> as ...`

#### Notification Bot (Jun 22 2022 at 00:27):

Jiahong Lee has marked this topic as resolved.

#### Paolo Giarrusso (Jun 22 2022 at 03:31):

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.
``````

#### Paolo Giarrusso (Jun 22 2022 at 03:32):

For a slightly less compact proof:

``````Proof.
intros b [Hcontra|Hb]%orb_true_iff.
- discriminate Hcontra.
- apply Hb.
Qed.
``````

#### Jiahong Lee (Jun 22 2022 at 05:55):

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.
``````

#### Jiahong Lee (Jun 22 2022 at 05:57):

Takeway: You can destruct the application of an iff theorem with the `intros ...%<THEOREM>` pattern.

Last updated: Jan 29 2023 at 01:02 UTC