CODEWITHSUNDEEP
coqtheorem-proving
aleator
aleator

Reputation: 4486

Coq: How to prove "a=b -> nat_compare a b = Eq."?

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?

Upvotes: 1

Views: 411

Answers (1)

daniel gratzer
daniel gratzer

Reputation: 53871

I was able to prove this with

Theorem triv : forall a b, a = b -> nat_compare a b = Eq.
  intros; subst; induction b; auto.
Qed.

The trick here is to leave the inductive hypothesis lying around. destruct is a weaker form of induction that doesn't give you an inductive hypothesis which you need for this proof.

Upvotes: 2

Related Questions