I currently am at chapter 5 of "Software foundations" but felt the need to get back to chapter one to clarify a couple of things. In particular there is an exercise I did not quite digested, in which we are asked to use destruct twice to prove a result on booleans. Here it is with names and other details changed.
Inductive bool: Type :=
|true: bool
|false: bool.
Definition fb (b1:bool) (b2:bool) : bool :=
match b1, b2 with
| false, false => false
| _, _ => true
end.
Theorem th: forall a b: bool,
fb a b = false -> b = false.
Proof.
intros [] [] H.
- rewrite <- H. reflexivity.
- reflexivity.
- rewrite <- H. reflexivity.
- reflexivity.
Qed.
When at the first tick, context and goal are both nonsense:
H : fb true true = false
______________________________________(1/1)
true = false
Second tick the hypothesis is false. Third tick is same kind of nonsense as first one. Only fourth tick is reasonable with:
H : fb false false = false
______________________________________(1/1)
false = false
I understand that by the rewrite rules, all these things do work. However I have the impression we are quitting the narrow path of truth for the wilderness of falsity. More precisely, and AFAIK, a false hypothesis can be made to prove ANY statement, true or false. Here we use it to prove that false = true, OK why not, but still that makes me feel somewhat uncomfortable. I would not have expected a proof assistant to allow this.
Elaborating a bit
In a typical proof by contradiction, I would pick an hypothesis at random, and derive the goal till I find either a tautology or a contradiction. I would then conclude whether my hypothesis was true or false.
What happens here, in cases 1 (same for case 3), Coq starts from an hypothesis that is false:
H : fb true true = false
applies it to a goal that is a contradiction:
true = false
and combines them to find a tautology.
That is not a way of reasoning I am aware of. That recalls student 'jokes' where starting with 0=1 any absurd result on natural numbers can be proven.
Followup
So this morning during my commute I was thinking about what I had just written above. I now believe that cases 1 and 3 are proper proofs by contradiction. Indeed H is false and we use it to prove a goal that is a false. Hypotheses (values of a and b) have to be rejected. What may have confused me is that using rewrite we are doing part of the way "backward", starting from the goal.
I am a bit undecided for case 2, which reads:
H : fb true false = false
______________________________________(1/1)
false = false
which is basically false -> true
, a tautology under the "principle of explosion". I would not think that could be used so directly in a proof.
Oh well, not sure I completely understood what's under the hood, but trust in Coq is untouched. Gotta go on and return to chapter 5. Thanks all for your comments.
0=1
Indeed, it is easy to see that from that, you can prove that any two numbers are equal, and indeed you can prove any statement! Is that magic? No, it is not. In fact, you could think of it as "eliminating impossible cases". Imagine you are trying to prove something for positive numbers, thus you havex > 0
, then, when you apply induction, you will get0>0
which is not possible, so in a sense, you are done. – ejgallego