## Stream: Coq users

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

#### Jiahong Lee (Jun 20 2022 at 07:57):

Hi, I have a question with this example.

Given this

``````Theorem orb_true_iff : forall b1 b2,
b1 || b2 = true <-> b1 = true \/ b2 = true.
``````

the example proves by first "specialising" the theorem, then demonstrates how one can use `destruct` on an applied theorem:

``````Lemma orb_true : forall b1 b2 : bool,
b1 || b2 = true -> b1 = true \/ b2 = true.
Proof.
intros b1 b2. apply orb_true_iff.
Qed.

Example lemma_application_ex2' : forall b : bool,
false || b = true -> b = true.
Proof.
intros b H. destruct (orb_true _ _ H) as [Hcontra | Hb].
- discriminate Hcontra.
- apply Hb.
Qed.
``````

My questions are:

1. Why can't I apply `destruct` with `orb_true_iff` directly?

My attempt

``````Example lemma_application_ex2 : forall b : bool,
false || b = true -> b = true.
Proof.
intros b H. destruct (orb_true_iff false _ H) as [Hcontra | Hb].
...
Qed.
``````

fails with the error message:

``````Error: Illegal application (Non-functional construction):
The expression "orb_true_iff false ?b2" of type "false || ?b2 = true <-> false = true \/ ?b2 = true"
cannot be applied to the term
"H" : "false || b = true"
``````

which is confusing. It seems to me perfectly fine for Coq to substitute `b` into the `?b2` of `orb_true_iff`, then figure out I'm trying to apply `->` of the bidirectional.

1. Can I apply the `->` version of the `orb_true_iff` theorem to bypass the error message? If so, how?

Thanks!

#### Michael Soegtrop (Jun 20 2022 at 08:11):

`A <-> B` means `A->B /\ B->A`. So unlike an implication `A -> B` the propositional equivalence `A <-> B` is not a functional construct. For this reason you cannot apply it to `H`. If `orb_true_iff` would be an implication rather than an `<->` this would work.

#### Jiahong Lee (Jun 21 2022 at 00:36):

Michael Soegtrop said:

`A <-> B` means `A->B /\ B->A`. So unlike an implication `A -> B` the propositional equivalence `A <-> B` is not a functional construct. For this reason you cannot apply it to `H`. If `orb_true_iff` would be an implication rather than an `<->` this would work.

Hmm, that's intriguing.

With `orb_true_iff`, I can prove it as such:

``````Example lemma_application_ex2' : forall b : bool,
false || b = true -> b = true.
Proof.
intros b H. apply orb_true_iff in H. destruct H as [Hcontra | Hb].
- discriminate Hcontra.
- apply Hb.
Qed.
``````

And the given example above can also be rewritten as such:

``````Example lemma_application_ex2' : forall b : bool,
false || b = true -> b = true.
Proof.
intros b H. apply orb_true in H. destruct H as [Hcontra | Hb].
- discriminate Hcontra.
- apply Hb.
Qed.
``````

As you can see, there is a similarity between the two. So as a user, I would expect both to work with the `destruct (orb_true _ _ H) as [...]` shorthand... And from your answer, it seems like there is no way for the `destruct` shorthand to work with `orb_true_iff`?

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

UPDATE: Read below.

#### 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: Jun 25 2024 at 15:02 UTC