%{Main conclusions:

Think about one context
The context might be dynamically extended.
We do not consider coloring yet.

In the example of nd to seq:

Start with empty context:

        ctx ::= .
        
During the proof: (since splitting over nd)

        ctx ::= . | ctx, x:nd A

The proof requires introduction of left assumptions.

        ctx ::= . | ctx, x:nd A, y:left A

with this context, the proof goes through.

Statement of the theorem: 

        For all contexts: ctx
          forall formulas A,
          forall derivations D : nd A. 
                using assumptions from ctx
          exists derivation  P : right A.
                using assumptions from ctx

Example:

Consider the proof of A imp A.

Context :   
        Let A be formula, ctx = .
        Proof of nd (A imp A) :   (impr ([u:nd A] u))
        
        first step   ctx = u:nd A, l:left A
        prove it for u:nd A  => l:left A
        
        Apply axiom         (axiom l) : right A
        apply impr (which empties the context):  
                impr (axiom l) : right A imp A        
        and ctx = .



The proof as a function


nd2seq' =
  rec F. cun G. pfun A:o. fun D:nd A.
    case D of
    | %u% => (ccase %u% of               /* Parameter case */
                [%u%:nd A', %l% :left A'] => axiom %l%)   
    | lam ([u:nd A'] D' u) =>
        new u:nd A. impr ([v:left A'] F (G, u:nd A', v:left A') A' (D' u))
    | app D1' D2' => cut (F G (A1 => A2) D1') 
                        ([X5:left (A1 => A2)]
                        impl (F G  A1 D2') ([X6:left A2] init X6) X5)

nd2seq = pfun A:o. fun D:nd A. nd2seq' (.) A D 

======================================================================
Example: natural deduction to hilbert deduction

        After the proof
        
        ctx ::= . | ctx, u : ! A, v : |- A  

Statement of the theorem:


        Generalize the abstraction lemma:
        Forall context ctx
        Forall formulas ctx |- A, B
        If ctx |--  |- A implies |-B 
        then ctx |-- |- A imp B   


        Forall context ctx
        Forall formulas ctx |-- A  (:o)
        Forall natural deduction derivations ctx |-- D (: ! A)
        Exists hilbert deduction   ctx |-- H ( : |- A) 
        true.

        where forall u : ! A in ctx (!)
        there exists x : |-- A in ctx (|--)


abs = 
  rec F. cun G. pfun A:o. pfun B:o. fun D: |- A -> |- B.
    case D of 
      [x: |- A] %v% => MP K v
    | [x: |- A] x => MP (MP S K) K 
    ... 2 cases as before ...
    | [x: |- A] MP (D1 x) (D2 x) =>
        MP (MP S (F G (A1 => A2) ([x:|- A] D1 x)))
           (F G A2 ([x: |- A] D2 x))

nd2hil' = 
  rec F. cun G. pfun A:o. fun D: ! A.
    case D of
      %u% => ccase u of
               [u: ! A, v: |- A] => v
    | impliesI ([u: ! A1'] D' u) =>
        new u:! A1'. abs G A1' A2'
                        ([v: |- A1'] F A2' (G, u: ! A1', v: |- A1')) (D' u)
    | impliesE D1' D2' => (MP (F G (A1' imp A2') D1') (F G A1' D2'))

new introduces parameter which cannot occur in the result because
of subordination.


% Cut Admissibilty:


Context 

  G ::= . | G, u : hyp A


Admissibility of cut as function:


ca =
  rec F. cun G. fun C. fun A:o. fun D: conc A. fun E: hyp A -> conc C. 
  case D of 
    axiom H' => E H'
  | impr  ([u: hyp A'] D' u) =>
      case E of
        [u' : hyp (A' imp B')] axiom A'' (F' u') => 
          case F' of 
            [u' : hyp A''] u' => (impr ([u: hyp A'] D' u))      (* A'' = A imp B *) 
          | [u' : hyp A''] %u% => axiom %u%
      | [u' : hyp (A' imp B')] impr  ([u: hyp A''] D'' u u') =>  
          impr ([u: hyp A''] F (G, u: hyp A'') (A imp B) 
            (impr ([u: hyp A'] D' u)) 
            ([u' : hyp (A' imp B')] (D'' u u')))
      | [u' : hyp (A' imp B')] impl  (F1' u') ([u: hyp B''] F2' u' u) (F3' u') =>
          case F3' of
            [u' : hyp (A' imp B')] u' =>  (* A'' = A', B'' = B' *)
              (F G B'
                (F G A' 
                  (F G (A' imp B') (impr  ([u: hyp A'] D' u)) ([u' : hyp (A' imp B')] F1' u'))
                  ([u: hyp A'] D' u))
                ([u: hyp B'] F (G, u : hyp B') (A' imp B') (impr ([u: hyp A'] D' u))
                  ([u' : hyp (A' imp B')] F2' u' u)))
          | [u' : hyp (A' imp B')] %u% =>  
              (impl
                  (F G (A' imp B') (impr  ([u: hyp A'] D' u)) ([u' : hyp (A' imp B')] F1' u'))
                  ([u: hyp B'] F (G, u : hyp B') (A' imp B') (impr ([u: hyp A'] D' u))
                  ([u' : hyp (A' imp B')] F2' u' u))
                %u%)
  | impl D1' ([u: hyp A3'] D2' u) ([v: hyp A2' imp A3'] D3' v) =>
      case E of 
        [u' : hyp C'] axiom A'' (F' u') => 
          case F' of 
            [u' : hyp A''] u' => (impl D1' ([u: hyp A3'] D2' u) ([v: hyp A2' imp A3'] D3' v))
          | [u' : hyp A''] %u% => axiom %u%
      | [u' : hyp C'] impr ([u: hyp A''] E'' u u') =>  
          impl D1' 
            ([u:hyp A3'] F (G, u:hyp A3') (D2' u) ([u' : hyp C'] impr ([u'': hyp A''] E'' u'' u')))
      | [u' : hyp C'] impl (E1' u') ([u: hyp B''] E2' u' u) (E3' u') =>
          (impl D1' 
            ([u'': hyp A3'] F (G, u'':hyp A3') A1' (D2 u'') 
                                ([u' : hyp C'] impl (E1' u') ([u: hyp B''] E2' u' u) (E3' u')))
            ([v: hyp A2' imp A3'] D3' v))



% Note sometimes variables get instantiated... how exactly?


- look at the copy example.
- ccase is a little strange
- first try for implementation should allow the user to express the theorems as above.
- instances of the context should be named for relational representation.
- how does it generalize to more structured contexts?
- compare to lambda box


The copy example:

exp : type.
app : exp -> exp -> exp.
lam : (exp -> exp) -> exp.

cp : exp -> exp -> type.
cp_app : cp (app D1 D2) (app E1 E2) 
         <- cp D1 E1
         <- cp D2 E2.
cp_lam : cp (lam ([x:exp] D x)) (lam ([x:exp] E x))
         <- ({x:exp} cp x x -> cp (D x) (E x)). 

Form of the context:
        
        ctx ::= . | ctx, x : exp, u : cp x x 

        forall context ctx
        forall expressions ctx |-- x : exp
         exists derivation  ctx |-- D : cp x x

 
        rec F. cun G. fun x:exp.
          case x of
          | %x% => ccase G(%x%) of
                       %x% : exp, %u% : cp %x% %x% => %u%                                            
          | app D1 D2 =>
              cp_app (F G D1) (F G D2)
          | lam ([x:exp] D x) = >
              cp_lam ([x:exp] [u: cp x x] F (G, x : exp, u: cp x x) (D x))


The copy example with coloring:

exp : type.
app : exp -> exp -> exp.
lam : (exp -> exp) -> exp.

exp' : type.
app' : exp' -> exp' -> exp'.
lam' : (exp' -> exp') -> exp'.

cp : exp -> exp' -> type.
cp_app : cp (app D1 D2) (app' E1 E2) 
         <- cp D1 E1
         <- cp D2 E2.
cp_lam : cp (lam ([x:exp] D x)) (lam' ([y:exp'] E x y))
         <- ({x:exp} {y:exp'} cp x y -> cp (D x) (E y)). 

Form of the context:
        
        ctx ::= . | ctx, x : exp, y : exp', u : cp x y

        forall context ctx
        forall expressions ctx |-- x : exp
        exists expression  ctx |-- y : exp'
         exists derivation  ctx |-- D : cp x y


         rec F. cun G. fun x:exp. 
          case x of
          | %x% => ccase G(%x%) of
                       %x% : exp, %y% : exp', %u% : cp %x% %y% => <%y%, %u%>
             | app D1 D2 =>
              let <X, E1> = (F G D1) in
                let <Y, E2> = (F G D2) in
                  <app X Y, cp_app E2 E1>
                  
          | lam ([x:exp] D x) = >
              new x:exp. new y:exp'. new u:cp x y.
                  let <Y, E> = F (G, x: exp , y:exp', u: cp x y) (D x) in 
                   <lam [y:exp'] Y, cp_lam ([x: exp] [y:exp'] [u: cp x y] E x y u)>

          | lam ([x:exp] D x) = >
                  let [x:exp] [y:exp'] [u:cp x u] <Y y, E x y u> =
                    [x:exp] [y:exp'] [u:cp x y] F (G, x: exp , y:exp', u: cp x y) (D x) in 
                   <lam Y, cp_lam E>

More than one result can be unpleasant...



Representation of the non-colored version in a box like calculus.


 
        rec F. cun G. fun x:exp.
          case x of
          | %x% => ccase G(%x%) of
                       %x% : exp, %u% : cp %x% %x% => %u%                                            
          | app D1 D2 =>
              cp_app (F G D1) (F G D2)
          | lam ([x:exp] D x) = >
              cp_lam ([x:exp] [u: cp x x] F (G, x : exp, u: cp x x) (D x))


        fun x: $exp. 
           it x < exp -> {x: exp} cp x x > of
             app => [D1: cp x x] [D2:  
             lam D =>     


I don't know how to do it.



A third order example: call_cc



exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.
callcc : ((exp -> exp) -> exp) -> exp.

exp' : type.
lam' : (exp' -> exp') -> exp'.
app' : exp' -> exp' -> exp'.
callcc' : ((exp' -> exp') -> exp') -> exp'.

cp : exp -> exp' -> type.

cp_app : cp E1 F1 -> cp E2 F2 -> cp (app E1 E2) (app' F1 F2).
cp_lam : ({x:exp} {y:exp'} cp x y -> cp (E x) (F y)) 
          -> cp (lam [x:exp] E x) (lam [y:exp'] F y).
cp_callcc: ({c:exp -> exp} {d:exp' -> exp'}
             ({x:exp} {y:exp'} cp x y -> cp (c x) (d y)) 
             -> cp (E c) (F d))
             -> cp (callcc [c:exp -> exp] E c) (callcc [d:exp' -> exp'] F d).


        
        ctx ::= . | ctx, x : exp, y : exp', u : cp x y
                  | ctx, c : exp -> exp, d : exp' -> exp',
                         f : ({x:exp} {y:exp'} cp x y -> cp (c x) (d y)) 

        forall context ctx
        forall expressions ctx |-- x : exp
        exists expression  ctx |-- y : exp'
         exists derivation  ctx |-- D : cp x y


         rec COPY. cun G. fun x:exp. fun y:exp'.
          case x of
          | %x% => ccase G(%x%) of
                       %x% : exp, %y% : exp', %u% : cp %x% %y% => <%y%, %u%>
          | %c% D => ccase G (%c%) of
                       %c% : exp -> exp, %d% : exp' -> exp',
                         %f% : ({x:exp} {y:exp'} cp x y -> cp (%c% x) (%d% y)) 
                     => let <E, F> = (COPY G D)
                        in <%d% E, %f% D E F>
                        end
          | app D1 D2 =>
              let <X, E1> = (COPY G D1) in
                let <Y, E2> = (COPY G D2) in
                  <app X Y, cp_app E2 E1>
          | lam ([x:exp] D x) =>
                  let [x:exp] [y:exp'] [u:cp x u] <Y y, E x y u> =
                    [x:exp] [y:exp'] [u:cp x y] COPY (G, x: exp , y:exp', u: cp x y) (D x) in 
                   <lam Y, cp_lam E>
          | callcc ([c:exp -> exp] D c) =>
                let [c:exp -> exp] [d:exp' -> exp'] 
                        [f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)]
                           <Y d, E c d f> =        
                    [c:exp -> exp] [d:exp' -> exp'] 
                        [f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)]
                            (COPY (G, c:exp -> exp, d:exp' -> exp', 
                                   f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)) (D c)
                 in
                  <callcc [d:exp' -> exp'] Y d, cp_callcc ([c:exp -> exp] [d:exp' -> exp'] 
                        [f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)] E c d f)>


A fourth order example: quantifying over call_cc's

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.
callcc : ((exp -> exp) -> exp) -> exp.
reset  : (((exp -> exp) -> exp) -> exp) -> exp.

exp' : type.
lam' : (exp' -> exp') -> exp'.
app' : exp' -> exp' -> exp'.
callcc' : ((exp' -> exp') -> exp') -> exp'.
reset'  : (((exp' -> exp') -> exp') -> exp') -> exp'.

cp : exp -> exp' -> type.

cp_app : cp E1 F1 -> cp E2 F2 -> cp (app E1 E2) (app' F1 F2).
cp_lam : ({x:exp} {y:exp'} cp x y -> cp (E x) (F y)) 
          -> cp (lam [x:exp] E x) (lam [y:exp'] F y).
cp_callcc: ({c:exp -> exp} {d:exp' -> exp'}
             ({x:exp} {y:exp'} cp x y -> cp (c x) (d y)) 
             -> cp (E c) (F d))
             -> cp (callcc [c:exp -> exp] E c) (callcc [d:exp' -> exp'] F d).
cp_reset: ({c: (exp -> exp) -> exp} {d: (exp' -> exp') -> exp'}
            ({f: exp -> exp} {g: exp' -> exp'} 
              ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))
              -> cp (c f) (d g))
            -> cp (E c) (F d))
          -> cp (reset [c: (exp -> exp) -> exp] E c) 
                (reset [d: (exp' -> exp') -> exp'] F d) 

        
        ctx ::= . | ctx, x : exp, y : exp', u : cp x y
                  | ctx, c : exp -> exp, d : exp' -> exp',
                         f : ({x:exp} {y:exp'} cp x y -> cp (c x) (d y)) 
                  | ctx, c: (exp -> exp) -> exp, d: (exp' -> exp') -> exp',
                         h: {f: exp -> exp} {g: exp' -> exp'} 
                            ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))
                              -> cp (c f) (d g)        



         rec COPY. cun G. fun x:exp. fun y:exp'.
          case x of
          | %x% => ccase G(%x%) of
                       %x% : exp, %y% : exp', %u% : cp %x% %y% => <%y%, %u%>
          | %c% D => ccase G (%c%) of
                       %c% : exp -> exp, %d% : exp' -> exp',
                         %f% : ({x:exp} {y:exp'} cp x y -> cp (%c% x) (%d% y)) 
                     => let <e, f> = (COPY G D)
                        in <%d% e, %f% D e f>
                        end
          | %c% [x: exp] D x => ccase G (%c%) of
                      %c%: (exp -> exp) -> exp, %d%: (exp' -> exp') -> exp',
                      %h%: {f: exp -> exp} {g: exp' -> exp'} 
                            ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))
                              -> cp (%c% f) (%d% g)        
                      => let  [x:exp] [y:exp'] [u:cp x y] <Y y, E x y u>
                             = [x:exp] [y:exp'] [u:cp x y]  (* this context is already 
                                                                 defined, maybe we should define
                                                                 a new one because it's for a 
                                                                 different order? *)
                                   COPY (G, x:exp, y:exp', u: cp x y) (D x)
                         in 
                           <%d% [y:exp'] Y y, %h% ([x:exp] D x) ([y : exp'] Y y)    
                                                  ([x:exp] [y:exp'] [u:cp x y] E x y u)> 
          | app D1 D2 =>
              let <X, E1> = (COPY G D1) in
                let <Y, E2> = (COPY G D2) in
                  <app X Y, cp_app E2 E1>
          | lam ([x:exp] D x) =>
                  let [x:exp] [y:exp'] [u:cp x u] <Y y, E x y u> =
                    [x:exp] [y:exp'] [u:cp x y] COPY (G, x: exp , y:exp', u: cp x y) (D x) in 
                   <lam Y, cp_lam E>
          | callcc ([c:exp -> exp] D c) =>
                let [c:exp -> exp] [d:exp' -> exp'] 
                        [f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)]
                           <Y d, E c d f> =        
                    [c:exp -> exp] [d:exp' -> exp'] 
                        [f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)]
                            COPY (G, c:exp -> exp, d:exp' -> exp', 
                                   f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)) (D c)
                 in
                  <callcc [d:exp' -> exp'] Y d, cp_callcc ([c:exp -> exp] [d:exp' -> exp'] 
                        [f: {x:exp} {y:exp'} cp x y -> cp (c x) (d y)] E c d f)>
           
          | reset ([c: (exp -> exp) -> exp] D c)
              let  [c: (exp -> exp) -> exp] [d: (exp' -> exp') -> exp']
                     [h: {f: exp -> exp} {g: exp' -> exp'} 
                            ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))
                              -> cp (c f) (d g)] <Y d, E c d h>
                 = [c: (exp -> exp) -> exp] [d: (exp' -> exp') -> exp']
                     [h: {f: exp -> exp} {g: exp' -> exp'} 
                            ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))
                              -> cp (c f) (d g)] 
                        COPY (G, c: (exp -> exp) -> exp, d: (exp' -> exp') -> exp',
                                      h: {f: exp -> exp} {g: exp' -> exp'} 
                                        ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))
                                   -> cp (c f) (d g)) (D c)
              in 
                <reset [d: (exp' -> exp') -> exp'] Y d,
                 cp_reset [c: (exp -> exp) -> exp] [d: (exp' -> exp') -> exp']
                     [h: {f: exp -> exp} {g: exp' -> exp'} 
                            ({x: exp} {y:exp'} cp x y -> cp (f x) (g y))] E c d h>
                





A last example: Copying of typing derivations:
Explicit coloring:

exp : type.
lam : (exp -> exp) -> exp.
app : exp -> exp -> exp.

tp  : type.
=>  : tp -> tp -> tp.    %infix left 39 =>.

of : exp -> tp -> type.
of_lam : ({x:exp} of x T1 -> of (E x) T2) -> of (lam E) (T1 => T2).
of_app : of E1 (T2 => T1) -> of E2 T2 -> of (app E1 E2) T1.
 
 	 
of' : exp -> tp -> type.
of_lam' : ({x:exp} of' x T1 -> of' (E x) T2) -> of (lam E) (T1 => T2).
of_app' : of' E1 (T2 => T1) -> of' E2 T2 -> of' (app E1 E2) T1.


cp : of E T -> of' E T -> type. 
cp_app : cp D1 D1' -> cp D2 D2' -> cp (of_app D1 D2) (of_app' D1' D2').
cp_lam : ({x:exp} {u:of x T1} {u':of' x T1} cp u u' -> cp (D1 x u) (D1' x u'))
	  -> cp (of_lam [x:exp] [u:of x T1] D1 x u) (of_lam' [x:exp] [u':of' x T1] D1' x u').



Form of a context:

	ctx ::= . | ctx,  x: exp, u: of x T1, u' :of' x T1, e : cp u u'
 	 

        forall context ctx
        forall expressions ctx |-- e : exp
	forall types       ctx |-- t : exp
	forall derivations ctx |-- d : of e t
        exists derivation  ctx |-- d' : of' e t
        exists derivation  ctx |-- E : cp d d'
	true 


rec COPY. cun G. fun e: exp. fun t: tp. fun d: of e t.
  case d 
  of %u% => ccase G(%u%) of
	      %x%:exp, %u%: of %x% T1, %u'% :of' %x% T1, %e%: cp %u% %u'% => <%u'%, %e%>
  | of_lam ([x:exp] [u: of x T1] D1 x u) : of (lam ([x:exp] E' x) (T1 => T2)) =>
      let <[x:exp] [u:of x T1] [u': of' x T1] [e: cp u u'] d1' x u', 
	   [x:exp] [u:of x T1] [u': of' x T1] [e: cp u u'] e1 x u u' e> = 
	 COPY (G, x:exp, u: of x T1, u' of x T1, e: cp u u')  (E' x) T2 (D1 x u)  
      in  <of_lam' ([x : exp] [u': of' x T1] d1' x u'), 
		cp_lam  ([x:exp] [u:of x T1] [u': of' x T1] [e: cp u u'] e1 x u u' e)>
  | of_app D1 D2 : of (app E1 E2) T1 => 
      let <d1', e1> = COPY G E1 (T2 => T1) D1 
	let <d2', e2> = COPY  G E2 T2 D2
	  in <of_app' d1' d2', cp_app e1 e2>