Generally, when you do a case analysis in a theorem prover, a lot of the cases boil down to "cannot happen". For example, if you are proving some fact about the integers, you may need to do a case analysis of whether the integer i is positive, zero, or negative. But there may be other hypotheses lying around in your context, or perhaps some part of your goal, that is contradictory with one of the cases. You may know from a previous assertion, for example, that i can never be negative.
However Coq is not that smart. So you still have to go through the mechanics of actually showing that the two contradictory hypotheses can be glued together into a proof of absurdity and hence a proof of your theorem.
Think about it like in a computer program:
switch (k) {
case X:
/* do stuff */
break;
case Y:
/* do other stuff */
break;
default:
assert(false, "can't ever happen");
}
The false = true goal is the "can't ever happen". But you can't just assert your way out in Coq. You actually have to put down a proof term.
So above, you have to prove the absurd goal false = true. And the only thing you have to work with is the hyothesis H: andb false c = true. A moment's thought will show you that actually this is an absurd hypothesis (because andb false y reduces to false for any y and hence cannot possibly be true). So you bang on the goal with the only thing at your disposal (namely H) and your new goal is false = andb false c.
So you apply an absurd hypothesis trying to achive an absurd goal. And lo and behold you end up with something you can actually show by reflexivity. Qed.
UPDATE Formally, here's what's going on.
Recall that every inductive definition in Coq comes with an induction principle. Here are the types of the induction principles for equality and the False proposition (as opposed to the term false of type bool):
Check eq_ind.
eq_ind
: forall (A : Type) (x : A) (P : A -> Prop),
P x -> forall y : A, x = y -> P y
Check False_ind.
False_ind
: forall P : Prop, False -> P
That induction principle for False says that if you give me a proof of False, I can give you a proof of any proposition P.
The induction principle for eq is more complicated. Let's consider it confined to bool. And specifically to false. It says:
Check eq_ind false.
eq_ind false
: forall P : bool -> Prop, P false -> forall y : bool, false = y -> P y
So if you start with some proposition P(b) that depends on a boolean b, and you have a proof of P(false), then for any other boolean y that is equal to false, you have a proof of P(y).
This doesn't sound terribly exiciting, but we can apply it to any proposition P that we want. And we want a particularly nasty one.
Check eq_ind false (fun b : bool => if b then False else True).
eq_ind false (fun b : bool => if b then False else True)
: (fun b : bool => if b then False else True) false ->
forall y : bool,
false = y -> (fun b : bool => if b then False else True) y
Simplifying a bit, what this says is True -> forall y : bool, false = y -> (if y then False else True).
So this wants a proof of True and then some boolean y that we get to pick. So let's do that.
Check eq_ind false (fun b : bool => if b then False else True) I true.
eq_ind false (fun b : bool => if b then False else True) I true
: false = true -> (fun b : bool => if b then False else True) true
And here we are: false = true -> False.
Combining with what we know about the induction principle for False, we have: if you give me a proof of false = true, I can prove any proposition.
So back to andb_true_elim1. We have a hypothesis H that is false = true. And we want to prove some kind of goal. As I've shown above, there exists a proof term that turns proofs of false = true into proofs of anything you want. So in particular H is a proof of false = true, so you can now prove any goal you want.
The tactics are basically machinery that builds the proof term.
discriminate. (I see it's an old post) – Fisken