The Coq mailing list

[Hugo Herbelin <herbelin AT pauillac.inria.fr>]

  Hi Pierre,

A) About the numbering of occurrences in n-ary "pattern".

>  I have some difficulties ine adapting the proof of unicity
> of proofs of n <= m (Coq, Faq, question 136).
> 
>  At some moment, we've got the following goal :
> 
>   n : nat
>   q : n <= n
>   ============================
>    forall e : n = n, eq_rect n (fun n0 : nat => n <= n0) (le_n n) n e
>                      = q
> 
>  The sequence (which works :-)) is :
> 
>   pattern n at 2 4 6 10, q; case q; [intro | intros m l e].
>
>   If I count the occurrences of "n" in the subgoal above, I find only
>  6 of them (8 if I count the type of le_n n), but not 10.
> 
>  Is there a way to infer which argument is to be given to pattern from
> the current goal?

  I agree that these n-ary "pattern" incantations are difficult to
follow. To know which occurrences of the dependent subterm(s) (here n)
are concerned, what I usually do is

  - abstract only on the first subterm(s) to abstract (here q)
  - make explicit all implicit arguments

le_uniqueness_proof < 
  
  n : nat
  q : n <= n
  ============================
   forall e : n = n, eq_rect n (fun n0 : nat => n <= n0) (le_n n) n e = q

le_uniqueness_proof < pattern q.
  
  n : nat
  q : n <= n
  ============================
   (fun l : n <= n =>
    forall e : n = n, eq_rect n (fun n0 : nat => n <= n0) (le_n n) n e = l) q

le_uniqueness_proof < Set Printing All (* or Set Printing Implicit *) . Show.

  n : nat
  q : le n n
  ============================
   (fun l : le n n =>
    forall e : @eq nat n n,
    @eq (le n n) (@eq_rect nat n (fun n0 : nat => le n n0) (le_n n) n e) l) q

  And indeed the 10 occurrences of n are here.


B) About the unicity of proofs

>  More generally, where can I find some more examples of proofs of
>  proof unicity?

  You obtain a first example of such proofs by accepting
proof-irrelevance as a valid principle!

  Another example is the one given in file Eqdep_dec.v which shows
the unicity of equality proofs when the domain is decidable.

  Otherwise, I believe that the proof about "n<=m" discussed above is
somehow archetypical and that it should apply more or less canonically
to any predicate on decidable types whose proofs are first-order
objects uniquely determined from the arguments of the predicate.

  E.g. an exercice left open in the answer to question 137 of the faq
is to show "forall x y : nat, forall p q : x<>y, p=q" for a
deterministic algebraic definition of <> on nat.

  Hugo