Understanding Coq through a simple theorem proof

Question

I'm very new to Coq, and now I'm stuck trying to understand how Coq "reasons" with a simple theorem:

Theorem andb_true_elim2 : forall b c : bool,
  andb b c = true -> c = true.

I supposed that the proof would be just:

Proof.
  intros b c.
  destruct c.
    - destruct b.
     + reflexivity.
     + reflexivity.
    - destruct b.
     + reflexivity.
     + reflexivity.
  Qed.

But it fails with:

In environtment
H: true && false = true
Unable to unify "true" with "false"

The subgoal failing is the third reflexivity, where c is false and b is true:

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

Why is that? Wasn't it equivalent to an implication?

true && (false = true) -> (false = true)
true && false -> false
false -> false
true

Answer 1

There are a few issues with this proof. First, you misunderstood what Coq wanted; the actual goal was the following:

((true && false) = true) -> (false = true)

This does not follow by reflexivity, as the conclusion of this formula, false = true, is an equality between two syntactically different expressions.

Second, Coq does not simplify the operators -> and = in the manner you described. Coq's theory allows automatic simplification in a few select expressions, such as those defined by case analysis. For instance, && is syntactic sugar for the andb function, which is defined in the standard library as follows:

Definition andb b c :=
  if b then c else false.

When Coq sees an expression such as false && true, it expands it to the equivalent if false then true else false, which in turn simplifies to the else branch true. You can test this by calling the simpl tactic on the problematic branch.

The -> and = operators, on the other hand, are defined differently: the first one is a primitive in the logic, whereas the other one is a so-called inductive proposition. Neither of those can be automatically simplified in Coq, because they express concepts that are in general not computable: for instance, we can use = to express the equality of two functions f and g that take infinitely many natural numbers as inputs. This question discusses this difference in more detail.

If you want, you can state your theorem in a purely computable way with alternate definitions of implication and equality:

Definition negb b := if b then false else true.

Definition eqb b c := if b then c else negb c.

Definition implb b c := if b then c else true.

Lemma test : forall b c, (implb (eqb (andb b c) true) (eqb c true))
                         = true.
Proof. intros [] []; reflexivity. Qed.

However, a statement like this is generally harder to use in Coq.