The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT lri.fr>]

On Thu, 28 Apr 2005, robert dockins wrote:

>
> The answer is yes.  The proof required a stronger induction principle
> and inversion lemma than the usual ones and some fancy dancing to avoid
> second-order unification.  The main interesting point of the development
> is the lemma:
>
> Lemma le_eq : forall (x y:nat) (p1 p2: x <= y), p1 = p2.
>
>
> Development attached for the curious.
>
> Robert Dockins
>

Hi Robert

Thanks for this nice proof. I would just like to add a comment:

When having a look at your file, I've noticed that you take advantage of
results in Eqdep.v. To my point of view, that's slightly unsatisfactory,
since this file relies on one axiom, the eq_rect_eq you use a few times.
This axiom is equivalent to the Uniqueness of Identity Proof (UIP)
discussed by Benjamin in his last mail:

  forall (U:Type) (x y:U) (p1 p2:x = y), p1 = p2.

Sure, this axiom is part of the Standard Library, hence harmless. But we
can in fact do without, since you only use it on nat, where UIP is
provable, as mentionned by Benjamin. (Btw: I tried at first to prove UIP
for nat by myself, before discovering that it's 1) really hard 2) already
done in Eqdep_dec.v)

The attached file contains a proof of le_eq with no use of axioms (plus a
few other stylistic changes).

Best regards,
Pierre Letouzey
Require Import Le.
Require Import Peano_dec.
Require Import Eqdep_dec.

Lemma nat_dec : forall n m:nat, n=m \/ n<>m.
intros; destruct (eq_nat_dec n m); [left|right]; auto.
Qed.

(* The UIP from Eqdep_dec specialized to nat: *)
Check (eq_proofs_unicity nat_dec).
 (* : forall (x y : nat) (p1 p2 : x = y), p1 = p2 *)

Scheme le_rec := Induction for le Sort Prop.

Lemma le_inversion :
  forall (x y:nat) (P:le x y),
    (exists H:x=y, P = (eq_rect x (le x) (le_n x) y H)) \/
    (exists y':nat, exists R:(S y') = y, exists H:(le x y'), 
        P = (eq_rect (S y') (le x) (le_S x y' H) y R)).
Proof.
intros x y P.
case P. (* No need here for the special le_rec *)
left.
exists (refl_equal x); auto.
intros m H.
right.
exists m.
exists (refl_equal (S m)).
exists H; auto.
Qed.

Lemma le_eq : forall (x y:nat) (p1 p2: x <= y), p1 = p2.
Proof.
intros x y p1.
elim p1 using le_rec.
intros p2.
(* I _love_ those complex intro patterns *)
destruct (le_inversion x x p2) as [(x0,H0)|(x0,(x1,(x2,_)))].
rewrite H0.
rewrite (eq_proofs_unicity nat_dec x0 (refl_equal x)); auto.
subst.
absurd (S x0 <= x0); auto with arith.

intros.
destruct (le_inversion x (S m) p2) as [(x0,H0)|(x0,(x1,(x2,H0)))].
absurd (S m <= m); auto with arith.
rewrite x0 in l.
assumption.

injection x1; intros; subst.
rewrite (H x2).
rewrite (eq_proofs_unicity nat_dec x1 (refl_equal (S m))); auto.
Qed.