% Small-step semantics for the DB language: 
% simply-typed lambda-calculus with _mutable_ dynamically-scoped variables.
%
% See Fig 1, Section 2 and Section 6.1 of the 
%     `Delimited Dynamic Binding'
%     http://pobox.com/~oleg/ftp/papers/DDBinding.pdf
% This is the joint work with Chung-chieh Shan and Amr Sabry.
%
% The presented approach closely follows the `Syntactic Approach to Type
% Soundness' with contexts, focusing and redexing. 
% Evaluation contexts are modeled as meta-level functions.
%
% The notable complication is that contexts and pre-values are mutually
% dependent and so pre-val and focus functions are mutually recursive.
% Another complication is that our type system specifically permits
% a well-type expression attempt to access an unbound dynamic variable,
% resulting in an error. This reflects the behavior of most of the real
% systems that use dynamic variables. We have to model this error
% behavior and account for it in our progress proofs. 
%
% We still managed to keep the semantics small-step. And we model
% mutable variables without any need of a `state' or state threading!
%
% The type preservation and progress proofs indeed factor out into
% the type preservation for redexes, and the progress for typed pre-values.
% Plus the context typing rules, which are shared across the
% preservation and progress proofs.
% Indeed, the lemma `tpsfocus' -- asserting that if an expression is
% well-typed then the result of its focusing is well-typed --
% is used both in the type preservation proof (see `tps' -- only one line
% of proof) and in the progress proof (see `fprog' below -- again
% only one rule).


% object-level type
tp : type.				%name tp T.

% Dynamic variables (aka parameters) are in a distinct category.
dv : type.				%name dv W.

% type constructors
=> : tp -> tp -> tp.			%infix right 10 =>.
tu : tp.				% Unit. Other base types can be added

% value constructors and constants: the term language

exp : type.				%name exp M.
lam  : tp -> (exp -> exp) -> exp.	% binders are annotated with types
app  : exp -> exp -> exp.
unit : exp.				% literal ()

val : exp -> type.			%name val P.
  % to be fully defined later. This is just a forward declaration

dref : dv -> exp.			% unlike the paper, we use a special
					% form for dereferencing a dynvar
dset : {W:dv} {V:val M} exp.		% set p to V    -- mutation
dlet : {W:dv} {V:val M} exp -> exp.     % dlet p = V in M


% val : exp -> type.			%name val P.
%mode val +M.
val_lam   : val (lam T M).
val_unit  : val (unit).
%terminates M (val M).
%worlds () (val _).

% We need to define equality and disequality of dynvars
% to be able to state when dlet and dref refer to the same or a different
% variable. An attempt to state
% dv-neq : dv -> dv -> type.
% %mode dv-neq +W1 +W2.
% - : dv-neq W1 W2 <- (dv-eq W1 W2 -> falsum).
% doesn't pass the regression tests below. So, we should either use
% HO syntax for names, put "neq w1 w2" in the assumptions (as we
% we do for the sig below):
%   %query 0 1 {w1:dv} {w2:dv} sig w1 tu -> sig w2 (tu => tu) ->
% 	   dv-neq w1 w1.
% or use the explicit names for parameters. BTW, if we had Miller's nablas,
% then writing nabla w1 nabla w2 already would have given us
% neq w1 w2.
% OK, to stay close to the paper and because it is late, I go for
% explicit names. 

nat : type.				%name nat N.
z : nat.
s : nat -> nat.
d : nat -> dv.				% names of dynvars are labeled w/ nat

nat-eq : nat -> nat -> type.
%mode nat-eq +N1 +N2.
nat-eq-refl : nat-eq N N.
%worlds () (nat-eq _ _).
%terminates {} (nat-eq _ _).

nat-neq : nat -> nat -> type.
%mode nat-neq +N1 +N2.
nat-neq-zs : nat-neq z (s N).
nat-neq-sz : nat-neq (s N) z.
nat-neq-ss : nat-neq (s N1) (s N2) <- nat-neq N1 N2.
%worlds () (nat-neq _ _).
%terminates {N1 N2} (nat-neq N1 N2).

% The assertion that any two nats are either equal or not
nat-cmp : nat -> nat -> type.
%mode nat-cmp +N1 +N2.
nat-cmp-eq  : nat-eq N1 N2  -> nat-cmp N1 N2.
nat-cmp-neq : nat-neq N1 N2 -> nat-cmp N1 N2.

% Now we prove it
nat-cmp-decide : {N1:nat} {N2:nat} nat-cmp N1 N2 -> type.
%mode nat-cmp-decide +N1 +N2 -NC.
- : nat-cmp-decide z z (nat-cmp-eq nat-eq-refl).
- : nat-cmp-decide _ _ (nat-cmp-neq nat-neq-zs).
- : nat-cmp-decide _ _ (nat-cmp-neq nat-neq-sz).

% Case analysis -- it is always so tortuous in Twelf
lemma-ncd : nat-cmp N1 N2 -> nat-cmp (s N1) (s N2) -> type.
%mode lemma-ncd +NC1 -NC2.
- : lemma-ncd (nat-cmp-eq (nat-eq-refl : nat-eq N N))
	(nat-cmp-eq (nat-eq-refl : nat-eq (s N) (s N))).
- : lemma-ncd (nat-cmp-neq NC) (nat-cmp-neq (nat-neq-ss NC)).
%worlds () (lemma-ncd _ _).
%total {} (lemma-ncd _ _).

- : nat-cmp-decide (s N1) (s N2) NC1
	<- nat-cmp-decide N1 N2 NC
	<- lemma-ncd NC NC1.
%worlds () (nat-cmp-decide _ _ _).
%total {N1 N2} (nat-cmp-decide N1 N2 _). % It's a total function -- proof

% lift the comparison of nats to the comparison of dvars

dv-eq : dv -> dv -> type.
%mode dv-eq +W1 +W2.
dv-eq-refl : dv-eq W W.
%worlds () (dv-eq _ _).
%terminates {} (dv-eq _ _).

dv-neq : dv -> dv -> type.
%mode dv-neq +W1 +W2.
dv-neq1 : dv-neq (d N1) (d N2) <- nat-neq N1 N2.
%worlds () (dv-neq _ _).
%terminates {} (dv-neq _ _).

% The assertion that any two dvs are either equal or not
dv-cmp : dv -> dv -> type.
%mode dv-cmp +W1 +W2.
dv-cmp-eq  : dv-eq W1 W2  -> dv-cmp W1 W2.
dv-cmp-neq : dv-neq W1 W2 -> dv-cmp W1 W2.

lemma-dvc : nat-cmp N1 N2 -> dv-cmp (d N1) (d N2) -> type.
%mode lemma-dvc +NC -WC.
- : lemma-dvc (nat-cmp-eq (nat-eq-refl : nat-eq N N))
	(dv-cmp-eq (dv-eq-refl : dv-eq (d N) (d N))).
- : lemma-dvc (nat-cmp-neq P) (dv-cmp-neq (dv-neq1 P)).
%worlds () (lemma-dvc _ _).
%total {} (lemma-dvc _ _).

% Now we prove it
dv-cmp-decide : {W1:dv} {W2:dv} dv-cmp W1 W2 -> type.
%mode dv-cmp-decide +W1 +W2 -WC.
- : dv-cmp-decide (d N1) (d N2) WC 
	<- nat-cmp-decide N1 N2 NC
	<- lemma-dvc NC WC.
%worlds () (dv-cmp-decide _ _ _).
%total {} (dv-cmp-decide _ _ _).

% Predefine some parameters.
w0 = d z.
w1 = d (s z).
w2 = d (s (s z)).

%query 0 1 dv-neq w1 w1.
%query 1 1 dv-neq w2 w1.


% ----------------------------------------------------------------------
% Static semantics: type checking

sig : dv -> tp -> type.			% Signature of dynvars
% One may uncomment the following for the world-less debugging.
% In full proofs, we define no clauses for 'sig'. Instead, 'sig'
% is considered a `universal' (that is, `world') assumption.
% see tp_ds below.
% This approach matches the intuition (in the paper) of the signature
% to be a pervasive assumption...
% sig0 : sig w0 tu.
% sig1 : sig w1 (tu => tu).
%mode sig +W -T.
%terminates W (sig W _).
%worlds () (sig _ _).

of : exp -> tp -> type.			%name of P.
%mode of +M *T.				% Expression E has type T
tp-lam : of (lam T1 M) (T1 => T2)
    <- {x:exp} of x T1 -> of (M x) T2.
tp-app : of (app M1 M2) T2
    <- of M1 (T1 => T2)
    <- of M2 T1.
tp-unit : of (unit) (tu).

% Uncomment the following, deliberately erroneous line,
% to see that the type preservation theorem fails indeed!
% tp-dref : {_:sig W T} of (dref W) tu.
tp-dref : {_:sig W T} of (dref W) T.

tp-dset : {_:sig W TV} of (dset W (V : val MV)) TV
	<- of MV TV.

tp-dlet : {_:sig W TV} of (dlet W (V : val MV) M) TM
	<- of MV TV
	<- of M TM.

%terminates M (of M T).
%block tp_var  : some {T:tp} block {x:exp} {u:of x T}.
%block tp_ds   : block {W:dv} {TV:tp} {u:sig W TV}.
%worlds (tp_var | tp_ds) (sig _ _).
%worlds (tp_var | tp_ds) (of M T).
%covers of +M *T.


% examples of typechecking of various expressions

v0 = (lam tu [x] x).
v1 = (lam (tu => tu) [f] lam tu [x] (app f x)).
v2 = (lam (tu => tu) [f] lam tu [x] (app f (app f x))).


stuck1 = (dlet w0 val_unit (lam (tu => tu) [z] (dref w0))).

term1 = (dlet w0 val_unit (app v0 (dref w0))).
term2 = (dlet w1 val_unit 
			  (dlet w2 (val_lam : val v0) (app v0 (dref w1)))).

term3 = (dlet w1 val_unit 
	    (dlet w2 (val_lam : val v1)
		(app (lam ((tu => tu) => tu => tu) [_] (dref w2))
		     (dset w2 (val_lam : val v2))))).

term4 = (dlet w1 val_unit 
	    (dlet w2 (val_lam : val v1)
		(app (lam ((tu => tu) => tu => tu) [_] (dref w2))
		     (dset w1 val_unit)))).

%query 1 2 of v1 T.

% %{
%query 1 2 sig w0 (tu => tu) -> of (lam tu [x] (dref w0)) T.

%query 1 2 sig w0 tu -> of stuck1 T.

%query 1 2 sig w0 tu -> of term1 T.
%query 1 2 sig w1 tu -> sig w2 (tu => tu) -> of term2 T.
%query 1 2 sig w1 tu -> sig w2 ((tu => tu) => tu => tu) -> 
	of term3 ((tu => tu) => tu => tu).
%query 1 2 sig w1 tu -> sig w2 ((tu => tu) => tu => tu) -> 
	of term3 ((tu => tu) => tu => tu).
% }%

% ----------------------------------------------------------------------
% Classification of expressions: values and contexts

% A dynvar W is free in the context C. See the BP function in Fig 1
% of the paper.
% The following 'wfree' function turns out not needed. I'd like
% to keep it here nevertheless, as it shows off the power of Twelf
% to inspect abstractions, _under_ lambdas.

wfree : dv -> (exp -> exp) -> type.
%mode wfree +W +C.
- : wfree W ([x] x).
- : wfree W ([x] (app (C x) M)) <- wfree W C.
- : wfree W ([x] (app M (C x))) <- wfree W C.
- : wfree W ([x] (dlet W2 V (C x))) <- dv-neq W W2 <- wfree W C.
%worlds () (wfree _ _).
%terminates {C} (wfree _ C).

%query 1 2 wfree w1 ([x] (app v0 (app x unit))).

%query 1 1 wfree w1 ([x] (app v0 (dlet w2 (val_lam : val v0) x))).


% pre-values: non-values that can't be focused further
% That is, pre-values can either be reduced by a redex rule, or
% otherwise get stuck.
% Some non-values can become BP-stuck (see the paper), and we
% specifically account for that.

pre-stuck : exp -> dv -> type.
%mode pre-stuck +M -W.
prestuck-dref  : pre-stuck (dref W) W.
prestuck-dset  : pre-stuck (dset W _) W.

% forward declarations
pre-val   : exp -> type.
% %mode pre-val +M.

prevalstuck : exp -> type.		% The union of pre-val and pre-stuck
% %mode prevalstuck +M.
prevalstuck-pval : pre-val M     -> prevalstuck M.
prevalstuck-pst  : pre-stuck M _ -> prevalstuck M.


% Focusing: given a non-value expression, return prevalstuck and
% its context. Actually, we return the proof of a prevalstuck (from
% whose type we can extract the pre-value and pre-stuck themselves).
% A context is a function exp->exp.
% We later prove that any non-value can be focused.
% We can't assign any mode to focus, due to the way the rules
% (e.g., focus-app) are formulated. 
% Therefore, we can't assign any mode to pre-val.
% Notice that pre-val and focus are mutually recursive!

focus : prevalstuck _ -> (exp -> exp) -> type. %name focus F.
% %mode focus *P -C.

% Define pre-values -- the ones that really should reduce
% The rule preval-dlet12 corresponds to (dlet W V M) providing the
% binding for the otherwise dynamically unbound variable W in the body M.
% The rule guarantees that any dynvar reference refers to the
% closest (in the enclosing evaluation context) occurrence of dlet
% for the same variable -- if any exists.

preval-app   : val M1 -> val M2 -> pre-val (app M1 M2).
preval-dlet1 : val M -> pre-val (dlet W V M).
preval-dlet2 : focus (prevalstuck-pst (_ : pre-stuck M W)) C ->
	       pre-val (dlet W V (C M)).


% Define the focusing operation

% The `hypothesis' {PE1 : val M1} is essentially non-deterministic
% and so precludes assigning any useful mode to focus.

focus-app   : {PE1 : val M1} {PE2 : val M2}
	focus (prevalstuck-pval (preval-app PE1 PE2)) ([x] x).
focus-app1  : focus PPV C1 ->
	focus PPV ([x] (app (C1 x) M2)).
focus-app2  : val M1 -> focus PPV C2 ->
	focus PPV ([x] (app M1 (C2 x))).

% dref W and dset W V outside of any context that may bind W
% are BP-stuck.
focus-pst : focus (prevalstuck-pst _) ([x] x).


focus-dlet01 : {PE : val M} focus
	(prevalstuck-pval ((preval-dlet1 PE) : pre-val (dlet W V M))) ([x] x).

% (dlet W V M) where W \in BP[M], see Fig 1 of the paper
focus-dlet02 : {PS : focus (prevalstuck-pst (_ : pre-stuck M W)) C}
	focus
	(prevalstuck-pval ((preval-dlet2 PS) : pre-val (dlet W V (C M))))
	([x] x).

% the following two rules for the case
% (dlet W V M) where W \not\in BP[M], see Fig 1 of the paper
focus-dlet11 : focus (prevalstuck-pst (PS : pre-stuck _ W1)) C ->
	      dv-neq W W1 ->
	focus (prevalstuck-pst PS) ([x] (dlet W V (C x))).

focus-dlet12 : focus (prevalstuck-pval P) C -> 
	focus (prevalstuck-pval P) ([x] (dlet W V (C x))).

%{
%worlds () (pre-val _).
%worlds () (focus _ _).
}%


% Proving the classification theorem: every expression is either a value
% or can be focused (that is, decomposed into the context and a prevalstuck).
% This is the most tiresome part...
% It's purely syntactical, there aren't any (object-level) types involved...

val-or-focus : exp -> type.		% The (dependent) sum type
val-or-focus-val   : val E                       -> val-or-focus E.
val-or-focus-focus : focus (_ : prevalstuck M) C -> val-or-focus (C M).

% classification of expressions.
val-focus-disj : {M:exp} val-or-focus M -> type.
%mode val-focus-disj +M -VOF.
- : val-focus-disj _ (val-or-focus-val val_lam).
- : val-focus-disj _ (val-or-focus-val val_unit).

% lemma for application. Factoring.
vfd-app : val-or-focus M1 -> val-or-focus M2 -> val-or-focus (app M1 M2)
	-> type.
%mode vfd-app +P1 +P2 -P3.
- : vfd-app (val-or-focus-val P1) (val-or-focus-val P2) 
	    (val-or-focus-focus (focus-app P1 P2)).
- : vfd-app (val-or-focus-focus P1) _ (val-or-focus-focus (focus-app1 P1)).
- : vfd-app (val-or-focus-val P1) (val-or-focus-focus P2)
	(val-or-focus-focus (focus-app2 P1 P2)).
%worlds (tp_ds) (vfd-app _ _ _).
%total {} (vfd-app _ _ _).

- : val-focus-disj _ P
	<- val-focus-disj _ PE1 <- val-focus-disj _ PE2 <- vfd-app PE1 PE2 P.

- : val-focus-disj (dref W)   (val-or-focus-focus (focus-pst
	: focus (prevalstuck-pst prestuck-dref) [x] x)).
- : val-focus-disj (dset W V) (val-or-focus-focus (focus-pst
	: focus (prevalstuck-pst prestuck-dset) [x] x)).

vfd-dlet : {W:dv} {V:val M2} val-or-focus M1 -> 
		val-or-focus (dlet W V M1) -> type.
%mode vfd-dlet +W +V +P1 -P2.
- : vfd-dlet _ _ (val-or-focus-val P1) (val-or-focus-focus (focus-dlet01 P1)).
- : vfd-dlet _ _ 
	(val-or-focus-focus (PF : focus (prevalstuck-pval _) _))
	(val-or-focus-focus (focus-dlet12 PF)).

% Note: it is important that {V:val M2} appears near the end, rather
% than at the beginning. If we write
% {V:val M2} dv-cmp W W1 -> focus M1 ... -> val-or-focus (dlet W V M1) -> type.
% then both arguments, dv-cmp and focus become skolemized over V.
% It is clear though that they do not depend on V. Therefore,
% we have to put the quantification over V close to the end to show
% that dv-cmp and focus arguments to vdf-dlet1 do not depend on V.

vfd-dlet1 : dv-cmp W W1 -> 
	    focus (prevalstuck-pst (_ : pre-stuck M W1)) C ->
	    {V:val M2}
		val-or-focus (dlet W V (C M)) -> type.
%mode vfd-dlet1 +WC +PF +V -P.
- : vfd-dlet1 (dv-cmp-eq (dv-eq-refl : dv-eq W W)) PF V
	(val-or-focus-focus ((focus-dlet02 PF) : focus _ _)).
- : vfd-dlet1 (dv-cmp-neq (PN : dv-neq W W1)) PF V
	(val-or-focus-focus ((focus-dlet11 PF PN) : focus _ _)).
%worlds (tp_ds) (vfd-dlet1 _ _ _ _).
%total {} (vfd-dlet1 _ _ _ _).

- :  vfd-dlet W V
	(val-or-focus-focus 
            (PF : focus (prevalstuck-pst (_ : pre-stuck _ W1)) _))
	P
	<- dv-cmp-decide W W1 WC
	<- vfd-dlet1 WC PF V P.

%worlds (tp_ds) (lemma-dvc _ _).
%worlds (tp_ds) (dv-cmp-decide _ _ _).
%worlds (tp_ds) (vfd-dlet _ _ _ _).
%total {} (vfd-dlet _ _ _ _).

- : val-focus-disj (dlet W V M) P <- val-focus-disj _ PM1 
	<- vfd-dlet W V PM1 P.


%worlds (tp_ds) (val-focus-disj _ _).
%total M (val-focus-disj M _). % At long last...


% ----------------------------------------------------------------------
% Dynamic semantics: small-step evaluation relation

% Redexes and their reductions. The small-step semantics.
% At last the interesting part.

rdx : exp -> exp -> type.		%name rdx R.
% %mode rdx +M1 -M2.
rdx-app  : rdx (app (lam _ M1) M2) (M1 M2) <- val M2.
rdx-dletv : rdx (dlet W V M) M <- val M.
rdx-dletr : rdx (dlet W (V : val MV) (C (dref W))) (dlet W V (C MV))
	<- focus (prevalstuck-pst (_ : pre-stuck (dref W) W)) C.
rdx-dlets : rdx (dlet W (V : val MV) (C (dset W V'))) (dlet W V' (C MV))
	<- focus (prevalstuck-pst (_ : pre-stuck (dset W V') W)) C.
% %terminates M (rdx M _).
% %worlds () (rdx _ _).


% Combine focusing and evaluation.
% We can now reap the fruits of our labor: the eval relation
% is fully generic and does not depend on the details of focusing
% or reductions. We can freely add more reduction/context rules.

eval : exp -> exp -> type.		%name eval D.
eval1 : eval (CF ER) (CF ER') 
	<- focus (prevalstuck-pval (_ : pre-val ER)) CF 
	<- rdx ER ER'.


% Big step: transitive closure of eval*: just to be able to run examples
eval* : exp -> exp -> type.
eval1* : eval* E E <- val E.
eval2* : eval* E E'' <- eval E E' <- eval* E' E''.

% sample example


%query 1 2 eval*
    (app v0 unit)
    M.

%query 1 1 eval*
    (dlet w0 val_unit (app v0 unit))
    M.


%query 1 2 rdx
    (dlet w0 val_unit (dref w0))
    (dlet w0 val_unit unit).

% Need to check why we have the second solution here too...
%query 1 1 eval
    term1
    M.
% dlet w0 val_unit (app v0 unit)

%query 1 1 eval*
    term1
    unit.

%query 1 1 eval*
    term2
    M.

%query 1 1 eval*
    term3
    v2.

%query 1 1 eval*
    term4
    v1.

%query 0 1 eval*
    (app stuck1 v0)
    M.


% ----------------------------------------------------------------------
% Proving type-preservation: small-step evaluation preserves types

% If an expression is well-typed, then the result of its focusing
% is well-typed.
% The last argument of tpsfocus is to prove the reverse, that is,
% the context substitution.
tpsfocus : focus (prevalstuck-pval (PPV : pre-val ER)) CF 
	-> of (CF ER) T -> of ER TR 
	-> ({ER':exp} {p:of ER' TR} of (CF ER') T)
	-> type.
%mode tpsfocus +F +P -P' -PF.
- : tpsfocus (focus-app _ _) P P ([e] [p] p).
- : tpsfocus (focus-app1 F) (tp-app PA PO) PO' ([e] [p] (tp-app PA (PF _ p)))
	<- tpsfocus F PO PO' PF.
- : tpsfocus (focus-app2 _ F) (tp-app PA PO) PA' ([e] [p] (tp-app (PF _ p) PO))
	<- tpsfocus F PA PA' PF.

- : tpsfocus (focus-dlet01 PE) P P ([e] [p] p).
- : tpsfocus (focus-dlet02 PS) P P ([e] [p] p).
- : tpsfocus (focus-dlet12 F) (tp-dlet PW PM PV) PM' 
	     ([e] [p] (tp-dlet PW (PF _ p) PV))
	<- tpsfocus F PM PM' PF.
%worlds (tp_ds) (tpsfocus _ _ _ _).
%total F (tpsfocus F _ _ _).




% The following is the complement of tpsfocus above,
% for a PPV which is of the type (pre-stuck _ W).
% There is a duplication, but only in app-related clauses.
% The dref/dset-related clauses are complimentary.

tpsfocus+ : focus (prevalstuck-pst (_ : pre-stuck MW W)) CF 
	-> of (CF MW) T -> sig W TR 
	-> of MW TR
	-> ({ER':exp} {p:of ER' TR} of (CF ER') T)
	-> type.
%mode tpsfocus+ +F +P +S -P' -PF.
% - : tpsfocus+ (focus-app _ _) P S P ([e] [p] p).
- : tpsfocus+ (focus-app1 F) (tp-app PA PO) S PO' 
	      ([e] [p] (tp-app PA (PF _ p)))
	<- tpsfocus+ F PO S PO' PF.
- : tpsfocus+ (focus-app2 _ F) (tp-app PA PO) S PA'
	      ([e] [p] (tp-app (PF _ p) PO))
	<- tpsfocus+ F PA S PA' PF.

- : tpsfocus+ (focus-pst) (tp-dref S  ) S (tp-dref S  ) ([e] [p] p).
- : tpsfocus+ (focus-pst) (tp-dset S P) S (tp-dset S P) ([e] [p] p).
- : tpsfocus+ (focus-dlet11 F NE) (tp-dlet PW PM PV) S PM'
	     ([e] [p] (tp-dlet PW (PF _ p) PV))
	<- tpsfocus+ F PM S PM' PF.
%worlds (tp_ds) (tpsfocus+ _ _ _ _ _).
%total F (tpsfocus+ F _ _ _ _).

% Show that redex reductions preserve typing. These
% are the interesting rules in this section.

tpsrdx : rdx M M' -> of M T -> of M' T -> type.
%mode tpsrdx +R +P -Q.
- : tpsrdx (rdx-app _) (tp-app P2 (tp-lam P1)) (P1 _ P2).
- : tpsrdx (rdx-dletv _) (tp-dlet TW TM TV) TM.
- : tpsrdx (rdx-dletr PF)
	   (tp-dlet TW TM TV) (tp-dlet TW (C _ TV) TV)
	<- tpsfocus+ PF TM TW _ C.
- : tpsrdx (rdx-dlets PF)
	   (tp-dlet TW TM TV) (tp-dlet TW (C _ TV) TV')
	<- tpsfocus+ PF TM TW (tp-dset _ TV') C.
%worlds (tp_ds) (tpsrdx D P _).
%total D (tpsrdx D P _).

% Now, the full preservation. It is only one rule now, regardless
% of evaluation and typing rules.
tps : eval E E' -> of E T -> of E' T -> type.
%mode tps +R +P -Q.
- : tps (eval1 PR PF) PTE (PF' _ PTR')
	<- tpsfocus PF PTE PTR PF'
	<- tpsrdx PR PTR PTR'.
%worlds (tp_ds) (tps D P _).
%total D (tps D P _).


% ----------------------------------------------------------------------
% Proving progress: a well-typed expression is either a value,
% or can be reduced, or is BP-stuck.

% If a preval has a type, it is a redex.
% This is the only interesting rule.
% To make sure we're not proving the empty proposition
% (that is, our world is correct), try commenting out
% one of the clauses. One should get a coverage failure.

typed-preval : {PV:pre-val M} of M T -> rdx M M' -> type.
%mode typed-preval +PPV +PT -R.
- : typed-preval (preval-app PV1 PV2) (tp-app _ _) (rdx-app PV2).
- : typed-preval (preval-dlet1 PV) _ (rdx-dletv PV).
- : typed-preval 
	(preval-dlet2 
	      (PS : focus ((prevalstuck-pst _) : prevalstuck (dref W)) _))
	(tp-dlet TM TV TW) (rdx-dletr PS).
- : typed-preval
	(preval-dlet2 
	      (PS : focus ((prevalstuck-pst _) : prevalstuck (dset W _)) _))
	(tp-dlet TM TV TW) (rdx-dlets PS).
%worlds (tp_ds) (typed-preval _ _ _).
%total {} (typed-preval _ _ _).


% If a focusable to a pre-val expression has a type, it can make progress.
% This rule has only one clause and it is generic over the number
% of evaluation/typing rules.
fprog : focus (prevalstuck-pval PPV : prevalstuck M) C -> of (C M) T -> eval (C M) M' -> type.
%mode fprog +F +P -D.
- : fprog (PF : focus (prevalstuck-pval PPV) _) PT (eval1 R PF) 
	<- tpsfocus PF PT PTPV _
	<- typed-preval PPV PTPV R.
%worlds (tp_ds) (fprog _ _ _).
%total {} (fprog _ _ _).


% The final straw: any typed expression is either a value,
% BP-stuck, or can make progress.

progress : exp -> type.			% The sum type.
progress-val  : val M             -> progress M.
progress-bps  : focus (prevalstuck-pst _ : prevalstuck M) C  -> progress (C M).
progress-eval : eval M M'         -> progress M.

% Aux lemma
tprog-vf : {M:exp} val-or-focus M -> of M T -> progress M -> type.
%mode tprog-vf +M +VF +T -G.
- : tprog-vf _ (val-or-focus-val PV) _ (progress-val PV).
- : tprog-vf _ (val-or-focus-focus (PF : focus (prevalstuck-pval PPV) C)) T 
	(progress-eval D)
	<- fprog PF T D.
- : tprog-vf _ (val-or-focus-focus (PF : focus (prevalstuck-pst PS) C)) T 
	(progress-bps PF).
%worlds (tp_ds) (tprog-vf _ _ _ _).
%total VF (tprog-vf VF _ _ _).


tprog : {E:exp} of E T -> progress E -> type.
%mode tprog +E +T -G.
- : tprog E T G <- val-focus-disj E VF <- tprog-vf E VF T G.
%worlds (tp_ds) (tprog _ _ _).
%total {} (tprog _ _ _).
	% And Twelf agrees with us. We've got a proof!