The Coq mailing list

[Mathieu Boespflug <(e29315a54f%hidden_head%e29315a54f)mboes(e29315a54f%hidden_at%e29315a54f)tweag.net(e29315a54f%hidden_end%e29315a54f)>]

Hi Yves,

On Mon, May 14, 2012 at 03:36:11PM +0200, bertot wrote:
> Dear all,
> 
> I have unclear memories of formal proofs that proofs of comparison
> (not equalities) are unique.  More precisely, proofs of the
> following proposition:
> 
> forall n m, forall h1 h2 : le n m,  h1 = h2
> 
> Could someone point me to one such development?

SSReflect has a proof of this fact, repeated here for convenience:

(* From ssrnat.v *)
Lemma le_irrelevance : forall m n lemn1 lemn2,
  lemn1 = lemn2 :> (m <= n)%coq_nat.
Proof.
move=> m n; elim: {n}n.+1 {-1}n (erefl n.+1) => // n IHn _ [<-] lemn1
  lemn2.
pose def_n2 := erefl n; transitivity (eq_ind _ _ lemn2 _ def_n2) => //.
move def_n1: {1 4 5 7}n lemn1 lemn2 def_n2 => n1 lemn1.
case: n1 / lemn1 def_n1 => [|n1 lemn1] def_n1 [|n2 lemn2] def_n2.
- by rewrite [def_n2]eq_axiomK.
- by move/leP: (lemn2); rewrite -{1}def_n2 ltnn.
- by move/leP: (lemn1); rewrite {1}def_n2 ltnn.
case: def_n2 (def_n2) lemn2 => ->{n2} def_n2 lemn2.
rewrite [def_n2]eq_axiomK /=; congr le_S; exact: IHn.
Qed.

It uses the fact that all proofs of equality on nat are equal, which is
provable in coq because equality on natural numbers is decidable.

Hope this helps,

-- Mathieu