The Coq mailing list

[Gabriel Scherer <gabriel.scherer AT gmail.com>]

For the (Foo tt) example, note that there *is* a trivial proof... term.
(Because inference of depend pattern matching annotations is good enough.)

Goal forall f g : Foo tt, f = g.
  refine (fun f g =>
            match f, g with
            | foo, foo => eq_refl
            end).
Qed.

On Thu, Dec 15, 2016 at 2:18 PM, Jonathan Leivent <jonikelee AT gmail.com> 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?

I appreciate having a different proof of this!  However, my biggest problem is acquiring the intuition as to why "obviously" unique field-less constructors (like eq_refl) of indexed types require so much work to demonstrate their uniqueness.  The most trivial case is:

Inductive Foo : unit -> Set :=
 foo : Foo tt.

Goal forall f g : Foo tt, f = g.

One has to do a bit of non-trivial work here to complete this proof.  I just can't get past my naive view that this proof should be just as trivial as would be the case if Foo was missing that unit index.  The stubbornness of this incorrect intuition keeps plaguing me in other proofs.  Learning the tricks to complete such a proof is one thing.  Internalizing why they are needed and how they are motivated is not as easy.

-- Jonathan