The Coq mailing list

[Christine Paulin <Christine.Paulin AT lri.fr>]

In Coq version V8, Leibniz's equality is defined on U : Type,
there in one axiom eq_rect_eq in file Eqdep.v 

Axiom eq_rect_eq :
    forall (p:U) (Q:U -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.

and the 
proof that it implies the property 
Lemma UIP_refl : forall (U:Type) (x:U) (p:x = x), p = refl_equal x.

(the other direction is trivial)
There is also a proof that it is equivalent to the K axiom of
Streicher, 
Lemma Streicher_K :
 forall (U:Type) (x:U) (P:x = x -> Prop),
   P (refl_equal x) -> forall p:x = x, P p.

which can be added safely to the theory (see work by M. Hofmann and Th
Streicher). Furthermore in case there is a decidable equality on A,
then this property can be proven but in a non trivial way (see
Eqdep_dec.v)
>From 
  Variable A : Type
  Variable eq_dec : forall x y:A, x = y \/ x <> y.
get   
Theorem K_dec :
   forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.


Christine Paulin



Nadeem Abdul Hamid writes:
 > OK, I see now how to do this: you have to generalize over the dependent 
 > terms and then rewrite and then use the "eq_rec_eq" axiom.
 > 
 > Now, another question: Is it possible to prove that
 >    (x:A)(D:x=x) D==(refl_equal A x)
 > from the Eqdep library as it is? If not, has it been shown that adding 
 > this as an axiom is safe? Can this replace the eq_rec_eq axiom in Eqdep?
 > 
 > Thanks for any help on these issues,
 > --- nadeem
 > 
 > Require Eqdep.
 > 
 > Variable i:nat.
 > Variable Fty:nat->Set.
 > Variable F:(Fty i).
 > Variable R:(i:?)(Fty i) -> bool.
 > Variable D:i=O.
 > 
 > Lemma eqR_F : (R i F)=(R O (eq_rec ? i ? F ? D)).
 > Generalize F.
 > Generalize D.
 > Rewrite D.
 > Intros.
 > Replace (eq_rec nat O Fty f O e) with f; Auto.
 > Apply eq_rec_eq.
 > Save.
 > 
 > 
 > 
 > 
 > 
 > 
 > Nadeem Abdul Hamid wrote:
 > 
 > > Hello all,
 > > Is it possible to prove the following at all (i.e. using the Eqdep 
 > > library):
 > >
 > >
 > > Variable i:nat.
 > > Variable Fty:nat->Set.
 > > Variable F:(Fty i).
 > > Variable R:(i:?)(Fty i) -> bool.
 > > Variable D:i=O.
 > >
 > > Lemma eqR_F : (R i F)=(R O (eq_rec ? i ? F ? D)).
 > >
 > >
 > > Thanks,
 > > --- nadeem
 > >
 > > --------------------------------------------------------
 > > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > > Archives: http://pauillac.inria.fr/pipermail/coq-club
 > >          http://pauillac.inria.fr/bin/wilma/coq-club
 > > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club
 > >
 > 
 > --------------------------------------------------------
 > Bug reports: http://coq.inria.fr/bin/coq-bugs
 > Archives: http://pauillac.inria.fr/pipermail/coq-club
 >           http://pauillac.inria.fr/bin/wilma/coq-club
 > Info: http://pauillac.inria.fr/mailman/listinfo/coq-club

-- 
  Christine Paulin-Mohring             mailto : 
Christine.Paulin AT lri.fr
  LRI, UMR 8623 CNRS, Bat 490, Université Paris Sud,   91405 ORSAY Cedex 
  tel : (+33) (0)1 69 15 66 35         fax : (+33) (0)1 69 15 65 86