Library Coq.Logic.Eqdep_dec

We prove that there is only one proof of x=x, i.e eq_refl x. This holds if the equality upon the set of x is decidable. A corollary of this theorem is the equality of the right projections of two equal dependent pairs.

Author: Thomas Kleymann |<tms@dcs.ed.ac.uk>| in Lego adapted to Coq by B. Barras

Credit: Proofs up to K_dec follow an outline by Michael Hedberg

Table of contents:

1. Streicher's K and injectivity of dependent pair hold on decidable types

1.1. Definition of the functor that builds properties of dependent equalities from a proof of decidability of equality for a set in Type

1.2. Definition of the functor that builds properties of dependent equalities from a proof of decidability of equality for a set in Set

Streicher's K and injectivity of dependent pair hold on decidable types

Set Implicit Arguments.

Section EqdepDec.

  Variable A : Type.

  Let comp (x y y´:A) (eq1:x = y) (eq2:x = y´) : y = y´ :=
    eq_ind _ (fun a => a = y´) eq2 _ eq1.

  Remark trans_sym_eq : forall (x y:A) (u:x = y), comp u u = eq_refl y.

  Variable eq_dec : forall x y:A, x = y \/ x <> y.

  Variable x : A.

  Let nu (y:A) (u:x = y) : x = y :=
    match eq_dec x y with
      | or_introl eqxy => eqxy
      | or_intror neqxy => False_ind _ (neqxy u)
    end.

  Let nu_constant : forall (y:A) (u v:x = y), nu u = nu v.

  Qed.

  Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (eq_refl x)) v.

  Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.

  Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.

  Theorem K_dec :
    forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p.

The corollary

  Let proj (P:A -> Prop) (exP:ex P) (def:P x) : P x :=
    match exP with
      | ex_intro x´ prf =>
        match eq_dec x´ x with
          | or_introl eqprf => eq_ind x´ P prf x eqprf
          | _ => def
        end
    end.

  Theorem inj_right_pair :
    forall (P:A -> Prop) (y y´:P x),
      ex_intro P x y = ex_intro P x y´ -> y = y´.

End EqdepDec.

Require Import EqdepFacts.

We deduce axiom K for (decidable) types

Theorem K_dec_type :
  forall A:Type,
    (forall x y:A, {x = y } + {x <> y }) ->
    forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.

Theorem K_dec_set :
  forall A:Set,
    (forall x y:A, {x = y } + {x <> y }) ->
    forall (x:A) (P:x = x -> Prop), P (eq_refl x) -> forall p:x = x, P p.

We deduce the eq_rect_eq axiom for (decidable) types

Theorem eq_rect_eq_dec :
  forall A:Type,
    (forall x y:A, {x = y } + {x <> y }) ->
    forall (p:A) (Q:A -> Type) (x:Q p) (h:p = p), x = eq_rect p Q x p h.

We deduce the injectivity of dependent equality for decidable types

Theorem eq_dep_eq_dec :
  forall A:Type,
    (forall x y:A, {x = y } + {x <> y }) ->
     forall (P:A->Type) (p:A) (x y:P p), eq_dep A P p x p y -> x = y.

Theorem UIP_dec :
  forall (A:Type),
    (forall x y:A, {x = y } + {x <> y }) ->
    forall (x y:A) (p1 p2:x = y), p1 = p2.

Unset Implicit Arguments.

Definition of the functor that builds properties of dependent equalities on decidable sets in Type

The signature of decidable sets in Type

Module Type DecidableType.

Parameter U:Type.
Axiom eq_dec : forall x y:U, {x = y } + {x <> y }.

End DecidableType.

The module DecidableEqDep collects equality properties for decidable set in Type

Module DecidableEqDep (M:DecidableType).

Import M.

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.

Injectivity of Dependent Equality

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

Uniqueness of Identity Proofs (UIP)

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

Uniqueness of Reflexive Identity Proofs

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

Streicher's axiom K

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

Injectivity of equality on dependent pairs in Type

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

Proof-irrelevance on subsets of decidable sets

  Lemma inj_pairP2 :
    forall (P:U -> Prop) (x:U) (p q:P x),
      ex_intro P x p = ex_intro P x q -> p = q.

End DecidableEqDep.

Definition of the functor that builds properties of dependent equalities on decidable sets in Set

The signature of decidable sets in Set

Module Type DecidableSet.

Parameter U:Type.
Axiom eq_dec : forall x y:U, {x = y } + {x <> y }.

End DecidableSet.

The module DecidableEqDepSet collects equality properties for decidable set in Set

Module DecidableEqDepSet (M:DecidableSet).

Import M.
Module N:=DecidableEqDep(M).

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.

Injectivity of Dependent Equality

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

Uniqueness of Identity Proofs (UIP)

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

Uniqueness of Reflexive Identity Proofs

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

Streicher's axiom K

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

Proof-irrelevance on subsets of decidable sets

  Lemma inj_pairP2 :
    forall (P:U -> Prop) (x:U) (p q:P x),
      ex_intro P x p = ex_intro P x q -> p = q.

Injectivity of equality on dependent pairs in Type

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

Injectivity of equality on dependent pairs with second component in Type

Notation inj_pairT2 := inj_pair2.

End DecidableEqDepSet.

From decidability to inj_pair2

Lemma inj_pair2_eq_dec : forall A:Type, (forall x y:A, {x =y }+{x <>y }) ->
( forall (P:A -> Type) (p:A) (x y:P p), existT P p x = existT P p y -> x = y ).