The Coq mailing list

[Théo Zimmermann <theo.zimmi AT gmail.com>]

In this case I would recommend using discriminate after intro. That's the most adapted (and most basic) tactic here.

But I concur with the previous remark: you can search a bit more before asking questions here. You may also have a look at Stack Overflow where many similar questions are already answered.

In particular, this question was already discussed there: https://stackoverflow.com/questions/42355062/proof-on-booleans-false-true

(I found it again by searching "[coq] false = true" in Stack Overflow search bar.)

Théo

Le lun. 14 mai 2018 à 12:15, Saulo Araujo <saulo2 AT gmail.com> a écrit :

I believe intros. trivial. should do Theo job.

Em seg, 14 de mai de 2018 07:03, Gergely Buday <gbuday AT gmail.com> escreveu:

Hi,

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.
Proof.
  intros  b c. destruct c.
  - reflexivity.
  - destruct b.
    + simpl.

leads to

1 subgoal
______________________________________(1/1)
false = true -> false = true

which is clearly true but I do not see how this can be resolved with
the tools mentioned in Software Foundations.

I would think of both the premise and the conclusion evaluates to the
builtin_false constant because of the nature of inductive definitions

and then by the usual truth table line

  builtin_false -> builtin_false

should be true.

How can I make this work in Coq?

- Gergely