Computation and Deduction 2009/20090429

From The Twelf Project
Jump to: navigation, search
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 _ _ _).