Library Coq.Logic.EqdepFacts



This file defines dependent equality and shows its equivalence with equality on dependent pairs (inhabiting sigma-types). It derives the consequence of axiomatizing the invariance by substitution of reflexive equality proofs and shows the equivalence between the 4 following statements
  • Invariance by Substitution of Reflexive Equality Proofs.
  • Injectivity of Dependent Equality
  • Uniqueness of Identity Proofs
  • Uniqueness of Reflexive Identity Proofs
  • Streicher's Axiom K
These statements are independent of the calculus of constructions 2.
References:
1 T. Streicher, Semantical Investigations into Intensional Type Theory, Habilitationsschrift, LMU München, 1993. 2 M. Hofmann, T. Streicher, The groupoid interpretation of type theory, Proceedings of the meeting Twenty-five years of constructive type theory, Venice, Oxford University Press, 1998
Table of contents:
1. Definition of dependent equality and equivalence with equality of dependent pairs and with dependent pair of equalities
2. Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K
3. Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq

Definition of dependent equality and equivalence with equality of dependent pairs


Import EqNotations.

Section Dependent_Equality.

  Variable U : Type.
  Variable P : U -> Type.

Dependent equality

  Inductive eq_dep (p:U) (x:P p) : forall q:U, P q -> Prop :=
    eq_dep_intro : eq_dep p x p x.
  Hint Constructors eq_dep: core.

  Lemma eq_dep_refl : forall (p:U) (x:P p), eq_dep p x p x.

  Lemma eq_dep_sym :
    forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep q y p x.
  Hint Immediate eq_dep_sym: core.

  Lemma eq_dep_trans :
    forall (p q r:U) (x:P p) (y:P q) (z:P r),
      eq_dep p x q y -> eq_dep q y r z -> eq_dep p x r z.

  Scheme eq_indd := Induction for eq Sort Prop.

Equivalent definition of dependent equality as a dependent pair of equalities

  Inductive eq_dep1 (p:U) (x:P p) (q:U) (y:P q) : Prop :=
    eq_dep1_intro : forall h:q = p, x = rew h in y -> eq_dep1 p x q y.

  Lemma eq_dep1_dep :
    forall (p:U) (x:P p) (q:U) (y:P q), eq_dep1 p x q y -> eq_dep p x q y.

  Lemma eq_dep_dep1 :
    forall (p q:U) (x:P p) (y:P q), eq_dep p x q y -> eq_dep1 p x q y.

End Dependent_Equality.


Dependent equality is equivalent to equality on dependent pairs

Lemma eq_sigT_eq_dep :
  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    existT P p x = existT P q y -> eq_dep p x q y.

Notation eq_sigS_eq_dep := eq_sigT_eq_dep (compat "8.2").
Lemma eq_dep_eq_sigT :
  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    eq_dep p x q y -> existT P p x = existT P q y.

Lemma eq_sigT_iff_eq_dep :
  forall (U:Type) (P:U -> Type) (p q:U) (x:P p) (y:P q),
    existT P p x = existT P q y <-> eq_dep p x q y.

Notation equiv_eqex_eqdep := eq_sigT_iff_eq_dep (only parsing).
Lemma eq_sig_eq_dep :
  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
    exist P p x = exist P q y -> eq_dep p x q y.

Lemma eq_dep_eq_sig :
  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
    eq_dep p x q y -> exist P p x = exist P q y.

Lemma eq_sig_iff_eq_dep :
  forall (U:Prop) (P:U -> Prop) (p q:U) (x:P p) (y:P q),
    exist P p x = exist P q y <-> eq_dep p x q y.

Dependent equality is equivalent to a dependent pair of equalities

Set Implicit Arguments.

Lemma eq_sigT_sig_eq : forall X P (x1 x2:X) H1 H2, existT P x1 H1 = existT P x2 H2 <-> {H:x1=x2 | rew H in H1 = H2}.

Lemma eq_sigT_fst :
  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), x1 = x2.

Lemma eq_sigT_snd :
  forall X P (x1 x2:X) H1 H2 (H:existT P x1 H1 = existT P x2 H2), rew (eq_sigT_fst H) in H1 = H2.

Lemma eq_sig_fst :
  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), x1 = x2.

Lemma eq_sig_snd :
  forall X P (x1 x2:X) H1 H2 (H:exist P x1 H1 = exist P x2 H2), rew (eq_sig_fst H) in H1 = H2.

Unset Implicit Arguments.

Exported hints

Hint Resolve eq_dep_intro: core.
Hint Immediate eq_dep_sym: core.

Eq_rect_eq <-> Eq_dep_eq <-> UIP <-> UIP_refl <-> K


Section Equivalences.

  Variable U:Type.

Invariance by Substitution of Reflexive Equality Proofs

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

Injectivity of Dependent Equality

  Definition Eq_dep_eq :=
    forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.

Uniqueness of Identity Proofs (UIP)

  Definition UIP_ :=
    forall (x y:U) (p1 p2:x = y), p1 = p2.

Uniqueness of Reflexive Identity Proofs

  Definition UIP_refl_ :=
    forall (x:U) (p:x = x), p = eq_refl x.

Streicher's axiom K

  Definition Streicher_K_ :=
    forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.

Injectivity of Dependent Equality is a consequence of Invariance by Substitution of Reflexive Equality Proof

  Lemma eq_rect_eq__eq_dep1_eq :
    Eq_rect_eq -> forall (P:U->Type) (p:U) (x y:P p), eq_dep1 p x p y -> x = y.

  Lemma eq_rect_eq__eq_dep_eq : Eq_rect_eq -> Eq_dep_eq.

Uniqueness of Identity Proofs (UIP) is a consequence of Injectivity of Dependent Equality

  Lemma eq_dep_eq__UIP : Eq_dep_eq -> UIP_.

Uniqueness of Reflexive Identity Proofs is a direct instance of UIP

  Lemma UIP__UIP_refl : UIP_ -> UIP_refl_.

Streicher's axiom K is a direct consequence of Uniqueness of Reflexive Identity Proofs

  Lemma UIP_refl__Streicher_K : UIP_refl_ -> Streicher_K_.

We finally recover from K the Invariance by Substitution of Reflexive Equality Proofs

  Lemma Streicher_K__eq_rect_eq : Streicher_K_ -> Eq_rect_eq.

Remark: It is reasonable to think that eq_rect_eq is strictly stronger than eq_rec_eq (which is eq_rect_eq restricted on Set):
Definition Eq_rec_eq := forall (P:U -> Set) (p:U) (x:P p) (h:p = p), x = eq_rec p P x p h.
Typically, eq_rect_eq allows to prove UIP and Streicher's K what does not seem possible with eq_rec_eq. In particular, the proof of UIP requires to use eq_rect_eq on fun y -> x=y which is in Type but not in Set.

End Equivalences.

Section Corollaries.

  Variable U:Type.

UIP implies the injectivity of equality on dependent pairs in Type

 Definition Inj_dep_pair :=
   forall (P:U -> Type) (p:U) (x y:P p), existT P p x = existT P p y -> x = y.

 Lemma eq_dep_eq__inj_pair2 : Eq_dep_eq U -> Inj_dep_pair.

End Corollaries.

Notation Inj_dep_pairS := Inj_dep_pair.
Notation Inj_dep_pairT := Inj_dep_pair.
Notation eq_dep_eq__inj_pairT2 := eq_dep_eq__inj_pair2.

Definition of the functor that builds properties of dependent equalities assuming axiom eq_rect_eq


Module Type EqdepElimination.

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

End EqdepElimination.

Module EqdepTheory (M:EqdepElimination).

  Section Axioms.

    Variable U:Type.

Invariance by Substitution of Reflexive Equality Proofs

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

Lemma eq_rec_eq :
  forall (p:U) (Q:U -> Set) (x:Q p) (h:p = p), x = eq_rec p Q x p h.

Injectivity of Dependent Equality

Lemma eq_dep_eq : forall (P:U->Type) (p:U) (x y:P p), eq_dep p x p y -> x = y.

Uniqueness of Identity Proofs (UIP) is a consequence of Injectivity of Dependent Equality

Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.

Uniqueness of Reflexive Identity Proofs is a direct instance of UIP

Lemma UIP_refl : forall (x:U) (p:x = x), p = eq_refl x.

Streicher's axiom K is a direct consequence of Uniqueness of Reflexive Identity Proofs

Lemma Streicher_K :
  forall (x:U) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.

End Axioms.

UIP implies the injectivity of equality on dependent pairs in Type

Lemma inj_pair2 :
 forall (U:Type) (P:U -> Type) (p:U) (x y:P p),
   existT P p x = existT P p y -> x = y.

Notation inj_pairT2 := inj_pair2.

End EqdepTheory.