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