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:

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

- Can I apply the
`->`

version of the`orb_true_iff`

theorem to bypass the error message? If so, how?

Thanks!

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

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`

?

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.

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