The Coq mailing list

[Pierre Corbineau <Pierre.Corbineau AT imag.fr>]

A simpler version :

Require Import JMeq.
A second (simpler) version.

Pierre

Axiom UIP : forall (A:Type) (a:A) (e e':a = a) , e=e'.
Scheme real_JMeq_ind := Induction for JMeq Sort Prop.

Section A.

Let T:=Type.

Theorem JMeq_eq: forall (A:T) (x y:A), JMeq x y -> x = y.
intros A x y H.
change (x = eq_rect A (fun t => t) y A (refl_equal A) ).
generalize (refl_equal A).
revert y H.
generalize A at 1 3 4 7.
intros B y H.
elim H using real_JMeq_ind.
intro e;rewrite (UIP Type A e (refl_equal A)).
reflexivity.
Qed.

End A.


Christian Doczkal a écrit :
> Hello
>
> I have a question about the JMeq Library
>
> It introduces the following axiom:
>
> Axiom JMeq_eq : forall (A:Type) (x y:A), JMeq x y -> x = y.
>
>
> In [1] McBride says that the elimination principles on can derive using
> this axiom "give[s] exactly the same strength as Martin-Löfs equality
> extended with Altenkirch and Streicher's 'uniqueness of identity proofs'
> axiom."
>
> So is JMeq_eq is provable in Coq using UIP? Does anyone have a proof?

--
Pierre Corbineau          | 
Pierre.Corbineau AT imag.fr
VERIMAG - Centre Équation | Tel: (+33 / 0) 4 56 52 04 42
2, avenue de Vignate      | Office nr B7
38610 GIÈRES - FRANCE     | http://www-verimag.imag.fr/~corbinea/
begin:vcard
fn:Pierre Corbineau
n:Corbineau;Pierre
org;quoted-printable:Universit=C3=A9 Joseph Fourier - Grenoble 1;Laboratoire VERIMAG - Polytech' Grenoble
adr;quoted-printable;quoted-printable:2, avenue de Vignate;;VERIMAG - Centre =C3=89QUATION ;GI=C3=88RES ;;38610;France
email;internet:Pierre.Corbineau AT imag.fr
title;quoted-printable:Ma=C3=AEtre de Conf=C3=A9rences
tel;work:+33 (0) 4 56 52 04 42
tel;fax:+33 (0) 4 56 52 03 44
x-mozilla-html:FALSE
url:http://www-verimag.imag.fr/~corbinea
version:2.1
end:vcard

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature