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

6. Implication elimination and introduction; metalogic vs. object logic.

The style of inference rules that we use in our object logic,
with introduction rules (such as imp_i, and_i) and elimination rules 
(such as imp_e, and_e1, and_e2) is called "natural deduction."  
Here I will illustrate some more proofs in natural deduction.

Theorem: implication is transitive.
We can encode this theorem in many different ways; here are two
examples:

imp_trans: pf (A imp B) -> pf (B imp C) -> pf (A imp C) = ...

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = ...

imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = ...

What's the difference?  "imp" is the implication connective of
the object logic; "->" is the function arrow of the metalogic.
They play similar roles; in fact, the imp_i and imp_e rules of
the logic can convert between them:

imp_i   : (pf A -> pf B) -> pf (A imp B).
imp_e   : pf (A imp B) -> pf A -> pf B.

For practical purposes, we can view the three versions of imp_trans
as proving almost the same thing, but with different "user interfaces".
For example, suppose we know

y: tm num.
fact1: pf (  (eq y (plus y y))  imp  (eq y zero)  ).
fact2: pf (  (eq y zero)  imp  (eq (times y y) zero) ).

(Load these three declarations with control-c control-d).

Then we can prove  (eq y (plus y y))  imp  (eq (times y y) zero)
as follows:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
 hole ( (eq y (plus y y))  imp  (eq (times y y) zero) ).

(Load this definition.)
To fill the hole, we can use imp_i, as follows: 

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_i [p1: pf (eq y (plus y y))]
  hole ((eq (times y y) zero) ).

(Load this.)
Now, to fill the remaining hole, we need a proof of  y*y=0.
The proof "fact2" can provide this for us, using implication-elimination:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_i [p1: pf (eq y (plus y y))]
  imp_e fact2 (hole (eq y zero)).

(Load this.) Imp_e takes two arguments -- a proof of (A imp B) and a proof
of A -- and produces a proof of B.  It is sometimes called "modus ponens".
In our case, A is "eq y zero", and our proof of it is a hole.

To prove "eq y zero" we can use fact1, which requires another imp_e:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_i [p1: pf (eq y (plus y y))]
  imp_e fact2 
  (imp_e
   (hole (eq y (plus y y)  imp  eq y zero))
   (hole (eq y (plus y y)))).

(Load this.) Now it's a simple matter to fill the two holes:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_i [p1: pf (eq y (plus y y))]
  imp_e fact2 
  (imp_e
   fact1
   p1).

   (hole (eq y (plus y y)))).

(Load this version of fact3.)  What's the stray line (hole (eq y ...
doing there?  Well, in editing the proof to fill in the holes, I inserted
p1 into the proof and just left the hole there.  This doesn't bother
the Twelf-Emacs "Check Declaration" command (control-c control-d) and
it reminds me what hole I'm filling.  Check Declaration stops at the
first period or the first blank line, whichever comes first.
But now that the proof is finished, it would be wise to delete the
stray lines, because they will confuse the "Check File" (control-c control-s)
and "Check Configuration" (control-c control-c) commands.

Now let's return to proving imp_trans:

imp_trans: pf (A imp B) -> pf (B imp C) -> pf (A imp C) =  ...

It's a metalogic function of two arguments -- these are the
"premises" of the proof -- so the implementation of imp_trans can
start with two formal parameters:

imp_trans: pf (A imp B) -> pf (B imp C) -> pf (A imp C) = 
  [p1: pf (A imp B)]
  [p2: pf (B imp C)]
  hole (A imp C).

(Load this.)  Twelf rejects this; fix the problem and continue.
In fact, now you should be able to complete the proof by filling
the hole.  Do this exercise; if you get stuck, the answer is
in proving2a.elf.  (Note: if your current buffer  "proving2.elf" is
read-only, you should visit a new (writable) file "anything.elf"
to do your work.)

Now let's prove 

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = ...

Since this is not a Twelf function -- it is just a single proof object --
there are no formal parameters:

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = 
  hole ((A imp B) imp (B imp C) imp (A imp C)).

(Load this.)  The imp operator binds more tightly on the right.  Visit
the file coreTCB/logic.elf and search for "%infix right 10 imp" to
see how the syntactic precedence of imp is declared.
Thus, what we want to prove is equivalent to (in fully parenthesized form):

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = 
  hole ((A imp B) imp ((B imp C) imp (A imp C))).

(Load this.)  This is just an implication, so we can use imp_i:

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = 
  imp_i [p1: pf (A imp B)]
  hole ((B imp C) imp (A imp C)).

Now the hole is just another implication, so we can use imp_i again:

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = 
  imp_i [p1: pf (A imp B)]
  imp_i [p2: pf (B imp C)]
  hole (A imp C).

To fill the hole, we could repeat the proof of imp_trans, but instead
we can just use imp_trans as a lemma:

imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = 
  imp_i [p1: pf (A imp B)]
  imp_i [p2: pf (B imp C)]
  imp_trans p1 p2.

That was easy.

Finally, let us prove 

imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = ...

This is a function of two parameters, so we have

imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = 
  [p1: pf A -> pf B]
  [p2: pf B -> pf C]
  % need a value of type   pf A -> pf C
  .

(Load this if you like, but it will fail.)
We have a comment "% need a value" instead of a hole, because
"hole" can only construct a thing of type "pf(X)" for some X, but
we need something of type "pf(A)->pf(B)".   Since what we need
is a function, we can make a formal parameter for it,

%abbrev
imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = 
  [p1: pf A -> pf B]
  [p2: pf B -> pf C]
  [p3: pf A]
  hole C.

(Load this.)  Now we can fill the hole using the proof-constructor p2:


%abbrev
imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = 
  [p1: pf A -> pf B]
  [p2: pf B -> pf C]
  [p3: pf A]
  p2 (hole B).

Finally, we can fill this hole using the proof-constructor p1:

%abbrev
imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = 
  [p1: pf A -> pf B]
  [p2: pf B -> pf C]
  [p3: pf A]
  p2 (p1 p3).

(Load this.) Now that we've used all the arguments, it might seem that 
we can delete the %abbrev keyword:

imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = 
  [p1: pf A -> pf B]
  [p2: pf B -> pf C]
  [p3: pf A]
  p2 (p1 p3).

(Load this; it fails!)  This is a real annoyance.  It can be evaded
using the following hack, which I will introduce here but explain in
a later section.

imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = 
  [p1: pf A -> pf B]
  [p2: pf B -> pf C]
  [p3: pf A]
  strictify A (strictify B (
   strictify_pf_pf p1 (strictify_pf_pf p2 (strictify_pf p3 (
  p2 (p1 p3)))))).

This is really ugly; there's no need (yet) to understand it.  But in
any case the theorem is proved. (Load it.)

Now, we have our three versions of the "imp is transitive" theorem:

imp_trans: pf (A imp B) -> pf (B imp C) -> pf (A imp C) = ...
imp_trans_x: pf ((A imp B) imp (B imp C) imp (A imp C)) = ...
imp_trans_y: (pf A -> pf B) -> (pf B -> pf C) -> (pf A -> pf C) = ...

Suppose we had

y: tm num.
fact1: pf (  (eq y (plus y y))  imp  (eq y zero)  ).
fact2: pf (  (eq y zero)  imp  (eq (times y y) zero) ).

and we wish to prove fact3; then imp_trans is most convenient:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_trans fact1 fact2.

(Load this.)

Using imp_trans_x is almost as convenient, but we need imp_e:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_e (imp_e imp_trans_x fact1) fact2.

Actually, formulas with multiple implications are so common that
there's a lemma "imp2_e" to do two imp-eliminations in a row:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp2_e imp_trans_x fact1 fact2.

Similarly, there is imp3_e, imp4_e, etc.

Using imp_trans_y, we would need to insert imp_e and imp_i:

fact3: pf ( (eq y (plus y y))  imp  (eq (times y y) zero) ) =
  imp_i (imp_trans_y (imp_e fact1) (imp_e fact2)).

(Load this.  Then figure out how it works.)

Depending on how you think the theorem will be used in practice, you
may state your theorem with object-logic implication (as in imp_trans_x), 
metalogic implication (as in imp_trans_y), or a mixture (as in imp_trans).
The most generally useful seems to be the mixed format (imp_trans).


7.  Or, false, not.

The natural deduction rules for or, false, not, are as follows (from
core/basiclem.elf):

or_i1   : pf A -> pf (A or B) 
or_i2   : pf B -> pf (A or B)
or_e    : pf (A or B) -> (pf A -> pf C) -> (pf B -> pf C) -> pf C 

false_e : pf false -> pf A 

not_i : (pf A -> pf false) -> pf (not A) 
not_e : pf (not A) -> pf A -> pf false 

Given these declarations (load them):

y: tm num.
fact5: pf (eq y zero imp not (gt y zero)).
fact6: pf (eq y zero imp not (lt y zero)).

Let us prove,

theorem7: pf ((gt y zero) or (lt y zero)) -> pf (not (eq y zero)) = ...

We start in the usual way:

%abbrev
theorem7: pf ((gt y zero) or (lt y zero)) -> pf (not (eq y zero)) = 
 [p1: pf (gt y zero  or  lt y zero)]
 hole (not (eq y zero)).
 
To prove a negation, we can use not_i:

%abbrev
theorem7: pf ((gt y zero) or (lt y zero)) -> pf (not (eq y zero)) = 
 [p1: pf (gt y zero  or  lt y zero)]
 not_i [p2: pf (eq y zero)]
 hole false.

Now we've got an extra "fact" (y=0) but we have to prove a contradiction
("false").  This is called "reductio ad absurdum", reduction to the absurd.

Now we can try to make use of p1.  or_e takes p1 and then two
extra arguments, each of which is a function.  Therefore, the 2nd and
3rd argument of or_e will each take a formal parameter that is a proof:

%abbrev
theorem7: pf ((gt y zero) or (lt y zero)) -> pf (not (eq y zero)) = 
 [p1: pf (gt y zero  or  lt y zero)]
 not_i [p2: pf (eq y zero)]
 or_e p1
 ([p11: pf (gt y zero)]
  hole false)
 ([p21: pf (lt y zero)]
  hole false).

Each of these two functions will have a "result" that is the same
as what we were trying to prove when we did the or-elimination;
in this case, "false".

Now, in the first hole we can use fact5 to prove (not (y>0)).
But p11 is a proof of (y>0).  When we have a proof of   not X  and a proof
of X, we can use not_e to prove "false":

%abbrev
theorem7: pf ((gt y zero) or (lt y zero)) -> pf (not (eq y zero)) = 
 [p1: pf (gt y zero  or  lt y zero)]
 not_i [p2: pf (eq y zero)]
 or_e p1
 ([p11: pf (gt y zero)]
  not_e (hole (not (gt y zero))) (hole (gt y zero)))
 ([p21: pf (lt y zero)]
  hole false).

(Load this.)
Now we fill in the holes of the not_e:

%abbrev
theorem7: pf ((gt y zero) or (lt y zero)) -> pf (not (eq y zero)) = 
 [p1: pf (gt y zero  or  lt y zero)]
 not_i [p2: pf (eq y zero)]
 or_e p1
 ([p11: pf (gt y zero)]
  not_e (imp_e fact5 p2) p11)
 ([p21: pf (lt y zero)]
  hole false).

Exercise:  fill in the other hole and delete the %abbrev.
(Solution: proving2b.elf)

In contrast, or introduction is easy.  Let us prove

or_symm:  pf (A or B) -> pf (B or A) = ...

Exercise:  do this yourself.  Start out with or-elimination.
Then, within each branch, use or_i1 or or_i2. 
The solution is in core/basiclem.elf.

More exercises:  Prove each of the following theorems.
Solutions can be found in core/basiclem.elf.

not_imp_i: pf (A and not B) -> pf (not (A imp B)) 

a_or_b_and_not_a : pf (A or B) -> pf (not A) -> pf B

or3_e: pf (A1 or A2 or A3) -> (pf A1 -> pf C) -> (pf A2 -> pf C)
                -> (pf A3 -> pf C) -> pf C

distribute_or_and_1 : pf ((A and B) or C) -> pf ((A or C) and (B or C))

distrib_imp_and_1 : pf (A imp (B and C)) -> pf ((A imp B) and (A imp C))

and_imp : pf (A imp B imp C) -> pf ((A and B) imp C)



Visit proving3.elf to continue the tutorial.