Natural Deductions to Annotated Natural Deductions

%%% Annotating Minimal Linear Natural Deductions.
%%% Author: Frank Pfenning
%%%
%%% Implementation is also linear, over linear index derivations.

nd2i : nd A -> intro A -> type.
nd2e : nd A -> elim A -> type.

%% Multiplicative Connectives

nd2i_impi : nd2i (impi D1) (impi' I1)
	     o- ({h:nd A} {u:elim A}
		   nd2e h u & nd2i h (e2i u)
		   -o nd2i (D1 h) (I1 u)).

nd2e_impi : nd2e (impi D1) (i2e I)
	     o- nd2i (impi D1) I.

nd2i_impe : nd2i (impe D1 D2) (e2i E)
	     o- nd2e (impe D1 D2) E.

nd2e_impe : nd2e (impe D1 D2) (impe' I1 E2)
	     o- nd2i D1 I1
	     o- nd2e D2 E2.

nd2i_timesi : nd2i (timesi D1 D2) (timesi' I1 I2)
	       o- nd2i D1 I1
	       o- nd2i D2 I2.

nd2e_timesi : nd2e (timesi D1 D2) (i2e I)
	       o- nd2i (timesi D1 D2) I.

nd2i_timese : nd2i (timese D1 D2) (timese' I1 E2)
	       o- ({h1:nd A} {u1:elim A}
		     {h2:nd B} {u2:elim B}
		     nd2e h1 u1
		     & nd2i h1 (e2i u1)
		     -o nd2e h2 u2
		        & nd2i h2 (e2i u2)
		        -o nd2i (D1 h1 h2) (I1 u1 u2))
	       o- nd2e D2 E2.

nd2e_timese : nd2e (timese D1 D2) (i2e I)
	       o- nd2i (timese D1 D2) I.

nd2i_onei : nd2i (onei) (onei').

nd2e_onei : nd2e (onei) (i2e I)
	     o- nd2i (onei) I.

nd2i_onee : nd2i (onee D1 D2) (onee' I1 E2)
	     o- nd2i D1 I1
	     o- nd2e D2 E2.

nd2e_onee : nd2e (onee D1 D2) (i2e I)
	     o- nd2i (onee D1 D2) I.

%% Additive Connectives

nd2i_withi : nd2i (withi (D1 , D2)) (withi' (I1 , I2))
	      o- nd2i D1 I1
		 & nd2i D2 I2.

nd2e_withi : nd2e (withi (D1 , D2)) (i2e I)
	      o- nd2i (withi (D1 , D2)) I.

nd2i_withe1 : nd2i (withe1 D1) (e2i E)
	       o- nd2e (withe1 D1) E.

nd2i_withe2 : nd2i (withe2 D2) (e2i E)
	       o- nd2e (withe2 D2) E.

nd2e_withe1 : nd2e (withe1 D1) (withe1' E1)
	       o- nd2e D1 E1.

nd2e_withe2 : nd2e (withe2 D2) (withe2' E2)
	       o- nd2e D2 E2.

nd2i_topi : nd2i (topi ()) (topi' ())
	     o- <T>.

nd2e_topi : nd2e (topi ()) (i2e I)
	     o- nd2i (topi ()) I.

% no tope

nd2i_plusi1 : nd2i (plusi1 D1) (plusi1' I1)
	       o- nd2i D1 I1.

nd2i_plusi2 : nd2i (plusi2 D2) (plusi2' I2)
	       o- nd2i D2 I2.

nd2e_plusi1 : nd2e (plusi1 D1) (i2e I)
	       o- nd2i (plusi1 D1) I.

nd2e_plusi2 : nd2e (plusi2 D2) (i2e I)
	       o- nd2i (plusi2 D2) I.

nd2i_pluse : nd2i (pluse (D1 , D2) D3) (pluse' (I1 , I2) E3)
	      o- (({h1:nd A} {u1:elim A}
		     nd2e h1 u1 & nd2i h1 (e2i u1)
		     -o nd2i (D1 h1) (I1 u1))
		    & ({h2:nd B} {u2:elim B}
			 nd2e h2 u2 & nd2i h2 (e2i u2)
			 -o nd2i (D2 h2) (I2 u2)))
	      o- nd2e D3 E3.

nd2e_pluse : nd2e (pluse (D1 , D2) D3) (i2e I)
	      o- nd2i (pluse (D1 , D2) D3) I.

% no zeroi

nd2i_zeroe : nd2i (zeroe () D1) (zeroe' () E1)
	      o- nd2e D1 E1
	      o- <T>.

nd2e_zeroe : nd2e (zeroe () D1) (i2e I1)
	      o- nd2i (zeroe () D1) I1.

%% Quantifiers

nd2i_foralli : nd2i (foralli D1) (foralli' I1)
		o- ({a:i} nd2i (D1 a) (I1 a)).

nd2e_foralli : nd2e (foralli D1) (i2e I)
		o- nd2i (foralli D1) I.

nd2i_foralle : nd2i (foralle T D1) (e2i E)
		o- nd2e (foralle T D1) E.

nd2e_foralle : nd2e (foralle T D1) (foralle' T E1)
		o- nd2e D1 E1.

nd2i_existsi : nd2i (existsi T D1) (existsi' T I1)
		o- nd2i D1 I1.

nd2e_existsi : nd2e (existsi T D1) (i2e I)
		o- nd2i (existsi T D1) I.

nd2i_existse : nd2i (existse D1 D2) (existse' I1 E2)
		o- ({a:i}
		      {h1:nd (A a)} {u1:elim (A a)}
		      nd2e h1 u1 & nd2i h1 (e2i u1)
		      -o nd2i (D1 a h1) (I1 a u1))
		o- nd2e D2 E2.

nd2e_existse : nd2e (existse D1 D2) (i2e I)
		o- nd2i (existse D1 D2) I.

%% Exponentials

nd2i_!i : nd2i (!i D1) (!i' I1)
	   <- nd2i D1 I1.

nd2e_!i : nd2e (!i D1) (i2e I)
	   o- nd2i (!i D1) I.

nd2i_!e : nd2i (!e D1 D2) (!e' I1 E2)
	   o- ({h!:nd A} {u!:elim A}
		 nd2e h! u! & nd2i h! (e2i u!)
		 -> nd2i (D1 h!) (I1 u!))
	   o- nd2e D2 E2.

nd2e_!e : nd2e (!e D1 D2) (i2e I)
	   o- nd2i (!e D1 D2) I.

Frank Pfenning