The Coq mailing list

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

More specifically, Thomas Steicher exhibited models of Type Theory where 
there are non standard closed proofs of (A = A). In these models, pf 
might be one of those non-standard proofs (i.e. semantically distinct 
from (refl_equal A)). Since Type (the type of A) is not decidable, 
you're out of luck without Streicher's K axiom (or its equivalent in Coq).

On a more speculative side, I am working on adding the K axiom to Coq's 
Type system by relaxing some typing constraints, but I cannot give you 
any date for completion.

Pierre




Adam Chlipala a écrit :
> Pierre-Marie Pédrot wrote:
> > I am currently facing a somewhat simple problem which is very close to
> > one example that can be found in Adam's book :
> >
> > Lemma tricky : forall (A : Type) (X : A) (pf : A = A), X = match pf in
> > (_ = A) return A with refl_equal =>  X end.
> >
> > [...]
> >
> > Any clues (axiom-free, of course) ?
> >    
>
> It seems likely that you can't prove this without an axiom.  Note that 
> your theorem is _very_ close to the [Eqdep] module's axiom:
>     http://coq.inria.fr/stdlib/Coq.Logic.Eqdep.html
> If you unfold the definition of [eq_rect] there, the statement is almost 
> your [tricky] lemma.  The only generalization is allowing any [return] 
> clause, not just [return A].
>
> Whoever thought hard about metatheory here concluded that [eq_rect_eq] 
> isn't provable.  Maybe your specialization of it _is_ provable, but I'm 
> not aware of 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