The Coq mailing list

[Cyprien Mangin <cyprien.mangin AT m4x.org>]

You actually only need any constant function x = y -> x = y (see below), so your projection function will work too. nu is just the most simple constant function you can define from decidable equality.

Section eqdep_cons.
  Variable A : Type.
  Variable nu : forall (x y : A), x = y -> x = y.
  Arguments nu [_ _] _.
  Variable nu_cons : forall x y (p q : x = y), nu p = nu q.

  Definition nu_inv {x y : A} (p : x = y) : x = y :=
    eq_ind _ (fun a => a = y) p _ (nu eq_refl).

  Lemma nu_left_inv : forall x y (p : x = y), nu_inv (nu p) = p.
  Proof.
    destruct p. unfold nu_inv. destruct (nu eq_refl).
    reflexivity.
  Qed.

  Lemma UIP : forall (x y : A) (p q : x = y), p = q.
  Proof.
    intros.
    replace p with (nu_inv (nu p)) by (apply nu_left_inv).
    replace q with (nu_inv (nu q)) by (apply nu_left_inv).
    f_equal. apply nu_cons.
  Qed.
End eqdep_cons.

On Thu, Dec 15, 2016 at 10:09 AM, ikdc <ikdc AT mit.edu> wrote:

On 12/15/2016 04:05 AM, Chunhui He wrote:

Hi all,

I'm reading the proof of UIP on decidable domains in the standard
library of coq:
source: theories/Logic/Eqdep_dec.v
doc: https://coq.inria.fr/library/Coq.Logic.Eqdep_dec.html

The proof "eq_proofs_unicity_on" uses some definitions like "nu" and "nu_inv".
I think the proof is confusing, does anyone know the meaning of "nu"
and "nu_inv"?

I try to simplify the proof by inlining (see below).
I find we can use a projection instead of "nu" and "nu_inv".
maybe it seem cleaner than the original proof?

Thanks!

Chunhui

---
Section eqdep_dec.
  Variable A : Type.
  Variable A_dec : forall (x y : A), x = y \/ x <> y.

  Definition or_proj {x' y : A} (oreq : x' = y \/ x' <> y)
             (x : A) (def : x = y) : x = y :=
    match oreq with
    | or_introl H =>
      match A_dec x' x with
      | or_introl e =>
        match e in _ = y' return y' = y with
        | eq_refl => H
        end
      | or_intror _ => def
      end
    | or_intror _ => def
    end.

  Lemma or_proj_eq : forall {x y : A} (u : x = y), or_proj (A_dec x y) x u = u.
  Proof.
    intros x y u.
    unfold or_proj.
    case u.
    case (A_dec x x) as [Heq | Hneq].
    { case Heq. apply eq_refl. }
    { exfalso; apply (Hneq eq_refl). }
  Qed.

  Theorem eq_proofs_unicity : forall {x y : A} (p1 p2 : x = y), p1 = p2.
  Proof.
    intros x y p1 p2.
    case (or_proj_eq p1).
    case (or_proj_eq p2).
    unfold or_proj.
    case (A_dec x y) as [Heq | Hneq].
    { case (A_dec x x) as [Heq' | Hneq'] .
      { apply eq_refl. }
      { exfalso; apply (Hneq' eq_refl). } }
    { exfalso; apply (Hneq p1). }
  Qed.
End eqdep_dec.

The idea is that nu is a sort of "normalization" function which takes all equalities between x and y and maps them all to the same canonical equality between x and y.  This is the intuition behind nu_constant.