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!

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

.

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

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.

Jiahong Lee has marked this topic as resolved.

Last updated: Oct 04 2023 at 23:01 UTC