coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Unicity of proofs for integer comparisons

From: St�phane Glondu <(e29315a54f%hidden_head%e29315a54f)steph(e29315a54f%hidden_at%e29315a54f)glondu.net(e29315a54f%hidden_end%e29315a54f)>
To: bertot <(e29315a54f%hidden_head%e29315a54f)Yves.Bertot(e29315a54f%hidden_at%e29315a54f)inria.fr(e29315a54f%hidden_end%e29315a54f)>
Cc: Coq Club <(e29315a54f%hidden_head%e29315a54f)coq-club(e29315a54f%hidden_at%e29315a54f)inria.fr(e29315a54f%hidden_end%e29315a54f)>
Subject: Re: [Coq-Club] Unicity of proofs for integer comparisons
Date: Mon, 14 May 2012 16:14:51 +0200

Le 14/05/2012 15:36, bertot a �crit :
> 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

This looks like le_unique in the standard library and a FAQ item :-)

And I guess the same would apply for other comparisons (as long as they
don't use negation).

Cheers,

--
St�phane

[Coq-Club] Unicity of proofs for integer comparisons, bertot, 05/14/2012
- Re: [Coq-Club] Unicity of proofs for integer comparisons, St�phane Glondu, 05/14/2012
- Re: [Coq-Club] Unicity of proofs for integer comparisons, Mathieu Boespflug, 05/14/2012