The Coq mailing list

[Yasuaki Kudo <yasu AT yasuaki.com>]

HI Matej,

 

Thank you so much for your kind reply – It is clearer to me now.  I really appreciate your kind help – studying by myself is hard and your advice really helps.

 

Regards,

Yasuaki

 

 

 

From: Matej Kosik
Sent: Friday, November 20, 2015 11:24 PM
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Coq'Art questions (Page 101)

 

 

Hi Yasuaki and welcome,

 

On 11/20/2015 11:22 AM, Yasuaki Kudo wrote:

> Sorry I meant in my last sentence the second argument *Prop* (not B)

>

> On Nov 20, 2015, at 19:17, Yasuaki Kudo <yasu AT yasuaki.com <mailto:yasu AT yasuaki.com>> wrote:

>

>> Hi,

>> 

>> 

>> 

>> I have a question regarding the section of Existential Quantification on Page 101 of /Interactive Theorem Proving and Program Development (Coq’Art)/

>> 

>> 

>> 

>> I hope this is not too nitpicking but because I am self-studying, I want to ensure that I understand the foundation correctly.

>> 

>> 

>> 

>> On Page 78 (4.1.1.6), the book says:

>> 

>> /Types for the logical connectives and operator like prod are constructed thanks to the following rule, yet another extension of Prod.  The types that are formed in this way are called /higher-order

>> types.

>> 

>> / /

>> 

>> / /

>> 

>> /E, G |-  A:Type/

>> 

>> /E, G |-  B:Type/

>> 

>> /------------------------------------------ Prod-sup /

>> 

>> /E, G |-  A->B : Type/

>> 

>> 

>> 

>> 

>> 

>> On Page 101 (4.3.5.1):

>> 

>> /The type of the constant ex has the sort Type; the formation of this type is summarized by the following sequence of judgements (only the third and the forth ones use the rule for building

>> higher-order types):/

>> 

>> / /

>> 

>> /[A:Type] |- Prop : Type/

>> 

>> /[A:Type] |- A-> Prop : Type/

>> 

>> /[A:Type] |- (A -> Prop) -> Prop : Type/

>> 

>> /|- //∀A:Type, (A -> Prop) -> Prop : Type/

>> 

>> 

>> 

>> On contrary to the note in parenthesis /(only the third and the forth…)/, it seems that the second example *IS* an example of the formation above where the first argument is *A* and the second being

>> *B*?   Am I wrong?

 

Myself, I see there two utilizations of the Prod-sup rule (for the second and the third judgements)

and one utilization of Prod(s,s',s'') rule (for the fourth judgment)

 

Here's the corresponding proof-tree I just sketched

 

              http://matej-kosik.github.io/www/tmp/4.html

 

(I am not inlining it because I am not sure what MUA would do to it)

(the root is the original goal; children are hypotheses; inner nodes are intermediate goals; leafs are axioms or trivial judgments)

 

>> 

>> 

>> 

>> In addition, what does /Prod-sup/ mean?  I have seen terms like /dependent *product*/ in the book but I don’t know what product means.

 

The Prod-sup, like Prod-Set and Prod-Prop is just a special case of Prod(s,s',s'') rule.

 

Dependent product is defined here:

https://coq.inria.fr/refman/Reference-Manual003.html#hevea_default22

 

In other words this:

 

              A → Prop

 

is a non-dependent product whereas this:

 

              ∀ A:Type, (A -> Prop) -> Prop

 

is a dependept product (because the term "(A -> Prop) -> Prop" contains "A" as a free variable).

 

 

Hope this helps,

 

Regards,

---

m