Library Stdlib.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 (x y:A) (u:x = y) : comp u u = eq_refl y.

  Variable x : A.

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

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

  Local Lemma nu_constant (y:A) (u v:x = y) : nu u = nu v.

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

  Remark nu_left_inv_on (y:A) (u:x = y) : nu_inv (nu u) = u.

  Theorem eq_proofs_unicity_on (y:A) (p1 p2:x = y) : p1 = p2.

  Theorem K_dec_on (P:x = x -> Prop) (H:P (eq_refl x)) (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' with
          | or_introl eqprf => eq_ind x' P prf x (eq_sym eqprf)
          | _ => def
        end
    end.

  Theorem inj_right_pair_on (P:A -> Prop) (y y':P x) :
    ex_intro P x y = ex_intro P x y' -> y = y'.

End EqdepDec.

Now we prove the versions that require decidable equality for the entire type rather than just on the given element. The rest of the file uses this total decidable equality. We could do everything using decidable equality at a point (because the induction rule for eq is really an induction rule for { y : A | x = y }), but we don't currently, because changing everything would break backward compatibility and no-one has yet taken the time to define the pointed versions, and then re-define the non-pointed versions in terms of those.

Theorem eq_proofs_unicity A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
: forall (y:A) (p1 p2:x = y), p1 = p2.

Theorem K_dec A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
: forall P:x = x -> Prop, P (eq_refl x) -> forall p:x = x, P p.

Theorem inj_right_pair A (eq_dec : forall x y : A, x = y \/ x <> y) (x : A)
: forall (P:A -> Prop) (y y':P x),
    ex_intro P x y = ex_intro P x y' -> y = y'.

Require Import EqdepFacts.

We deduce axiom K for (decidable) types
Theorem K_dec_type (A:Type) (eq_dec:forall x y:A, {x = y} + {x <> y}) (x:A)
  (P:x = x -> Prop) (H:P (eq_refl x)) (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.

  Monomorphic 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:Set.
  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 ).

Register inj_pair2_eq_dec as core.eqdep_dec.inj_pair2.

Examples of short direct proofs of unicity of reflexivity proofs on specific domains

Lemma UIP_refl_unit (x : tt = tt) : x = eq_refl tt.

Lemma UIP_refl_bool (b:bool) (x : b = b) : x = eq_refl.

Lemma UIP_refl_nat (n:nat) (x : n = n) : x = eq_refl.

Lemma UIP_None_l {A} (x : option A) (p1 p2 : None = x) : p1 = p2.

Lemma UIP_None_r {A} (x : option A) (p1 p2 : x = None) : p1 = p2.

Lemma UIP_None_None {A} (p1 p2 : None = None :> option A) : p1 = p2.

Lemma UIP_nil_l {A} (x : list A) (p1 p2 : nil = x) : p1 = p2.

Lemma UIP_nil_r {A} (x : list A) (p1 p2 : x = nil) : p1 = p2.

Lemma UIP_nil_nil {A} (p1 p2 : nil = nil :> list A) : p1 = p2.