The Coq mailing list

[Matej Kosik <5764c029b688c1c0d24a2e97cd764f AT gmail.com>]

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