The Coq mailing list

[Alan Schmitt <alan.schmitt AT inria.fr>]

Hello,

I’ve long wanted to understand the magic behind the unicity of identity
proofs for decidable equality
(https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html), and doing so
made me realize one can use a weaker hypothesis: a function that, given
an identity proof, returns a canonical one of that type.

#+BEGIN_SRC coq
Variable A : Type.
Variable x : A.

Variable nu : forall y, (x=y) -> (x=y).
Axiom nu_canon : forall y e1 e2, nu y e1 = nu y e2.
#+END_SRC

It is easy to show that if equality is decidable, then it has this property
(this is the same proof as the file above).

#+BEGIN_SRC coq
Definition eq_dec := forall x y : A, x = y \/ x <> y.

Definition nudec (H:eq_dec) y (u : x = y) : x = y :=
  match (H x y) with
  | or_introl eqtt => eqtt
  | or_intror neqtt => False_ind (x = y) (neqtt u)
  end.

Lemma eqdec_canon : forall H:eq_dec, forall y e1 e2, nudec H y e1 = nudec H y 
e2.
  intros.
  unfold nudec.
  destruct (H x y); trivial.
  exfalso; auto.
Qed.
#+END_SRC

I’m wondering about the converse: are there types for which equality is not
decidable, but that have canonical equality proofs hence UIP?

For the record, here is how I showed UIP using nu_canon. It’s basically a
rewriting of Coq.Logic.Eqdep_dec. The first step is the crucial one, and it
always holds (there is no hypothesis on type A):

#+BEGIN_SRC coq
Lemma quasi_UIPrefl : forall (y : A) (e : x = y), (eq_trans (eq_sym e) e) = 
eq_refl.
  intros.
  exact (
      match e return eq_trans (eq_sym e) e = eq_refl with
      | eq_refl => eq_refl
      end
    ).
Qed.
#+END_SRC

One may use this to rewrite an equality to one that is base on a canonical 
one.

#+BEGIN_SRC coq
Lemma inv : forall (y : A) (u : x = y), eq_trans (eq_sym (nu x eq_refl)) (nu 
y u) = u.
  intros.
  rewrite <- u. (* to change u into eq_refl and y to x *)
  apply quasi_UIPrefl.
Qed.
#+END_SRC

To conclude, one uses inv to rewrite both equalities, and the fact that nu
returns a canonical equality.

#+BEGIN_SRC coq
Theorem UIP : forall (y : A) (p1 p2 : x = y), p1 = p2.
  intros.
  rewrite <- (inv _ p1).
  rewrite <- (inv _ p2).
  rewrite (nu_canon y p1 p2).
  reflexivity.
Qed.
#+END_SRC

Best,

Alan

-- 
OpenPGP Key ID : 040D0A3B4ED2E5C7
Monthly Athmospheric CO₂, Mauna Loa Obs. 2015-08: 398.93, 2016-08: 402.25

Attachment: signature.asc
Description: PGP signature