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.

2. 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: Apr 16 2024 at 12:01 UTC