The Coq mailing list

[Pierre Letouzey <Pierre.Letouzey AT pps.jussieu.fr>]

On Wed, Oct 15, 2008 at 07:30:49PM +0200, Julien Forest wrote:
> Dear all, 
> I wonder if one can manage to show proof irrelevance for le without
> using any axiom nor importing ProofIrrelevance library. 
> 
> At least, I want to be able to show that le is ProofIrrelevant enough
> to be changed in the exist construtor. 
> 
> 
> Julien
> 

Hello Julien, 

I've something like that in my archives, see below. Funny thing : it's
coming from an old thread on coq-club (but I'm too lazy to precisely
search which one ...)

Best,
Pierre

---------------------------------------------------------------------------

(** We have unicity of the proofs of le for nat
    Source: Coq-club
*)

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.

Check (eq_proofs_unicity nat_dec).

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)).

intros x y P.
case P.
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.
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.
assumption.

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