The Coq mailing list

[Chunhui He <iuhnuhceh AT gmail.com>]

Thanks!
My next question is, how to construct more constant functions? Where
can I get more info about it?

On 15 December 2016 at 09:27, Cyprien Mangin 
<cyprien.mangin AT m4x.org>
 wrote:
> 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.
>>
>