Stream: Coq users

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

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!

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

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

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.

Notification Bot (Jun 07 2022 at 06:28):

Jiahong Lee has marked this topic as resolved.

Last updated: Oct 04 2023 at 23:01 UTC