The Coq mailing list

[Chunhui He <iuhnuhceh AT gmail.com>]

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.