The Coq mailing list

[ikdc <ikdc AT mit.edu>]

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.