***DRAFT*** (Sep 1, 2006)

Syntax

t = A | t->t | t/\t | %t

=======================================================

Source language rules:

G = {...t...}

G,t |- t

G,ta |- tb
-----------
G |- ta->tb

G |- ta->tb
G |- ta
-----------
G |- tb

G |- t1
G |- t2
-----------
G |- t1/\t2

G |- t1/\t2
----------- k in {1,2}
G |- tk

G |- t
-------
G |- %t

G |- %(ta->tb)
G |- %ta
-----------
G |- %tb

=======================================================

Target language rules: See figure 4.1 of Simpson (omitting False and \/)

G = {...w(t)...}

G,w(t) |- w(t)

G,w(ta) |- w(tb)
----------------
G |- w(ta->tb)

G |- w(ta->tb)
G |- w(ta)
--------------
G |- w(tb)

G |- w(t1)
G |- w(t2)
--------------
G |- w(t1/\t2)

G |- w(t1/\t2)
-------------- k in {1,2}
G |- w(tk)

G,wRw' |- wRw'

G,wRw' |- w'(t)
---------------- where w' does not appear in G |- w(%t)
G |- w(%t)

G |- w(%t)
G |- wRw'
----------
G |- w'(t)

G |- w(t)
G |- wRw'
----------
G |- w'(t)
  (note: not in Simpson)

=======================================================

Lemma[soundness]

If t1...tn |- t0
then w(t1)...w(tn) |- w(t0)

Proof by induction on t1...tn |- t0.


CASE

G,t |- t
G = t1...tn
G' = w(t1)...w(tn)
G',w(t) |- w(t)


CASE

G,ta |- tb
-----------
G |- ta->tb

G = t1...tn
G' = w(t1)...w(tn)
induction: G',w(ta) |- w(tb)

  G',w(ta) |- w(tb)
  -----------------
  G' |- w(ta->tb)


CASE

G |- ta->tb
G |- ta
-----------
G |- tb

G = t1...tn
G' = w(t1)...w(tn)
induction: G' |- w(ta->tb)
induction: G' |- w(ta)

  G' |- w(ta->tb)
  G' |- w(ta)
  ---------------
  G' |- w(tb)


EASY CASES:

G |- t1
G |- t2
-----------
G |- t1/\t2

G |- t1/\t2
----------- k in {1,2}
G |- tk


CASE

G |- t
-------
G |- %t

G = t1...tn
G' = w(t1)...w(tn)
induction: G' |- w(t)
By weakening, G',wRw' |- w(t) where w' is fresh.

  G',wRw' |- w(t)
  ----------------
  G',wRw' |- w'(t)
  ----------------
  G' |- w(%t)


CASE

G |- %(ta->tb)
G |- %ta
-----------
G |- %tb

G = t1...tn
G' = w(t1)...w(tn)
induction: G' |- w(%(ta->tb))
induction: G' |- w(%ta)
By weakening: 
  G',wRw' |- w(%(ta->tb))
  G',wRw' |- w(%ta)
where w' is fresh.

  G',wRw' |- w(%(ta->tb))    G',wRw' |- w(%ta)
  -----------------------    -----------------
  G',wRw' |- w'(ta->tb)      G',wRw' |- w'(ta)
  --------------------------------------------
  G',wRw' |- w'(tb)
  -----------------
  G' |- w(%tb)

=======================================================

Definitions.

Let Graph(G,w1,...,wn) be the smallest directed graph satisfying:
  - Graph(G,...wk...) contains a node wk
  - if G contains w'Rw'', then Graph(G,w) contains a node w', a node w'',
    and an edge from w' to w''

Say that a graph contains a path w1...wn (where n>=1) if for
each wk,wk+1, wk and wk+1 are nodes in the graph and there is
an edge in the graph from wk to wk+1.  Call a path w1...wn "a path
from w1 to wn".

Define a list with head w1 and tail wn to be a directed graph with
nodes w1,w2,...,wn (where n>=1) where for each wk,wk+1 there is an edge
from wk,wk+1, and there are no other edges.

Define the depth "Depth(L,w')" of a node w' in a list L to be the distance from L's head to the node.

For any context G, let w(G) be the union of the following sets:
  - {w'(t) in G | there is a path from w' to w in Graph(G)}
  - {w''Rw' in G | there is a path from w' to w in Graph(G)}

=======================================================

Lemma[Possible future irrelevance]:
 (1) if G |- w(t) then w(G) |- w(t)
 (2) if G |- wRw' then w'(G) |- wRw'

Proof by induction on derivation of G |- w(t).

CASE

G,w(t) |- w(t)

w(G,w(t)) contains w(t), so:
w(G,w(t)) |- w(t)


CASE

G,w(ta) |- w(tb)
----------------
G |- w(ta->tb)

induction: w(G,w(ta)) |- w(tb)
w(G,w(ta)) = w(G) union {w(ta)}, so w(G),w(ta) |- w(tb)
  w(G),w(ta) |- w(tb)
  -------------------
  w(G) |- w(ta->tb)


EASY CASES:

G |- w(ta->tb)
G |- w(ta)
--------------
G |- w(tb)

G |- w(t1)
G |- w(t2)
--------------
G |- w(t1/\t2)

G |- w(t1/\t2)
-------------- k in {1,2}
G |- w(tk)


CASE

G,wRw' |- wRw'

w'(G,wRw') contains wRw', so w'(G,wRw') |- wRw'


CASE

G,wRw' |- w'(t)
---------------- where w' does not appear in G |- w(%t)
G |- w(%t)

induction: w'(G,wRw') |- w'(t)

w' does not appear in G, so Graph(G,wRw') equals Graph(G) with
one extra node w' and one extra edge from w to w'.  Therefore,
any path from any node w1 in Graph(G,wRw') to w' go through w
(unless w1=w').  Therefore:
  w'(G,wRw') = w(G),wRw'
so:
  w(G),wRw' |- w'(t)
  ------------------
  w(G) |- w(%t)


CASE

G |- w(%t)
G |- wRw'
----------
G |- w'(t)

induction: w(G) |- w(%t)
By inversion, G contains wRw', so Graph(G) contains an edge from w to w'.
Therefore, for any path from any node w1 in Graph(G) to w, there is
a path in Graph(G) from w1 to w'.  Therefore, w(G) is a subset of w'(G).
By weakening:  w'(G) |- w(%t).
Since w'(G) contains wRw', w'(G) |- wRw'.
  w'(G) |- w(%t)
  w'(G) |- wRw'
  --------------
  w'(G) |- w'(t)


CASE

G |- w(t)
G |- wRw'
----------
G |- w'(t)

induction: w(G) |- w(t)
Just as in the previous case, conclude w'(G) |- w(t) and w'(G) |- wRw'.
  w'(G) |- w(t)
  w'(G) |- wRw'
  --------------
  w'(G) |- w'(t)


=======================================================

Define [G] = ...t... where G = ...w(t)...

Lemma[completeness]:
  if   G |- wn(t)
  and  Graph(G,wn) is a list L = w1...wn
  then there is some ...tk... such that
    [G],...tk... |- t
    and there is a mapping F from each tk to some j where 1<=j<n
    and for each tk:
      [wj(G)],...ti... |- %tk
      where F(tk)=j and ...F(ti)<j...
Corollary: if |- w1(t) then |- t
Proof of corollary:
  L = w1, so n = 1.
  There is no j such that 1<=j<1, so there are no tk.
  Therefore |- t.

Proof of lemma by induction on G |- wn(t).

CASE

G,w(t) |- w(t)

[G],t |- t
[G,w(t)] |- t


CASE

G,wn(ta) |- wn(tb)
------------------
G |- wn(ta->tb)

Graph((G,wn(ta)),wn) = Graph(G,wn)

induction: [G,wn(ta)],...tk... |- tb
           for each tk: [wj(G,wn(ta))],...ti... |- %tk where j<n
When j<n, wj(G,wn(ta)) = wj(G).
[G,wn(ta)] = [G],ta
  [G],ta,...tk... |- tb
  ----------------------
  [G],...tk... |- ta->tb
goal:
  [G],...tk... |- ta->tb
  for each tk: [wj(G)],...ti... |- %tk


CASE

G |- w(ta->tb)
G |- w(ta)
--------------
G |- w(tb)

induction:
    [G],...tk... |- ta->tb
    [G],...tk'... |- ta
  Let ...tk''... = ...tk...,...tk'...
  By weakening:
    [G],...tk''... |- ta->tb
    [G],...tk''... |- ta
  Conclude [G],...tk''... |- tb.


CASE

G |- w(t1)
G |- w(t2)
--------------
G |- w(t1/\t2)

induction:
    [G],...tk... |- t1
    [G],...tk'... |- t2
  Let ...tk''... = ...tk...,...tk'...
  By weakening:
    [G],...tk''... |- t1
    [G],...tk''... |- t2
  Conclude [G],...tk''... |- t1/\t2.


CASE

G |- w(t1/\t2)
-------------- z in {1,2}
G |- w(tz)

induction: [G],...tk... |- t1/\t2
  Conclude [G],...tk... |- tz.


CASE

G,wRw' |- wRw'

not applicable


CASE

G,(wn)R(wn+1) |- wn+1(t)
------------------------ where wn+1 does not appear in G |- wn(%t)
G |- wn(%t)

Let L = Graph(G,wn) = w1...wn.
Let L' = Graph((G,(wn)R(wn+1))).
Since wn+1 does not appear in Graph(G,wn), L' is a list, equal to w1...wn,wn+1.

induction:
    [G,(wn)R(wn+1)],...tk'... |- t
    and for each tk', [wj(G,(wn)R(wn+1))],...ti'... |- %tk'
      where F(tk')=j and ...F(ti')<j...
  [G,(wn)R(wn+1)] = [G]
  Since 1<=j<n+1 for each F(tk')=j, wj(G,(wn)R(wn+1)) = wj(G).
Each tk' falls into one of two categories:
  (1) F(tk')=j where 1<=j<n.
  (2) F(tk')=j where j=n.
Let ...tk... be all the tk' from category (1).  For each of these, we have:
  [wj(G,(wn)R(wn+1))],...ti'... |- %tk, where F(tk)=j and ...F(ti')<j...
  [wj(G)],...ti'... |- %tk where F(tk)=j and ...F(ti')<j...
We also know [G],...tk'... |- t, but to use this to prove [G],...tk... |- %t,
we must somehow remove the category (2) tk' from the assumptions (since
these are not part of ...tk...).
For each category (2) tk', we know [wj(G)],...ti'... |- %tk'.
  Since [wj(G)] is a subset of [G], we can weaken this to:
    [G],...ti'... |- %tk'
  Since for each ti', F(ti')<j and F(tk')=j=n, we know F(ti')<n, so ti' is
  category (1) and is one of the ...tk....  Therefore, we can weaken to:
    [G],...tk... |- %tk'
Let tk1'...tkm' be the tk' from category (2).
Now we can derive:
    [G],...tk...,tkm',...,tk2',t1' |- t
    ----------------------------------------
    [G],...tk...,tkm',...,tk2' |- tk1'->t
    ----------------------------------------
    ...
    ----------------------------------------
    [G],...tk...,tkm' |- ...->tk2'->tk1'->t
    ----------------------------------------
    [G],...tk... |- tkm'->...->tk2'->tk1'->t
    -------------------------------------------
    [G],...tk... |- %(tkm'->...->tk2'->tk1'->t)       [G],...tk... |- %tkm'
    -----------------------------------------------------------------------
    ...
    -----------------------------------------------------------------------
    [G],...tk... |- %(tk2'->tk1'->t)                  [G],...tk... |- %tk2'
    -----------------------------------------------------------------------
    [G],...tk... |- %(tk1'->t)                        [G],...tk... |- %tk1'
    -----------------------------------------------------------------------
    [G],...tk... |- %(t)

goal: [G],...tk... |- %t and for each tk,
  [wj(G)],...ti... |- %tk where F(tk)=j and ...F(ti)<j...


CASE

G |- wn(%t)
G |- (wn)R(wn+1)
----------------
G |- wn+1(t)

By inversion, (wn)R(wn+1) appears in G, so Graph(G,wn+1) contains an edge
from wn to wn+1.
Let L' = Graph(G,wn+1) = w1...wn,wn+1.
Let L = Graph(wn(G),wn) = w1...wn.
By the possible future irrelevance lemma, wn(G) |- wn(%t).

induction:
    [wn(G)],...tk... |- %t
    and there is a mapping F from each tk to some j where 1<=j<n
    and for each tk:
      [wj(G)],...ti... |- %tk
      where F(tk)=j and ...F(ti)<j...
Here we "pass the buck" by adding t to the tk, making it trivial to verify t:
    [G],...tk...,t |- t
Now the t must satisfy the same conditions that the tk satisfy.
Let F(t) = n.  Then 1<=F(t)<n+1 and for t, let ...ti... = ...tk...:
    [wn(G)],...tk... |- %t where F(t)=n and ...F(ti)<n...

goal:
    [G],...tk...,t |- t
    and there is a mapping F from each tk to some j where 1<=j<n+1
    and for each tk:
      [wj(G)],...ti... |- %tk where F(tk)=j and ...F(ti)<j...
    and F(t) = j where 1<=j<n+1 and:
      [wj(G)],...ti... |- %t where F(t)=j and ...F(ti)<j...


CASE

G |- wn(t)
G |- (wn)R(wn+1)
----------------
G |- wn+1(t)

By inversion, (wn)R(wn+1) appears in G, so Graph(G,wn+1) contains an edge
from wn to wn+1.
Let L' = Graph(G,wn+1) = w1...wn,wn+1.
Let L = Graph(wn(G),wn) = w1...wn.
By the possible future irrelevance lemma, wn(G) |- wn(t).

induction:
    [wn(G)],...tk... |- t
    and there is a mapping F from each tk to some j where 1<=j<n
    and for each tk:
      [wj(G)],...ti... |- %tk
      where F(tk)=j and ...F(ti)<j...

By weakening, [G],...tk... |- t.
For each tk, 1<=F(tk)<n implies 1<=F(tk)<n+1.

goal:
    [G],...tk... |- t
    and there is a mapping F from each tk to some j where 1<=j<n+1
    and for each tk:
      [wj(G)],...ti... |- %tk where F(tk)=j and ...F(ti)<j...