In an attempt to get a grasp what Coq is about, I ended up in a situation where I essentially need to prove that a=b -> nat_compare a b = Eq
.
I can get a handy start by doing:
Coq < Theorem foo: forall (a:nat) (b:nat), a=b->nat_compare a b=Eq.
1 subgoal
============================
forall a b : nat, a = b -> nat_compare a b = Eq
foo < intros. rewrite H. destruct b.
which gives me:
2 subgoals
a : nat
H : a = 0
============================
nat_compare 0 0 = Eq
subgoal 2 is:
nat_compare (S b) (S b) = Eq
The first is trivial:
foo < simpl. reflexivity.
But the next goal stumps me:
1 subgoal
a : nat
b : nat
H : a = S b
============================
nat_compare (S b) (S b) = Eq
I can do
foo < rewrite <- H.
which gives:
1 subgoal
a : nat
b : nat
H : a = S b
============================
nat_compare a a = Eq
(I can also arrive to this exact point by simpl
, which seems to make more sense.)
Now, with pen an paper, I'd just claim that here is my proof by induction..
Am I approaching this at all in a correct way? Where can I best learn how to do this properly?