coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Pierre Corbineau <Pierre.Corbineau AT imag.fr>
- To: Christian Doczkal <doczkal AT ps.uni-sb.de>
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] JMeq_eq vs. UIP
- Date: Fri, 19 Mar 2010 12:25:17 +0100
- Organization: Verimag
This is how you do (Coq v8.2pl1).
Require Import JMeq.
Axiom UIP : forall (A:Type) (a:A) (e e':a = a) , e=e'.
Scheme real_JMeq_ind := Induction for JMeq Sort Prop.
Theorem JMeq_eq: forall (A:Type) (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) ).
revert H.
refine ((_ : forall e,
JMeq x y -> x= eq_rect A (fun t : Type => t) y A e ) (refl_equal A)).
revert y.
generalize A at 1 2 5 7.
intros B y e H.
revert e.
apply (real_JMeq_ind A x (fun B y _ => forall e : B=A, x = eq_rect B (fun t => t) y A e)).
2:assumption.
intro e.
rewrite (UIP Type A e (refl_equal A)).
simpl.
apply refl_equal.
Qed.
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
- [Coq-Club] JMeq_eq vs. UIP, Christian Doczkal
- Re: [Coq-Club] JMeq_eq vs. UIP, Pierre Corbineau
- Re: [Coq-Club] JMeq_eq vs. UIP, Pierre Corbineau
- Re: [Coq-Club] JMeq_eq vs. UIP, Adam Chlipala
Archive powered by MhonArc 2.6.16.