StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

PO
text
Body
copied!<p>In fact, <code>even_list_mut</code> takes 6 arguments:</p> <pre><code>even_list_mut : forall (P : even_list -> Prop) (* 1 *) (P0 : odd_list -> Prop), (* 2 *) P ENil -> (* 3 *) (forall (n : nat) (o : odd_list), P0 o -> P (ECons n o)) -> (* 4 *) (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> (* 5 *) forall e : even_list, (* 6 *) P e </code></pre> <p>You can think of the arrow as just syntactic sugar:</p> <pre><code>A -> B === forall _ : A, B </code></pre> <p>So you could rewrite <code>even_list_mut</code> this way:</p> <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)) (e : even_list), P e </code></pre> <p>Sometimes when you apply such a term, some of the arguments can be inferred by unification (comparing the return type of the term with your goal), so these arguments do not become goals because Coq figured it out. For instance, say I have:</p> <pre><code>div_not_zero : forall (a b : Z) (Anot0 : a <> 0), a / b <> 0 </code></pre> <p>And I apply it to the goal <code>42 / 23 <> 0</code>. Coq is able to figure out that <code>a</code> ought to be <code>42</code> and <code>b</code> ought to be <code>23</code>. The only goal left is to prove <code>42 <> 0</code>. But indeed, Coq implicitly passes <code>42</code> and <code>23</code> as arguments to <code>div_not_zero</code>.</p> <p>I hope this helps.</p> <hr> <p><strong>EDIT 1:</strong></p> <p>Answering your additional question:</p> <pre><code>fun (el1 : even_list) => forall (el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 : even_list -> Prop </code></pre> <p>is a function of one argument, <code>el1 : even_list</code>, which returns the type <code>forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2</code>. Informally, given a list <code>el1</code>, it constructs the statement <code>for every list el2, the length of appending it to el1 is the sum of its length and el1's length</code>.</p> <pre><code>fun (el1 el2 : even_list) => elength (eapp el1 el2) = elength el1 + elength el2 : even_list -> even_list -> Prop </code></pre> <p>is a function of two arguments <code>el1 : even_list</code> and <code>el2 : even_list</code>, which returns the type <code>elength (eapp el1 el2) = elength el1 + elength el2</code>. Informally, given two lists, it constructs the statement <code>for these particular two lists, the length of appending them is the sum of their length</code>.</p> <p>Notice two things: - first I said "construct the statement", which is very different from "constructing a proof of the statement". These two functions just return types/propositions/statements, that may be true or false, may be provable or unprovable. - the first one, once fed some list <code>el1</code>, returns a quite interesting type. If you had a proof of that statement, you would know that for any choice of <code>el2</code>, the length of appending it to <code>el1</code> is the sum of lengths.</p> <p>In fact, here is another type/statement to consider:</p> <pre><code>forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 : Prop </code></pre> <p>This statement says that for any two lists, the length of appending is the sum of the lengths.</p> <hr> <p>One thing that may be confusing you too is that this is going on:</p> <pre><code>fun (el1 el2 : even_list) => (* some proof of elength (eapp el1 el2) = elength el1 + elength el2 *) </code></pre> <p>is a term whose type is</p> <pre><code>forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 </code></pre> <p>which is a statement whose type is</p> <pre><code>Prop </code></pre> <p>So you see that <code>fun</code> and <code>forall</code> are two things related but very different. In fact, everything of the form <code>fun (t : T) => p t</code> is a term whose type is <code>forall (t : T), P t</code>, assuming <code>p t</code> has type <code>P t</code>.</p> <p>Therefore, the confusion arises when you write:</p> <pre><code>fun (t : T) => forall (q : Q), foo ^^^^^^^^^^^^^^^^^^^ this has type Prop </code></pre> <p>because this has type:</p> <pre><code>forall (t : T), Prop (* just apply the rule *) </code></pre> <p>So <code>forall</code> can indeed appear in two contexts, because this calculus is able to compute types. Therefore, you might see <code>forall</code> within a computation (which hints at the fact that this is a type-building computation), or you might see it within a type (which is where you usually see it). But it is the same <code>forall</code> for all intents and purposes. On the other hand, <code>fun</code> only appears in computations.</p>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload