%%% Representation of the Proof of Type Preservation
%%% Author: Frank Pfenning

%%% Algorithmic subtyping

below : tp -> tp -> type.		%name below B b.
below' : tp -> tp -> type.		%name below' B' b'.
%mode below +T +S.
%mode below' +T +S.

% Intersections
below_&r : below T (S1 & S2)
	     <- below T S1
	     <- below T S2.

below_&l1 : below' (T1 & T2) S
	     <- below' T1 S.
below_&l2 : below' (T1 & T2) S
	     <- below' T2 S.

% Top
below_topr : below T (top).
% no below_topl rules

% Coercion
below_ : below T S
	   <- below' T S.

% Atomic types
below_nn : below' nat nat.
below_pn : below' pos nat.
below_pp : below' pos pos.
below_zn : below' zero nat.
below_zz : below' zero zero.

% Product types
below_* : below' (T1 * T2) (S1 * S2)
	       <- below T1 S1
	       <- below T2 S2.

% Function types
below_=> : below' (T1 => T2) (S1 => S2)
	       <- below S1 T1
	       <- below T2 S2.

% Cannot check termination because of contravariance

% Monotonicity
mon1 : below T S -> below (T & T') S -> type.
%mode +{T:tp} +{S:tp} +{T':tp} +{B:below T S} -{B':below (T & T') S}
      mon1 B B'.

mon1_&r : mon1 (below_&r B2 B1) (below_&r B2' B1')
	   <- mon1 B1 B1'
	   <- mon1 B2 B2'.
mon1_topr : mon1 (below_topr) (below_topr).
mon1' : mon1 (below_ B) (below_ (below_&l1 B)).

%total B (mon1 B _).

mon2 : below T S -> below (T' & T) S -> type.
%mode +{T:tp} +{S:tp} +{T':tp} +{B:below T S} -{B':below (T' & T) S}
      mon2 B B'.

mon2_&r : mon2 (below_&r B2 B1) (below_&r B2' B1')
	   <- mon2 B1 B1'
	   <- mon2 B2 B2'.
mon2_topr : mon2 (below_topr) (below_topr).
mon2' : mon2 (below_ B) (below_ (below_&l2 B)).

%total B (mon2 B _).

% Reflexivity is admissible

refl : {T:tp} below T T -> type.
%mode refl +T -B.
refl_& : refl (and S1 S2) (below_&r B12_2 B12_1)
	   <- refl S1 B11
	   <- refl S2 B22
	   <- mon1 B11 B12_1
	   <- mon2 B22 B12_2.
refl_top : refl (top) (below_topr).
refl_n : refl nat (below_ below_nn).
refl_p : refl pos (below_ below_pp).
refl_z : refl zero (below_ below_zz).
refl_* : refl (cross T1 T2) (below_ (below_* B2 B1)) % T1 * T2 fails here
	  <- refl T1 B1
	  <- refl T2 B2.
refl_=> : refl (arrow T1 T2) (below_ (below_=> B2 B1)) % T1 => T2 fails here
	   <- refl T1 B1
	   <- refl T2 B2.
%total T (refl T _).

% Transitivity is admissible

% second copy is redundant --- only for totality checker
trans   : below T S -> below S R -> below T R -> type.
%mode trans +B +C -D.
% %mode trans' +B +C -D.
trans_&r : trans B (below_&r C2 C1) (below_&r D2 D1)
	    <- trans B C1 D1
	    <- trans B C2 D2.
trans_tr : trans B (below_topr) (below_topr).
trans_tl1 : trans (below_&r B2 B1) (below_ (below_&l1 C1)) D1
	     <- trans B1 (below_ C1) D1.
trans_tl2 : trans (below_&r B2 B1) (below_ (below_&l2 C2)) D2
	     <- trans B2 (below_ C2) D2.
trans_n- : trans (below_ below_nn) C C.
trans_p- : trans (below_ below_pp) C C.
trans_z- : trans (below_ below_zz) C C.
trans_-n : trans B (below_ below_nn) B.
trans_-p : trans B (below_ below_pp) B.
trans_-z : trans B (below_ below_zz) B.
trans_* : trans (below_ (below_* B2 B1)) (below_ (below_* C2 C1))
	        (below_ (below_* D2 D1))
	       <- trans B1 C1 D1
	       <- trans B2 C2 D2.
trans_=> : trans (below_ (below_=> B2 B1)) (below_ (below_=> C2 C1))
	         (below_ (below_=> D2 D1))
	    <- trans C1 B1 D1
	    <- trans B2 C2 D2.
%covers trans +B +C -D.

%{
% second copy
trans_n- : trans' (below_nn) C C.
trans_p- : trans' (below_pp) C C.
trans_z- : trans' (below_zz) C C.
trans_-n : trans' B (below_nn) B.
trans_-p : trans' B (below_pp) B.
trans_-z : trans' B (below_zz) B.
trans_*  : trans' (below_* B2 B1) (below_* C2 C1) (below_* D2 D1)
	    <- trans' B1 C1 D1
	    <- trans' B2 C2 D2.
trans_=> : trans' (below_=> B2 B1) (below_=> C2 C1) (below_=> D2 D1)
	    <- trans C1 B1 D1
	    <- trans' B2 C2 D2.
%total [(C C') (B B')] (trans B C _) (trans' C' B' _).

% Soundness of algorithmic subtyping
bs : below T S -> sub T S -> type.
%mode bs +B -C.
bs_nn : bs (below_nn) (sub_refl).
bs_pn : bs (below_pn) (sub_pn).
bs_pp : bs (below_pp) (sub_refl).
bs_zn : bs (below_zn) (sub_zn).
bs_zz : bs (below_zz) (sub_refl).
bs_* : bs (below_* B2 B1) (sub_* C1 C2)
	<- bs B1 C1
	<- bs B2 C2.
bs_=> : bs (below_=> B2 B1) (sub_=> C1 C2)
	 <- bs B1 C1
	 <- bs B2 C2.
%total B (bs B _).

% Completeness of algorithmic subtyping
bc : sub T S -> below T S -> type.
%mode bc +C -B.
bc_refl : bc (sub_refl) B
	   <- refl T B.
bc_trans : bc (sub_trans C1 C2) B
	    <- bc C1 B1
	    <- bc C2 B2
	    <- trans B1 B2 B.
bc_pn : bc (sub_pn) (below_pn).
bc_zn : bc (sub_zn) (below_zn).
bc_* : bc (sub_* C1 C2) (below_* B2 B1)
	<- bc C1 B1
	<- bc C2 B2.
bc_=> : bc (sub_=> C1 C2) (below_=> B2 B1)
	 <- bc C1 B1
	 <- bc C2 B2.
%total C (bc C _).

% Inversion principles

impossible : type.
% no constructors

% A contradiction implies everything
impossibleAll : impossible -> of E T -> type.
% no constuctors
%mode impossibleAll +I -P.
%total [] (impossibleAll I _).

% no inv_z_nat

inv_z_pos : of z T -> below T pos -> impossible -> type.
%mode inv_z_pos +P +B -I.
izp_sub : inv_z_pos (tp_sub C' P') B I
	   <- bc C' B'
	   <- trans B' B B''
	   <- inv_z_pos P' B'' I.
%total P (inv_z_pos P B _).

% no inv_z_zero

inv_s_pos : of (s E) T -> below T pos -> of E nat -> type.
%mode inv_s_pos +P +B -Q.
isp_sub : inv_s_pos (tp_sub C' P') B Q
	   <- bc C' B'
	   <- trans B' B B''
	   <- inv_s_pos P' B'' Q.
isp_nat : inv_s_pos (tp_s_nat P') B P'.
isp_pos : inv_s_pos (tp_s_pos P') B P'.
%total P (inv_s_pos P B _).

inv_s_nat : of (s E) T -> below T nat -> of E nat -> type.
%mode inv_s_nat +P +B -Q.
isn_sub : inv_s_nat (tp_sub C' P') B Q
	   <- bc C' B'
	   <- trans B' B B''
	   <- inv_s_nat P' B'' Q.
isn_nat : inv_s_nat (tp_s_nat P') B P'.
ins_pos : inv_s_nat (tp_s_pos P') B P'.
%total P (inv_s_nat P B _).

inv_s_zero : of (s E) T -> below T zero -> impossible -> type.
%mode inv_s_zero +P +B -I.
isz_sub : inv_s_zero (tp_sub C' P') B I
	   <- bc C' B'
	   <- trans B' B B''
	   <- inv_s_zero P' B'' I.
%total P (inv_s_zero P B _).

inv_lam : of (lam E) T -> below T (arrow T1 T2)
	  -> ({x:exp} of x T1 -> of (E x) T2) -> type.
%mode inv_lam +P +B -Q.
inv_lam_sub : inv_lam (tp_sub C' P') B Q
	       <- bc C' B'
	       <- trans B' B B''
	       <- inv_lam P' B'' Q.
inv_lam_ : inv_lam (tp_lam P') (below_=> B2 B1)
	    ([x:exp] [u:of x T1] tp_sub C2 (P' x (tp_sub C1 u)))
	    <- bs B1 C1
	    <- bs B2 C2.
%total P (inv_lam P B _).

inv_pair : of (pair E1 E2) T -> below T (cross T1 T2)
           -> of E1 T1 -> of E2 T2 -> type.
%mode inv_pair +P +B -Q1 -Q2.
inv_pair_sub : inv_pair (tp_sub C' P') B Q1 Q2
		<- bc C' B'
		<- trans B' B B''
		<- inv_pair P' B'' Q1 Q2.
inv_pair_ : inv_pair (tp_pair P2 P1) (below_* B2 B1) (tp_sub C1 P1) (tp_sub C2 P2)
	     <- bs B1 C1
	     <- bs B2 C2.
%total P (inv_pair P B _ _).

tps : eval E V -> of E T -> of V T -> type.
%mode tps +D +P -Q.

% Subsumption
tps_sub : tps D (tp_sub C P') (tp_sub C Q')
	   <- tps D P' Q'.

% Natural Numbers
tps_z     : tps (ev_z) Q Q.
tps_s_nat : tps (ev_s D1) (tp_s_nat P1) (tp_s_nat Q1)
	     <- tps D1 P1 Q1.
tps_s_pos : tps (ev_s D1) (tp_s_pos P1) (tp_s_pos Q1)
	     <- tps D1 P1 Q1.

tps_case_z_nat : tps (ev_case_z D2 D1) (tp_case_nat P3 P2 P1) Q2
		  <- tps D2 P2 Q2.
tps_case_z_pos : tps (ev_case_z D2 D1) (tp_case_pos P3 P1) Q2
		  <- tps D1 P1 Q1
		  <- inv_z_pos Q1 (below_pp) I
		  <- impossibleAll I Q2.
tps_case_z_zero : tps (ev_case_z D2 D1) (tp_case_zero P2 P1) Q2
		   <- tps D2 P2 Q2.

tps_case_s_nat : tps (ev_case_s D3 D1) (tp_case_nat P3 P2 P1) Q3
		  <- tps D1 P1 Q1
		  <- inv_s_nat Q1 (below_nn) Q1'
		  <- tps D3 (P3 V1 Q1') Q3.
tps_case_s_pos : tps (ev_case_s D3 D1) (tp_case_pos P3 P1) Q3
		  <- tps D1 P1 Q1
		  <- inv_s_pos Q1 (below_pp) Q1'
		  <- tps D3 (P3 V1 Q1') Q3.
tps_case_s_zero : tps (ev_case_s D3 D1) (tp_case_zero P2 P1) Q3
		   <- tps D1 P1 Q1
		   <- inv_s_zero Q1 (below_zz) I
		   <- impossibleAll I Q3.
% Pairs
tps_pair : tps (ev_pair D2 D1) (tp_pair P2 P1) (tp_pair Q2 Q1)
	      <- tps D1 P1 Q1
	      <- tps D2 P2 Q2.
tps_fst  : tps (ev_fst D1) (tp_fst P1) Q1
	      <- tps D1 P1 Q
	      <- refl (cross T1 T2) B
	      <- inv_pair Q B Q1 Q2.
tps_snd  : tps (ev_snd D1) (tp_snd P1) Q2
	      <- tps D1 P1 Q
	      <- refl (cross T1 T2) B
	      <- inv_pair Q B Q1 Q2.

% Functions
tps_lam  : tps (ev_lam) P P.

tps_app  : tps (ev_app D3 D2 D1) (tp_app P2 P1) Q3
	    <- tps D1 P1 Q		% before (tp_lam Q1')
	    <- refl (arrow T2 T1) B
	    <- inv_lam Q B Q1'
	    <- tps D2 P2 Q2
	    <- tps D3 (Q1' V2 Q2) Q3.

% Definitions
tps_letv : tps (ev_letv D2 D1) (tp_letv P2 P1) Q2
	    <- tps D1 P1 Q1
	    <- tps D2 (P2 V1 Q1) Q2.

tps_letn : tps (ev_letn D2) (tp_letn P2 P1) Q2
	    <- tps D2 P2 Q2.

% Recursion
tps_fix : tps (ev_fix D1) (tp_fix P1) Q1
	    <- tps D1 (P1 _ (tp_fix P1)) Q1.

%total {D P} (tps D P _).
}%