Computation and Deduction 2009/20090408

From The Twelf Project
Jump to: navigation, search
This is Literate Twelf
Code: here
Status: %% OK %%
Output: here.

Code from class, April 8.

tp : type.  %name tp A.

tensor : tp -> tp -> tp.
1 : tp.
with : tp -> tp -> tp.
top : tp.
plus : tp -> tp -> tp.
0 : tp.
lolli : tp -> tp -> tp.
! : tp -> tp.

exp : type.  %name exp M x.

tens : exp -> exp -> exp.
lett : exp -> (exp -> exp -> exp) -> exp.
pair : exp -> exp -> exp.
pi1  : exp -> exp.
pi2  : exp -> exp.
star : exp.
lets : exp -> exp -> exp.
unit : exp.
in1  : exp -> exp.
in2  : exp -> exp.
case : exp -> (exp -> exp) -> (exp -> exp) -> exp.
abort : exp -> exp.
lam : tp -> (exp -> exp) -> exp.
app : exp -> exp -> exp.
bang : exp -> exp.
letb : exp -> (exp -> exp) -> exp.

linear : (exp -> exp) -> type.
of : exp -> tp -> type.

linear/var : linear ([x] x).

linear/tens1 : linear ([x] tens (M x) N)
		<- linear ([x] M x).

linear/tens2 : linear ([x] tens M (N x))
		<- linear ([x] N x).

of/tens : of (tens M N) (tensor A B)
	   <- of M A
	   <- of N B.

linear/lett1 : linear ([z] lett (M z) ([x] [y] N x y))
		<- linear ([x] M x).

linear/lett2 : linear ([z] lett M ([x] [y] N z x y))
		<- ({x} {y} linear ([z] N z x y)).

of/lett : of (lett M ([x] [y] N x y)) C
	   <- of M (tensor A B)
	   <- ({x:exp} of x A -> {y:exp} of y B -> of (N x y) C)
	   <- ({y:exp} linear ([x] N x y))
	   <- ({x:exp} linear ([y] N x y)).

linear/pair : linear ([x] pair (M x) (N x))
	       <- linear ([x] M x)
	       <- linear ([x] N x).

of/pair : of (pair M N) (with A B)
	   <- of M A
	   <- of N B.

linear/pi1 : linear ([x] pi1 (M x))
	      <- linear ([x] M x).

linear/pi2 : linear ([x] pi2 (M x))
	      <- linear ([x] M x).

of/pi1 : of (pi1 M) A
	  <- of M (with A B).

of/pi2 : of (pi1 M) B
	  <- of M (with A B).

of/star : of star 1.

linear/lets1 : linear ([x] lets (M x) N)
		<- linear ([x] M x).

linear/lets2 : linear ([x] lets M (N x))
		<- linear ([x] N x).

of/lets : of (lets M N) C
	   <- of M 1
	   <- of N C.

linear/unit : linear ([x] unit).

of/unit : of unit top.

linear/in1 : linear ([x] in1 (M x))
	      <- linear ([x] M x).

linear/in2 : linear ([x] in2 (M x))
	      <- linear ([x] M x).

of/in1 : of (in1 M) (plus A B)
	  <- of M A.

of/in2 : of (in2 M) (plus A B)
	  <- of M B.

linear/case1 : linear ([z] case (M z) ([x] N x) ([x] O x))
		<- linear ([z] M z).

linear/case2 : linear ([z] case M ([x] N z x) ([x] O z x))
		<- ({x:exp} linear ([z] N z x))
		<- ({x:exp} linear ([z] O z x)).

of/case : of (case M ([x] N x) ([x] O x)) C
	   <- of M (plus A B)
	   <- ({x} of x A -> of (N x) C)
	   <- ({x} of x B -> of (O x)C)
	   <- linear ([x] N x)
	   <- linear ([x] O x).

linear/abort1 : linear ([x] abort (M x))
		 <- linear ([x] M x).

linear/abort2 : linear ([x] abort M).

of/abort : of (abort M) C
	    <- of M O.

linear/lam : linear ([x] (lam A ([y] (M x y))))
	  <- {y:exp} linear ([x] M x y).

of/lam : of (lam A ([x] M x)) (lolli A B)
	  <- ({x} (of x A) -> of (M x) B)
	  <- linear ([x] M x).

linear/app1 : linear ([x] (app (M x) N))
	       <- linear ([x] M x).

linear/app2 : linear ([x] (app M (N x)))
	       <- linear ([x] N x).

of/app : of (app M N) B
	  <- of M (lolli A B)
	  <- of N A.

of/bang : of (bang M) (! A)
	   <- of M A.

linear/letb1 : linear ([x] (letb (M x) ([y] (N y))))
		<- linear ([x] M x).

linear/letb2 : linear ([x] (letb M ([y] N x y)))
		<- ({y} linear ([x] N x y)).

of/letb : of (letb M ([x] N x)) C
	   <- of M (! A)
	   <- ({x} (of x A) -> of (N x) C).


reduce : exp -> exp -> type.

reduce/lam : reduce (lam A ([x] M x)) (lam A ([x] N x))
	      <- ({x} reduce (M x) (N x)).

reduce/app1 : reduce (app M N) (app M' N)
	       <- reduce M M'.

reduce/app2 : reduce (app M N) (app M N')
	       <- reduce N N'.

reduce/beta : reduce (app (lam A ([x] M x)) N) (M N).

%block block : block {x:exp}.
%block bind : some {A:tp} block {x:exp} {d : of x A}.

exp-eq : exp -> exp -> type.
exp-eq/i : exp-eq M M.

exp-compat: {M : exp -> exp} exp-eq N N' -> exp-eq (M N) (M N') -> type.
%mode exp-compat +I +I1 -O.
 
- : exp-compat M _ exp-eq/i.

%worlds (block) (exp-compat _ _ _).
%total {} (exp-compat _ _ _). 


lam-compat: ({x:exp} exp-eq (N x) (N' x)) -> exp-eq (lam A N) (lam A N') -> type.
%mode +{N:exp -> exp} +{N':exp -> exp} +{A:tp} +{D1:{x:exp} exp-eq (N x) (N' x)}
   -{D2:exp-eq (lam A ([x:exp] N x)) (lam A ([x:exp] N' x))} (lam-compat D1 D2).

-: lam-compat ([x] exp-eq/i) exp-eq/i.

%worlds (block) (lam-compat _ _).
%total {} (lam-compat _ _).

linear-resp: ({x:exp} exp-eq (M x) (N x) ) -> linear M -> linear N -> type.
%mode linear-resp +I +I2 -O.

-: linear-resp _ D D.
  
%worlds (block) (linear-resp _ _ _).
%total {} (linear-resp _ _ _). 

reduce-closed : ({x:exp} reduce M (N x)) -> ({x:exp} exp-eq N' (N x) ) -> type.
%mode reduce-closed +D -D'.

-: reduce-closed ([x] reduce/app1 (Dreduce x : reduce M1 (N1 x)) ) Deq'
	<- reduce-closed Dreduce (Deq : {x} exp-eq N1' (N1 x))
	<- ({x} exp-compat ([y] app y M2) (Deq x) (Deq' x : exp-eq (app N1' M2) (app (N1 x) M2))).

-: reduce-closed ([x] reduce/app2 (Dreduce x :reduce M2 (N2 x))) Deq'
	<- reduce-closed Dreduce (Deq : {x} exp-eq N2' (N2 x))
	<- ({x} exp-compat ([y] app M1 y) (Deq x) (Deq' x : exp-eq (app M1 N2') (app M1 (N2 x)))).

-: reduce-closed ([x] reduce/lam (Dreduce x : {y} reduce (M y) (N x y))) Deq'
	<- ({y} reduce-closed ([x] Dreduce x y) ([x] Deq x y: exp-eq (N' y) (N x y)))
	<- ({x} lam-compat ([y] Deq x y) (Deq' x : exp-eq (lam A ([y] (N' y))) (lam A ([y] (N x y))))).

-: reduce-closed ([x] reduce/beta : reduce (app (lam A ([y] M y)) N) (M N)) ([x] exp-eq/i).

%worlds (block) (reduce-closed _ _).
%total D (reduce-closed D _).


linear-compose: linear ([x] M x) -> linear ([y] N y) -> linear ([y] M (N y)) -> type.
%mode linear-compose +I +I1 -O.

-: linear-compose linear/var D D.

-: linear-compose linear/unit _ linear/unit.

-: linear-compose (linear/app1 (D1 :linear ([x] M1 x)) ) (D2:linear ([y] N y)) 
    (linear/app1 D)
    <- linear-compose D1 D2 (D: linear ([y] M1 (N y))).

-: linear-compose (linear/app2 (D1 :linear ([x] M1 x)) ) (D2 : linear ([y] N y))
	(linear/app2 D) 
    <- linear-compose D1 D2 D.
-: linear-compose (linear/tens1 (D1 : linear ([x] M1 x))) 
		(D2 : linear ([y] N y))   
		(linear/tens1 D) 
    <- linear-compose D1 D2 D.
-: linear-compose (linear/tens2 (D1 : linear ([x] M1 x))) 
		(D2 : linear ([y] N y))   
		(linear/tens2 D) 
    <- linear-compose D1 D2 D.
-: linear-compose (linear/lett1 (D1 : linear ([x] M1 x))) 
		(D2 : linear ([y] N y))
		(linear/lett1 D)
    <- linear-compose D1 D2 D.
-: linear-compose (linear/lett2 (D1 : {x} {y} linear ([z] M1 x y z)))
		(D2 : linear ([k] N k))
		(linear/lett2 D )
    <- ({x} {y} linear-compose (D1 x y) D2 (D x y)).

-: linear-compose (linear/pair (X1 : linear ([x] M1 x)) (X2 : linear ([y] M2 y)))
 D1
 	(linear/pair A B)
    <- linear-compose X1 D1 A
    <- linear-compose X2 D1 B.
-: linear-compose (linear/pi1 (D1 : linear ([x] M1 x)))
	D2
	(linear/pi1 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/pi2 (D1 : linear ([x] M1 x)))
	D2
	(linear/pi2 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/lets1 (D1 : linear ([x] M1 x)))
	D2
	(linear/lets1 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/lets2 (D1 : linear ([x] M1 x)))
	D2
	(linear/lets2 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/in1 (D1 : linear ([x] M1 x)))
	D2
	(linear/in1 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/in2 (D1 : linear ([x] M1 x)))
	D2
	(linear/in2 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/case1 (D1 : linear ([x] M1 x)))
	D2
	(linear/case1 D)
	<- linear-compose D1 D2 D.

-: linear-compose (linear/case2 ([x] D1 x) ([x] D2 x)) D3 (linear/case2 D4 D5)
	<- ({x} linear-compose (D1 x) D3 (D4 x))
	<- ({x} linear-compose (D2 x) D3 (D5 x)).

-: linear-compose (linear/abort1 (D1 : linear ([x] M1 x)))
	D2
	(linear/abort1 D)
	<- linear-compose D1 D2 D.

-: linear-compose (linear/abort2) _ linear/abort2.

-: linear-compose (linear/lam ([y] X1 y)) X2 (linear/lam D)
	<- ({x} linear-compose (X1 x) X2 (D x)).

-: linear-compose (linear/letb1 (D1 : linear ([x] M1 x)))
	D2
	(linear/letb1 D)
	<- linear-compose D1 D2 D.
-: linear-compose (linear/letb2 ([y] X1 y)) X2 (linear/letb2 D)
	<- ({x} linear-compose (X1 x) X2 (D x)).

%worlds (block) (linear-compose _ _ _).
%total (R) (linear-compose R _ _).


srl : ({x} (of x A) -> of (M x) B) -> linear ([x] M x) -> ({x} reduce (M x) (M' x)) -> linear ([x] M' x) -> type.
%mode srl +D1 +D2 +D3 -D4.

- : srl
     ([x] [d:of x A] of/lam (DDD x) (Dof x d : {y} of y B -> of (M x y) C))
     (linear/lam (Dlinear : {y} linear ([x] M x y)))
     ([x] reduce/lam (Dreduce x : {y} reduce (M x y) (N x y)))
     (linear/lam ([y] Dlinear' y))
     <- ({y} {dy:of y B} srl ([x] [dx:of x A] Dof x dx y dy) (Dlinear y) ([x] Dreduce x y)
	   (Dlinear' y : linear ([x] N x y))).

- : srl
     ([x] [d:of x A] of/app _ (Dof x d : of (M x) (lolli B C)))
     (linear/app1 (Dlinear : linear ([x] M x)))
     ([x] reduce/app1 (Dreduce x : reduce (M x) (M' x)))
     (linear/app1 Dlinear')
   <- srl Dof Dlinear Dreduce (Dlinear' : linear ([x] M' x)).

- : srl
     _
     (linear/app2 (Dlinear : linear ([x] N x)))
     ([x] reduce/app1 (Dreduce x : reduce M (M' x)))
     Dlinear'
     <- reduce-closed Dreduce (Deq: {x} exp-eq  M'' (M' x)  )
     <- ({x} exp-compat ([z] app z (N x)) (Deq x) (Deq' x : exp-eq (app M'' (N x) ) (app (M' x) (N x))))
     <- linear-resp Deq' (linear/app2 Dlinear) (Dlinear' : linear ([x] app (M' x) (N x))).

- : srl 
     _
     (linear/app1 (linear/lam (Dlinear:{y} linear ([x] M x y))))
     ([x] reduce/beta)
     (Dlinear _).

-: srl
    ([x][d:of x A] of/app _ (of/lam (Dlinear' x : linear ([y] M y)) _ ))
    (linear/app2 (Dlinear : linear ([x] N x) ))
    ([x] reduce/beta)
    Dlinear''
    <- linear-compose (Dlinear' unit) Dlinear (Dlinear'' : linear ([x] M (N x))).

-: srl
    ([x] [d : of x A] of/app (Dof x d : of (N x) B) _)
    (linear/app2 (Dlinear : linear ([x] N x)))
    ([x] reduce/app2 (Dreduce x : reduce (N x) (N' x)))
    (linear/app2 Dlinear')
    <- srl Dof Dlinear Dreduce (Dlinear' : linear ([x] N' x)).

-: srl 
    _
    (linear/app1 (Dlinear : linear ([x] M x)))
    ([x] reduce/app2 (Dreduce x : reduce N (N' x)))
    Dlinear'
    <- reduce-closed Dreduce (Deq : {x} exp-eq N'' (N' x))
    <- ({x} exp-compat ([z] app (M x) z) (Deq x) (Deq' x : exp-eq (app (M x) N'') (app (M x) (N' x))))
    <- linear-resp Deq' (linear/app1 Dlinear) (Dlinear' : linear ([x] app (M x) (N' x))).

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


sr : of M A -> reduce M M' -> of M' A -> type.
%mode sr +D1 +D2 -D3.

- : sr
     (of/app (DofN : of N A) (DofM : of M (lolli A B)))
     (reduce/app1 (Dreduce : reduce M M'))
     (of/app DofN DofM')
     <- sr DofM Dreduce (DofM' : of M' (lolli A B)).

- : sr
     (of/app (DofN : of N A) (DofM : of M (lolli A B)))
     (reduce/app2 (Dreduce : reduce N N'))
     (of/app DofN' DofM)
     <- sr DofN Dreduce (DofN' : of N' A).

- : sr
     (of/app (DofN : of N A) (of/lam _ (DofM : {x} (of x A) -> of (M x) B)))
     reduce/beta
     (DofM N DofN).

- : sr
     (of/lam
	(Dlinear : linear ([x] M x))
	(DofM : {x} (of x A) -> of (M x) B))
     (reduce/lam (Dreduce : {x} reduce (M x) (N x)))
     (of/lam
	Dlinear'
	DofN)
     <- ({x} {dx:of x A}
	   sr (DofM x dx) (Dreduce x) (DofN x dx : of (N x) B))
     <- srl DofM Dlinear Dreduce (Dlinear': linear ([x] N x)).

%worlds (bind) (sr _ _ _).
%total D1 (sr _ D1 _).