Computation and Deduction 2009/20090415

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

Code from class, April 15.

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.

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.

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.


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/lam (DofeM x : {y} ofe (cons (G x) y B) (M x y) C))
    _
    <- ({y} {dy : isvar y J} 

esubst ([x] append/cons (Dappend x)) (append/cons Dappend') (ordered/cons (_ : bounded (G x) y)) _ _ _).

%worlds (bind) (esubst _ _ _ _ _ _).
%total D (esubst _ _ _ _ D _).