Computation and Deduction 2009/20090318
From The Twelf Project
| 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' _ _).
