# Library Coq.Logic.Eqdep_dec

``` ```
We prove that there is only one proof of `x=x`, i.e `refl_equal 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

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 = refl_equal y.   Proof.     intros.     case u; trivial.   Qed.   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.     intros.     unfold nu in |- *.     case (eq_dec x y); intros.     reflexivity.     case n; trivial.   Qed.   Let nu_inv (y:A) (v:x = y) : x = y := comp (nu (refl_equal x)) v.   Remark nu_left_inv : forall (y:A) (u:x = y), nu_inv (nu u) = u.   Proof.     intros.     case u; unfold nu_inv in |- *.     apply trans_sym_eq.   Qed.   Theorem eq_proofs_unicity : forall (y:A) (p1 p2:x = y), p1 = p2.   Proof.     intros.     elim nu_left_inv with (u := p1).     elim nu_left_inv with (u := p2).     elim nu_constant with y p1 p2.     reflexivity.   Qed.   Theorem K_dec :     forall P:x = x -> Prop, P (refl_equal x) -> forall p:x = x, P p.   Proof.     intros.     elim eq_proofs_unicity with x (refl_equal x) p.     trivial.   Qed. ```
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'.   Proof.     intros.     cut (proj (ex_intro P x y) y = proj (ex_intro P x y') y).     simpl in |- *.     case (eq_dec x x).     intro e.     elim e using K_dec; trivial.     intros.     case n; trivial.     case H.     reflexivity.   Qed. 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 (refl_equal x) -> forall p:x = x, P p. Proof.   intros A eq_dec x P H p.   elim p using K_dec; intros.   case (eq_dec x0 y); [left|right]; assumption.   trivial. Qed. Theorem K_dec_set :   forall A:Set,     (forall x y:A, {x = y} + {x <> y}) ->     forall (x:A) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p. Proof fun A => K_dec_type (A:=A). ```
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. Proof.   intros A eq_dec.   apply (Streicher_K__eq_rect_eq A (K_dec_type eq_dec)). Qed. 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.   Proof eq_rect_eq_dec eq_dec. ```
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.   Proof (eq_rect_eq__eq_dep_eq U eq_rect_eq). ```
Uniqueness of Identity Proofs (UIP)
```   Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.   Proof (eq_dep_eq__UIP U eq_dep_eq). ```
Uniqueness of Reflexive Identity Proofs
```   Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.   Proof (UIP__UIP_refl U UIP). ```
Streicher's axiom K
```   Lemma Streicher_K :     forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.   Proof (K_dec_type eq_dec). ```
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 eq_dep_eq__inj_pairT2 U eq_dep_eq. ```
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.   Proof.     intros.     apply inj_right_pair with (A:=U).     intros x0 y0; case (eq_dec x0 y0); [left|right]; assumption.     assumption.   Qed. End DecidableEqDep. ```

## B 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.   Proof eq_rect_eq_dec eq_dec. ```
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.   Proof N.eq_dep_eq. ```
Uniqueness of Identity Proofs (UIP)
```   Lemma UIP : forall (x y:U) (p1 p2:x = y), p1 = p2.   Proof N.UIP. ```
Uniqueness of Reflexive Identity Proofs
```   Lemma UIP_refl : forall (x:U) (p:x = x), p = refl_equal x.   Proof N.UIP_refl. ```
Streicher's axiom K
```   Lemma Streicher_K :     forall (x:U) (P:x = x -> Prop), P (refl_equal x) -> forall p:x = x, P p.   Proof N.Streicher_K. ```
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.   Proof N.inj_pairP2. ```
Injectivity of equality on dependent pairs in `Type`
```   Lemma inj_pair2 :     forall (P:U -> Type) (p:U) (x y:P p),       existS P p x = existS P p y -> x = y.   Proof eq_dep_eq__inj_pair2 U N.eq_dep_eq. ```
Injectivity of equality on dependent pairs with second component in `Type`
```   Notation inj_pairT2 := inj_pair2. End DecidableEqDepSet. ```