Annotated Natural Deductions to Sequent Derivations

%%% Translating Annotated Natural Deductions to Sequent Derivations
%%% Author: Frank Pfenning

i2lv : intro A -> (pos A -o #) -> type.
e2lv : elim A -> (neg A -o #) -> # -> type.

%% Coercions

i2lv_e2i : i2lv (e2i E1) Q
	    o- ({p:pos A}
		  e2lv E1 ([n^neg A] axiom n p) (Q p)).

e2lv_i2e : e2lv (i2e I1) Q (cut Q1 Q)
	    o- i2lv I1 Q1.

%% Multiplicative Connectives

i2lv_impi : i2lv (impi' I1) (impr Q)
	     o- ({u1:elim A} {n1:neg A}
		   ({Q':neg A -o #} e2lv u1 Q' (Q' n1))
		   -o i2lv (I1 u1) (Q n1)).

e2lv_impe : e2lv (impe' I1 E2) Q Q'
	     o- i2lv I1 Q1
	     o- e2lv E2 (impl Q1 Q) Q'.

i2lv_timesi : i2lv (timesi' I1 I2) (timesr Q1 Q2)
	       o- i2lv I1 Q1
	       o- i2lv I2 Q2.

i2lv_timese : i2lv (timese' I1 E2) Q2
	       o- ({u1:elim A} {n1:neg A}
		     {u2:elim B} {n2:neg B}
		     ({Q':neg A -o #} e2lv u1 Q' (Q' n1))
		     -o ({Q'':neg B -o #} e2lv u2 Q'' (Q'' n2))
		     -o i2lv (I1 u1 u2) (Q1 n1 n2))
	       o- ({p:pos C} 
		     e2lv E2 (timesl ([n1^] [n2^] Q1 n1 n2 p)) (Q2 p)).

i2lv_onei : i2lv (onei') (oner).

i2lv_onee : i2lv (onee' I1 E2) Q2
	     o- i2lv I1 Q1
	     o- ({p:pos C} e2lv E2 (onel (Q1 p)) (Q2 p)).

%% Additive Connectives

i2lv_withi : i2lv (withi' (I1 , I2)) (withr (Q1 , Q2))
	      o- i2lv I1 Q1
		 & i2lv I2 Q2.

e2lv_withe1 : e2lv (withe1' E1) Q Q1
	       o- e2lv E1 (withl1 Q) Q1.

e2lv_withe2 : e2lv (withe2' E2) Q Q2
	       o- e2lv E2 (withl2 Q) Q2.

i2lv_topi : i2lv (topi' ()) (topr ())
	     o- <T>.

% not tope

i2lv_plusi1 : i2lv (plusi1' I1) (plusr1 Q1)
	       o- i2lv I1 Q1.

i2lv_plusi2 : i2lv (plusi2' I2) (plusr2 Q2)
	       o- i2lv I2 Q2.

i2lv_pluse : i2lv (pluse' (I1 , I2) E3) Q3
	      o- (({u1:elim A} {n1:neg A}
		     ({Q':neg A -o #} e2lv u1 Q' (Q' n1))
		     -o i2lv (I1 u1) (Q1 n1))
		    & ({u2:elim B} {n2:neg B}
			 ({Q'':neg B -o #} e2lv u2 Q'' (Q'' n2))
			 -o i2lv (I2 u2) (Q2 n2)))
	      o- ({p:pos C}
		    e2lv E3 (plusl (([n1^] Q1 n1 p) , ([n2^] Q2 n2 p)))
		    (Q3 p)).

% no zeroi

i2lv_zeroe : i2lv (zeroe' () E1) Q1
	      o- <T>
	      o- ({p:pos C}
		    e2lv E1 (zerol ()) (Q1 p)).
%% Quantifiers

i2lv_foralli : i2lv (foralli' I1) (forallr Q1)
		o- ({a:i} i2lv (I1 a) (Q1 a)).

e2lv_foralle : e2lv (foralle' T E1) Q Q1
		o- e2lv E1 (foralll T Q) Q1.

i2lv_existsi : i2lv (existsi' T I1) (existsr T Q1)
		o- i2lv I1 Q1.

i2lv_existse : i2lv (existse' I1 E2) Q2
		o- ({a:i}
		      {u1:elim (A a)} {n1:neg (A a)}
		      ({Q':neg (A a) -o #} e2lv u1 Q' (Q' n1))
		      -o i2lv (I1 a u1) (Q1 a n1))
		o- ({p:pos C}
		      e2lv E2 (existsl ([a:i] [n1:neg (A a)] Q1 a n1 p))
		      (Q2 p)).

%% Exponentials

i2lv_!i : i2lv (!i' I1) (!r Q1)
	   <- i2lv I1 Q1.

i2lv_!e : i2lv (!e' I1 E2) Q2
	   o- ({u1!:elim A} {n1!:neg! A}
		 ({Q':neg A -o #} e2lv u1! Q' (!d Q' n1!))
		 -> i2lv (I1 u1!) (Q1 n1!))
	   o- ({p:pos C} e2lv E2 (!l ([n1!] Q1 n1! p)) (Q2 p)).

Frank Pfenning