The Coq mailing list

[Santiago Zanella <Santiago.Zanella AT sophia.inria.fr>]

In fact, you don't need any axiom to prove proof irrelevance for [lt]. 
Here's an axiom-free proof, inspired by a recent message on the list by
Pierre Letouzey.


(** LtIrrelevance.v : Proof irrelevance for [le] and [lt] *)

Require Export Eqdep_dec.
Require Import Arith.

Set Implicit Arguments.

Lemma nat_dec : forall n m:nat, n = m \/ n <> m.
Proof.
 intros n m; destruct (eq_nat_dec n m); auto.
Qed.

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', 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; [left | intros m H; right].
 exists (refl_equal x); auto.
 exists m.
 exists (refl_equal (S m)).
 exists H; auto.
Qed.

Lemma le_irrelevance : 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 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 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.

Lemma lt_irrelevance : forall x y (H1 H2: x < y), H1 = H2.
Proof.
 intros; hnf in *.
 rewrite (le_irrelevance H1 H2); reflexivity.
Qed.

Print Assumptions lt_irrelevance.