Coq -- understanding `forall` syntax

Question

I'm learning Coq by reading the book "Certified Programming with Dependent Types" and I'm having trouble udnerstanding forall syntax.

As an example let's think this mutually inductive data type: (code is from the book)

Inductive even_list : Set :=
| ENil : even_list
| ECons : nat -> odd_list -> even_list

with odd_list : Set :=
| OCons : nat -> even_list -> odd_list.

and this mutually recursive function definitions:

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.

and we have induction schemes generated:

Scheme even_list_mut := Induction for even_list Sort Prop
with odd_list_mut    := Induction for odd_list Sort Prop.

Now what I don't understand is, from the type of even_list_mut I can see it takes 3 arguments:

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

But in order to apply it we need to supply it two parameters, and it replaces the goal with 3 premises (for P ENil, forall (n : nat) (o : odd_list), P0 o -> P (ECons n o) and forall (n : nat) (e : even_list), P e -> P0 (OCons n e) cases).

So it's like it actually gets 5 parameters, not 3.

But then this idea fails when we think of this types:

fun el1 : even_list =>
  forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2
       : even_list -> Prop

and

fun el1 el2 : even_list => elength (eapp el1 el2) = elength el1 + elength el2
     : even_list -> even_list -> Prop

Can anyone explain how does forall syntax work?

Thanks,

Ptival Ptival · Accepted Answer · 2013-07-04T09:57:31

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 n o)) ->  (* 4 *)
     (forall (n : nat) (e : even_list), P e -> P0 (OCons n e)) -> (* 5 *)
     forall e : even_list,                                        (* 6 *)
     P e

You can think of the arrow as just syntactic sugar:

A -> B
===
forall _ : A, B

So you could rewrite even_list_mut this way:

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

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:

div_not_zero :
  forall (a b : Z) (Anot0 : a <> 0), a / b <> 0

And I apply it to the goal 42 / 23 <> 0. Coq is able to figure out that a ought to be 42 and b ought to be 23. The only goal left is to prove 42 <> 0. But indeed, Coq implicitly passes 42 and 23 as arguments to div_not_zero.

I 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 one argument, el1 : even_list, which returns the type forall el2 : even_list, elength (eapp el1 el2) = elength el1 + elength el2. Informally, given a list el1, it constructs the statement for every list el2, the length of appending it to el1 is the sum of its length and el1's 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. Informally, given two lists, it constructs the statement for these particular two lists, the length of appending them is the sum of their length.

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 el1, returns a quite interesting type. If you had a proof of that statement, you would know that for any choice of el2, the length of appending it to el1 is the sum of lengths.

In fact, here is another type/statement to consider:

forall (el1 el2 : even_list), elength (eapp el1 el2) = elength el1 + elength el2
: Prop

This statement says that for any two lists, the length of appending is the sum of the lengths.

One thing that may be confusing you too is that this is going on:

fun (el1 el2 : even_list) =>
  (* some proof of elength (eapp el1 el2) = elength el1 + elength el2 *)

is a term whose type is

forall (el1 el2 : even_list),
  elength (eapp el1 el2) = elength el1 + elength el2

which is a statement whose type is

Prop

So you see that fun and forall are two things related but very different. In fact, everything of the form fun (t : T) => p t is a term whose type is forall (t : T), P t, assuming p t has type P t.

Therefore, the confusion arises when you write:

fun (t : T) => forall (q : Q), foo
               ^^^^^^^^^^^^^^^^^^^
               this has type  Prop

because this has type:

forall (t : T), Prop (* just apply the rule *)

So forall can indeed appear in two contexts, because this calculus is able to compute types. Therefore, you might see forall 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 forall for all intents and purposes. On the other hand, fun only appears in computations.

Coq -- understanding `forall` syntax

1 Answers