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