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