Hints on proving theorems in Twelf, continued
                  Andrew W. Appel
                  February 2000


8.  Twelf metalogic quantification.

Recall the theorem about symmetry of conjunction:

symm_and: pf (A and B) -> pf (B and A) =
 [p1: pf (A and B)]
 and_l p1
        [p2: pf A]
        [p3: pf B]
 and_i p3 p2.

In this theorem, A and B are "formula variables".  What we mean is
that for any formula A, and any formula B, from a proof of formula (A and B) 
we can construct a proof of (B and A).  Statements like "for any" are
called "universal quantification", and when we write a variable
starting with a capital letter, Twelf implicitly assumes that the
variable is universally quantified.

In Twelf we can explicitly write the universal quantification, using
curly braces.  The fully explicit form of the theorem is

symm_and_x: {A: tm form}{B: tm form}pf (A and B) -> pf (B and A) =
 [A: tm form][B: tm form]
 [p1: pf (A and B)]
 and_l p1
        [p2: pf A]
        [p3: pf B]
 and_i p3 p2.

Note that we explicitly quantify {A} and {B} in the type of symm_and_x,
and we explicitly bind [A] and [B] in the body of symm_and_x.
In general, a curly-brace binding in a Twelf type will correspond
to a square-bracket binding in the Twelf value.

Now, load the value symm_and_x (control-c control-d), and examine
the output in the *twelf-server* buffer.  It will look like this,
which is just a restatement of what was loaded.

symm_and_x : {A:tm form} {B:tm form} pf (A and B) -> pf (B and A)
   = [A:tm form] [B:tm form] [p1:pf (A and B)]
        and_l p1 ([p2:pf A] [p3:pf B] and_i p3 p2).

Next, load the value symm_and (above), and examine the output.
It looks like this:

symm_and : {A:tm form} {B:tm form} pf (A and B) -> pf (B and A)
   = [A:tm form] [B:tm form] [p1:pf (A and B)]
        and_l p1 ([p2:pf A] [p3:pf B] and_i p3 p2).

This is not exactly what was loaded; instead, it is the explicitly
quantified version of symm_and.  Even though Twelf reports the
same thing for symm_and_x and symm_and, these theorems are not
interchangeable.  To use symm_and_x, one must explictly provide
actual parameters corresponding to A and B.  Compare these two
proofs of the same thing:

y: tm num.
fact8: pf (gt y zero  and   lt y (const 10)).

theorem9: pf (lt y (const 10) and gt y zero) = 
  symm_and fact8.

theorem10: pf (lt y (const 10) and gt y zero) = 
  symm_and_x (gt y zero) (lt y (const 10)) fact8.

As you can see, the explicit formal parameter [A: tm form] of
symm_and_x demands an argument -- in this case, (gt y zero) --
and similarly for [B: tm form].

Usually there is no need to write your theorems with explicit metalogic
quantification (i.e., curly braces).  However, it can be useful
in some circumstances, such as debugging of Twelf error messages.
Furthermore, it's good to have some understanding of what Twelf is
doing internally, and the first thing that Twelf does is (internally)
make all quantification explicit.

9.  Types in the object logic.

In the object logic we have numbers, formulas, predicates, and so on.
Each has its own object-logic type:

O.L.Type               Examples

num                    (const 7)   (plus A (const 2))    zero
form                   true   false     (A and (B imp C))
num arrow form         (lam [X] gt X zero)

An object-logic type is called a "tp".  (const 7) is a term of type "num"
in the object logic; we can write this fact in the metalogic as

seven: tm num = const 7.

In coreTCB/logic.elf you can see the following declarations:

tp     : type.
tm     : tp -> type.
form   : tp.
arrow  : tp -> tp -> tp.  %infix right 14 arrow.
pf     : tm form -> type.

That is, "tp" is a metalogic type.  "tm" is a metalogic constructor
that takes a tp and returns a type.  Therefore, since "form" is a tp,
"tm form" is a type in Twelf.  We can pronounce "tm form" as "object-logic
term of type formula" or just "formula" for short.  For example:

a8: tm form =  (gt y zero  and   lt y (const 10)).

Now consider the predicate "odd", which takes a number and tells
whether it is an odd integer:

odd: tm (num arrow form) = 
   lam [X] exists [N] isInt N and eq X (plus (times N two) one).

(Load this definition.)  By the way, we have a predicate isInt (in
coreTCB/arith.elf) because not all nums are integers:

x: tm num = const 3.7.

To apply an object-logic function (or predicate) to an argument, use
the @ operator:

a9: tm form =   odd @ seven.

Here we have a predicate of type "num arrow form", an argument of type
"num", so the application yields a term of type "form", a formula.
(The @ operator is declared in coreTCB/logic.elf.)

This "odd" is an object-logic predicate.  In contrast, "isInt" is
a metalogic predicate (declared in coreTCB/arith.elf):

odd: tm (num arrow form) = ...
isInt: tm num -> tm form.

a10: tm form =  isInt seven.

Why have application both in the object logic and in the metalogic?
Because we want to quantify over predicates in the object logic.
We would like to say, "Any predicate over numbers that accepts all odd
numbers must also accept 5".  We can write this as,

a11: tm form = forall [F] (forall [X] odd @ X imp F @ X) imp F @ (const 5).

For any T, our object logic can quantify (i.e., with "forall") over terms
of type T.  To see this, let's examine a more explicit version of a11:

a11: tm form = forall [F: tm (num arrow form)] 
                           (forall [X: tm num] odd @ X imp F @ X) 
                         imp F @ (const 5).

In this case, the first forall quantifies over terms of type "num arrow form",
and the second one quantifies over terms of type "num".
But we cannot quantify over something of type "tm num -> tm form", because
this is not a term type in our object logic; it is a function from
terms to terms.

The difference between object-logic functions (using "arrow") and
metalogic functions (using  -> )  may seem trivial, and in some sense
it is.  The redundancy can sometimes be annoying.  But it seems to
be a necessity, or at least, the least annoying solution.

10.  Creating object-logic functions and predicates.

The operator "lam", short for the lambda of lambda-calculus which creates
function expressions, is defined in coreTCB/logic.elf:

lam    : (tm T1 -> tm T2) -> tm (T1 arrow T2).
@      : tm (T1 arrow T2) -> tm T1 -> tm T2.  
%infix left 20 @.

Lam converts a metalogic function to an object logic function.
For example, isInt is a metalogic function (tm num -> tm form);
but

isInt_x : tm (num arrow form) = lam isInt.

is an object-logic function.

Here's another example:

odd_big: tm num -> tm form =  [N] odd @ N and gt N (const 100).

odd_big_x: tm (num arrow form) = lam odd_big.

But it's much more common to write object-logic functions by applying
"lam" directly to a meta-logic lambda-expression:

odd_big_x: tm (num arrow form) = lam [N] odd @ N and gt N (const 100).

Exercise: complete these definitions, and load them into Twelf
(control-c control-d) to make sure they type-check.

int_nonzero: tm (num arrow form) = % integer and nonzero

even: tm (num arrow form) = % integer and not odd, or if you like,
                            % there exists an integer N such that 2*N ...

square: tm num -> tm num =  % square(x) = x*x.

double: tm (num arrow (num arrow form)) = % double(x,y) iff x+x=y.

Solutions are in proving3a.elf.

NOTE: Before continuing, load all the definitions from proving3a.elf;
you can do this by visiting proving3a.elf and doing control-c control-s.

When a metalogic function is applied to an argument, the expression
is automatically interchangeable with the expansion of the
definition.  That is, the expressions

 (odd_big three)
 (odd @ three and gt three (const 100))

mean the same in all contexts (assuming the definition of odd_big
above).  However, (odd_big_x @ three) is not the same as these two;
instead, it is the same as

 ((lam [N] odd @ N and gt N (const 100)) three)

The "beta" rule (in core/basiclem.elf) relates a metalogic function
to an object-logic function:

beta : pf (eq ((lam F) @ X) (F X)) = ...

Thus, the following proof:

oddbig_p: pf (eq (odd_big_x @ three) (odd @ three and gt three (const 100))) =
 beta.

11.  Object logic quantification.

In our object logic there are formula constructors forall, exists, 
and proof-constructors forall_i, forall_e, exists_i, exists_e.
Forall and its inference rules are in coreTCB/logic.elf,
exists and its lemmas are in coreTCB/coredefs.elf and core/basiclem.elf.

forall : (tm T -> tm form) -> tm form.
forall_i : ({X:tm T}pf (A X)) -> pf (forall A).
forall_e : pf(forall A) -> {X:tm T}pf (A X).

exists : (tm T -> tm form) -> tm form = ...
exists_i : {X:tm T}pf (A X) -> pf(exists A) = ...
exists_e : pf (exists A) -> ({X:tm T} pf (A X) -> pf B) -> pf B = ...

The _i rules introduce a quantifier (forall or exists), and the _e 
rules eliminate a quantifier.

To introduce a forall, for example to prove a formula  "forall [X] F(X)", 
we must show some meta-logic function G(X), such that for any X, G(X)
is a proof of F(X).  This is easier than it sounds.  Let's take an
example:

fact12: pf (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)) = ...

This theorem says that for any X, if X is odd and greater than zero,
than X is odd.  Here's how to prove it.  Step one is the usual,
create a hole, and load the definition into Twelf just to make
sure we are on the right track:

fact12: pf (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)) =  
  hole (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)).

Step two is to use the forall_i rule to create a proof of forall:

fact12: pf (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)) =  
  forall_i [X]
  hole ((odd @ X and gt X zero) imp (odd @ X)).

Now we have to prove the implication, which can be done using imp_i:

fact12: pf (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)) =  
  forall_i [X]
  imp_i [p1: pf (odd @ X and gt X zero)]
  hole (odd @ X).

When we have a proof of "and", the natural way to get at the pieces
is to use and_l:

fact12: pf (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)) =  
  forall_i [X]
  imp_i [p1: pf (odd @ X and gt X zero)]
  and_l p1
        [p2: pf (odd @ X)]
        [p3: pf (gt X zero)]
  hole (odd @ X).

Now we have a "hole (odd @ X)" within the scope of [p2: pf (odd @ X)],
so we can just fill the hole with p2:

fact12: pf (forall [X: tm num] (odd @ X and gt X zero) imp (odd @ X)) =  
  forall_i [X]
  imp_i [p1: pf (odd @ X and gt X zero)]
  and_l p1
        [p2: pf (odd @ X)]
        [p3: pf (gt X zero)]
  p2.

(Load this definition.)

Now a more interesting one.  Let's prove a11 (from above):

thm11: pf (forall [F: tm (num arrow form)] 
                           (forall [X: tm num] odd @ X imp F @ X) 
                         imp F @ (const 5)) =
 hole (forall [F: tm (num arrow form)] 
                           (forall [X: tm num] odd @ X imp F @ X) 
                         imp F @ (const 5)).

Do the forall_i and imp_i steps yourself.  (Solution: proving3b.elf)

Now we have to prove (F @ const 5), but we have available a proof p1 of
(forall [X: tm num] odd @ X imp F @ X).  

Suppose we had a proof of (odd @ (const 5) imp F @ (const 5)).
Then we'd be able to complete the proof.  We can illustrate this
hypothesis by using a hole:

thm11: pf (forall [F: tm (num arrow form)] 
                           (forall [X: tm num] odd @ X imp F @ X) 
                         imp F @ (const 5)) =
 forall_i [F]
 imp_i [p1: pf (forall [X: tm num] odd @ X imp F @ X)]
 imp_e (hole (odd @ (const 5) imp F @ (const 5))) (hole (odd @ const 5)).

In fact, this proof has two holes.  The second one (odd @ const 5) is
obviously true, but I haven't yet shown you all that you need for proving it.
So here's a proof (you don't need to understand the details of this proof):

odd5: pf (odd @ (const 5)) = 
  def1_i 
  (exists_i two 
   (and_i 
    (congr isInt 
     (symm eval_plus)
     (closure_add p_one p_one))
     (congr ([Z] eq five (plus Z one)) eval_times
      (symm eval_plus)))).

(Load this definition.)
To fill the other hole, we must use p1. To make use of a forall fact,
we use forall-elimination.  Forall_e requires a proof of forall [X] H(X),
and a value X1, and produces a proof of H(X1).  Thus:

(forall_e p1 (const 5))   is a proof of (odd @ const 5 imp F @ const 5).

This completes our proof of thm11:

thm11: pf (forall [F: tm (num arrow form)] 
                           (forall [X: tm num] odd @ X imp F @ X) 
                         imp F @ (const 5)) =
 forall_i [F]
 imp_i [p1: pf (forall [X: tm num] odd @ X imp F @ X)]
 imp_e (forall_e p1 (const 5)) odd5.


Now for existential quantification.  We wish to prove that there is
a number >= 100:

thm12: pf (exists [X] geq X (const 100)) = ...

We do this by exists_i, which takes two arguments:  a value Y, and
a proof that Y is greater than 100.  So what value should we use?
A simple idea is to use 100.

thm12: pf (exists [X] geq X (const 100)) = 
  exists_i (const 100)
  hole (geq (const 100) (const 100)).

Load this definition.  It fails.  The problem is that function application
in the metalogic binds more tightly on the left, so that our attempt
is equivalent to

thm12: pf (exists [X] geq X (const 100)) = 
  (exists_i (const 100)
  hole) (geq (const 100) (const 100)).

which is nonsensical.  The properly parenthesized proof is

thm12: pf (exists [X] geq X (const 100)) = 
  exists_i (const 100)
  (hole (geq (const 100) (const 100))).

(Load this definition.)  To prove 100>=100, we can use the 
ord_reflexivity rule (from coreTCB/arith.elf):

ord_reflexivity : pf (geq A A).

Therefore:

thm12: pf (exists [X] geq X (const 100)) = 
  exists_i (const 100)
  ord_reflexivity.

Load this definition.

To make use of an existential, we use exists_e.  That is, we have
available a fact "exists [I] F(I)" and we eliminate the existential
in this fact to get "F(J)" for some unknown J.

Suppose we wish to prove:

thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = ...

We start in the usual way:

%abbrev
thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = 
  [p1: pf (exists [I] isInt I and Mystery @ (plus I I))]
  hole (exists [N] even @ N and Mystery @ N).

Now it's tempting to use exists_i to prove exists [N] ...
but we don't know what value of N to use.  So we must make use of p1:

thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = 
  [p1: pf (exists [I] isInt I and Mystery @ (plus I I))]
  exists_e p1 [I]
        [p2: pf (isInt I and Mystery @ (plus I I))]
  hole (exists [N] even @ N and Mystery @ N).

(Load this definition.  Note that I've removed %abbrev because p1 is now
used.)  We still don't know what number the variable I stands for,
but we do know  (isInt I and Mystery @ (plus I I)).  We use and_l:

thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = 
  [p1: pf (exists [I] isInt I and Mystery @ (plus I I))]
  exists_e p1 [I]
        [p2: pf (isInt I and Mystery @ (plus I I))]
  and_l p2
        [p3: pf (isInt I)]
        [p4: pf (Mystery @ (plus I I))]
  hole (exists [N] even @ N and Mystery @ N).

Now we guess that N=(plus I I), and we can use exists_i:

thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = 
  [p1: pf (exists [I] isInt I and Mystery @ (plus I I))]
  exists_e p1 [I]
        [p2: pf (isInt I and Mystery @ (plus I I))]
  and_l p2
        [p3: pf (isInt I)]
        [p4: pf (Mystery @ (plus I I))]
  exists_i (plus I I)
  (hole (even @ (plus I I) and Mystery @ (plus I I))).

We can break up the hole into two smaller holes:

thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = 
  [p1: pf (exists [I] isInt I and Mystery @ (plus I I))]
  exists_e p1 [I]
        [p2: pf (isInt I and Mystery @ (plus I I))]
  and_l p2
        [p3: pf (isInt I)]
        [p4: pf (Mystery @ (plus I I))]
  exists_i (plus I I)
  (and_i
   (hole (even @ (plus I I)))
   (hole (Mystery @ (plus I I)))).

(Load this definition.) The first hole can be filled with the following
lemma:

even_i: pf (isInt N) -> pf (even @ (plus N N)) =
 [p1: pf (isInt N)]
 def1_i (exists_i N (and_i p1 refl)).

(Load this definition.  If it fails, then go back to NOTE above and follow
the instructions there, and try even_i again.)

The second hole in thm14 can be filled with p4, yielding:

thm14: pf (exists [I] isInt I and Mystery @ (plus I I)) ->
       pf (exists [N] even @ N and Mystery @ N) = 
  [p1: pf (exists [I] isInt I and Mystery @ (plus I I))]
  exists_e p1 [I]
        [p2: pf (isInt I and Mystery @ (plus I I))]
  and_l p2
        [p3: pf (isInt I)]
        [p4: pf (Mystery @ (plus I I))]
  exists_i (plus I I)
  (and_i
   (even_i p3)
   p4).


Continue in proving4.elf.