Computation and Deduction 2009/20090318

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% ABORT %%
Output: here.

Code from class, March 18.

ttp : type. %name ttp T.

tnum : ttp.
tnot : ttp -> ttp.
tprod : ttp -> ttp -> ttp.

texp : type. %name texp E.
tval : type. %name tval V.

tlet : tval -> (tval -> texp) -> texp.
tpi1 : tval -> (tval -> texp) -> texp.
tpi2 : tval -> (tval -> texp) -> texp.
tifz : tval -> texp -> (tval -> texp) -> texp.
tapp : tval -> tval -> texp.

tz : tval.
ts : tval -> tval.
tpair : tval -> tval -> tval.
tlam : ttp -> (tval -> texp) -> tval.

tof : tval -> ttp -> type.
twf : texp -> type.

tof/z : tof tz tnum.

tof/s : tof (ts V) tnum
 <- tof V tnum.

tof/pair : tof (tpair V1 V2) (tprod T1 T2)
    <- tof V1 T1
    <- tof V2 T2.

tof/lam : tof (tlam T ([x] E x)) (tnot T)
   <- ({x} tof x T -> twf (E x)).

twf/let : twf (tlet V ([x] E x))
   <- tof V T
   <- ({x} tof x T -> twf (E x)).

twf/pi1 : twf (tpi1 V ([x] E x))
   <- tof V (tprod T1 T2)
   <- ({x} tof x T1 -> twf (E x)).

twf/pi2 : twf (tpi2 V ([x] E x))
   <- tof V (tprod T1 T2)
   <- ({x} tof x T2 -> twf (E x)).

twf/ifz : twf (tifz V E0 ([x] E1 x))
   <- tof V tnum
   <- twf E0
   <- ({x} tof x tnum -> twf (E1 x)).

twf/app : twf (tapp V1 V2)
   <- tof V1 (tnot T)
   <- tof V2 T.

ttrans : tp -> ttp -> type.

ttrans/num : ttrans num tnum.

ttrans/arr : ttrans (arr T1 T2) (tnot (tprod T1' (tnot T2')))
      <- ttrans T1 T1'
      <- ttrans T2 T2'.

suspend : ttp -> tval -> tval
        = [t] [v] (tlam (tnot t) ([f] tapp f v)).

trans : term -> tp -> tval -> type.

trans/z : trans z num (suspend tnum tz).

trans/s : trans (s E) num (tlam (tnot tnum) ([f] tapp V (tlam tnum ([x] tapp f (ts x)))))
   <- trans E num V.

trans/ifz : trans (ifz E E0 ([x] E1 x)) T
     (tlam (tnot T')
		   ([f] tapp V (tlam tnum ([y] tifz y (tapp V0 f)
								     ([y'] tlet (tlam (tnot tnum) ([g] tapp g y'))
									       ([x'] tapp (V1 x') f))))))
     <- ttrans T T'
     <- trans E num V
     <- trans E0 T V0
     <- ({x} {x'} trans x num x' -> trans (E1 x) T (V1 x')).

trans/lam : trans (lam T1 ([x] E x)) (arr T1 T2)
             (suspend (tnot (tprod T1' (tnot T2')))
					                (tlam (tprod T1' (tnot T2'))
										         ([y] tpi1 y
												    ([y'] (tpi2 y
																   ([g] tlet (suspend T1' y')
																	      ([x'] tapp (V x') g)))))))
     <- ttrans T1 T1'
     <- ttrans T2 T2'
     <- ({x} {x'} trans x T1 x' -> trans (E x) T2 (V x')).

trans/app : trans (app E1 E2) T2
             (tlam (tnot T2') 
                ([f] tapp V1
                   (tlam (tnot (tprod T1' (tnot T2')))
                      ([x1] tapp V2 (tlam T1' ([x2] tapp x1 (tpair x2 f)))))))
             <- ttrans T1 T1'
             <- ttrans T2 T2'
             <- trans E1 (arr T1 T2) V1
             <- trans E2 T1 V2.

tof/suspend : tof (suspend T V) (tnot (tnot T))
               <- tof V T
            = [D : tof V T] (tof/lam ([x] [d : tof x (tnot T)] (twf/app D d))).

ttp-eq : ttp -> ttp -> type.

ttp-eq/i : ttp-eq T T.

ttrans-fun : ttrans T T' -> ttrans T T'' -> ttp-eq T' T'' -> type.
%mode ttrans-fun +D1 +D2 -D3.



%worlds () (ttrans-fun _ _ _).
%trustme %total D (ttrans-fun D _ _).

tof-resp : ttp-eq T T' -> tof V T -> tof V T' -> type.
%mode tof-resp +D1 +D2 -D3.

tof-resp/i : tof-resp ttp-eq/i D D.

%block tbind : some {T : ttp} block {x : tval} {d : tof x T}.
%worlds (tbind) (tof-resp _ _ _).

%total {} (tof-resp _ _ _).

ttp-resp : {T : ttp -> ttp} ttp-eq T1 T2 -> ttp-eq (T T1) (T T2) -> type.
%mode ttp-resp +D1 +D2 -D3.

- : ttp-resp T ttp-eq/i ttp-eq/i.

%worlds () (ttp-resp _ _ _).
%total {} (ttp-resp _ _ _).

correct : trans E T V -> ttrans T T' -> tof V (tnot (tnot T')) -> type.
%mode correct +D1 -D2 -D3.

correct' : trans E T V -> ttrans T T' -> tof V (tnot (tnot T')) -> type.
%mode correct' +D1 +D2 -D3.

- : correct'
	 (DtransE : trans E T V)
	 (DtransT : ttrans T T')
	 DofV'
	 <- correct DtransE 
		(DtransT' : ttrans T T'')
		(DofV : tof V (tnot (tnot T'')))
	 <- ttrans-fun DtransT' DtransT (Deq : ttp-eq T'' T')
	 <- ttp-resp ([t] (tnot (tnot t))) Deq (Deq' : ttp-eq (tnot (tnot T'')) (tnot (tnot T')))
	 <- tof-resp Deq' DofV (DofV' : tof V (tnot (tnot T'))).

- : correct trans/z ttrans/num (tof/suspend tof/z).

- : correct 
     (trans/s 
	  (D : trans E num V))
     ttrans/num 
     (tof/lam 
	  ([f] [df:tof f (tnot tnum)] 
	      twf/app 
		     (tof/lam ([x] [dx:tof x tnum] (twf/app (tof/s dx) df))) 
			    D'))
     <- correct' D ttrans/num (D': tof V (tnot (tnot tnum))).

- : correct
     (trans/ifz
		(DtransE1 : {x} {x'} trans x num x' -> trans (E1 x) T (V1 x'))
		(DtransE0 : trans E0 T V0)
		(DtransE : trans E num V)
		(DtransT : ttrans T T'))
     DtransT
     (tof/lam
		([f] [df:tof f (tnot T')]
		      twf/app
		      (tof/lam
				       ([x] [dx:tof x tnum]
						   twf/ifz
						   ([y'] [dy':tof y' tnum]
							      twf/let
							      ([x'] [dx':tof x' (tnot (tnot tnum))]
									        twf/app
									        df
									        (DofV1 x' dx'))
							      (tof/lam
									        ([g] [dg:tof g (tnot tnum)]
											     twf/app dy' dg)))
						   (twf/app df DofV0)
						   dx))
		      DofV))
     <- correct' DtransE ttrans/num (DofV : tof V (tnot (tnot tnum)))
     <- correct' DtransE0 DtransT (DofV0 : tof V0 (tnot (tnot T')))
	 <- ({x} {x'} {dx' : tof x' (tnot (tnot tnum))}
		   {dt : trans x num x'}
		   correct dt ttrans/num dx'
		   -> correct' (DtransE1 x x' dt) DtransT (DofV1 x' dx' : tof (V1 x') (tnot (tnot T')))).

- : correct 
     (trans/lam 
	  (D3: ({x} {x'} trans x T1 x' -> trans (E x) T2 (V x')))
	  (D2: ttrans T2 T2')
	  (D1: ttrans T1 T1'))
     (ttrans/arr D2 D1)
     (tof/suspend 
	  (tof/lam 
	      ([y] [dy:tof y (tprod T1' (tnot T2'))] 
		         twf/pi1 
				       ([y'][dy': tof y' T1']  
						 twf/pi2 
						  ([g][dg:tof g (tnot T2')] 
						       (twf/let 
								       ([x'] [dx':tof x' (tnot (tnot T1'))] 
										  twf/app 
										    dg 
											  (DV x' dx'))
									          (tof/suspend dy'))) 
						   dy)
					         dy)))
     <- ({x} {x'} {dx': tof x' (tnot (tnot T1'))}  
			    {dt: trans x T1 x'}
				   correct dt D1 dx' 
				      -> correct' (D3 x x' dt) D2 (DV x' dx' : tof (V x') (tnot (tnot T2')))).

- : correct
     (trans/app
		(DtransE2 : trans E2 T1 V2)
		(DtransE1 : trans E1 (arr T1 T2) V1)
		(DtransT2 : ttrans T2 T2')
		(DtransT1 : ttrans T1 T1'))
     DtransT2
     (tof/lam
		([f] [df:tof f (tnot T2')]
		      twf/app
		      (tof/lam
				       ([x1] [dx1:tof x1 (tnot (tprod T1' (tnot T2')))]
						   twf/app
						   (tof/lam
							      ([x2] [dx2:tof x2 T1']
									        twf/app
									        (tof/pair df dx2)
									        dx1))
						   DofV2))
		      DofV1))
     <- correct' DtransE1 (ttrans/arr DtransT2 DtransT1)
		(DofV1 : tof V1 (tnot (tnot (tnot (tprod T1' (tnot T2'))))))
     <- correct' DtransE2 DtransT1
		(DofV2 : tof V2 (tnot (tnot T1'))).

%block transbind : some {T : tp} {T' : ttp} {DTT : ttrans T T'}
                    block
                    {x : term} 
                    {x' : tval} {dx' : tof x' (tnot (tnot T'))}
                    {dt : trans x T x'}
                    {thm : correct dt DTT dx'}.


%worlds (transbind) (correct _ _ _) (correct' _ _ _).
%total (D D') (correct D _ _) (correct' D' _ _).