Lily
From The Twelf Project
This case study concerns the metatheory of the linear Lily language.
It is incomplete; ask User:varming for updates.
In this example I will show examples of the following:
- Encoding of a linear type system.
- Definition of an abstract machine using evaluation frames.
- Correspondence between the big step semantics and the machine.
- Complete induction on the height of a derivation.
Contents |
[edit] Lily - the language
[edit] Grammar
I define the grammar for the types
% Lily meta theory % By Carsten Varming 2006 tp : type. %name tp Tp. func : tp -> tp -> tp. all : (tp -> tp) -> tp. bang : tp -> tp. i : tp. tensor : tp -> tp -> tp. %freeze tp.
and the grammar for the terms and values
term : type. %name term M. lam : tp -> (term -> term) -> term. app : term -> term -> term. tlam : (tp -> term) -> term. tapp : term -> tp -> term. thunk : tp -> (term -> term) -> term. letb : term -> (term -> term) -> term. unit : term. letu : term -> term -> term. tens : term -> term -> term. lett : term -> (term -> term -> term) -> term. %freeze term. value : term -> type. %mode value +V. val_lam : value (lam _ _). val_tlam : value (tlam _). val_thunk : value (thunk _ _). val_unit : value unit. val_tens : value (tens _ _). %worlds () (value _). %terminates {} (value _). %freeze value.
Next I define the call-by-name big step evaluation relation
\n/ : term -> term -> type. %mode \n/ +M -V. %name \n/ EV. %infix none 500 \n/. ev_lam : lam T M \n/ lam T M. ev_tlam : tlam M \n/ tlam M. ev_thunk : thunk T M \n/ thunk T M. ev_unit : unit \n/ unit. ev_tens : tens M N \n/ tens M N. ev_app : app M N \n/ V <- M \n/ lam _ M' <- M' N \n/ V. ev_tapp : tapp M T \n/ V <- M \n/ tlam M' <- M' T \n/ V. ev_letb : letb M N \n/ V <- M \n/ thunk T M' <- N (letb (thunk T M') M') \n/ V. ev_letu : letu M N \n/ V <- M \n/ unit <- N \n/ V. ev_lett : lett M N \n/ V <- M \n/ tens M' M'' <- (N M' M'') \n/ V. %worlds () (\n/ _ _). %covers \n/ +M -V. %freeze \n/. \/ : term -> type. %postfix 500 \/. %mode \/ +M. terminate : M \/ <- M \n/ V. %freeze \/.
I also have an strict (call-by-value) evaluation relation for Lily.
\s/ : term -> term -> type. %mode \s/ +M -V. %name \s/ EV. %infix none 500 \s/. evs_lam : lam T M \s/ lam T M. evs_tlam : tlam M \s/ tlam M. evs_thunk : thunk T M \s/ thunk T M. evs_unit : unit \s/ unit. evs_tens : tens M N \s/ tens M N. evs_app : app M N \s/ V <- M \s/ lam _ M' <- N \s/ V' <- M' V' \s/ V. evs_tapp : tapp M T \s/ V <- M \s/ tlam M' <- M' T \s/ V. evs_letb : letb M N \s/ V <- M \s/ thunk T M' <- N (letb (thunk T M') M') \s/ V. evs_letu : letu M N \s/ V <- M \s/ unit <- N \s/ V. evs_lett : lett M N \s/ V <- M \s/ tens M' M'' <- (N M' M'') \s/ V. %worlds () (\s/ _ _). %covers \s/ +M -V. %freeze \s/.
[edit] Value soundness
By now I can prove value soundness for the two evaluation relations.
value_soundness : M \n/ V -> value V -> type. %mode value_soundness +D -V. vs_lam : value_soundness ev_lam val_lam. vs_tlam : value_soundness ev_tlam val_tlam. vs_thunk : value_soundness ev_thunk val_thunk. vs_unit : value_soundness ev_unit val_unit. vs_tens : value_soundness ev_tens val_tens. vs_app : value_soundness (ev_app D' _) V <- value_soundness D' V. vs_tapp : value_soundness (ev_tapp D' _) V <- value_soundness D' V. vs_letb : value_soundness (ev_letb D' _) V <- value_soundness D' V. vs_letu : value_soundness (ev_letu D' _) V <- value_soundness D' V. vs_lett : value_soundness (ev_lett D' _) V <- value_soundness D' V. %worlds () (value_soundness _ _). %freeze value_soundness. %total D (value_soundness D _). value_soundness_s : M \s/ V -> value V -> type. %mode value_soundness_s +D -V. vs_lam : value_soundness_s evs_lam val_lam. vs_tlam : value_soundness_s evs_tlam val_tlam. vs_thunk : value_soundness_s evs_thunk val_thunk. vs_unit : value_soundness_s evs_unit val_unit. vs_tens : value_soundness_s evs_tens val_tens. vs_app : value_soundness_s (evs_app D' _ _) V <- value_soundness_s D' V. vs_tapp : value_soundness_s (evs_tapp D' _) V <- value_soundness_s D' V. vs_letb : value_soundness_s (evs_letb D' _) V <- value_soundness_s D' V. vs_letu : value_soundness_s (evs_letu D' _) V <- value_soundness_s D' V. vs_lett : value_soundness_s (evs_lett D' _) V <- value_soundness_s D' V. %worlds () (value_soundness_s _ _). %freeze value_soundness_s. %total D (value_soundness_s D _).
It is also neat to know that values evaluate to themselves.
selfeval : value V -> (V \n/ V) -> type. %mode selfeval +V -E. selfeval_lam : selfeval val_lam ev_lam. selfeval_tlam : selfeval val_tlam ev_tlam. selfeval_thunk : selfeval val_thunk ev_thunk. selfeval_tens : selfeval val_tens ev_tens. selfeval_unit : selfeval val_unit ev_unit. %worlds () (selfeval _ _). %freeze selfeval. %total V (selfeval V _). selfevals : value V -> (V \s/ V) -> type. %mode selfevals +V -E. selfevals_lam : selfevals val_lam evs_lam. selfevals_tlam : selfevals val_tlam evs_tlam. selfevals_thunk : selfevals val_thunk evs_thunk. selfevals_tens : selfevals val_tens evs_tens. selfevals_unit : selfevals val_unit evs_unit. %worlds () (selfevals _ _). %freeze selfevals. %total V (selfevals V _).
[edit] Equalities
I need some equalities on types and terms:
eqt : tp -> tp -> type. %mode eqt +T -T'. eqt_ref : eqt T T. %worlds () (eqt _ _). %freeze eqt. %total D (eqt D _). eqt_symm : eqt T T' -> eqt T' T -> type. %mode eqt_symm +Q -Q'. eqt_symm_rule : eqt_symm eqt_ref eqt_ref. %worlds () (eqt_symm _ _). %freeze eqt_symm. %total {} (eqt_symm _ _). eqt_ctx : eqt T T' -> {C : tp -> tp} eqt (C T) (C T') -> type. %mode eqt_ctx +E +C -E'. eqt_ctx_ref : eqt_ctx eqt_ref _ eqt_ref. %worlds () (eqt_ctx _ _ _). %freeze eqt_ctx. %total D (eqt_ctx D _ _). eqt_ctx2 : eqt T T' -> eqt T2 T2' -> {C : tp -> tp -> tp} eqt (C T T2) (C T' T2') -> type. %mode eqt_ctx2 +E +E' +C -E''. eqt_ctx2_ref : eqt_ctx2 eqt_ref eqt_ref _ eqt_ref. %worlds () (eqt_ctx2 _ _ _ _). %freeze eqt_ctx2. %total {} (eqt_ctx2 _ _ _ _). eq : term -> term -> type. %mode eq +M -M'. eq_ref : eq M M. %worlds () (eq _ _). %freeze eq. %total D (eq D _). eq_ctx : eq M M' -> {C : term -> term} eq (C M) (C M') -> type. %mode eq_ctx +Q +C -Q'. eq_ctx_ref : eq_ctx eq_ref _ eq_ref. %worlds () (eq_ctx _ _ _). %freeze eq_ctx. %total D (eq_ctx D _ _). eq_ctx2 : eq M M' -> eq M2 M2' -> {C : term -> term -> term} eq (C M M2) (C M' M2') -> type. %mode eq_ctx2 +Q +Q2 +C -Q'. eq_ctx2_ref : eq_ctx2 eq_ref eq_ref _ eq_ref. %worlds () (eq_ctx2 _ _ _ _). %freeze eq_ctx2. %total D (eq_ctx2 D _ _ _). eq_eval : eq M M' -> (M \n/ V) -> (M' \n/ V) -> type. %mode eq_eval +Q +E -E'. eq_eval_rule : eq_eval eq_ref E E. %worlds () (eq_eval _ _ _). %freeze eq_eval. %total D (eq_eval D _ _). eq_eval2 : eq V V' -> (M \n/ V) -> (M \n/ V') -> type. %mode eq_eval2 +Q +E -E'. eq_eval2_rule : eq_eval2 eq_ref E E. %worlds () (eq_eval2 _ _ _). %freeze eq_eval2. %total D (eq_eval2 D _ _). eq_res_s : eq V V' -> M \s/ V -> M \s/ V' -> type. %mode eq_res_s +Q +E -E. eq_res_s_rile : eq_res_s eq_ref E E. %worlds () (eq_res_s _ _ _). %freeze eq_res_s. %total {} (eq_res_s _ _ _). eq_evaluations : (M \n/ V) -> (M' \n/ V') -> type. %mode eq_evaluations +EV -EV'. eq_evaluations_ref : eq_evaluations E E. %worlds () (eq_evaluations _ _). %freeze eq_evaluations. %total D (eq_evaluations D _). eq_tens : eq (tens M1 M2) (tens M1' M2') -> eq M1 M1' -> eq M2 M2' -> type. %mode eq_tens +EQ1 -EQ2 -EQ3. eq_tens_rule : eq_tens eq_ref eq_ref eq_ref. %worlds () (eq_tens _ _ _). %freeze eq_tens. %total D (eq_tens D _ _). eq_thunk : eq (thunk T E) (thunk T' E') -> eq (letb (thunk T E) E) (letb (thunk T' E') E') -> type. %mode eq_thunk +EQ -EQ'. eq_thunk_rule : eq_thunk eq_ref eq_ref. %worlds () (eq_thunk _ _). %freeze eq_thunk. %total D (eq_thunk D _). eq_lam : eq (lam T E) (lam T' E') -> eq X X' -> eq (E X) (E' X') -> type. %mode eq_lam +E +E' -E''. eq_lam_rule : eq_lam eq_ref eq_ref eq_ref. %worlds () (eq_lam _ _ _). %freeze eq_lam. %total D (eq_lam D _ _). eq_tlam : eq (tlam E) (tlam E') -> eqt X X' -> eq (E X) (E' X') -> type. %mode eq_tlam +E +E' -E''. eq_tlam_rule : eq_tlam eq_ref eqt_ref eq_ref. %worlds () (eq_tlam _ _ _). %freeze eq_tlam. %total D (eq_tlam D _ _). eq_sym : eq A B -> eq B A -> type. %mode eq_sym +E -Q. eq_sym_rule : eq_sym eq_ref eq_ref. %worlds () (eq_sym _ _). %freeze eq_sym. %total D (eq_sym D _).
[edit] Determinism
Evaluation is deterministic.
eval_determ : M \n/ V -> M \n/ V' -> eq V V' -> type. %mode eval_determ +E +E' -Q. eval_determ_unit : eval_determ ev_unit ev_unit eq_ref. eval_determ_tens : eval_determ ev_tens ev_tens eq_ref. eval_determ_tlam : eval_determ ev_tlam ev_tlam eq_ref. eval_determ_lam : eval_determ ev_lam ev_lam eq_ref. eval_determ_thunk : eval_determ ev_thunk ev_thunk eq_ref. eval_determ_app : eval_determ ((ev_app EV2 EV1) : (app M1 M2) \n/ V) ((ev_app EV2' EV1') : (app M1 M2 \n/ V')) Q <- eval_determ EV1 EV1' Q1 <- eq_lam Q1 (eq_ref : eq M2 M2) Q3 <- eq_sym Q3 Q4 <- eq_eval Q4 EV2' EV2s <- eval_determ EV2 EV2s Q. eval_determ_tapp : eval_determ ((ev_tapp EV2 EV1) : (tapp M1 T2) \n/ V) ((ev_tapp EV2' EV1') : (tapp M1 T2 \n/ V')) Q <- eval_determ EV1 EV1' Q1 <- eq_tlam Q1 (eqt_ref : eqt T2 T2) Q3 <- eq_sym Q3 Q4 <- eq_eval Q4 EV2' EV2s <- eval_determ EV2 EV2s Q. eval_determ_letb : eval_determ ((ev_letb EV2 EV1) : (letb M1 M2) \n/ V) ((ev_letb EV2' EV1') : (letb M1 M2 \n/ V')) Q <- eval_determ EV1 EV1' Q1 <- eq_thunk Q1 Q2 <- eq_ctx Q2 M2 Q3 <- eq_sym Q3 Q4 <- eq_eval Q4 EV2' EV2s <- eval_determ EV2 EV2s Q. eval_determ_letu : eval_determ ((ev_letu EV2 EV1) : (letu M1 M2) \n/ V) ((ev_letu EV2' EV1') : (letu M1 M2 \n/ V')) Q <- eval_determ EV2 EV2' Q. eval_determ_lett : eval_determ ((ev_lett EV2 EV1) : (lett M1 M2) \n/ V) ((ev_lett EV2' EV1') : (lett M1 M2 \n/ V')) Q <- eval_determ EV1 EV1' Q1 <- eq_tens Q1 Q2 Q3 <- eq_ctx2 Q2 Q3 M2 Q4 <- eq_sym Q4 Q4' <- eq_eval Q4' EV2' EV2s <- eval_determ EV2 EV2s Q. %worlds () (eval_determ _ _ _). %freeze eval_determ. %total D (eval_determ D _ _).
And transitive:
eval_trans : M \n/ V -> V \n/ V' -> M \n/ V' -> type. %mode eval_trans +EV +EV' -EV''. eval_trans_rule : eval_trans EV EV' EV'' <- value_soundness EV Vv <- selfeval Vv EVv' <- eval_determ EVv' EV' Q <- eq_eval2 Q EV EV''. %worlds () (eval_trans _ _ _). %total {} (eval_trans _ _ _). eq_val : eq M M' -> value M -> value M' -> type. %mode eq_val +Q +V -V'. eq_val_rule : eq_val eq_ref V V. %worlds () (eq_val _ _ _). %freeze eval_trans. %total {} (eq_val _ _ _).
[edit] Frame stack semantics
The abstract machine is defined as a relation on tuples consisting of a frame stack and a term to evaluate in that stack.
[edit] Evaluation frames
The frame stack is a stack of evaluation frames that provides a context on which we will continue evaluation after we have computed a value for the current term.
frame : (term -> term) -> type. %name frame F. fletb : {M} frame [a] letb a M. fapp : {M} frame [a] app a M. ftapp : {T} frame [a] tapp a T. fletu : {M} frame [a] letu a M. flett : {M} frame [a] lett a M. %freeze frame.
Evaluation frames are functions from terms to terms and sometimes I need to apply such a function to a term.
frameapp : frame F -> term -> term -> type. %mode frameapp +F +M -M'. frameapp_app : % {F : frame F'} frameapp (F : frame F') M (F' M). %worlds () (frameapp _ _ _). %freeze frameapp. %total D (frameapp D _ _). frameapp_exists : {F}{M} (frameapp F M M') -> type. %mode frameapp_exists +F +M -FM. frameapp_exists_rule : frameapp_exists F M frameapp_app. %worlds () (frameapp_exists _ _ _). %freeze frameapp_exists. %total D (frameapp_exists D _ _).
The definition of the frame stack and application of frame stacks to terms.
framestack : type. %name framestack Fs. cons : frame F -> framestack -> framestack. nil : framestack. %freeze framestack. frameapply : framestack -> term -> term -> type. %mode frameapply +FS +M -M'. frameapply_nil : frameapply nil M M. frameapply_cons : frameapply (cons F Fs) M M' <- frameapp F M M'' <- frameapply Fs M'' M'. %worlds () (frameapply _ _ _). %freeze frameapply. %total D (frameapply D _ _).
I should move you:
%block blam : block {y:term}.
[edit] Equalities on frame stacks
I also need some equational reasoning on frame stacks:
eqf : framestack -> framestack -> type. %mode eqf +Fs -Fs'. eqf_ref : eqf Fs Fs. %freeze eqf. eqf_symm : eqf Fs Fs' -> eqf Fs' Fs -> type. %mode eqf_symm +Q -Q'. eqf_symm_rule : eqf_symm eqf_ref eqf_ref. %worlds (blam) (eqf_symm _ _). %freeze eqf_symm. %total {} (eqf_symm _ _). eqf_trans : eqf Fs Fs' -> eqf Fs' Fs'' -> eqf Fs Fs'' -> type. %mode eqf_trans +Q +Q' -Q''. eqf_trans_rule : eqf_trans eqf_ref eqf_ref eqf_ref. %worlds (blam) (eqf_trans _ _ _). %freeze eqf_trans. %total {} (eqf_trans _ _ _). eqf_extend : {F} eqf Fs Fs' -> eqf (cons F Fs) (cons F Fs') -> type. %mode eqf_extend +F +Q -Q'. eqf_extend_rule : eqf_extend _ eqf_ref eqf_ref. %worlds (blam) (eqf_extend _ _ _). %freeze eqf_extend. %total {} (eqf_extend _ _ _). frameapply_eq : eqf Fs Fs' -> frameapply Fs M FsM -> frameapply Fs' M FsM -> type. %mode frameapply_eq +Q +FA -FA. frameapply_eq_rule : frameapply_eq eqf_ref FA FA. %worlds (blam) (frameapply_eq _ _ _). %freeze frameapply_eq. %total {} (frameapply_eq _ _ _). frameapply_nil_eq : frameapply nil M M' -> eq M M' -> type. %mode frameapply_nil_eq +F -Q. frameapply_nil_eq_rule : frameapply_nil_eq frameapply_nil eq_ref. %worlds (blam) (frameapply_nil_eq _ _). %freeze frameapply_nil_eq. %total {} (frameapply_nil_eq _ _).
[edit] More metatheorems about frame application
frameapply_exists : {Fs}{M} (frameapply Fs M M') -> type. %mode frameapply_exists +Fs +M -A. frameapply_exists_nil : frameapply_exists nil M frameapply_nil. frameapply_exists_cons_letu : frameapply_exists (cons (fletu N) Fs) M (frameapply_cons FsA frameapp_app) <- frameapply_exists Fs (letu M N) FsA. frameapply_exists_cons_letb : frameapply_exists (cons (fletb N) Fs) M (frameapply_cons FsA frameapp_app) <- frameapply_exists Fs (letb M N) FsA. frameapply_exists_cons_lett : frameapply_exists (cons (flett N) Fs) M (frameapply_cons FsA frameapp_app) <- frameapply_exists Fs (lett M N) FsA. frameapply_exists_cons_app : frameapply_exists (cons (fapp N) Fs) M (frameapply_cons FsA frameapp_app) <- frameapply_exists Fs (app M N) FsA. frameapply_exists_cons_tapp : frameapply_exists (cons (ftapp N) Fs) M (frameapply_cons FsA frameapp_app) <- frameapply_exists Fs (tapp M N) FsA. %worlds () (frameapply_exists _ _ _). %freeze frameapply_exists. %total D (frameapply_exists D _ _).
[edit] Frame stack evaluation
Here I define the evaluation relation for the abstract machine.
--> : framestack -> term -> framestack -> term -> type. %mode --> +Fs +M -Fs' -M'. evfs_letu : --> Fs (letu M N) (cons (fletu N) Fs) M. evfs_letb : --> Fs (letb M N) (cons (fletb N) Fs) M. evfs_lett : --> Fs (lett M N) (cons (flett N) Fs) M. evfs_app : --> Fs (app M N) (cons (fapp N) Fs) M. evfs_tapp : --> Fs (tapp M T) (cons (ftapp T) Fs) M. evfs_lam : --> (cons (fapp N) Fs) (lam _ M') Fs (M' N). evfs_tlam : --> (cons (ftapp T) Fs) (tlam M') Fs (M' T). evfs_unit : --> (cons (fletu N) Fs) unit Fs N. evfs_tens : --> (cons (flett N) Fs) (tens M1 M2) Fs (N M1 M2). evfs_thunk : --> (cons (fletb N) Fs) (thunk T M) Fs (N (letb (thunk T M) M)). %worlds () (--> _ _ _ _). %covers --> -Fs +M -Fs' -M'. %freeze -->. eq_step : eq M M' -> --> Fs M Fs1 M1 -> --> Fs M' Fs1 M1 -> type. %mode eq_step +Q +S -S'. eq_step_rule : eq_step eq_ref S S. %worlds () (eq_step _ _ _). %total {} (eq_step _ _ _). -->* : framestack -> term -> framestack -> term -> type. -->*_ref : -->* Fs M Fs M. -->*_step : -->* Fs M Fs' M' <- --> Fs'' M'' Fs' M' <- -->* Fs M Fs'' M''. %freeze -->*.
[edit] Meta theory of the abstract machine
Here are some basic properties of the abstract machine:
concat-->* : (-->* Fs M Fs'' M'') -> (-->* Fs'' M'' Fs' M') -> (-->* Fs M Fs' M') -> type. %mode concat-->* +S1 +S2 -S. concatref : concat-->* S -->*_ref S. concatstep : concat-->* S' (-->*_step Ss S) (-->*_step Sc S) <- concat-->* S' Ss Sc. %worlds () (concat-->* _ _ _). %freeze concat-->*. %total D (concat-->* _ D _). -->*_impossible : --> nil V Fs M -> value V -> -->* Fs' M' Fs'' M'' -> type. %mode +{V:term} +{Fs:framestack} +{M:term} +{Fs':framestack} +{M':term} +{Fs'':framestack} +{M'':term} +{S:--> nil V Fs M} +{V1:value V} -{R:-->* Fs' M' Fs'' M''} (-->*_impossible S V1 R). %worlds () (-->*_impossible _ _ _). %freeze -->*_impossible. %total {} (-->*_impossible _ _ _). lemma44 : {Fs : framestack} {M} frameapply Fs M FsM -> (-->* nil FsM Fs M) -> type. %mode lemma44 +Fs +M +FA -E. lemma44_nil : lemma44 nil M frameapply_nil -->*_ref. lemma44_cons_letu : lemma44 (cons (fletu N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_letu) <- lemma44 Fs (letu M N) FA MS. lemma44_cons_letb : lemma44 (cons (fletb N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_letb) <- lemma44 Fs (letb M N) FA MS. lemma44_cons_lett : lemma44 (cons (flett N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_lett) <- lemma44 Fs (lett M N) FA MS. lemma44_cons_app : lemma44 (cons (fapp N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_app) <- lemma44 Fs (app M N) FA MS. lemma44_cons_tapp : lemma44 (cons (ftapp N) Fs) M (frameapply_cons FA frameapp_app) (-->*_step MS evfs_tapp) <- lemma44 Fs (tapp M N) FA MS. %worlds () (lemma44 _ _ _ _). %freeze lemma44. %total D (lemma44 D _ _ _). frameApplyUnique : (frameapply Fs M FsM) -> (frameapply Fs M FsM') -> (eq FsM FsM') -> type. %mode frameApplyUnique +FA1 +FA2 -Q. frameApplyUnique_nil : frameApplyUnique frameapply_nil frameapply_nil eq_ref. frameApplyUnique_cons : frameApplyUnique (frameapply_cons FsA frameapp_app) (frameapply_cons FsA' frameapp_app) Q <- frameApplyUnique FsA FsA' Q. %worlds () (frameApplyUnique _ _ _). %freeze frameApplyUnique. %total D (frameApplyUnique D _ _).
[edit] Correspondence between the big step semantics and the abstract machine
lemma48 : {Fs} {M} (M \n/ V) -> (-->* Fs M Fs V) -> type. %mode lemma48 +Fs +M +E -Ss. lemma48_lam : lemma48 _ _ ev_lam -->*_ref. lemma48_tens : lemma48 _ _ ev_tens -->*_ref. lemma48_thunk : lemma48 _ _ ev_thunk -->*_ref. lemma48_tlam : lemma48 _ _ ev_tlam -->*_ref. lemma48_unit : lemma48 _ _ ev_unit -->*_ref. lemma48_app : lemma48 Fs (app M1 M2) (ev_app EM' EM1) Sr <- lemma48 (cons (fapp M2) Fs) M1 (EM1 : M1 \n/ (lam _ M')) SM1 <- lemma48 Fs (M' M2) (EM' : (M' M2) \n/ V) SM' <- concat-->* (-->*_step SM1 evfs_lam) SM' S <- concat-->* (-->*_step -->*_ref evfs_app) S Sr. lemma48_tapp : lemma48 Fs (tapp M1 T) (ev_tapp EM' EM1) Sr <- lemma48 (cons (ftapp T) Fs) M1 (EM1 : M1 \n/ (tlam M')) SM1 <- lemma48 Fs (M' T) (EM' : (M' T) \n/ V) SM' <- concat-->* (-->*_step SM1 evfs_tlam) SM' S <- concat-->* (-->*_step -->*_ref evfs_tapp) S Sr. lemma48_letu : lemma48 Fs (letu M1 M2) (ev_letu EM' EM1) Sr <- lemma48 (cons (fletu M2) Fs) M1 (EM1 : M1 \n/ unit) SM1 <- lemma48 Fs M2 (EM' : M2 \n/ V) SM' <- concat-->* (-->*_step SM1 evfs_unit) SM' S <- concat-->* (-->*_step -->*_ref evfs_letu) S Sr. lemma48_letb : lemma48 Fs (letb M1 M2) (ev_letb EM' EM1) Sr <- lemma48 (cons (fletb M2) Fs) M1 (EM1 : M1 \n/ (thunk T M')) SM1 <- lemma48 Fs (M2 (letb (thunk T M') M')) (EM' : (M2 (letb (thunk T M') M')) \n/ V) SM' <- concat-->* (-->*_step SM1 evfs_thunk) SM' S <- concat-->* (-->*_step -->*_ref evfs_letb) S Sr. lemma48_lett : lemma48 Fs (lett M1 M2) (ev_lett EM' EM1) Sr <- lemma48 (cons (flett M2) Fs) M1 (EM1 : M1 \n/ (tens M' M'')) SM1 <- lemma48 Fs (M2 M' M'') (EM' : (M2 M' M'') \n/ V) SM' <- concat-->* (-->*_step SM1 evfs_tens) SM' S <- concat-->* (-->*_step -->*_ref evfs_lett) S Sr. %worlds () (lemma48 _ _ _ _). %freeze lemma48. %total D (lemma48 _ _ D _). lemma46a : {Fs : framestack} (M' \n/ V) -> (frameapply Fs M M') -> (frameapply Fs V' N) -> (M \n/ V') -> (N \n/ V) -> type. lemma46b : {Fs : framestack} (M \n/ V') -> (N \n/ V) -> (frameapply Fs M M') -> (frameapply Fs V' N) -> (M' \n/ V) -> type. %mode lemma46a +Fs +As +FaM -FV' -Res1 -Res2. %mode lemma46b +Fs +As1 +As2 +FaM +FV' -Res1. lemma46a_nil : lemma46a nil E frameapply_nil frameapply_nil E EV <- (value_soundness E Vv) <- (selfeval Vv EV). lemma46a_letu : lemma46a (cons (fletu N) Fs) (E : M' \n/ V) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E' <- lemma46a Fs E FA FA' (ev_letu (RN : N \n/ V') RM) (R2 : _ \n/ V) <- frameapply_exists Fs (letu unit N) FAu <- lemma46b Fs (ev_letu RN ev_unit : letu unit N \n/ V') R2 FAu FA' E'. lemma46a_app : lemma46a (cons (fapp N) Fs) (E : M' \n/ V) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E' <- lemma46a Fs E FA FA' (ev_app RN (RM : M \n/ (lam T M1))) R2 <- frameapply_exists Fs (app (lam T M1) N) FAu <- lemma46b Fs (ev_app RN ev_lam) R2 FAu FA' E'. lemma46a_tapp : lemma46a (cons (ftapp N) Fs) (E : M' \n/ V) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E' <- lemma46a Fs E FA FA' (ev_tapp RN (RM : M \n/ (tlam T))) R2 <- frameapply_exists Fs (tapp (tlam T) N) FAu <- lemma46b Fs (ev_tapp RN ev_tlam) R2 FAu FA' E'. lemma46a_letb : lemma46a (cons (fletb N) Fs) (E : M' \n/ V) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E' <- lemma46a Fs E FA FA' (ev_letb RN (RM : M \n/ (thunk T M1))) R2 <- frameapply_exists Fs (letb (thunk T M1) N) FAu <- lemma46b Fs (ev_letb RN ev_thunk) R2 FAu FA' E'. lemma46a_lett : lemma46a (cons (flett N) Fs) (E : M' \n/ V) (frameapply_cons FA frameapp_app) (frameapply_cons FAu frameapp_app) RM E' <- lemma46a Fs E FA FA' (ev_lett RN (RM : M \n/ (tens M1 M2))) R2 <- frameapply_exists Fs (lett (tens M1 M2) N) FAu <- lemma46b Fs (ev_lett RN ev_tens) R2 FAu FA' E'. lemma46b_nil : lemma46b nil (E : M1 \n/ M2) E' frameapply_nil frameapply_nil E'' <- value_soundness E V <- selfeval V EV <- eval_determ EV E' Q <- eq_eval2 Q E E''. lemma46b_letu : lemma46b (cons (fletu M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3 <- lemma46a Fs1 E2 X2 X3 (ev_letu EM6 EM2) EN <- eval_trans E1 EM2 EM1 <- lemma46b Fs1 (ev_letu EM6 EM1) EN X1 X3 E3. lemma46b_lett : lemma46b (cons (flett M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3 <- lemma46a Fs1 E2 X2 X3 (ev_lett EM6 EM2) EN <- eval_trans E1 EM2 EM1 <- lemma46b Fs1 (ev_lett EM6 EM1) EN X1 X3 E3. lemma46b_app : lemma46b (cons (fapp M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3 <- lemma46a Fs1 E2 X2 X3 (ev_app EM6 EM2) EN <- eval_trans E1 EM2 EM1 <- lemma46b Fs1 (ev_app EM6 EM1) EN X1 X3 E3. lemma46b_tapp : lemma46b (cons (ftapp M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3 <- lemma46a Fs1 E2 X2 X3 (ev_tapp EM6 EM2) EN <- eval_trans E1 EM2 EM1 <- lemma46b Fs1 (ev_tapp EM6 EM1) EN X1 X3 E3. lemma46b_letb : lemma46b (cons (fletb M6) Fs1) E1 E2 (frameapply_cons X1 frameapp_app) (frameapply_cons X2 frameapp_app) E3 <- lemma46a Fs1 E2 X2 X3 (ev_letb EM6 EM2) EN <- eval_trans E1 EM2 EM1 <- lemma46b Fs1 (ev_letb EM6 EM1) EN X1 X3 E3. %worlds () (lemma46a _ _ _ _ _ _) (lemma46b _ _ _ _ _ _). %freeze lemma46b lemma46a. %total (D E) (lemma46a D _ _ _ _ _) (lemma46b E _ _ _ _ _). lemma47 : (--> Fs M Fs' M') -> (frameapply Fs' M' FsM') -> (frameapply Fs M FsM) -> (FsM' \n/ V) -> (FsM \n/ V) -> type. %mode lemma47 +S +FA' -FA +EV' -EV. lemma47_letu : lemma47 evfs_letu (frameapply_cons X1 frameapp_app) X1 EV' EV'. lemma47_letb : lemma47 evfs_letb (frameapply_cons X1 frameapp_app) X1 EV' EV'. lemma47_lett : lemma47 evfs_lett (frameapply_cons X1 frameapp_app) X1 EV' EV'. lemma47_app : lemma47 evfs_app (frameapply_cons X1 frameapp_app) X1 EV' EV'. lemma47_tapp : lemma47 evfs_tapp (frameapply_cons X1 frameapp_app) X1 EV' EV'. lemma47_unit : lemma47 evfs_unit X1 (frameapply_cons X3 frameapp_app) EV' EV <- lemma46a Fs EV' X1 X2 (EM2 : M2 \n/ V') EN <- frameapply_exists Fs (letu unit M2) X3 <- lemma46b Fs (ev_letu EM2 ev_unit) EN X3 X2 EV. lemma47_tens : lemma47 evfs_tens X1 (frameapply_cons X3 frameapp_app) EV' EV <- lemma46a Fs EV' X1 X2 EM2 EN <- frameapply_exists Fs (lett (tens M3 M4) M2) X3 <- lemma46b Fs (ev_lett EM2 ev_tens) EN X3 X2 EV. lemma47_thunk : lemma47 evfs_thunk X1 (frameapply_cons X3 frameapp_app) EV' EV <- lemma46a Fs EV' X1 X2 EM2 EN <- frameapply_exists Fs (letb (thunk T M4) M2) X3 <- lemma46b Fs (ev_letb EM2 ev_thunk) EN X3 X2 EV. lemma47_lam : lemma47 evfs_lam X1 (frameapply_cons X3 frameapp_app) EV' EV <- lemma46a Fs EV' X1 X2 EM2 EN <- frameapply_exists Fs (app (lam T M4) M2) X3 <- lemma46b Fs (ev_app EM2 ev_lam) EN X3 X2 EV. lemma47_tlam : lemma47 evfs_tlam X1 (frameapply_cons X3 frameapp_app) EV' EV <- lemma46a Fs EV' X1 X2 EM2 EN <- frameapply_exists Fs (tapp (tlam M4) M2) X3 <- lemma46b Fs (ev_tapp EM2 ev_tlam) EN X3 X2 EV. %worlds () (lemma47 _ _ _ _ _). %freeze lemma47. %total S (lemma47 S _ _ _ _). -->r* : framestack -> term -> framestack -> term -> type. -->r*_ref : -->r* Fs M Fs M. -->r*_step : -->r* Fs M Fs' M' <- --> Fs M Fs'' M'' <- -->r* Fs'' M'' Fs' M'. %freeze -->r*. concat-->r* : -->r* Fs M Fs' M' -> -->r* Fs' M' Fs'' M'' -> -->r* Fs M Fs'' M'' -> type. %mode concat-->r* +A +B -C. concat-->r*_ref : concat-->r* -->r*_ref D D. concat-->r*_step : concat-->r* (-->r*_step R S) D (-->r*_step D' S) <- concat-->r* R D D'. %worlds () (concat-->r* _ _ _). %freeze concat-->r*. %total D (concat-->r* D _ _). -->r*_impossible : --> nil V Fs M -> value V -> -->r* Fs' M' Fs'' M'' -> type. %mode +{V:term} +{Fs:framestack} +{M:term} +{Fs':framestack} +{M':term} +{Fs'':framestack} +{M'':term} +{S:--> nil V Fs M} +{V1:value V} -{R:-->r* Fs' M' Fs'' M''} (-->r*_impossible S V1 R). %worlds () (-->r*_impossible _ _ _). %freeze -->r*_impossible. %total {} (-->r*_impossible _ _ _). concat-->r*_exists : {R : -->r* F1 M1 Fs M} {S : -->r* (Fs : framestack) (M : term) (Fs2 : framestack) (M2 : term)} (concat-->r* R S RS) -> type. %mode concat-->r*_exists +R +S -P. concat-->r*_exists_ref : concat-->r*_exists -->r*_ref _ concat-->r*_ref. concat-->r*_exists_step : concat-->r*_exists (-->r*_step R S) B (concat-->r*_step E) <- concat-->r*_exists R B E. %worlds () (concat-->r*_exists _ _ _). %freeze concat-->r*_exists. %total D (concat-->r*_exists D _ _). -->*_to_-->r*_lem : -->* Fs M Fs' M' -> -->r* Fs M Fs' M' -> type. %mode -->*_to_-->r*_lem +F -R. -->*_to_-->r*_lem_ref : -->*_to_-->r*_lem -->*_ref -->r*_ref. -->*_to_-->r*_lem_step : -->*_to_-->r*_lem (-->*_step R S) R'' <- -->*_to_-->r*_lem R R' <- concat-->r* R' (-->r*_step -->r*_ref S) R''. %worlds () (-->*_to_-->r*_lem _ _). %freeze -->*_to_-->r*_lem. %total D (-->*_to_-->r*_lem D _). -->r*_to_-->*_lem : -->r* Fs M Fs' M' -> -->* Fs M Fs' M' -> type. %mode -->r*_to_-->*_lem +F -R. -->r*_to_-->*_lem_ref : -->r*_to_-->*_lem -->r*_ref -->*_ref. -->r*_to_-->*_lem_step : -->r*_to_-->*_lem (-->r*_step R S) R'' <- -->r*_to_-->*_lem R R' <- concat-->* (-->*_step -->*_ref S) R' R''. %worlds () (-->r*_to_-->*_lem _ _). %freeze -->r*_to_-->*_lem. %total D (-->r*_to_-->*_lem D _). -->r*_add_step : (--> Fs M Fs' M') -> (-->r* Fs M nil V) -> (value V) -> (-->r* Fs' M' nil V) -> type. %mode -->r*_add_step +S +R +V -R'. -->r*_add_step_ref : -->r*_add_step S -->r*_ref V R <- -->r*_impossible S V R. -->r*_add_step_step : -->r*_add_step S (-->r*_step Rr S) V Rr. %worlds () (-->r*_add_step _ _ _ _). %freeze -->r*_add_step. %total {} (-->r*_add_step _ _ _ _). -->*_add_step : (--> Fs M Fs' M') -> (-->* Fs M nil V) -> (value V) -> (-->* Fs' M' nil V) -> type. %mode -->*_add_step +S +R +V -R'. -->*_add_step_rule : -->*_add_step S R V R' <- -->*_to_-->r*_lem R Rr <- -->r*_add_step S Rr V R'r <- -->r*_to_-->*_lem R'r R'. %worlds () (-->*_add_step _ _ _ _). %freeze -->*_add_step. %total {} (-->*_add_step _ _ _ _). -->*_to_-->r*_lem_exists : {S : -->* _ _ _ _} -->*_to_-->r*_lem S R -> type. %mode -->*_to_-->r*_lem_exists +S -P. -->*_to_-->r*_lem_exists_ref : -->*_to_-->r*_lem_exists -->*_ref -->*_to_-->r*_lem_ref. -->*_to_-->r*_lem_exists_step : -->*_to_-->r*_lem_exists (-->*_step R S) (-->*_to_-->r*_lem_step R'' R') <- -->*_to_-->r*_lem_exists R (R' : -->*_to_-->r*_lem R Rr) <- concat-->r*_exists Rr (-->r*_step -->r*_ref S) R''. %worlds () (-->*_to_-->r*_lem_exists _ _). %freeze -->*_to_-->r*_lem_exists. %total D (-->*_to_-->r*_lem_exists D _). eq_frame_eval_lemma : -->r* Fs M nil V -> value V -> frameapply Fs M FsM -> FsM \n/ V -> type. %mode eq_frame_eval_lemma +V +L -FA -EV. eq_frame_eval_lemma_z : eq_frame_eval_lemma -->r*_ref V frameapply_nil EV <- selfeval V EV. eq_frame_eval_lemma_s : eq_frame_eval_lemma (-->r*_step R S) V FA EV <- eq_frame_eval_lemma R V FA' EV' <- lemma47 S FA' FA EV' EV. %worlds () (eq_frame_eval_lemma _ _ _ _) . %freeze eq_frame_eval_lemma. %total D (eq_frame_eval_lemma D _ _ _). eq_frame_eval : -->* Fs M nil V -> value V -> frameapply Fs M FsM -> FsM \n/ V -> type. %mode eq_frame_eval +V +L -FA -EV. eq_frame_eval_rule : eq_frame_eval FE V FA E <- -->*_to_-->r*_lem FE R <- eq_frame_eval_lemma R V FA E. %worlds () (eq_frame_eval _ _ _ _). %freeze eq_frame_eval. %total D (eq_frame_eval D _ _ _). -->*_skew : -->* Fs M nil V -> (value V) -> (-->* Fs M Fs' M') -> (-->* Fs' M' nil V) -> type. %mode -->*_skew +R +V +R' -R''. -->*_skew_ref : -->*_skew R V -->*_ref R. -->*_skew_step : -->*_skew R V (-->*_step Rest S) RI <- -->*_skew R V Rest RI' <- -->*_add_step S RI' V RI. %worlds () (-->*_skew _ _ _ _) . %freeze -->*_skew. %total D (-->*_skew _ _ D _). eq_eval_frame : (frameapply Fs M FsM) -> (FsM \n/ V) -> (-->* Fs M nil V) -> type. %mode eq_eval_frame +FA +EV -R. eq_eval_frame_rule : eq_eval_frame (FA : frameapply Fs M FsM) EV