Stream: Coq users

Topic: ✔ Show that (false -> Q) holds?


view this post on Zulip Jiahong Lee (Jun 07 2022 at 05:38):

Hi, I'm very new and self-learning Coq. Here is a proving exercise:

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  Admitted.

Informally, I can see that andb b c = true is True iff b = true and c = true. And thus andb b c = true -> c = true holds. Then, for all the other cases, andb b c = true should be False, and thus the implication should be vacuously True. Qed.

I've managed to prove it in Coq, but I found my proof to be rather cumbersome/mechanical, mainly because Coq doesn't know that false -> Q for all Q is vacuously True. Thus, I wonder whether there is a more elegant way to prove it?

My solutions:

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros b [] H.
  - reflexivity.
  - rewrite <- H.
    destruct b eqn:Eb.
    -- reflexivity.
    -- simpl andb.
       reflexivity.
Qed.

Theorem andb_true_elim2' : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros [] [] H.
  - reflexivity.
  - rewrite <- H.
    reflexivity.
  - reflexivity.
  - rewrite <- H.
    reflexivity.
Qed.

Thanks!

view this post on Zulip Guillaume Melquiond (Jun 07 2022 at 05:46):

You only need to destruct b. Indeed, in the first case, you will get c = true -> c = true, while in the second case you will get false = true -> c = true. In both cases, you can use the easy tactic to conclude. So, the whole proof can be reduced to intros [] ; easy or equivalently now intros [].

view this post on Zulip Guillaume Melquiond (Jun 07 2022 at 05:50):

To expand a bit, easy combines simple tactics such as assumption (which takes care of the first case) and discriminate (which takes care of the second case).

view this post on Zulip Jiahong Lee (Jun 07 2022 at 06:25):

Thanks, discriminate does the job for me. My updated solution:

Theorem andb_true_elim2'' : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros [].
  - simpl andb.
    intros c H.
    apply H.
  - discriminate.
Qed.

As for easy and now, they are too much magic for me right now. So, I'll leave them for future usage.

view this post on Zulip Notification Bot (Jun 07 2022 at 06:28):

Jiahong Lee has marked this topic as resolved.


Last updated: Jun 25 2024 at 19:01 UTC