coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Hugo Herbelin <herbelin AT pauillac.inria.fr>
- To: casteran AT labri.fr
- Cc: coq-club AT pauillac.inria.fr
- Subject: Re: [Coq-Club] about pattern and Streicher technology
- Date: Tue, 26 Oct 2004 12:24:39 +0200 (MET DST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] about pattern and Streicher technology, casteran
- Re: [Coq-Club] about pattern and Streicher technology, Hugo Herbelin
Archive powered by MhonArc 2.6.16.