The Coq mailing list

[Tie Cheng <chengtie AT gmail.com>]

Dear Chlipala,

Thanks for your reply...

I see that they use "the syntax [A -> B] is sugar for [forall x : A, B], where [x] does not appear free in [B]", so we have

for the first case, r = 1, n = 2, q = 0

C (for [cons]) ≡ (∀ A:Set, A → List A → List A) ≡ ∀ A:Set, ∀ a1:A, ∀ a2:List A, (List A)

where "∀ a1:A, ∀ a2:List A" matches "∀ a1:A1, ∀ a2:A2" of the formula "C≡ ∀ p1:P1,…,∀ pr:Pr,∀ a1:A1, … ∀ an:An, (I p1 … pr t1… tq)", so A is A1, List A is A2 here.

On the other hand, in the previous example in the manual, they mention "Assuming ΓI is [I1:A1;…;Ik:Ak]". As we have [List:Set→Set] as ΓI in this exemple, "Set→Set" should match A1. So here comes the contradiction: I do not see how "Set→Set" could be A or List A via A1 or A2.

Hope my doubt is clearly presented... Thanks and regards

Tie CHENG

On Fri, May 6, 2011 at 2:39 AM, Adam Chlipala <adam AT chlipala.net> wrote:

Tie Cheng wrote:

I do not see how to fill in the "???" part here:

The first case, r = 1 and n = 0:

C (for [cons]) ≡ (∀ A:Set, A → List A → List A) ≡ ∀ A:Set, (List A ???)

I think I see the issue.  Remember that, in Coq, the syntax [A -> B] is sugar for [forall x : A, B], where [x] does not appear free in [B].  The extra arguments that the constructor takes can be considered as [forall]-bound.

In other words, your template above with [???] is, in fact, not a complete description of the possibilities.  My earlier advice was bad, as n should actually be 2 for [cons].  Sorry!