StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POCoq -- understanding `forall` syntax
primarykey
Id
17466817
data
AcceptedAnswerId
17467327
AnswerCount
1
ClosedDate
CommentCount
0
CommunityOwnedDate
CreationDate
2013-07-04T09:34:09.413
FavoriteCount
4
LastActivityDate
2013-07-04T14:36:50.620
LastEditDate
LastEditorUserId
0
OwnerUserId
691032
ParentId
0
PostTypeId
1
Score
5
ViewCount
664
LastEditorDisplayName
text
Body
I'm learning Coq by reading the book "Certified Programming with Dependent Types" and I'm having trouble udnerstanding <code>forall</code> syntax. As an example let's think this mutually inductive data type: (code is from the book) <pre><code>Inductive even_list : Set := | ENil : even_list | ECons : nat -> odd_list -> even_list with odd_list : Set := | OCons : nat -> even_list -> odd_list. </code></pre> and this mutually recursive function definitions: <pre><code>Fixpoint elength (el : even_list) : nat := match el with | ENil => O | ECons _ ol => S (olength ol) end with olength (ol : odd_list) : nat := match ol with | OCons _ el => S (elength el) end. Fixpoint eapp (el1 el2 : even_list) : even_list := match el1 with | ENil => el2 | ECons n ol => ECons n (oapp ol el2) end with oapp (ol : odd_list) (el : even_list) : odd_list := match ol with | OCons n el' => OCons n (eapp el' el) end. </code></pre> and we have induction schemes generated: <pre><code>Scheme even_list_mut := Induction for even_list Sort Prop with odd_list_mut := Induction for odd_list Sort Prop. </code></pre> <hr> Now what I don't understand is, from the type of <code>even_list_mut</code> I can see it takes 3 arguments: <pre><code>even_list_mut : forall (P : even_list -> Prop) (P0 : odd_list -> Prop), P ENil -> (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> forall e : even_list, P e </code></pre> But in order to apply it we need to supply it two parameters, and it replaces the goal with 3 premises (for <code>P ENil</code>, <code>forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)</code> and <code>forall (n : nat) (e : even_list), P e -> P0 (OCons n e)</code> cases). So it's like it actually gets 5 parameters, not 3. But then this idea fails when we think of this types: <pre><code>fun el1 : even_list => forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2 : even_list -> Prop </code></pre> and <pre><code>fun el1 el2 : even_list => elength (eapp el1 el2) = elength el1 + elength el2 : even_list -> even_list -> Prop </code></pre> <hr> Can anyone explain how does <code>forall</code> syntax work? Thanks,
Tags
<coq>
Title
Coq -- understanding `forall` syntax
singulars
PostAcceptedAnswerId
1. PO
 singulars
 PostTypePostTypeId
 PTAnswer
PostParentId
1. This table or related slice is empty.
PostTypePostTypeId
1. PTQuestion
UserLastEditorUserId
1. This table or related slice is empty.
UserOwnerUserId
1. USsinan
plurals
PostLinksPostIdRelatedPostId
1. This table or related slice is empty.
PostLinksRelatedPostIdPostId
1. This table or related slice is empty.
PostsAcceptedAnswerId
1. This table or related slice is empty.
PostsParentIdCreationDate
1. PO
 singulars
 PostTypePostTypeId
 PTAnswer
VotesPostIdCreationDate
1. VO
 singulars
 PostPostId
 POCoq -- understanding `forall` syntax
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
2. VO
 singulars
 PostPostId
 POCoq -- understanding `forall` syntax
 UserUserId
 USsinan
 VoteTypeVoteTypeId
 VTFavorite
3. VO
 singulars
 PostPostId
 POCoq -- understanding `forall` syntax
 UserUserId
 This table or related slice is empty.
 VoteTypeVoteTypeId
 VTUpMod
CommentsPostId
1. This table or related slice is empty.

Querying!

Guidance

A row detail

Detail views are divided into sections. All the information in the data section comes from columns in the selected row. The other sections display data from other, related rows.

Related data can be related in a to-one or a to-many fashion. Captions of data related in a to-many fashion link to a list view showing a filtered view of the table.

Try moving around until you find a non-empty to-many entry and click on the label to get to one. You can move back to the root by clicking on the database name in the header.