Computation and Deduction 2009/20090429
From The Twelf Project
This is Literate Twelf Code: here Status: %% OK %% Output: here. |
Code from class, April 29.
false : type. nat : type. %name nat N. 0 : nat. s : nat -> nat. lt : nat -> nat -> type. lt/0 : lt 0 (s N). lt/s : lt (s M) (s N) <- lt M N. lt-succ : {N : nat} lt N (s N) -> type. %mode lt-succ +N -D. %worlds () (lt-succ _ _). %trustme %total N (lt-succ N _). tp : type. %name tp T. exp : type. %name exp E x. o : tp. arr : tp -> tp -> tp. p : exp. lam : tp -> (exp -> exp) -> exp. app : exp -> exp -> exp. %% - : (exp -> tp) -> type. tp-eq : tp -> tp -> type. tp-eq/i : tp-eq A A. of : exp -> tp -> type. of/p : of p o. of/lam : of (lam T ([x] E x)) (arr T T') <- ({x} of x T -> of (E x) T'). of/app : of (app E1 E2) T' <- of E1 (arr T T') <- of E2 T. %block bind : some {T : tp} block {x :exp} {dx : of x T}. subst : ({x} of x T1 -> of (E1 x) T2) -> of E2 T1 -> of (E1 E2) T2 -> type. %mode subst +D1 +D2 -D3. %% - : subst D1 D2 (D1 _ D2). - : subst ([x] [d : of x T1] d) (D2 : of E2 T1) D2. - : subst ([x] [d : of x T1] D1) _ D1. - : subst ([x] [d : of x T1] of/app (D12 x d : of (E12 x) T2) (D11 x d : of (E11 x) (arr T2 T3))) (D2 : of E2 T1) (of/app D12' D11') <- subst D11 D2 (D11' : of (E11 E2) (arr T2 T3)) <- subst D12 D2 (D12' : of (E12 E2) T2). - : subst ([x] [dx : of x T1] of/lam (D1 x dx : {y} of y T2 -> of (E1 x y) T3)) (D2 : of E2 T1) (of/lam D) <- ({y} {dy : of y T2} subst ([x] [dx] D1 x dx y dy) D2 (D y dy : of (E1 E2 y) T3)). %worlds (bind) (subst _ _ _). %total D (subst D _ _). ctx : type. %name ctx G. nil : ctx. cons : ctx -> exp -> tp -> ctx. append : ctx -> ctx -> ctx -> type. append/nil : append G nil G. append/cons : append G1 (cons G2 X T) (cons G X T) <- append G1 G2 G. lookup : ctx -> exp -> tp -> type. lookup/hit : lookup (cons G X T) X T. lookup/miss : lookup (cons G X' T') X T <- lookup G X T. ofe : ctx -> exp -> tp -> type. ofe/closed : ofe G E T <- of E T. ofe/var : ofe G X T <- lookup G X T. ofe/p : ofe G p o = ofe/closed of/p. ofe/app : ofe G (app E1 E2) T' <- ofe G E1 (arr T T') <- ofe G E2 T. ofe/lam : ofe G (lam T ([x] E x)) (arr T T') <- ({x} ofe (cons G x T) (E x) T'). isvar : exp -> nat -> type. - : (isvar _ _ -> isvar _ _) -> type. %block ovar : some {I : nat} block {x : exp} {d : isvar x I}. precedes : exp -> exp -> type. precedes/i : precedes X Y <- isvar X I <- isvar Y J <- lt I J. bounded : ctx -> exp -> type. bounded/nil : bounded nil X <- isvar X _. bounded/cons : bounded (cons G X T) Y <- bounded G X <- precedes X Y. ordered : ctx -> type. ordered/nil : ordered nil. ordered/cons : ordered (cons G X T) <- bounded G X. ofe-resp : tp-eq A A' -> ofe G M A -> ofe G M A' -> type. %mode ofe-resp +D1 +D2 -D3. - : ofe-resp _ D D. %worlds (ovar | bind) (ofe-resp _ _ _). %total {} (ofe-resp _ _ _). bounded-isvar : bounded G X -> isvar X I -> type. %mode bounded-isvar +D1 -D2. - : bounded-isvar (bounded/nil D) D. - : bounded-isvar (bounded/cons (precedes/i _ D _) _) D. %worlds (ovar | bind) (bounded-isvar _ _). %total {} (bounded-isvar _ _). ordered-extend : ordered G -> ({x} isvar x I -> bounded G x) -> type. %mode ordered-extend +D1 -D2. - : ordered-extend ordered/nil ([x] [dx : isvar x 0] bounded/nil dx). - : ordered-extend (ordered/cons (Dbounded : bounded G Y)) ([x] [dx : isvar x (s J)] bounded/cons (precedes/i Dlt dx Disvar) Dbounded) <- bounded-isvar Dbounded (Disvar : isvar Y J) <- lt-succ J (Dlt : lt J (s J)). %worlds (ovar | bind) (ordered-extend _ _). %total {} (ordered-extend _ _). ofe-weaken : append G1 G2 G -> ofe G1 M A -> ofe G M A -> type. %mode ofe-weaken +D1 +D2 -D3. %worlds (ovar | bind) (ofe-weaken _ _ _). %trustme %total {} (ofe-weaken _ _ _). bounded-ordered : bounded G X -> ordered G -> type. %mode bounded-ordered +D1 -D2. %worlds (ovar | bind) (bounded-ordered _ _). %trustme %total {} (bounded-ordered _ _). bounded-increase : bounded G X -> precedes X Y -> bounded G Y -> type. %mode bounded-increase +D1 +D2 -D3. %worlds (ovar | bind) (bounded-increase _ _ _). %trustme %total {} (bounded-increase _ _ _). lt-irreflex : lt N N -> false -> type. %mode lt-irreflex +X1 -X2. %worlds (bind | ovar) (lt-irreflex _ _). %trustme %total {} (lt-irreflex _ _). precedes-contra : precedes X X -> false -> type. %mode precedes-contra +D1 -D2. - : precedes-contra (precedes/i (Dlt : lt I I) (Disvar : isvar X I) Disvar) DFalse <- lt-irreflex Dlt DFalse. %worlds (bind | ovar) (precedes-contra _ _). %total {} (precedes-contra _ _). bounded-lookup-contra : bounded G X -> lookup G X A -> false -> type. %mode bounded-lookup-contra +D1 +D2 -D3. - : bounded-lookup-contra (bounded/cons (Dprecedes : precedes Y X) (Dbounded : bounded G Y)) (lookup/miss (Dlookup : lookup G X A)) DFalse <- bounded-increase Dbounded Dprecedes (Dbounded' : bounded G X) <- bounded-lookup-contra Dbounded' Dlookup DFalse. - : bounded-lookup-contra (bounded/cons (Dprecedes : precedes X X) _) (lookup/hit) DFalse <- precedes-contra Dprecedes DFalse. %worlds (ovar | bind) (bounded-lookup-contra _ _ _). %total D (bounded-lookup-contra _ D _). false-implies-tp-eq : false -> {A} {B} tp-eq A B -> type. %mode false-implies-tp-eq +X1 +X2 +X3 -X4. %worlds (bind | ovar) (false-implies-tp-eq _ _ _ _). %total {} (false-implies-tp-eq _ _ _ _). false-implies-ofe : false -> {G} {M} {A} ofe G M A -> type. %mode false-implies-ofe +X1 +X2 +X3 +X4 -X5. %worlds (bind | ovar) (false-implies-ofe _ _ _ _ _). %total {} (false-implies-ofe _ _ _ _ _). append-lookup-eq : ({x} append (cons G1 x A) G2 (G x)) -> ({x} isvar x I -> ordered (G x)) -> ({x} lookup (G x) x B) -> (tp-eq A B) -> type. %mode append-lookup-eq +D1 +D2 +D3 -D. - : append-lookup-eq _ _ ([x] lookup/hit) tp-eq/i. - : append-lookup-eq ([x] append/cons (Dappend x : append (cons G1 x A) G2 (G x))) ([x] [dx : isvar x I] ordered/cons (Dbounded x dx : bounded (G x) Y)) ([x] lookup/miss (Dlookup x : lookup (G x) x B)) Deq <- ({x} {dx : isvar x I} bounded-ordered (Dbounded x dx) (Dordered x dx : ordered (G x))) <- append-lookup-eq Dappend Dordered Dlookup (Deq : tp-eq A B). - : append-lookup-eq ([x] append/nil) ([x] [dx : isvar x I] ordered/cons (Dbounded x dx : bounded G1 x)) ([x] lookup/miss (Dlookup x : lookup G1 x B)) Deq <- ({x} {dx} bounded-lookup-contra (Dbounded x dx) (Dlookup x) DFalse) <- false-implies-tp-eq DFalse _ _ Deq. %worlds (bind | ovar) (append-lookup-eq _ _ _ _). %total D (append-lookup-eq D _ _ _). lookup-pdv : ({x} append (cons G1 x A) G2 (G x)) -> append G1 G2 G' -> ({x} isvar x I -> ordered (G x)) %% Needed? -> ({x} lookup (G x) Y B) -> lookup G' Y B -> type. %mode lookup-pdv +D1 +D2 +D3 +D4 -D5. %worlds (bind | ovar) (lookup-pdv _ _ _ _ _). %trustme %total {} (lookup-pdv _ _ _ _ _). lookup-ordered : ordered G -> lookup G X A -> isvar X I -> type. %mode lookup-ordered +D1 +D2 -D3. %worlds (bind | ovar) (lookup-ordered _ _ _). %trustme %total {} (lookup-ordered _ _ _). lam-isvar-contra : isvar (lam A M) _ -> false -> type. %mode lam-isvar-contra +D1 -D2. %worlds (bind | ovar) (lam-isvar-contra _ _). %total {} (lam-isvar-contra _ _). app-isvar-contra : isvar (app N M) _ -> false -> type. %mode app-isvar-contra +D1 -D2. %worlds (bind | ovar) (app-isvar-contra _ _). %total {} (app-isvar-contra _ _). esubst : ({x} append (cons G1 x A) G2 (G x)) -> append G1 G2 G' -> ({x} isvar x I -> ordered (G x)) -> ofe G1 N A -> ({x} ofe (G x) (M x) B) %% -> ofe G' (M N) B -> type. %mode esubst +D1 +D2 +D3 +D4 +D5 -D6. - : esubst (Dappend : ({x} append (cons G1 x A) G2 (G x))) (Dappend' : append G1 G2 G') (Dordered : ({x} isvar x I -> ordered (G x))) (DofeN : ofe G1 N A) ([x] ofe/closed (DofM x : of (M x) B)) (ofe/closed (DofM N)). - : esubst (Dappend : ({x} append (cons G1 x A) G2 (G x))) (Dappend' : append G1 G2 G') (Dordered : ({x} isvar x I -> ordered (G x))) (DofeN : ofe G1 N A) ([x] ofe/var (Dlookup x : lookup (G x) x B)) DofeN'' <- ofe-weaken Dappend' DofeN (DofeN' : ofe G' N A) <- append-lookup-eq Dappend Dordered Dlookup (Deq : tp-eq A B) <- ofe-resp Deq DofeN' (DofeN'' : ofe G' N B). - : esubst (Dappend : ({x} append (cons G1 x A) G2 (G x))) (Dappend' : append G1 G2 G') (Dordered : ({x} isvar x I -> ordered (G x))) (DofeN : ofe G1 N A) ([x] ofe/var (Dlookup x : lookup (G x) Y B)) (ofe/var Dlookup') <- lookup-pdv Dappend Dappend' Dordered Dlookup (Dlookup' : lookup G' Y B). - : esubst (Dappend : ({x} append (cons G1 x A) G2 (G x))) (Dappend' : append G1 G2 G') (Dordered : ({x} isvar x I -> ordered (G x))) (DofeN : ofe G1 N A) ([x] ofe/var (Dlookup x : lookup (G x) (lam C (M x)) B)) Dofe <- ({x} {dx : isvar x I} lookup-ordered (Dordered x dx) (Dlookup x) (Disvar x dx : isvar (lam C (M x)) J)) <- ({x} {dx : isvar x I} lam-isvar-contra (Disvar x dx) Dfalse) <- false-implies-ofe Dfalse _ _ _ Dofe. - : esubst (Dappend : ({x} append (cons G1 x A) G2 (G x))) (Dappend' : append G1 G2 G') (Dordered : ({x} isvar x I -> ordered (G x))) (DofeN : ofe G1 N A) ([x] ofe/var (Dlookup x : lookup (G x) (app (M' x) (M x)) B)) Dofe <- ({x} {dx : isvar x I} lookup-ordered (Dordered x dx) (Dlookup x) (Disvar x dx : isvar (app (M' x) (M x)) J)) <- ({x} {dx : isvar x I} app-isvar-contra (Disvar x dx) Dfalse) <- false-implies-ofe Dfalse _ _ _ Dofe. - : esubst (Dappend : ({x} append (cons G1 x A) G2 (G x))) (Dappend' : append G1 G2 G') (Dordered : ({x} isvar x I -> ordered (G x))) (DofeN : ofe G1 N A) ([x] ofe/lam (DofeM x : {y} ofe (cons (G x) y B) (M x y) C)) (ofe/lam Dofe) <- ({x} {dx : isvar x I} ordered-extend (Dordered x dx) (Dbounded x dx : {y} isvar y J -> bounded (G x) y)) <- ({y} {dy : isvar y J} esubst ([x] append/cons (Dappend x)) (append/cons Dappend') ([x] [dx : isvar x I] ordered/cons (Dbounded x dx y dy: bounded (G x) y)) DofeN ([x] DofeM x y) (Dofe y : ofe (cons G' y B) (M N y) C)). %worlds (bind | ovar) (esubst _ _ _ _ _ _). %trustme %total D (esubst _ _ _ _ D _). ofi : ctx -> exp -> tp -> type. ofi/nil : ofi nil M A <- of M A. ofi/cons : ofi (cons G X A) M B <- ((of X A) -> ofi G M B). %block of-block : some {X:exp} {A:tp} block {dx : of X A}. ofi-app : ofi G E1 (arr T T') -> ofi G E2 T -> ofi G (app E1 E2) T' -> type. %mode ofi-app +D1 +D2 -D3. - : ofi-app (ofi/nil (Dof1 : of E1 (arr T T'))) (ofi/nil (Dof2 : of E2 T)) (ofi/nil (of/app Dof2 Dof1)). - : ofi-app (ofi/cons (Dof1 : of X A -> ofi G E1 (arr T T'))) (ofi/cons (Dof2 : of X A -> ofi G E2 T)) (ofi/cons Dof) <- ({d : of X A} ofi-app (Dof1 d) (Dof2 d) (Dof d : ofi G (app E1 E2) T')). %worlds (bind | of-block | ovar) (ofi-app _ _ _). %total D (ofi-app D _ _). ofe-implies-ofi : ofe G M A -> ofi G M A -> type. %mode ofe-implies-ofi +D1 -D2. - : ofe-implies-ofi (ofe/app (Dof2 : ofe G E2 T) (Dof1 : ofe G E1 (arr T T'))) Dofi <- ofe-implies-ofi Dof1 Dofi1 <- ofe-implies-ofi Dof2 Dofi2 <- ofi-app Dofi1 Dofi2 (Dofi : ofi G (app E1 E2) T'). %worlds (bind | ovar) (ofe-implies-ofi _ _). %trustme %total D (ofe-implies-ofi D _). ofe-implies-of : ofe nil M A -> of M A -> type. %mode ofe-implies-of +D1 -D2. - : ofe-implies-of (Dofe : ofe nil M A) Dof <- ofe-implies-ofi Dofe (ofi/nil (Dof : of M A)). %worlds (bind) (ofe-implies-of _ _). %total {} (ofe-implies-of _ _). cut-of : {M} ({x} of x A -> of (M x) B) -> ({x} lookup (G x) x A) -> ({x} ofe (G x) (M x) B) -> type. %mode cut-of +D1 +D2 +D3 -D4. cut-ofe : {M} ({x} of x A -> ofe (G x) (M x) B) -> ({x} lookup (G x) x A) -> ({x} ofe (G x) (M x) B) -> type. %mode cut-ofe +D1 +D2 +D3 -D4. - : cut-ofe ([x] lam B ([y] M x y)) ([x] [dx:of x A] ofe/lam (Dofe x dx : {y} ofe (cons (G x) y B) (M x y) C)) (Dlookup : {x} lookup (G x) x A) ([x] ofe/lam ([y] Dofe' x y)) <- ({y} cut-ofe ([x] M x y) ([x] [dx : of x A] Dofe x dx y) ([x] lookup/miss (Dlookup x)) ([x] Dofe' x y : ofe (cons (G x) y B) (M x y) C)). - : cut-ofe ([x] app (M x) (N x)) ([x] [dx : of x A] ofe/app (Dof2 x dx) (Dof1 x dx)) Dlookup ([x] ofe/app (Dofe2 x) (Dofe1 x)) <- cut-ofe M Dof1 Dlookup Dofe1 <- cut-ofe N Dof2 Dlookup Dofe2. - : cut-ofe _ ([x] [dx : of x A] ofe/var (Dlookup x : lookup (G x) (Y x) B)) _ ([x] ofe/var (Dlookup x)). - : cut-of ([x] app (M x) (N x)) ([x] [dx : of x A] of/app (Dof2 x dx) (Dof1 x dx)) Dlookup ([x] ofe/app (Dofe2 x) (Dofe1 x)) <- cut-of M Dof1 Dlookup Dofe1 <- cut-of N Dof2 Dlookup Dofe2. - : cut-ofe M ([x] [dx : of x A] ofe/closed (Dof x dx : of (M x) B)) (Dlookup : {x} lookup (G x) x A) Dofe <- cut-of M Dof Dlookup (Dofe : {x} ofe (G x) (M x) B). - : cut-of ([x] lam B ([y] M x y)) ([x] [dx:of x A] of/lam (Dof x dx : {y} of y B -> of (M x y) C)) (Dlookup : {x} lookup (G x) x A) ([x] ofe/lam ([y] Dofe' x y)) <- ({x} {dx : of x A} cut-of ([y] M x y) ([y] [dy: of y B] Dof x dx y dy) ([y] lookup/hit : lookup (cons (G x) y B) y B) (Dofe x dx : {y} ofe (cons (G x) y B) (M x y) C)) <- ({y} cut-ofe ([x] M x y) ([x] [dx : of x A] Dofe x dx y) ([x] lookup/miss (Dlookup x)) ([x] Dofe' x y : ofe (cons (G x) y B) (M x y) C)). - : cut-of _ ([x] [d:of x A] d) (Dlookup : {x} lookup (G x) x A) ([x] ofe/var (Dlookup x)). - : cut-of _ ([x] [d:of x A] Dof : of M B) _ ([x] ofe/closed Dof). %block var : block {x : exp}. %worlds (bind | var) (cut-of _ _ _ _) (cut-ofe _ _ _ _). %total (M1 M2) (cut-of M1 _ _ _) (cut-ofe M2 _ _ _). of1-implies-ofe : ({x} of x A -> of (M x) B) -> ({x} ofe (cons nil x A) (M x) B) -> type. %mode of1-implies-ofe +D1 -D2. - : of1-implies-ofe (Dof : {x} of x A -> of (M x) B) Dofe <- cut-of M Dof ([x] lookup/hit) (Dofe : {x} ofe (cons nil x A) (M x) B). %worlds (bind) (of1-implies-ofe _ _). %total {} (of1-implies-ofe _ _). of2-implies-ofe : ({x} of x A -> {y} of y B -> of (M x y) C) -> ({x} {y} ofe (cons (cons nil x A) y B) (M x y) C) -> type. %mode of2-implies-ofe +D1 -D2. - : of2-implies-ofe (Dof : {x} of x A -> {y} of y B -> of (M x y) C) Dofe' <- ({x} {dx : of x A} cut-of ([y] M x y) ([y] [dy : of y B] (Dof x dx y dy)) ([y] lookup/hit) (Dofe x dx : {y} ofe (cons (cons nil x A) y B) (M x y) C)) <- ({y} cut-ofe ([x] M x y) ([x] [dx : of x A] Dofe x dx y) ([x] lookup/miss lookup/hit) ([x] Dofe' x y : ofe (cons (cons nil x A) y B) (M x y) C)). %worlds (bind) (of2-implies-ofe _ _). %total {} (of2-implies-ofe _ _). subst : ({x} of x T1 -> of (E1 x) T2) -> of E2 T1 -> of (E1 E2) T2 -> type. %mode subst +D1 +D2 -D3. - : subst (Dof1 : {x} of x T1 -> of (E1 x) T2) (Dof2 : of E2 T1) Dof <- of1-implies-ofe Dof1 (Dofe1 : {x} ofe (cons nil x T1) (E1 x) T2) <- esubst ([x] append/nil) append/nil ([x] [dx : isvar x 0] ordered/cons (bounded/nil dx)) (ofe/closed Dof2) Dofe1 (Dofe : ofe nil (E1 E2) T2) <- ofe-implies-of Dofe (Dof : of (E1 E2) T2). %worlds (bind) (subst _ _ _). %total {} (subst _ _ _).