Dependent Pair Injectivity equivalent to K

Using Rocq
1

Ever since I learned Coq I was fascinated by the equivalence between dependent pair injectivity (DPI) and K. There are long winded proofs in the Coq library EqdepFacts. It turns out there are very short proofs for both direction. The trick for the direction K to DPI was given to me by Gaëtan Gilbert on Friday at Coq Club, and this was a real eye opener. Below are short proofs for both directions. Each direction has a lemma expressing a clever generalization making the proof go through. Code is below. Please tell me if the proofs have been posted before. Gert

Notation Sig := existT.
Notation pi1 := projT1.
Notation pi2 := projT2.

Definition K X := forall (x : X) (e: x = x), eq_refl = e.
Definition DPI X (p: X -> Type) := forall x u v, Sig p x u = Sig p x v -> u = v.

Definition cast {X} {x y: X} {p: X -> Type}
  :  x = y -> p x -> p y
  := fun e a => match e with eq_refl => a end.

Lemma K_DPI' {X} {p: X -> Type} {a b: sigT p} :
  K X  -> a = b -> forall e: pi1 a = pi1 b, cast e (pi2 a) = pi2 b.
Proof.
  intros H [] e. destruct (H _ e). reflexivity.
Qed.

Fact K_DPI X p :
  K X -> DPI X p.
Proof.
  intros H x u v e. apply (K_DPI' H e eq_refl).
Qed.

Lemma DPI_K' X (x y: X) :
  forall e: x = y,
    Sig (fun z => z = y) y eq_refl = Sig (fun z => z = y) x e.
Proof.
  intros []. reflexivity.
Qed.

Fact DPI_K X :
  (forall p, DPI X p) -> K X.
Proof.
  intros H x e. apply (H (fun z => z = x)), DPI_K'.
Qed.
4 Likes
2

This is indeed very nice and clear. Once could strengthen and simplify DPI_K a little by stressing that fun z => z = x is the only predicate that matters:

Fact DPI_K X :
  (forall x, DPI X (fun z => z = x)) -> K X.
Proof.
  intros H x e. apply H,DPI_K'.
Qed.
1 Like
3

@gert-smolka Thank you for sharing!

In case anyone is interested in an SSReflect-based solution (which is a mere translation of the original post):

From Coq Require Import ssreflect ssrfun.

Notation Sig := existT.
Notation pi1 := projT1.
Notation pi2 := projT2.

Definition K X :=
  forall (x : X) (e : x = x), erefl = e.
Definition DPI X (p : X -> Type) :=
  forall x u v, Sig p x u = Sig p x v -> u = v.

Definition cast {X} {x y : X} {p : X -> Type}
  :  x = y -> p x -> p y
  := fun e => let: erefl := e in id.

Lemma K_DPI' {X} {p : X -> Type} {a b : sigT p} :
  K X  -> a = b -> forall e: pi1 a = pi1 b, cast e (pi2 a) = pi2 b.
Proof. by move=> kx -> e; rewrite -(kx _ e). Qed.

Fact K_DPI X p :
  K X -> DPI X p.
Proof. move=> kx x u v e; exact: (K_DPI' kx e erefl). Qed.

Lemma DPI_K' X (x y : X) :
  forall e: x = y,
    Sig (fun z => z = y) y erefl = Sig (fun z => z = y) x e.
Proof. by case: _ /. Qed.

Fact DPI_K X :
  (forall p, DPI X p) -> K X.
Proof. move=> dpi x e; exact/(dpi (fun z => z = x))/DPI_K'. Qed.
4

Is there a short proof of CE X -> UIP' X not using dependent pair types?

Definition CE := forall (p: X -> Type) (x: X) (a: p x) (e: x = x), cast e a = a.
Definition UIP' := forall (x : X) (e: x = x), e = eq_refl.
5 
Definition cast {X} {x y: X} {p: X -> Type}
  :  x = y -> p x -> p y
  := fun e a => match e with eq_refl => a end.

Definition CE X := forall (p: X -> Type) (x: X) (a: p x) (e: x = x), cast e a = a.
Definition K X := forall (x : X) (e: x = x), e = eq_refl.

Definition cast_refl {X} {x y:X} (e : x=y) : cast e eq_refl = e
  := match e with eq_refl => eq_refl end.

Lemma CE_K X : CE X -> K X.
Proof. intros ce x e. rewrite <-(cast_refl e). apply ce. Qed.
1 Like