Annotated Natural Deduction to Natural Deductions

%%% Converting annotated natural deduction to natural deductions
%%% in minimal linear logic
%%% Author: Frank Pfenning

i2nd : intro A -> nd A -> type.
e2nd : elim A -> nd A -> type.

%% Coercions

i2nd_e2i : i2nd (e2i E1) D
	    o- e2nd E1 D.

i2nd_i2e : e2nd (i2e I1) D
	    o- i2nd I1 D.

%% Multiplicative Connectives

i2nd_impi : i2nd (impi' I1) (impi D1)
	     o- ({u2:elim A} {h2:nd A}
		   e2nd u2 h2
		   -o i2nd (I1 u2) (D1 h2)).

e2nd_impe : e2nd (impe' I1 E2) (impe D1 D2)
	     o- i2nd I1 D1
	     o- e2nd E2 D2.

i2nd_timesi : i2nd (timesi' I1 I2) (timesi D1 D2)
	       o- i2nd I1 D1
	       o- i2nd I2 D2.

i2nd_timese : i2nd (timese' I1 E2) (timese D1 D2)
	       o- ({u1:elim A} {h1:nd A}
		     {u2:elim B} {h2:nd B}
		     e2nd u1 h1
		     -o e2nd u2 h2
		     -o i2nd (I1 u1 u2) (D1 h1 h2))
	       o- e2nd E2 D2.

i2nd_onei : i2nd (onei') (onei).

i2nd_onee : i2nd (onee' I1 E2) (onee D1 D2)
	     o- i2nd I1 D1
	     o- e2nd E2 D2.

%% Additive Connectives

i2nd_withi : i2nd (withi' (I1 , I2)) (withi (D1 , D2))
	      o- (i2nd I2 D1
		    & i2nd I2 D2).

e2nd_withe1 : e2nd (withe1' E1) (withe1 D1)
	       o- e2nd E1 D1.

e2nd_withe2 : e2nd (withe2' E2) (withe2 D2)
	       o- e2nd E2 D2.

i2nd_topi : i2nd (topi' ()) (topi ())
	     o- <T>.

% no tope

i2nd_plusi1 : i2nd (plusi1' I1) (plusi1 D1)
	       o- i2nd I1 D1.

i2nd_plusi2 : i2nd (plusi2' I2) (plusi2 D2)
	       o- i2nd I2 D2.


i2nd_pluse : i2nd (pluse' (I1 , I2) E3) (pluse (D1 , D2) D3)
	      o- (({u1:elim A} {h1:nd A}
		     e2nd u1 h1
		     -o i2nd (I1 u1) (D1 h1))
		    &
		       ({u2:elim B} {h2:nd B}
			  e2nd u2 h2
			  -o i2nd (I2 u2) (D2 h2)))
	      o- e2nd E3 D3.

% no zeroi

i2nd_zeroe : i2nd (zeroe' () E1) (zeroe () D1)
	      o- e2nd E1 D1.

%% Quantifiers

i2nd_foralli : i2nd (foralli' I1) (foralli D1)
		o- ({a:i} i2nd (I1 a) (D1 a)).

e2nd_foralle : e2nd (foralle' T E1) (foralle T D1)
		o- e2nd E1 D1.

i2nd_existsi : i2nd (existsi' T I1) (existsi T D1)
		o- i2nd I1 D1.

i2nd_existse : i2nd (existse' I1 E2) (existse D1 D2)
		o- ({a:i}
		      {u1:elim (A a)} {h1:nd (A a)}
		      e2nd u1 h1
		      -o i2nd (I1 a u1) (D1 a h1))
		o- e2nd E2 D2.

%% Exponentials

i2nd_!i : i2nd (!i' I1) (!i D1)
	   <- i2nd I1 D1.

i2nd_!e : i2nd (!e' I1 E2) (!e D1 D2)
	   o- ({u1!:elim A} {h1!:nd A}
		 e2nd u1! h1!
		 -> i2nd (I1 u1!) (D1 h1!))
	   o- e2nd E2 D2.

Frank Pfenning