The Coq mailing list

[Tadeusz Litak <tadeusz.litak AT gmail.com>]

May I suggest not sending all these questions to this mailing list before you finish at least the first volume of SF? Lots of them will be resolved as you read. For some other ones, you can easily consult the official documentation. Only when these two routes fail, ask here (and there is also the Coq IRC channel: irc://irc.freenode.net/#coq)

On 14/05/18 12:03, Gergely Buday wrote:

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