Computation and Deduction 2009/20090420

This is Literate Twelf Code: here Status: %% ABORT %% Output: here.

Code from class, April 20.

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.

%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 _ _ _).


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.

%worlds (bind | ovar) (append-lookup-eq _ _ _ _).
%trustme %total D (append-lookup-eq D _ _ _).

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/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 _ _ _ _ _ _).
%total D (esubst _ _ _ _ D _).