In fact, even_list_mut takes 6 arguments:
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 no)) -> (* 4 *) (forall (n : nat) (e : even_list), P e -> P0 (OCons ne)) -> (* 5 *) forall e : even_list, (* 6 *) P e
You can think of the arrow as syntactic sugar:
A -> B
So you can rewrite even_list_mut as follows:
even_list_mut : forall (P : even_list -> Prop) (P0 : odd_list -> Prop) (_ : P ENil) (_ : forall (n : nat) (o : odd_list), P0 o -> P (ECons no)) (_ : forall (n : nat) (e : even_list), P e -> P0 (OCons ne)) (e : even_list), P e
Sometimes, when you use such a term, some arguments can be deduced by unification (comparing the type of the returned expression with your goal), so these arguments do not become targets, because Coq found out. For example, let's say I have:
div_not_zero : forall (ab : Z) (Anot0 : a <> 0), a / b <> 0
And I apply it to target 42 / 23 <> 0 . Coq can determine that a should be 42 , and b should be 23 . It remains only to prove that 42 <> 0 . But indeed, Coq implicitly passes 42 and 23 as arguments to div_not_zero .
Hope this helps.
EDIT 1:
Answering your additional question:
fun (el1 : even_list) => forall (el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 : even_list -> Prop
is a function of a single argument, el1 : even_list , which returns the type forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2 . Unofficially, given the list el1 , he builds the statement for every list el2, the length of appending it to el1 is the sum of its length and el1 length .
fun (el1 el2 : even_list) => elength (eapp el1 el2) = elength el1 + elength el2 : even_list -> even_list -> Prop
is a function of two arguments el1 : even_list and el2 : even_list , which returns the type elength (eapp el1 el2) = elength el1 + elength el2 . Unofficially, given the two lists, he builds a statement for these particular two lists, the length of appending them is the sum of their length .
Pay attention to two things: - First, I said “we will build a statement”, which is very different from “building a proof of a statement”. These two functions simply return types / sentences / statements that can be true or false, can be provable or unprovable. - the first, after submitting some list el1 , returns a rather interesting type. If you had proof of this statement, you would know that for any choice of el2 length of adding it to el1 is the sum of the lengths.
In fact, here is another type / statement:
forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2 : Prop
This statement says that for any two lists, the append length is the sum of the lengths.
One thing that can confuse you is that this is happening:
fun (el1 el2 : even_list) => (* some proof of elength (eapp el1 el2) = elength el1 + elength el2 *)
- a member whose type
forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2
which is an expression whose type
Prop
So you see that fun and forall are two related things, but very different. In fact, all forms fun (t : T) => pt is a member whose type is forall (t : T), P t if pt is of type pt .
Therefore, there is confusion when you write:
fun (t : T) => forall (q : Q), foo ^^^^^^^^^^^^^^^^^^^ this has type Prop
because it has a type:
forall (t : T), Prop (* just apply the rule *)
So forall can really appear in two contexts because this calculus is able to calculate types. That way, you can see forall as part of the calculation (which hints that it is a calculation by type), or you can see it in a type (which you usually see). But this is the same forall for all purposes and goals. On the other hand, fun only appears in calculations.