From f7badce82922e5a4e877ed8fe3903402054cb6da Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Mon, 24 Jun 2024 12:41:06 +0200 Subject: [PATCH 01/16] Added effect for first-order exceptions --- theories/effects/exceptions.v | 426 ++++++++++++++++++++++++++++++++++ 1 file changed, 426 insertions(+) create mode 100644 theories/effects/exceptions.v diff --git a/theories/effects/exceptions.v b/theories/effects/exceptions.v new file mode 100644 index 0000000..819584d --- /dev/null +++ b/theories/effects/exceptions.v @@ -0,0 +1,426 @@ +From gitrees Require Import gitree. +From iris.algebra Require Import list. + +Module Type ExcSig. + Parameter E : Set. + Parameter eq_dec_E : ∀ (x y : E), {x = y} + {x <> y}. +End ExcSig. + +Module Exc (Errors : ExcSig). + Import Errors. + + Structure exc := Exc { value : E }. + + Theorem eq_dec : ∀ (x y : exc), {x = y} + {x <> y}. + intros [x] [y]. + destruct (eq_dec_E x y) as [<-|HDiff]. + - left. reflexivity. + - right. intros Heq. injection Heq as <-. apply HDiff. reflexivity. + Defined. + + Canonical Structure excO := leibnizO exc. + Definition excOF := constOF exc. + + (** State functor, we keep track of the list of error handlers from most recently + registered to least recently registered along with the error they each + handle and the continuation present at the time of registration, this is + so that when raising an error we can erase only the context between the + raising of the error and the registering of the handler **) + Definition stateF : oFunctor := listOF (excOF * (▶ ∙ -n> ▶ ∙ ) * (▶ ∙ -n> ▶ ∙)). + + (** Register an exception handler for an exception type **) + Program Definition regE : opInterp := + {| + Ins := (excOF * (▶ ∙ -n> ▶ ∙ ) * (▶ ∙)); + Outs := (▶ ∙) + |}. + + Program Definition popE : opInterp := + {| + Ins := excOF; + Outs := unitO + |}. + + (** Throw an exception, empty Outs because we don't use the continuation **) + Program Definition throwE : opInterp := + {| + Ins := (excOF * (▶ ∙)); + Outs := Empty_setO; + |}. + + Definition exceptE := @[regE;popE;throwE]. + + (** Register a handler : Push the handler and current context on the stack **) + Definition reify_reg X `{Cofe X} : excO * (laterO X -n> laterO X) * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X) → option (laterO X * (stateF ♯ X)) := + λ '(e, h, b, σ, k), Some (b, (e,h,k)::σ). + + #[export] Instance reify_reg_ne X `{Cofe X}: NonExpansive (reify_reg X : excO * (laterO X -n> laterO X) * (laterO X) * (stateF ♯ X) * (laterO X -n> laterO X) → option (laterO X * (stateF ♯ X)) + ). + Proof. + solve_proper_prepare. + destruct x as [[[[? ?] ?] ?] ?]. + destruct y as [[[[? ?] ?] ?] ?]. + repeat rewrite e pair_dist in H0. + destruct H0 as [[[[? ?] ?] ?] ?]. + repeat f_equiv; done. + Qed. + + (** Unregister a handler : Remove the topmost handler, restore the ambient context from when it was registered **) + Definition reify_pop X `{Cofe X} : excO * (stateF ♯ X) * (unitO -n> laterO X) → option (laterO X * (stateF ♯ X)) := + λ '(err, σ, k), match σ with + | [] => None + | (err', h, k')::σ' => + (if (eq_dec err err') + then Some (k' (k ()), σ') + else None) end. + + #[export] Instance reify_pop_ne X `{Cofe X}: NonExpansive (reify_pop X : + excO * (stateF ♯ X) * (unitO -n> laterO X) → option (laterO X * (stateF ♯ X))). + Proof. + intros n [[e σ] k] [[e' σ'] k'] Hequiv. + rewrite pair_dist in Hequiv. + destruct Hequiv as [[He Hσ] Hk]. + simpl in *. + destruct σ' as [|p σ']. + - rewrite nil_dist_eq in Hσ. + rewrite Hσ. done. + - apply cons_dist_eq in Hσ. + destruct Hσ as (x & l' & Hx & Hl' & ->). + destruct x as [[xerr xh] xc]. + destruct p as [[perr ph] pc]. + repeat rewrite pair_dist in Hx. + destruct Hx as [[Herr Hh] Hc]. + rewrite He Herr. + destruct (eq_dec e' perr). + + rewrite Hl'. repeat f_equiv; done. + + reflexivity. + Qed. + + Fixpoint _cut_when {A : ofe} (p : (A -n> boolO)) (l : listO A) : optionO (A * listO A)%type := + match l with + | [] => None + | x::t => if p x then Some (x, t) else _cut_when p t + end. + + Program Definition cut_when {A} : (A -n> boolO) -n> (listO A) -n> optionO (A * listO A)%type + := λne p l, _cut_when p l. + Next Obligation. + Proof. + solve_proper_prepare. + generalize dependent y. + induction x as [|h t IH]. + - intros y Hy. + symmetry in Hy. + apply nil_dist_eq in Hy. + subst. + done. + - intros y Hy. + symmetry in Hy. + apply cons_dist_eq in Hy. + destruct Hy as (h' & t' & Hh & Ht & ->). + destruct (p h) eqn:Hp; + rewrite -Hh in Hp; + rewrite Hp. + + repeat f_equiv; done. + + apply IH. done. + Qed. + + Next Obligation. + Proof. + solve_proper_prepare. + induction x0 as [|h t IH]. + - done. + - simpl. + destruct H with h. + destruct (x h). + + done. + + apply IH. + Qed. + + Lemma cut_when_first_occ {A} : ∀ (p : A -n> bool) (l pre post : list A) (a : A), + l = pre ++ a::post → + p a = true → + Forall (λ x, p x = false) pre → + cut_when p l = Some (a, post). + Proof. + intros p l pre post a Hl Ha Hpre. + generalize dependent l. + induction pre as [|h t]. + - intros l ->. + simpl. + rewrite Ha. + exact eq_refl. + - intros l ->. + inversion Hpre as [|?? Hh Ht]. + simpl. + rewrite Hh. + apply IHt; done. + Qed. + + Program Definition aux {X} (err : exc) : (excO * (laterO X -n> laterO X) * (laterO X -n> laterO X))%type -n> boolO := + λne '(err', _, _), if eq_dec err err' then true else false. + Next Obligation. + Proof. + intros. + simpl. + intros [[e k] p] [[e' k'] p'] Heq. + rewrite pair_dist in Heq. + destruct Heq as [[He Hk] Hp]. + simpl in *. + rewrite He. + reflexivity. + Qed. + + (** Raise an error : Find the most recent handler handling this error and remove all handlers registered after it from the stack then invoke the handler inside the context from when it was registered **) + Definition reify_throw X `{Cofe X} : (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X) → option (laterO X * (stateF ♯ X)) := + λ '(x, σ, _), let (err,v) := x in + match cut_when (aux err) σ with + | None => None + | Some (_, h, k, σ') => Some (k (h v), σ') + end. + + #[export] Instance reify_throw_ne X `{Cofe X} : NonExpansive (reify_throw X : (excO * laterO X) * (stateF ♯ X) * (Empty_setO -n> laterO X) → option (laterO X * (stateF ♯ X))). + Proof. + solve_proper_prepare. + destruct x as [[[e v] σ] k]. + destruct y as [[[e' v'] σ'] k']. + destruct H0 as [[[He Hv] Hσ] Hk]. + simpl in *. + generalize dependent σ'. + induction σ as [|[[err hand] kont] σ]. + - intros. + symmetry in Hσ. + apply nil_dist_eq in Hσ. + rewrite Hσ. + done. + - intros. + symmetry in Hσ. + apply cons_dist_eq in Hσ. + destruct Hσ as ([[err' hand'] kont'] & σ'' & [[Herr Hhand] Hkont] & Hσ'' & ->). + simpl in *. + destruct (eq_dec e err) eqn:HEq. + + rewrite Herr -He. rewrite HEq. repeat f_equiv; done. + + symmetry in Hσ''. + setoid_replace (if eq_dec e' err' then true else false) with (if eq_dec e err then true else false). + * rewrite HEq. + exact (IHσ σ'' Hσ''). + * rewrite Herr -He. reflexivity. + Qed. + + + Canonical Structure reify_exc : sReifier CtxDep. + Proof. + simple refine {| sReifier_ops := exceptE; + sReifier_state := stateF + |}. + intros X HX op. + destruct op as [|[|[|[]]]]. + - simple refine (OfeMor (reify_reg X)). + - simple refine (OfeMor (reify_pop X)). + - simple refine (OfeMor (reify_throw X)). + Defined. + + Section constructors. + Context {Eff : opsInterp} {A} `{!Cofe A}. + Context {subEff0 : subEff exceptE Eff}. + Context {SubOfe0 : SubOfe unitO A}. + Notation IT := (IT Eff A). + Notation ITV := (ITV Eff A). + + + Program Definition _REG : excO -n> (laterO IT -n> laterO IT) -n> laterO IT -n> IT := + λne e h b, Vis (E:=Eff) (subEff_opid (inl ())) (subEff_ins (F:=exceptE) (op:=(inl ())) (e,h,b)) ((λne x, x) ◎ (subEff_outs (F:=exceptE) (op:=(inl ())))^-1). + Solve All Obligations with solve_proper. + + + Program Definition _POP : excO -n> IT := + λne e, Vis (E:=Eff) (subEff_opid (inr (inl ()))) (subEff_ins (F:=exceptE) (op:=(inr(inl ()))) e) ((λne _, Next $ Ret ()) ◎ (subEff_outs (F:=exceptE) (op:=(inr(inl ()))))^-1). + Solve All Obligations with solve_proper. + + Program Definition CATCH : excO -n> (laterO IT -n> laterO IT) -n> IT -n> IT := + λne err h b, + _REG err h (Next $ get_val + (λne res, get_val + (λne _, res) + (_POP err) + ) b + ). + Next Obligation. + Proof. + solve_proper_prepare. + done. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv; solve_proper. + Qed. + + Program Definition _THROW : excO -n> laterO IT -n> IT := + λne e v, + Vis (E:=Eff) (subEff_opid (inr (inr (inl ())))) (subEff_ins (F:=exceptE) (op:=(inr(inr(inl ())))) (e,v)) (λne x, Empty_setO_rec _ ((subEff_outs (F:=exceptE) (op:=(inr(inr(inl ())))))^-1 x)). + Next Obligation. + solve_proper_prepare. + destruct ((subEff_outs ^-1) x). + Qed. + Solve All Obligations with solve_proper. + + Program Definition THROW : excO -n> IT -n> IT := + λne e x, get_val (λne res, _THROW e (Next res)) x. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. + Proof. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + + End constructors. + + Section weakestpre. + + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {subR : subReifier reify_exc rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context {SubOfe0 : SubOfe unitO R}. + Context {SubOfe1 : SubOfe natO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!invGS Σ, !stateG rs R Σ}. + Notation iProp := (iProp Σ). + + Lemma wp_reg (σ : stateF ♯ IT) (err : excO) (h : laterO IT -n> laterO IT) (k : IT -n> IT) {Hk : IT_hom k} b β s Φ : + b ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate ((err, h, laterO_map k) :: σ) -∗ WP@{rs} β @ s {{ β, Φ β }}) -∗ + WP@{rs} k (_REG err h b) @ s {{ Φ }}. + Proof. + iIntros (Hβ) "Hσ Ha". + unfold _REG. simpl. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep with "Hσ"). + - simpl. + rewrite /ccompose /compose /=. + repeat f_equiv. + apply cons_equiv; last done. + apply pair_equiv. + split; first done. + trans (laterO_map k : laterO IT -n> laterO IT); last reflexivity. + intro. simpl. f_equiv. apply ofe_iso_21. + - done. + - iAssumption. + Qed. + + Lemma wp_pop (σ σ': stateF ♯ IT) (err : excO) h k (k' : IT -n> IT) {Hk' : IT_hom k'} β Φ : + σ = (err,h,k)::σ' → + k (later_map k' $ Next $ Ret ()) ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ' -∗ WP@{rs} β {{ β, Φ β }}) -∗ + WP@{rs} k' (_POP err) {{ Φ }}. + Proof. + iIntros (-> Hβ) "Hσ Ha". + unfold _POP. + simpl. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep with "Hσ"). + - simpl. + destruct (eq_dec err err); last done. + reflexivity. + - exact Hβ. + - done. + Qed. + + Lemma wp_catch_v σ (v : IT) Φ err h (k : IT -n> IT) {Hk : IT_hom k} `{!AsVal v} β : + k v ≡ β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β {{ Φ }}) -∗ + WP@{rs} k (CATCH err h v) {{ Φ }}. + Proof. + iIntros (Hβ) "Hσ Ha". + simpl. + iApply (wp_reg _ _ _ k with "Hσ"); first done. + iIntros "!> Hcr Hσ". + simpl. + rewrite get_val_ITV /=. + iApply (wp_pop with "Hσ"). + - reflexivity. + - simpl. unfold later_map. simpl. rewrite get_val_ret. simpl. rewrite Hβ. reflexivity. + - iAssumption. + Qed. + + Global Instance throw_hom {err : exc} : IT_hom (THROW err : IT -n> IT). + Proof. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite hom_tick. + - rewrite hom_vis. do 3 f_equiv. intro. simpl. done. + - by rewrite hom_err. + Qed. + + + Definition wp_throw (σ pre post : stateF ♯ IT) (err : excO) (h k : laterO IT -n> laterO IT) (k' : IT -n> IT) {Hk : IT_hom k'} (v : IT) `{!AsVal v} β Φ : + (Forall (λ '(err',_,_), err <> err') pre) → + k (h (Next v)) ≡ Next β → + σ = pre ++ (err,h,k) :: post → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate post -∗ WP@{rs} β {{ β, Φ β }}) -∗ + WP@{rs} k' (THROW err v) {{ Φ }}. + Proof. + iIntros (Hpre Hβ Hsplit) "Hσ Ha". + simpl. + rewrite get_val_ITV. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep with "Hσ"). + - simpl. + change (_cut_when (aux err) σ) with (cut_when (aux err) σ). + rewrite (cut_when_first_occ _ σ _ _ _ Hsplit). + + reflexivity. + + simpl. destruct (eq_dec err err); done. + + eapply Forall_impl; first by apply Hpre. + intros x Hx. + simpl. + destruct x as [[err' _] _] . simpl in *. + destruct (eq_dec err err'); done. + - exact Hβ. + - iAssumption. + Qed. + + Lemma wp_catch_throw σ (v : IT) `{!AsVal v} (k k': IT -n> IT) {Hk : IT_hom k} {Hk' : IT_hom k'} Φ err (h : laterO IT -n> laterO IT) β : + h (Next v) ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k' β {{ Φ }}) -∗ + WP@{rs} k' (CATCH err h (k (THROW err v))) {{ Φ }}. + Proof. + iIntros (Hβ) "Hσ Ha". + simpl. + iApply (wp_reg _ _ _ k' with "Hσ"); first done. + iIntros "!> Hcr Hσ". + simpl. + assert (H : ∀ x y, (get_val x (k y)) = ((get_val x) ∘ k) y). + { intros. reflexivity. } + rewrite H. + iApply (wp_throw _ _ _ _ _ _ ((get_val _) ◎ k) with "Hσ"). + - by apply Forall_nil. + - trans (laterO_map k' (h (Next v))); first reflexivity. + rewrite Hβ /= /later_map /=. reflexivity. + - simpl. reflexivity. + - iAssumption. + Qed. + + End weakestpre. + +End Exc. From 8a1a170c4047ff1157dec99e9c7951de78e00bed Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Tue, 25 Jun 2024 16:53:26 +0200 Subject: [PATCH 02/16] Added files to _CoqProject --- _CoqProject | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/_CoqProject b/_CoqProject index 02dc8bc..99cf0a8 100644 --- a/_CoqProject +++ b/_CoqProject @@ -31,6 +31,7 @@ theories/program_logic.v theories/effects/store.v theories/effects/callcc.v theories/effects/io_tape.v +theories/effects/exceptions.v theories/lib/pairs.v theories/lib/while.v @@ -51,6 +52,11 @@ theories/examples/input_lang/interp.v theories/examples/input_lang/logpred.v theories/examples/input_lang/logrel.v +theories/examples/except_lang/lang.v +theories/examples/except_lang/interp.v +theories/examples/except_lang/logpred.v +theories/examples/except_lang/logrel.v + theories/examples/affine_lang/lang.v theories/examples/affine_lang/logrel1.v theories/examples/affine_lang/logrel2.v From 6eae58bd981064f52ded7c352dc4e7b87c4a284b Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 27 Jun 2024 15:57:41 +0200 Subject: [PATCH 03/16] Start of except_lang --- theories/examples/except_lang/interp.v | 1301 ++++++++++++++++++++++++ theories/examples/except_lang/lang.v | 594 +++++++++++ 2 files changed, 1895 insertions(+) create mode 100644 theories/examples/except_lang/interp.v create mode 100644 theories/examples/except_lang/lang.v diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v new file mode 100644 index 0000000..0789c17 --- /dev/null +++ b/theories/examples/except_lang/interp.v @@ -0,0 +1,1301 @@ +From gitrees Require Import gitree lang_generic. +From iris.algebra Require Import list. +From gitrees.effects Require Export exceptions. +From gitrees.examples.except_lang Require Import lang. + +Require Import Binding.Lib Binding.Set. + + +Module interp (Errors : ExcSig). + + Module _LANG := Lang Errors. + Import _LANG. + Import _Exc. + + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {subE : subReifier reify_exc rs}. + Context {R} `{CR : !Cofe R}. + Context `{!SubOfe natO R}. + Context `{!SubOfe unitO R}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + + Global Instance denot_cont_ne (κ : IT -n> IT) : + NonExpansive (λ x : IT, Tau (laterO_map κ (Next x))). + Proof. + solve_proper. + Qed. + + (** Interpreting individual operators *) + + Program Definition interp_natop {A} (op : nat_op) (t1 t2 : A -n> IT) : A -n> IT := + λne env, NATOP (do_natop op) (t1 env) (t2 env). + Solve All Obligations with solve_proper_please. + + Global Instance interp_natop_ne A op : NonExpansive2 (@interp_natop A op). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_natop. + + Opaque laterO_map. + Program Definition interp_rec_pre {S : Set} (body : interp_scope (inc (inc S)) -n> IT) + : laterO (interp_scope S -n> IT) -n> interp_scope S -n> IT := + λne self env, Fun $ laterO_map (λne (self : interp_scope S -n> IT) (a : IT), + body (extend_scope (extend_scope env (self env)) a)) self. + Next Obligation. + intros. + solve_proper_prepare. + f_equiv; intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + f_equiv; intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + do 3 f_equiv; intros ??; simpl; f_equiv; + intros [| [| y']]; simpl; solve_proper. + Qed. + Next Obligation. + intros. + solve_proper_prepare. + by do 2 f_equiv. + Qed. + + Program Definition interp_rec {S : Set} + (body : interp_scope (inc (inc S)) -n> IT) : + interp_scope S -n> IT := + mmuu (interp_rec_pre body). + + Program Definition ir_unf {S : Set} + (body : interp_scope (inc (inc S)) -n> IT) env : IT -n> IT := + λne a, body (extend_scope + (extend_scope env (interp_rec body env)) + a). + Next Obligation. + intros. + solve_proper_prepare. + f_equiv. intros [| [| y']]; simpl; solve_proper. + Qed. + + Lemma interp_rec_unfold {S : Set} (body : interp_scope (inc (inc S)) -n> IT) env : + interp_rec body env ≡ Fun $ Next $ ir_unf body env. + Proof. + trans (interp_rec_pre body (Next (interp_rec body)) env). + { f_equiv. rewrite /interp_rec. apply mmuu_unfold. } + simpl. rewrite laterO_map_Next. repeat f_equiv. + simpl. unfold ir_unf. intro. simpl. reflexivity. + Qed. + + Program Definition interp_app {A} (t1 t2 : A -n> IT) : A -n> IT := + λne env, APP' (t1 env) (t2 env). + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + Global Instance interp_app_ne A : NonExpansive2 (@interp_app A). + Proof. solve_proper. Qed. + Typeclasses Opaque interp_app. + + Program Definition interp_if {A} (t0 t1 t2 : A -n> IT) : A -n> IT := + λne env, IF (t0 env) (t1 env) (t2 env). + Solve All Obligations with first [ solve_proper | solve_proper_please ]. + Global Instance interp_if_ne A n : + Proper ((dist n) ==> (dist n) ==> (dist n) ==> (dist n)) (@interp_if A). + Proof. solve_proper. Qed. + + Program Definition interp_nat (n : nat) {A} : A -n> IT := + λne env, Ret n. + + Program Definition interp_throw {A} (err : exc) (e : A -n> IT) : A -n> IT := + λne env, THROW err (e env). + Solve All Obligations with solve_proper. + + Global Instance interp_throw_ne A exc e : NonExpansive (@interp_throw A exc e). + Proof. solve_proper. Qed. + + Program Definition interp_catch {A} (err : exc) (exp : (interp_scope A) -n> IT) (h : (@interp_scope F R _ (inc A)) -n> IT) : interp_scope A -n> IT := + λne env, CATCH err (λne (v : laterO IT), laterO_map (λne x, h (extend_scope env x) ) v) (exp env). + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + intro a. + simpl. + destruct a; done. + Qed. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv; last done. + intros a. simpl. + repeat f_equiv. + intros a2. simpl. + repeat f_equiv. + intros a3. simpl. + destruct a3; done. + Qed. + + Program Definition interp_applk {A} + (K : A -n> (IT -n> IT)) + (q : A -n> IT) + : A -n> (IT -n> IT) := + λne env t, interp_app (λne env, K env t) q env. + Solve All Obligations with solve_proper. + + Program Definition interp_apprk {A} + (q : A -n> IT) + (K : A -n> (IT -n> IT)) + : A -n> (IT -n> IT) := + λne env t, interp_app q (λne env, K env t) env. + Solve All Obligations with solve_proper. + + Program Definition interp_natoprk {A} (op : nat_op) + (q : A -n> IT) + (K : A -n> (IT -n> IT)) : A -n> (IT -n> IT) := + λne env t, interp_natop op q (λne env, K env t) env. + Solve All Obligations with solve_proper. + + Program Definition interp_natoplk {A} (op : nat_op) + (K : A -n> (IT -n> IT)) + (q : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_natop op (λne env, K env t) q env. + Solve All Obligations with solve_proper. + + Program Definition interp_ifk {A} (K : A -n> (IT -n> IT)) (q : A -n> IT) + (p : A -n> IT) : A -n> (IT -n> IT) := + λne env t, interp_if (λne env, K env t) q p env. + Solve All Obligations with solve_proper. + + Program Definition interp_throwk {A} (err : exc) (K : A -n> (IT -n> IT)) : + A -n> (IT -n> IT) := + λne env t, interp_throw err (λne env, K env t) env. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. + Proof. + solve_proper_prepare. + repeat f_equiv. + solve_proper. + Qed. + Next Obligation. Proof. solve_proper. Qed. + + Program Definition interp_catchk {A} (err : exc) (K : interp_scope A -n> (IT -n> IT)) (h : interp_scope (inc A) -n> IT) : + (interp_scope A) -n> (IT -n> IT) := + λne env t, interp_catch err (λne env, K env t) h env. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. Proof. solve_proper. Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv; last done. + intros a. simpl. + repeat f_equiv. + intros a2. simpl. + repeat f_equiv. + intros a3. simpl. + destruct a3; done. + Qed. + + (** Interpretation for all the syntactic categories: values, expressions, contexts **) + Fixpoint interp_val {S} (v : val S) : interp_scope S -n> IT := + match v with + | LitV n => interp_nat n + | RecV e => interp_rec (interp_expr e) + end + with interp_expr {S} (e : expr S) : interp_scope S -n> IT := + match e with + | Val v => interp_val v + | Var x => interp_var x + | App e1 e2 => interp_app (interp_expr e1) (interp_expr e2) + | NatOp op e1 e2 => interp_natop op (interp_expr e1) (interp_expr e2) + | If e e1 e2 => interp_if (interp_expr e) (interp_expr e1) (interp_expr e2) + | Throw err v => interp_throw err (interp_expr v) + | Catch err b h => interp_catch err (interp_expr b) (interp_expr h) + end. + + Global Instance interp_val_asval {S} {v : val S} {env} : AsVal (interp_val v env). + Proof. + unfold AsVal. + destruct v. + - simpl. exists (RetV n). done. + - simpl. unfold interp_rec. + exists (FunV (Next (ir_unf (interp_expr e) env))). + simpl. + by rewrite interp_rec_unfold. + Qed. + + Program Fixpoint split_cont {S} (K : cont S) : interp_scope S → ((IT -n> IT) * (listO (excO * (laterO IT -n> laterO IT) * (laterO IT -n> laterO IT) )))%type := + λ env, + match K with + | END => (idfun, []) + | IfK e1 e2 K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, IF t + (interp_expr e1 env) + (interp_expr e2 env)), lst) + | AppLK v K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, t ⊙ (interp_val v env)), lst) + | AppRK e K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, (λne v, (interp_expr e env) ⊙ v) t), lst) + | NatOpRK op e K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, NATOP (do_natop op) (interp_expr e env) t), lst) + | NatOpLK op v K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, NATOP (do_natop op) t (interp_val v env)), lst) + + | ThrowK err K' => let (f, lst) := split_cont K' env in + (f ◎ (λne t, THROW err t), lst) + | CatchK err h K' => let (f, lst) := split_cont K' env in + (get_val (λne t, get_val (λne _, t) (_POP err)), (err, + laterO_map + (λne x, (interp_expr h) + (extend_scope env x) + ), laterO_map f) + ::lst) + end. + Solve All Obligations with try solve_proper. + Next Obligation. + solve_proper_please. + Qed. + Next Obligation. + Proof. + solve_proper_prepare. + f_equiv. + intros []; + done. + Qed. + + Global Instance split_cont_ne {S} {K : cont S} : NonExpansive (split_cont K). + Proof. + induction K; try done; intros n x y H; simpl; + assert (Hs : split_cont K x ≡{n}≡ split_cont K y); + try ( f_equiv; done ); + destruct (split_cont K x) as [f t]; + destruct (split_cont K y) as [f' t']; + rewrite pair_dist in Hs; + destruct Hs as [Hf Ht]; f_equiv; try done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; last done. + intro. simpl. repeat f_equiv. done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; done. + - intro. simpl. repeat f_equiv; done. + - repeat f_equiv; try done. + intro x0. simpl. f_equiv. intro x1. simpl. destruct x1; first done. + f_equiv. done. + Qed. + + Theorem split_cont_left_hom {S} {K : cont S} {env : interp_scope S} + : IT_hom (split_cont K env).1 . + Proof. + induction K. + - simple refine (IT_HOM _ _ _ _ _); + intros; + simpl; + repeat f_equiv. + change (λne x : IT, x) with (@idfun IT). + intros x. + rewrite /ccompose /compose /=. + apply laterO_map_id. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + simple refine (IT_HOM _ _ _ _ _). + + intros. simpl. + rewrite IF_Tick. + apply IHK. + + intros. simpl. + rewrite IF_Vis hom_vis. + f_equiv. + rewrite !/ccompose !/compose /=. + intros x. simpl. + rewrite -laterO_map_compose. + repeat f_equiv. + intro. + simpl. + done. + + intros e. simpl. + rewrite IF_Err. + apply IHK. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + + rewrite APP'_Tick_l. + apply IHK. + + rewrite APP'_Vis_l hom_vis. + f_equiv. + rewrite !/ccompose !/compose /=. + intro. simpl. + rewrite -laterO_map_compose. + f_equiv. + intro. done. + + rewrite APP'_Err_l. apply IHK. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + rewrite APP'_Tick_r. apply hom_tick. + + rewrite APP'_Vis_r hom_vis. + f_equiv. + intro. simpl. + rewrite laterO_map_compose. + f_equiv. + intro. done. + + rewrite APP'_Err_r. apply hom_err. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + rewrite NATOP_ITV_Tick_l. + apply hom_tick. + + rewrite NATOP_ITV_Vis_l hom_vis. + f_equiv. + intro. simpl. + rewrite -laterO_map_compose. + do 2 f_equiv. intro. simpl. done. + + rewrite NATOP_Err_l. + apply hom_err. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + by rewrite -hom_tick NATOP_Tick_r. + + rewrite NATOP_Vis_r hom_vis. + f_equiv. + intro. simpl. + rewrite laterO_map_compose. + f_equiv. intro. done. + + rewrite NATOP_Err_r. + apply hom_err. + - simpl. + specialize (IHK env). + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + rewrite /compose. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + do 2 rewrite hom_tick. + done. + + do 2 rewrite hom_vis. + f_equiv. + intro. simpl. + rewrite -laterO_map_compose. + f_equiv. + intros []. + done. + + by do 2 rewrite hom_err. + - simpl. + destruct (split_cont K env) as [f t] eqn:Heq. + simpl in *. + refine (IT_HOM _ _ _ _ _); intros; simpl. + + by rewrite -hom_tick. + + rewrite hom_vis. + do 3 f_equiv. intro. simpl. done. + + by rewrite hom_err. + Qed. + + Theorem split_cont_left_hom' {S} {K : cont S} {env} f t : split_cont K env = (f,t) → IT_hom f. + Proof. + intros H. + replace f with (split_cont K env).1. + - apply split_cont_left_hom. + - rewrite H. done. + Qed. + + Program Definition interp_config {S} (cfg : @config S) : interp_scope S -n> (IT * stateF ♯ IT)%type := + match cfg with + | Cexpr e => λne env, (interp_expr e env, []) + | Ceval e K => λne env, let (f,t) := split_cont K env in + (f (interp_expr e env), t) + | Ccont K v => λne env, let (f,t) := split_cont K env in + (f (interp_val v env), t) + | Cret v => λne env, (interp_val v env, []) + end. + Solve All Obligations with try solve_proper. + Next Obligation. + Proof. + solve_proper_prepare. + assert (Hs : split_cont K x ≡{n}≡ split_cont K y). { f_equiv. done. } + destruct (split_cont K x) as [f t]. + destruct (split_cont K y) as [f' t']. + rewrite pair_dist in Hs. + destruct Hs as [Hf Ht]. + repeat f_equiv; done. + Qed. + Next Obligation. + Proof. + solve_proper_prepare. + assert (Hs : split_cont K x ≡{n}≡ split_cont K y). { f_equiv. done. } + destruct (split_cont K x) as [f t]. + destruct (split_cont K y) as [f' t']. + rewrite pair_dist in Hs. + destruct Hs as [Hf Ht]. + repeat f_equiv; done. + Qed. + + + Global Instance ArrEquiv {A B : Set} : Equiv (A [→] B) := + fun f g => ∀ x, f x = g x. + + Global Instance ArrDist {A B : Set} `{Dist B} : Dist (A [→] B) := + fun n => fun f g => ∀ x, f x ≡{n}≡ g x. + + Global Instance ren_scope_proper {S S'} : + Proper ((≡) ==> (≡) ==> (≡)) (@ren_scope F _ CR S S'). + Proof. + intros D D' HE s1 s2 Hs. + intros x; simpl. + f_equiv. + - apply Hs. + - apply HE. + Qed. + + Lemma interp_expr_ren {S S'} env + (δ : S [→] S') (e : expr S) : + interp_expr (fmap δ e) env ≡ interp_expr e (ren_scope δ env) + with interp_val_ren {S S'} env + (δ : S [→] S') (e : val S) : + interp_val (fmap δ e) env ≡ interp_val e (ren_scope δ env). + (** with interp_cont_ren {S S'} env + (δ : S [→] S') (e : cont S) : + interp_cont (fmap δ e) env ≡ interp_cont e (ren_scope δ env). **) + Proof. + - destruct e; simpl. + + by apply interp_val_ren. + + reflexivity. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv; by apply interp_expr_ren. + + repeat f_equiv. + * intros []. simpl. do 2 rewrite laterO_map_Next. + f_equiv. simpl. + rewrite interp_expr_ren. + f_equiv. + intros []; by simpl. + * apply interp_expr_ren. + - destruct e; simpl. + + reflexivity. + + clear -interp_expr_ren. + apply bi.siProp.internal_eq_soundness. + iLöb as "IH". + rewrite {2}interp_rec_unfold. + rewrite {2}(interp_rec_unfold (interp_expr e)). + do 1 iApply f_equivI. iNext. + iApply internal_eq_pointwise. + rewrite /ir_unf. iIntros (x). simpl. + rewrite interp_expr_ren. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (y'). + destruct y' as [| [| y]]; simpl; first done. + * by iRewrite - "IH". + * done. + (* - destruct e; simpl; intros ?; simpl. + + reflexivity. + + repeat f_equiv; [by apply interp_cont_ren | by apply interp_expr_ren | by apply interp_expr_ren]. + + repeat f_equiv; [by apply interp_cont_ren | by apply interp_val_ren]. + + repeat f_equiv; [by apply interp_expr_ren | by apply interp_cont_ren]. + + repeat f_equiv; [by apply interp_expr_ren | by apply interp_cont_ren]. + + repeat f_equiv; [by apply interp_cont_ren | by apply interp_val_ren]. + + repeat f_equiv. by apply interp_cont_ren. + + repeat f_equiv; last done. + intro. + simpl. + destruct x0. + do 2 rewrite laterO_map_Next. + f_equiv. + simpl. + rewrite interp_expr_ren. + f_equiv. + intro. + destruct x0; done. *) + Qed. +(* + Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : cont S): + interp_expr (fill K e) env ≡ (interp_cont K) env ((interp_expr e) env). + Proof. + revert env. + induction K; simpl; intros env; first reflexivity; try (by rewrite IHK). + - repeat f_equiv. + by rewrite IHK. + - repeat f_equiv. + by rewrite IHK. + - repeat f_equiv. + by rewrite IHK. + Qed. +*) + Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') + : interp_scope S := λne x, interp_expr (δ x) env. + + Global Instance SubEquiv {A B : Set} : Equiv (A [⇒] B) := fun f g => ∀ x, f x = g x. + + Global Instance sub_scope_proper {S S'} : + Proper ((≡) ==> (≡) ==> (≡)) (@sub_scope S S'). + Proof. + intros D D' HE s1 s2 Hs. + intros x; simpl. + f_equiv. + - f_equiv. + apply HE. + - apply Hs. + Qed. + + Lemma interp_expr_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_expr (bind δ e) env ≡ interp_expr e (sub_scope δ env) + with interp_val_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env). +(* with interp_cont_subst {S S'} (env : interp_scope S') + (δ : S [⇒] S') e : + interp_cont (bind δ e) env ≡ interp_cont e (sub_scope δ env). *) + Proof. + - destruct e; simpl. + + by apply interp_val_subst. + + term_simpl. + reflexivity. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; by apply interp_expr_subst. + + repeat f_equiv; last done. + intros []. + do 2 rewrite laterO_map_Next. + f_equiv. + simpl. + rewrite interp_expr_subst. + f_equiv. + intros []; simpl. + * done. + * rewrite interp_expr_ren. + f_equiv. + intro. + simpl. + done. + + - destruct e; simpl. + + reflexivity. + + clear -interp_expr_subst. + apply bi.siProp.internal_eq_soundness. + iLöb as "IH". + rewrite {2}interp_rec_unfold. + rewrite {2}(interp_rec_unfold (interp_expr e)). + do 1 iApply f_equivI. iNext. + iApply internal_eq_pointwise. + rewrite /ir_unf. iIntros (x). simpl. + rewrite interp_expr_subst. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (y'). + destruct y' as [| [| y]]; simpl; first done. + * by iRewrite - "IH". + * do 2 rewrite interp_expr_ren. + iApply f_equivI. + iApply internal_eq_pointwise. + iIntros (z). + done. + (* - destruct e; simpl; intros ?; simpl. + + reflexivity. + + repeat f_equiv; [by apply interp_cont_subst | by apply interp_expr_subst | by apply interp_expr_subst]. + + repeat f_equiv; [by apply interp_cont_subst | by apply interp_val_subst]. + + repeat f_equiv; [by apply interp_expr_subst | by apply interp_cont_subst]. + + repeat f_equiv; [by apply interp_expr_subst | by apply interp_cont_subst]. + + repeat f_equiv; [by apply interp_cont_subst | by apply interp_val_subst]. + + repeat f_equiv. + by apply interp_cont_subst. + + repeat f_equiv; last done. + intros []. simpl. + do 2 rewrite laterO_map_Next. + f_equiv. simpl. + rewrite interp_expr_subst. + f_equiv. + intros []; simpl. + * done. + * rewrite interp_expr_ren. + f_equiv. + by intro. *) + Qed. + + + Theorem soundness {S} : ∀ c c' e e' σr σ σ' (env : interp_scope S), + interp_config c env = (e, σ) → + interp_config c' env = (e', σ') → + c ===> c' → + ∃ n, + ssteps (gReifiers_sReifier rs) + e (gState_recomp σr (sR_state σ)) + e' (gState_recomp σr (sR_state σ')) n. + Proof. + intros. + revert H H0. + induction H1; intros H0 H1. + - simpl in H0, H1. + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + rewrite H0 in H1. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + destruct (split_cont k env) as [f t]. + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + destruct (split_cont k env) as [f t]. + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + destruct (split_cont k env) as [f t]. + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + destruct (split_cont k env) as [f t] eqn:Heq. + assert (IT_hom f). + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 1. + econstructor. + + rewrite hom_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose (@subReifier_reify _ _ _ _ _ _ _ (inl ()) ?[x] (Next _) ?[k] t ?[σ'] σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ ?σ2)) , ?k' ◎ _) ≡ _ => instantiate (x := x'); + instantiate (k := k') + + end. + Unshelve. + 6 : { simpl. done. }. + 1 : { simpl in Hry|-*. + erewrite <-Hry. + repeat f_equiv; first by solve_proper. + intro. simpl. done. + } + + constructor. + * repeat f_equiv. + intro. simpl. + f_equiv. + f_equiv. (* Reflexivity doesn't work here, really funny, show Sergei *) + intro. + simpl. + done. + * simpl. + do 5 f_equiv; + f_equiv; + intro; + simpl; + done. + - simpl in H0, H1. + destruct (split_cont k env) as [f t] eqn:Heq. + assert (IT_hom f). + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + by constructor. + - simpl in H0, H1. + destruct (split_cont k env) as [f t] eqn:Heq. + assert (IT_hom f). + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + by constructor. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 1. + econstructor; last (econstructor; reflexivity). + apply sstep_tick; last done. + rewrite -hom_tick. + f_equiv. + pose (interp_rec_unfold (interp_expr f) env) as H. + assert (∀ x y z : IT, x ≡ y → x ⊙ z ≡ y ⊙ z) as APP'_equiv. + { intros x y z Hxy. + Transparent APP APP'. + simpl. + Opaque APP APP'. + repeat f_equiv. + intro. simpl. + f_equiv. + done. + } + rewrite (APP'_equiv _ _ _ H) APP_APP'_ITV APP_Fun Tick_eq /=. + do 2 rewrite interp_expr_subst. + do 3 f_equiv. + intros []. + + simpl. rewrite -interp_val_subst. + do 2 f_equiv. + pose @subst_shift_id as Hsbs. + unfold subst in Hsbs. + rewrite Hsbs. + done. + + destruct i; simpl. + * done. + * done. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; last done. + f_equiv. + destruct n. + + rewrite IF_False; last lia. + done. + + rewrite IF_True; last lia. + done. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; last done. + f_equiv. + destruct v1, v2. + 2, 3, 4 : contradict H; done. + simpl in H. + injection H as <-. + simpl. + apply NATOP_Ret. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 1. + econstructor; last (constructor; done). + rewrite get_val_ITV /= get_val_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inl ())) ?[x] (Next _) ?[k] ?[σ] ?[σ'] σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ (_ ?σ2) _)) , ?k1 ◎ (?k2 ◎ _)) ≡ _ => instantiate (x := x'); + instantiate (k := k1 ◎ k2); + instantiate (σ := σ2) + + end. + Unshelve. + 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. }. + 1 : { simpl in Hry|-*. + match goal with + | [Hry : _ ≡ ?r |- _ ] => transitivity r + end. + 2 : { repeat f_equiv. + Transparent laterO_map. + simpl. + Opaque laterO_map. + f_equiv. + apply get_val_ret. + } + + rewrite -Hry. + + repeat f_equiv; first by solve_proper. + intro. simpl. done. + } + - (** TODO : THROW **) + + + + + + + + + + + + + + + + + + + + + + (** ** Interpretation of evaluation contexts induces homomorphism *) + + #[local] Instance interp_cont_hom_emp {S} env : + IT_hom (interp_cont (EmptyIK : cont S) env). + Proof. + simple refine (IT_HOM _ _ _ _ _); intros; auto. + simpl. fold (@idfun IT). f_equiv. intro. simpl. + by rewrite laterO_map_id. + Qed. + + #[local] Instance interp_cont_hom_if {S} + (K : cont S) (e1 e2 : expr S) env : + IT_hom (interp_cont K env) -> + IT_hom (interp_cont (IfIK K e1 e2) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite -IF_Tick. do 3 f_equiv. apply hom_tick. + - assert ((interp_cont K env (Vis op i ko)) ≡ + (Vis op i (laterO_map (λne y, interp_cont K env y) ◎ ko))). + { by rewrite hom_vis. } + trans (IF (Vis op i (laterO_map (λne y : IT, interp_cont K env y) ◎ ko)) + (interp_expr e1 env) (interp_expr e2 env)). + { do 3 f_equiv. by rewrite hom_vis. } + rewrite IF_Vis. f_equiv. simpl. + intro. simpl. by rewrite -laterO_map_compose. + - trans (IF (Err e) (interp_expr e1 env) (interp_expr e2 env)). + { repeat f_equiv. apply hom_err. } + apply IF_Err. + Qed. + + #[local] Instance interp_cont_hom_appr {S} (K : cont S) + (e : expr S) env : + IT_hom (interp_cont K env) -> + IT_hom (interp_cont (AppRIK e K) env). + Proof. + intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. f_equiv. intro x. simpl. + by rewrite laterO_map_compose. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_cont_hom_appl {S} (K : cont S) + (v : val S) (env : interp_scope S) : + IT_hom (interp_cont K env) -> + IT_hom (interp_cont (AppLIK K v) env). + Proof. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite -APP'_Tick_l. do 2 f_equiv. apply hom_tick. + - trans (APP' (Vis op i (laterO_map (interp_cont K env) ◎ ko)) + (interp_val v env)). + + do 2f_equiv. rewrite hom_vis. do 3 f_equiv. by intro. + + rewrite APP'_Vis_l. f_equiv. intro x. simpl. + by rewrite -laterO_map_compose. + - trans (APP' (Err e) (interp_val v env)). + { do 2f_equiv. apply hom_err. } + apply APP'_Err_l, interp_val_asval. + Qed. + + #[local] Instance interp_cont_hom_natopr {S} (K : cont S) + (e : expr S) op env : + IT_hom (interp_cont K env) -> + IT_hom (interp_cont (NatOpRIK op e K) env). + Proof. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by rewrite !hom_tick. + - rewrite !hom_vis. f_equiv. intro x. simpl. + by rewrite laterO_map_compose. + - by rewrite !hom_err. + Qed. + + #[local] Instance interp_cont_hom_natopl {S} (K : cont S) + (v : val S) op (env : interp_scope S) : + IT_hom (interp_cont K env) -> + IT_hom (interp_cont (NatOpLIK op K v) env). + Proof. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite -NATOP_ITV_Tick_l. do 2 f_equiv. apply hom_tick. + - trans (NATOP (do_natop op) + (Vis op0 i (laterO_map (interp_cont K env) ◎ ko)) + (interp_val v env)). + { do 2 f_equiv. rewrite hom_vis. f_equiv. by intro. } + rewrite NATOP_ITV_Vis_l. f_equiv. intro x. simpl. + by rewrite -laterO_map_compose. + - trans (NATOP (do_natop op) (Err e) (interp_val v env)). + + do 2 f_equiv. apply hom_err. + + by apply NATOP_Err_l, interp_val_asval. + Qed. + + #[local] Instance interp_cont_hom_throw {S} (K : cont S) err (env : interp_scope S) : + IT_hom (interp_cont K env) -> + IT_hom (interp_cont (ThrowIK err K) env). + Proof. + Opaque THROW. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - by do 2 rewrite hom_tick. + - do 2 rewrite hom_vis. f_equiv. by intro. + - by do 2 rewrite hom_err. + Qed. + + + #[global] Instance interp_cont_hom {S} (IK : cont S) env : + (∃ K, IK = cont_of_cont K) → + IT_hom (interp_cont IK env). + Proof. + intros [K ->]. + induction K; try apply _. + Qed. + + (** ** Finally, preservation of reductions *) + Lemma interp_expr_head_step {S : Set} (env : interp_scope S) (e : expr S) e' n : + head_step e e' (n, 0) → + interp_expr e env ≡ Tick_n n $ interp_expr e' env. + Proof. + inversion 1; cbn-[IF APP' INPUT Tick get_ret2]. + - (* app lemma *) + subst. + erewrite APP_APP'_ITV; last apply _. + trans (APP (Fun (Next (ir_unf (interp_expr e1) env))) (Next $ interp_val v2 env)). + { repeat f_equiv. apply interp_rec_unfold. } + rewrite APP_Fun. simpl. rewrite Tick_eq. do 2 f_equiv. + simplify_eq. + rewrite !interp_expr_subst. + f_equiv. + intros [| [| x]]; simpl; [| reflexivity | reflexivity]. + rewrite interp_val_ren. + f_equiv. + intros ?; simpl; reflexivity. + - (* the natop stuff *) + simplify_eq. + destruct v1,v2; try naive_solver. simpl in *. + rewrite NATOP_Ret. + destruct op; simplify_eq/=; done. + - rewrite IF_True; last lia. + reflexivity. + - rewrite IF_False; last lia. + reflexivity. + Qed. + + Lemma interp_expr_fill_no_reify {S} K (env : interp_scope S) (e e' : expr S) n : + head_step e e' (n, 0) → + interp_expr (fill (cont_of_cont K) e) env + ≡ + Tick_n n $ interp_expr (fill (cont_of_cont K) e') env. + Proof. + intros He. + rewrite !interp_comp. + erewrite <-hom_tick_n. + - apply (interp_expr_head_step env) in He. + rewrite He. + reflexivity. + - apply interp_cont_hom. exists K. done. + Qed. + + Opaque extend_scope. + Opaque Ret. + (** + Lemma interp_expr_fill_yes_reify {S} K env (e e' : expr S) + (σ σ' : stateO) (σr : gState_rest sR_idx rs ♯ IT) n : + head_step e e' (n, 1) → + reify (gReifiers_sReifier rs) + (interp_expr (fill K e) env) (gState_recomp σr (sR_state σ)) + ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). + Proof. + intros Hst. + trans (reify (gReifiers_sReifier rs) (interp_cont K env (interp_expr e env)) + (gState_recomp σr (sR_state σ))). + { f_equiv. by rewrite interp_comp. } + inversion Hst; simplify_eq; cbn-[gState_recomp]. + - trans (reify (gReifiers_sReifier rs) (INPUT (interp_cont K env ◎ Ret)) (gState_recomp σr (sR_state σ))). + { + repeat f_equiv; eauto. + rewrite hom_INPUT. + do 2 f_equiv. by intro. + } + rewrite reify_vis_eq_ctx_indep //; first last. + { + epose proof (@subReifier_reify sz NotCtxDep reify_io rs _ IT _ (inl ()) () _ σ σ' σr) as H. + simpl in H. + simpl. + erewrite <-H; last first. + - rewrite H4. reflexivity. + - f_equiv; + solve_proper. + } + repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. + rewrite interp_comp. + rewrite ofe_iso_21. + simpl. + reflexivity. + - trans (reify (gReifiers_sReifier rs) (interp_cont K env (OUTPUT n0)) (gState_recomp σr (sR_state σ))). + { + do 3 f_equiv; eauto. + rewrite get_ret_ret//. + } + trans (reify (gReifiers_sReifier rs) (OUTPUT_ n0 (interp_cont K env (Ret 0))) (gState_recomp σr (sR_state σ))). + { + do 2 f_equiv; eauto. + by rewrite hom_OUTPUT_. + } + rewrite reify_vis_eq_ctx_indep //; last first. + { + epose proof (@subReifier_reify sz _ reify_io rs _ IT _ (inr (inl ())) n0 _ σ (update_output n0 σ) σr) as H. + simpl in H. + simpl. + erewrite <-H; last reflexivity. + f_equiv. + intros ???. by rewrite /prod_map H0. + } + repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. + rewrite interp_comp. + reflexivity. + Qed. + *) + + Example test1 err : expr ∅ := + (try + (#4) + #5 + catch err => #1 + )%syn. + + Example test2 err : expr ∅ := + (try + #9 + catch err => #1 + )%syn. + + Example uu err σr : ∃ n m σ t, + ssteps (gReifiers_sReifier rs) + (interp_expr (test1 err) (λne (x : leibnizO ∅), match x with end) : IT) + (gState_recomp σr (sR_state σ)) + t + (gState_recomp σr (sR_state σ)) n ∧ + ssteps (gReifiers_sReifier rs) + (interp_expr (test2 err) (λne (x : leibnizO ∅), match x with end) : IT) + (gState_recomp σr (sR_state σ)) + t + (gState_recomp σr (sR_state σ)) m. + Proof. + rewrite /test1 /test2. + simpl. + do 2 eexists. + exists []. + eexists. + split. + - eapply ssteps_many. + + eapply sstep_reify. + { f_equiv. rewrite /ccompose /compose /=. reflexivity. }. + Check reify_vis_eq_ctx_dep. + apply reify_vis_eq_ctx_dep. + + + + Proof. + intros H. + unfold test1 in H. + unfold test2 in H. + simpl in H. + + Compute . + + Lemma soundness {S} (e1 e2 : expr S) (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : + prim_step e1 e2 (n,m) → ∀ σ1, ∃ σ2, + ssteps (gReifiers_sReifier rs) + (interp_expr e1 env) (gState_recomp σr (sR_state σ1)) + (interp_expr e2 env) (gState_recomp σr (sR_state σ2)) n. + Proof. + Opaque gState_decomp gState_recomp. + intros Hstep. + inversion Hstep;simplify_eq/=. + - intros σ1. + eexists. + rewrite !interp_comp. + + + + unshelve eapply (interp_expr_fill_no_reify K) in H2; first apply env. + rewrite H2. + rewrite interp_comp. + eapply ssteps_tick_n. + + inversion H2;subst. + * eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. + rewrite interp_comp. + rewrite hom_INPUT. + change 1 with (Nat.add 1 0). econstructor; last first. + { apply ssteps_zero; reflexivity. } + eapply sstep_reify. + { Transparent INPUT. unfold INPUT. simpl. + f_equiv. reflexivity. } + simpl in H2. + rewrite -H2. + repeat f_equiv; eauto. + rewrite interp_comp hom_INPUT. + eauto. + * eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. + rewrite interp_comp. simpl. + rewrite get_ret_ret. + rewrite hom_OUTPUT_. + change 1 with (Nat.add 1 0). econstructor; last first. + { apply ssteps_zero; reflexivity. } + eapply sstep_reify. + { Transparent OUTPUT_. unfold OUTPUT_. simpl. + f_equiv. reflexivity. } + simpl in H2. + rewrite -H2. + repeat f_equiv; eauto. + Opaque OUTPUT_. + rewrite interp_comp /= get_ret_ret hom_OUTPUT_. + eauto. + Qed. + + + Section Examples. + Context `{!invGS Σ, !stateG rs R Σ}. + + Opaque CATCH. + + Example prog1 (err : exc) (n : nat) : expr ∅ := + (try + if #n then + throw err #5 + else #4 + catch err => ($0) * $0 + )%syn. + + Example wp_prog1 (err : exc) (n : nat) (σ : stateF ♯ IT) Φ : + has_substate σ -∗ + ▷(£1 -∗ has_substate σ -∗ (⌜n = 0⌝ -∗ Φ (RetV 4)) ∗ (⌜n > 0⌝ -∗ Φ (RetV 25))) -∗ + WP@{rs} (interp_expr (prog1 err n) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. + iIntros "Hσ H▷". + simpl. + destruct n. + - rewrite IF_False; last lia. + iApply (wp_catch_v _ _ (Ret 4) _ _ _ idfun with "Hσ"). + + by simpl. + + iIntros "!> H£ Hσ". + iPoseProof ("H▷" with "H£ Hσ") as "[HΦ _]". + iApply wp_val. + iModIntro. + by iApply "HΦ". + - rewrite IF_True; last lia. + iApply (wp_catch_throw _ _ (Ret 5) idfun idfun with "Hσ"). + + simpl. + rewrite laterO_map_Next. + simpl. + rewrite NATOP_Ret. + by simpl. + + simpl. + iIntros "!> H£ Hσ". + iPoseProof ("H▷" with "H£ Hσ") as "[_ HΦ]". + iApply wp_val. + iModIntro. + iApply "HΦ". + iPureIntro. + lia. + Qed. + + Example prog2 (err : exc) : expr ∅ := + (if ( + try + throw err #3 + catch err => ($0) * #4 + ) + then #1 + else #0 + )%syn. + + Example wp_prog2 (err : exc) (σ : stateF ♯ IT) Φ : + has_substate σ -∗ + ▷(£1 -∗ has_substate σ -∗ Φ (RetV 1)) -∗ + WP@{rs} (interp_expr (prog2 err) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. + Proof. + iIntros "Hσ H▷". + simpl. + iApply (wp_catch_throw _ _ (Ret 3) idfun (λne x, IF x (Ret 1) (Ret 0)) with "Hσ"). + - simpl. + rewrite laterO_map_Next /=. + rewrite NATOP_Ret. + by simpl. + - simpl. + iIntros "!>H£ Hσ". + rewrite IF_True; last lia. + iApply wp_val. + iModIntro. + iApply ("H▷" with "H£ Hσ"). + Qed. + + Example prog3 (err : exc) : expr ∅ := + (try + (if ( + throw err #3 + ) + then #1 + else #0) + catch err => ($0) * #4 + )%syn. + + Example wp_prog3 (err : exc) (σ : stateF ♯ IT) Φ : + has_substate σ -∗ + ▷(£1 -∗ has_substate σ -∗ Φ (RetV 12)) -∗ + WP@{rs} (interp_expr (prog3 err) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. + Proof. + iIntros "Hσ H▷". + simpl. + iApply (wp_catch_throw _ _ (Ret 3) (λne x, IF x (Ret 1) (Ret 0)) idfun with "Hσ"). + - by rewrite laterO_map_Next /= NATOP_Ret /=. + - iIntros "!> H£ Hσ". + iApply wp_val. + by iApply ("H▷" with "H£ Hσ"). + Qed. + + Example prog4 (err1 err2 : exc) : expr ∅ := + (try + try + throw err1 #3 + catch err2 => ($0) + $0 + catch err1 => ($0) * $0 + )%syn. + + Example wp_prog4 (err1 err2 : exc) (Herr : err1 <> err2) (σ : stateF ♯ IT) Φ : + has_substate σ -∗ + ▷(£1 -∗ has_substate σ -∗ Φ (RetV 9)) -∗ + WP@{rs} (interp_expr (prog4 err1 err2) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. + Proof. + Opaque _REG. + iIntros "Hσ H▷". + simpl. + iApply (wp_reg _ _ err1 _ idfun with "Hσ"). + { reflexivity. } + iIntros "!> H£ Hσ". + iApply (wp_reg _ _ _ _ (get_val _) with "Hσ"). + { reflexivity. } + iIntros "!> H£' Hσ". + iApply (wp_throw _ _ _ _ _ _ _ (get_val _) with "Hσ"). + 3: change (?a :: ?b :: σ) with ([a] ++ b::σ); reflexivity. + { constructor; first done. constructor. } + { by rewrite laterO_map_Next /= NATOP_Ret /=. } + iIntros "!> H£'' Hσ". + iApply wp_val. + iModIntro. + iApply ("H▷" with "H£ Hσ"). + Qed. + + End Examples. + +End interp. +#[global] Opaque INPUT OUTPUT_. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v new file mode 100644 index 0000000..26293bd --- /dev/null +++ b/theories/examples/except_lang/lang.v @@ -0,0 +1,594 @@ +From gitrees Require Export prelude effects.io_tape effects.exceptions. +Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. + +Module Lang (Errors : ExcSig). + + Module _Exc := Exc Errors. + + Import _Exc. + + Inductive nat_op := Add | Sub | Mult. + + Inductive expr {X : Set} : Type := + (* Values *) + | Val (v : val) : expr + | Var (x : X) : expr + (* Base lambda calculus *) + | App (e₁ : expr) (e₂ : expr) : expr + (* Base types and their operations *) + | NatOp (op : nat_op) (e₁ : expr) (e₂ : expr) : expr + | If (e₁ : expr) (e₂ : expr) (e₃ : expr) : expr + (* The effects *) + | Throw (err : exc) (e : expr) : expr + | Catch (err : exc) (e₁ : expr) (e₂ : @expr (inc X)) : expr + with val {X : Set} := + | LitV (n : nat) : val + | RecV (e : @expr (inc (inc X))) : val + with cont {X : Set} := + | END : cont + | IfK (e₁ : expr) (e₂ : expr) : cont → cont + | AppLK (v : val) : cont → cont + | AppRK (e : expr) : cont → cont + | NatOpLK (op : nat_op) (v : val) : cont → cont + | NatOpRK (op : nat_op) (e : expr) : cont → cont + | ThrowK (err : exc) : cont → cont + | CatchK (err : exc) (h : @expr (inc X)) : cont → cont. + + Arguments val X%bind : clear implicits. + Arguments expr X%bind : clear implicits. + Arguments cont X%bind : clear implicits. + + Local Open Scope bind_scope. + + Fixpoint emap {A B : Set} (f : A [→] B) (e : expr A) : expr B := + match e with + | Val v => Val (vmap f v) + | Var x => Var (f x) + | App e₁ e₂ => App (emap f e₁) (emap f e₂) + | NatOp o e₁ e₂ => NatOp o (emap f e₁) (emap f e₂) + | If e₁ e₂ e₃ => If (emap f e₁) (emap f e₂) (emap f e₃) + | Throw err e => Throw err (emap f e) + | Catch err e₁ e₂ => Catch err (emap f e₁) (@emap (inc A) (inc B) (f ↑) e₂) + end + with vmap {A B : Set} (f : A [→] B) (v : val A) : val B := + match v with + | LitV n => LitV n + | RecV e => RecV (emap ((f ↑) ↑) e) + end + with kmap {A B : Set} (f : A [→] B) (K : cont A) : cont B := + match K with + | END => END + | IfK e₁ e₂ K => IfK (emap f e₁) (emap f e₂) (kmap f K) + | AppLK v K => AppLK (vmap f v) (kmap f K) + | AppRK e K => AppRK (emap f e) (kmap f K) + | NatOpLK op v K => NatOpLK op (vmap f v) (kmap f K) + | NatOpRK op e K => NatOpRK op (emap f e) (kmap f K) + | ThrowK err K => ThrowK err (kmap f K) + | CatchK err h K => CatchK err (emap (f ↑) h) (kmap f K) + end. + +#[export] Instance FMap_expr : FunctorCore expr := @emap. +#[export] Instance FMap_val : FunctorCore val := @vmap. +#[export] Instance FMap_cont : FunctorCore cont := @kmap. + +#[export] Instance SPC_expr : SetPureCore expr := @Var. + +Fixpoint ebind {A B : Set} (f : A [⇒] B) (e : expr A) : expr B := + match e with + | Val v => Val (vbind f v) + | Var x => f x + | App e₁ e₂ => App (ebind f e₁) (ebind f e₂) + | NatOp o e₁ e₂ => NatOp o (ebind f e₁) (ebind f e₂) + | If e₁ e₂ e₃ => If (ebind f e₁) (ebind f e₂) (ebind f e₃) + | Throw err e => Throw err (ebind f e) + | Catch err e₁ e₂ => Catch err (ebind f e₁) (ebind (f ↑) e₂) + end +with vbind {A B : Set} (f : A [⇒] B) (v : val A) : val B := + match v with + | LitV n => LitV n + | RecV e => RecV (ebind ((f ↑) ↑) e) + end +. + +Fixpoint kbind {A B : Set} (f : A [⇒] B) (K : cont A) : cont B := + match K with + | END => END + | IfK e₁ e₂ K => IfK (ebind f e₁) (ebind f e₂) (kbind f K) + | AppLK v K => AppLK (vbind f v) (kbind f K) + | AppRK e K => AppRK (ebind f e) (kbind f K) + | NatOpLK op v K => NatOpLK op (vbind f v) (kbind f K) + | NatOpRK op e K => NatOpRK op (ebind f e) (kbind f K) + | ThrowK err K => ThrowK err (kbind f K) + | CatchK err h K => CatchK err (ebind (f ↑) h) (kbind f K) + end. + +#[export] Instance BindCore_expr : BindCore expr := @ebind. +#[export] Instance BindCore_val : BindCore val := @vbind. +#[export] Instance BindCore_cont : BindCore cont := @kbind. + +#[export] Instance IP_typ : SetPure expr. +Proof. + split; intros; reflexivity. +Qed. + +Fixpoint vmap_id X (δ : X [→] X) (v : val X) : δ ≡ ı → fmap δ v = v +with emap_id X (δ : X [→] X) (e : expr X) : δ ≡ ı → fmap δ e = e +with kmap_id X (δ : X [→] X) (e : cont X) : δ ≡ ı → fmap δ e = e. +Proof. + - auto_map_id. + - auto_map_id. + - auto_map_id. +Qed. + +Fixpoint vmap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (v : val A) : + f ∘ g ≡ h → fmap f (fmap g v) = fmap h v +with emap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (e : expr A) : + f ∘ g ≡ h → fmap f (fmap g e) = fmap h e +with kmap_comp (A B C : Set) (f : B [→] C) (g : A [→] B) h (e : cont A) : + f ∘ g ≡ h → fmap f (fmap g e) = fmap h e. +Proof. + - auto_map_comp. + - auto_map_comp. + - auto_map_comp. +Qed. + +#[export] Instance Functor_val : Functor val. +Proof. + split; [exact vmap_id | exact vmap_comp]. +Qed. +#[export] Instance Functor_expr : Functor expr. +Proof. + split; [exact emap_id | exact emap_comp]. +Qed. +#[export] Instance Functor_cont : Functor cont. +Proof. + split; [exact kmap_id | exact kmap_comp]. +Qed. + +Fixpoint vmap_vbind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (v : val A) : + f ̂ ≡ g → fmap f v = bind g v +with emap_ebind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (e : expr A) : + f ̂ ≡ g → fmap f e = bind g e +with kmap_kbind_pure (A B : Set) (f : A [→] B) (g : A [⇒] B) (e : cont A) : + f ̂ ≡ g → fmap f e = bind g e. +Proof. + - auto_map_bind_pure. + erewrite emap_ebind_pure; [reflexivity |]. + intros [| [| x]]; term_simpl; [reflexivity | reflexivity |]. + rewrite <-(EQ x). + reflexivity. + - auto_map_bind_pure. + - auto_map_bind_pure. +Qed. + +#[export] Instance BindMapPure_val : BindMapPure val. +Proof. + split; intros; now apply vmap_vbind_pure. +Qed. +#[export] Instance BindMapPure_expr : BindMapPure expr. +Proof. + split; intros; now apply emap_ebind_pure. +Qed. +#[export] Instance BindMapPure_cont : BindMapPure cont. +Proof. + split; intros; now apply kmap_kbind_pure. +Qed. + +Fixpoint vmap_vbind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (v : val A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ v) = fmap f₁ (bind g₁ v) +with emap_ebind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (e : expr A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ e) = fmap f₁ (bind g₁ e) +with kmap_kbind_comm (A B₁ B₂ C : Set) (f₁ : B₁ [→] C) (f₂ : A [→] B₂) + (g₁ : A [⇒] B₁) (g₂ : B₂ [⇒] C) (e : cont A) : + g₂ ∘ f₂ ̂ ≡ f₁ ̂ ∘ g₁ → bind g₂ (fmap f₂ e) = fmap f₁ (bind g₁ e). +Proof. + - auto_map_bind_comm. + erewrite emap_ebind_comm; [reflexivity |]. + erewrite lift_comm; [reflexivity |]. + erewrite lift_comm; [reflexivity | assumption]. + - auto_map_bind_comm. + - auto_map_bind_comm. +Qed. + +#[export] Instance BindMapComm_val : BindMapComm val. +Proof. + split; intros; now apply vmap_vbind_comm. +Qed. +#[export] Instance BindMapComm_expr : BindMapComm expr. +Proof. + split; intros; now apply emap_ebind_comm. +Qed. +#[export] Instance BindMapComm_cont : BindMapComm cont. +Proof. + split; intros; now apply kmap_kbind_comm. +Qed. + +Fixpoint vbind_id (A : Set) (f : A [⇒] A) (v : val A) : + f ≡ ı → bind f v = v +with ebind_id (A : Set) (f : A [⇒] A) (e : expr A) : + f ≡ ı → bind f e = e +with kbind_id (A : Set) (f : A [⇒] A) (e : cont A) : + f ≡ ı → bind f e = e. +Proof. + - auto_bind_id. + rewrite ebind_id; [reflexivity |]. + apply lift_id, lift_id; assumption. + - auto_bind_id. + - auto_bind_id. +Qed. + +Fixpoint vbind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (v : val A) : + f ∘ g ≡ h → bind f (bind g v) = bind h v +with ebind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (e : expr A) : + f ∘ g ≡ h → bind f (bind g e) = bind h e +with kbind_comp (A B C : Set) (f : B [⇒] C) (g : A [⇒] B) h (e : cont A) : + f ∘ g ≡ h → bind f (bind g e) = bind h e. +Proof. + - auto_bind_comp. + erewrite ebind_comp; [reflexivity |]. + erewrite lift_comp; [reflexivity |]. + erewrite lift_comp; [reflexivity | assumption]. + - auto_bind_comp. + - auto_bind_comp. +Qed. + +#[export] Instance Bind_val : Bind val. +Proof. + split; intros; [now apply vbind_id | now apply vbind_comp]. +Qed. +#[export] Instance Bind_expr : Bind expr. +Proof. + split; intros; [now apply ebind_id | now apply ebind_comp]. +Qed. +#[export] Instance Bind_cont : Bind cont. +Proof. + split; intros; [now apply kbind_id | now apply kbind_comp]. +Qed. + +Definition to_val {S} (e : expr S) : option (val S) := + match e with + | Val v => Some v + | _ => None + end. + +Definition do_natop (op : nat_op) (x y : nat) : nat := + match op with + | Add => plus x y + | Sub => minus x y + | Mult => mult x y + end. + +Definition nat_op_interp {S} (n : nat_op) (x y : val S) : option (val S) := + match x, y with + | LitV x, LitV y => Some $ LitV $ do_natop n x y + | _,_ => None + end. + +Fixpoint fill {X : Set} (K : cont X) (e : expr X) : expr X := + match K with + | END => e + | IfK e₁ e₂ K => fill K $ If e e₁ e₂ + | AppLK v K => fill K $ App e (Val v) + | AppRK e' K => fill K $ App e' e + | NatOpLK op v K => fill K $ NatOp op e (Val v) + | NatOpRK op e' K => fill K $ NatOp op e' e + | ThrowK err K => fill K $ Throw err e + | CatchK err e' K => fill K $ Catch err e e' + end. + +Lemma fill_emap {X Y : Set} (f : X [→] Y) (K : cont X) (e : expr X) + : fmap f (fill K e) = fill (fmap f K) (fmap f e). +Proof. + revert f. + induction K as [ | ???? IH + | ??? IH + | ??? IH + | ???? IH + | ???? IH + | ??? IH + | ???? IH ]; + intros f; term_simpl; first done; rewrite IH; reflexivity. +Qed. + +Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S + := match K2 with + | END => K1 + | IfK e₁ e₂ K => IfK e₁ e₂ (cont_compose K1 K) + | AppLK v K => AppLK v (cont_compose K1 K) + | AppRK e K => AppRK e (cont_compose K1 K) + | NatOpLK op v K => NatOpLK op v (cont_compose K1 K) + | NatOpRK op e K => NatOpRK op e (cont_compose K1 K) + | ThrowK err K => ThrowK err (cont_compose K1 K) + | CatchK err h K => CatchK err h (cont_compose K1 K) + end. + +Fixpoint unwind {S : Set} (err : exc) (k : cont S) := + match k with + | END => None + | IfK _ _ K' => unwind err K' + | AppLK _ K' => unwind err K' + | AppRK _ K' => unwind err K' + | NatOpLK _ _ K' => unwind err K' + | NatOpRK _ _ K' => unwind err K' + | ThrowK _ K' => unwind err K' + | CatchK err' h K' => if eq_dec err err' + then Some (h,K') + else unwind err K' + end. + +Variant config {S : Set} : Type := + | Cexpr : expr S → config + | Ccont : cont S → val S → config + | Ceval : expr S → cont S → config + | Cret : val S → config. + +Reserved Notation "c '===>' c'" + (at level 40, c' at level 30). + +Variant Cred {S : Set} : config → config → Prop := + | Cinit e : Cexpr e ===> Ceval e END + | Cval v k : Ceval (Val v) k ===> Ccont k v + | Capp e0 e1 k : Ceval (App e0 e1) k ===> Ceval e1 (AppRK e0 k) + | Cop op e0 e1 k : Ceval (NatOp op e0 e1) k ===> Ceval e1 (NatOpRK op e0 k) + | Cif cd e1 e2 k : Ceval (If cd e1 e2) k ===> Ceval cd (IfK e1 e2 k) + | Ccatch err e h k : Ceval (Catch err e h) k ===> Ceval e (CatchK err h k) + | Cthrow err e k : Ceval (Throw err e) k ===> Ceval e (ThrowK err k) + | Cappr e v k : Ccont (AppRK e k) v ===> Ceval e (AppLK v k) + | Cappl f (v : val S) k : Ccont (AppLK v k) (RecV f) ===> Ceval + (subst (Inc := inc) + (subst (F := expr) (Inc := inc) f + (Val (shift (Inc := inc) v))) + (Val (RecV f))) k + | Cifk n e1 e2 k : Ccont (IfK e1 e2 k) (LitV n) ===> Ceval (if (n =? 0) then e2 else e1) k + | Coprk op v e k : Ccont (NatOpRK op e k) v ===> Ceval e (NatOpLK op v k) + | Coplk op v1 v2 v3 k : nat_op_interp op v1 v2 = Some v3 → + Ccont (NatOpLK op v2 k) v1 ===> Ceval (Val v3) k + | Ccatchk err h v k : Ccont (CatchK err h k) v ===> Ceval (Val v) k + | Cthrowk err h v k k' : unwind err k = Some (h,k') → + Ccont (ThrowK err k) v ===> Ceval (subst (Inc := inc) h (Val v)) k' + +where "c ===> c'" := (Cred c c'). + +Inductive steps {S : Set} : (@config S) → (@config S) → Prop := +| step0 c : steps c c +| step_trans c c' c'' : c ===> c' → steps c' c'' → steps c c'' +. + +(** Carbonara from heap lang *) +Global Instance fill_item_inj {S} (Ki : cont S) : Inj (=) (=) (fill Ki). +Proof. induction Ki; intros ???; simplify_eq/=; auto with f_equal. Qed. + +Lemma fill_item_val {S} K (e : expr S) : + is_Some (to_val (fill K e)) → is_Some (to_val e). +Proof. + intros [v ?]. induction K; simpl in H; try apply IHK in H. + 1 : eauto. + all : contradict H; eauto. +Qed. + +Lemma fill_app {S} (K1 K2 : cont S) e : fill (cont_compose K1 K2) e = fill K1 (fill K2 e). +Proof. + revert K1. + revert e. + induction K2 as [ | ???? IH + | ??? IH + | ??? IH + | ???? IH + | ???? IH + | ??? IH + | ???? IH ]; + first done; intros e' K1; simpl; rewrite IH; reflexivity. +Qed. + +Lemma fill_val : ∀ {S} K (e : expr S), is_Some (to_val (fill K e)) → is_Some (to_val e). +Proof. + intros S K. + induction K as [ | ???? IH + | ??? IH + | ??? IH + | ???? IH + | ???? IH + | ??? IH + | ???? IH ]=> e' //=; + inversion 1 as [? HH]; + apply IH in H; + simpl in H; + contradict H; + eauto. +Qed. + +Lemma fill_not_val : ∀ {S} K (e : expr S), to_val e = None → to_val (fill K e) = None. +Proof. + intros S K e. rewrite !eq_None_not_Some. + eauto using fill_val. +Qed. + +Lemma fill_end {S} (e : expr S) : fill END e = e. +Proof. reflexivity. Qed. + +Lemma fill_comp {S} K1 K2 (e : expr S) : fill K2 (fill K1 e) = fill (cont_compose K2 K1) e. +Proof. by rewrite fill_app. Qed. + +Global Instance fill_inj {S} (K : cont S) : Inj (=) (=) (fill K). +Proof. + induction K as [ | | | | | | | ]; + rewrite /Inj; naive_solver. +Qed. + +(*** Type system *) + + +Inductive ty := + | Tnat : ty | Tarr : ty → ty → ty. + +Context {ETy : exc → ty}. + +Inductive typed {S : Set} (Γ : S -> ty) : expr S → ty → Prop := +| typed_Val (τ : ty) (v : val S) : + typed_val Γ v τ → + typed Γ (Val v) τ +| typed_Var (τ : ty) (v : S) : + Γ v = τ → + typed Γ (Var v) τ +| typed_App (τ1 τ2 : ty) e1 e2 : + typed Γ e1 (Tarr τ1 τ2) → + typed Γ e2 τ1 → + typed Γ (App e1 e2) τ2 +| typed_NatOp e1 e2 op : + typed Γ e1 Tnat → + typed Γ e2 Tnat → + typed Γ (NatOp op e1 e2) Tnat +| typed_If e0 e1 e2 τ : + typed Γ e0 Tnat → + typed Γ e1 τ → + typed Γ e2 τ → + typed Γ (If e0 e1 e2) τ +| typed_Throw err exp τ : + typed Γ exp (ETy err) → typed Γ (Throw err exp) τ +| typed_Catch err exp cexp τ : + typed Γ exp τ → + typed (Γ ▹ (ETy err)) cexp τ → + typed Γ (Catch err exp cexp) τ +with typed_val {S : Set} (Γ : S -> ty) : val S → ty → Prop := +| typed_Lit n : + typed_val Γ (LitV n) Tnat +| typed_RecV (τ1 τ2 : ty) (e : expr (inc (inc S))) : + typed (Γ ▹ (Tarr τ1 τ2) ▹ τ1) e τ2 → + typed_val Γ (RecV e) (Tarr τ1 τ2) +. + +(** TODO LATER + +Declare Scope syn_scope. +Delimit Scope syn_scope with syn. + +Coercion Val : val >-> expr. + +Coercion App : expr >-> Funclass. +Coercion AppLK : val >-> Funclass. +Coercion AppRK : expr >-> Funclass. + + +(* XXX: We use these typeclasses to share the notation between the +expressions and the evaluation contexts, for readability. It will be +good to also share the notation between different languages. *) + +Class AsSynExpr (F : Set -> Type) := { __asSynExpr : ∀ S, F S -> expr S }. + +Arguments __asSynExpr {_} {_} {_}. + +Global Instance AsSynExprValue : AsSynExpr val := { + __asSynExpr _ v := Val v + }. +Global Instance AsSynExprExpr : AsSynExpr expr := { + __asSynExpr _ e := e + }. + +Class OpNotation (A B C D : Type) := { __op : A -> B -> C -> D }. + +Global Instance OpNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : OpNotation (F S) nat_op (G S) (expr S) := { + __op e₁ op e₂ := NatOp op (__asSynExpr e₁) (__asSynExpr e₂) + }. + +Global Instance OpNotationLK {S : Set} : OpNotation (cont S) (nat_op) (val S) (cont S) := { + __op K op v := NatOpRK op K v + }. + +Global Instance OpNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : OpNotation (F S) (nat_op) (cont S) (cont S) := { + __op e op K := NatOpLK op (__asSynExpr e) K + }. + +Class IfNotation (A B C D : Type) := { __if : A -> B -> C -> D }. + +Global Instance IfNotationExpr {S : Set} {F G H : Set -> Type} `{AsSynExpr F, AsSynExpr G, AsSynExpr H} : IfNotation (F S) (G S) (H S) (expr S) := { + __if e₁ e₂ e₃ := If (__asSynExpr e₁) (__asSynExpr e₂) (__asSynExpr e₃) + }. + +Global Instance IfNotationK {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : IfNotation (cont S) (F S) (G S) (cont S) := { + __if K e₂ e₃ := IfK K (__asSynExpr e₂) (__asSynExpr e₃) + }. + +Class AppNotation (A B C : Type) := { __app : A -> B -> C }. + +Global Instance AppNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : AppNotation (F S) (G S) (expr S) := { + __app e₁ e₂ := App (__asSynExpr e₁) (__asSynExpr e₂) + }. + +Global Instance AppNotationLK {S : Set} : AppNotation (cont S) (val S) (cont S) := { + __app K v := AppLK K v + }. + +Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (cont S) (cont S) := { + __app e K := AppRK (__asSynExpr e) K + }. + +Class ThrowNotation (A B : Type) := { __throw : exc -> A -> B}. + +Global Instance ThrowNotationExpr {S : Set} {F: Set -> Type} `{AsSynExpr F} : ThrowNotation (F S) (expr S) := + { + __throw e v := Throw e (__asSynExpr v) + }. + +Global Instance ThrowNotationK {S : Set} : ThrowNotation (cont S) (cont S) := + { + __throw e K := ThrowK e K + }. + +Class CatchNotation (A B C : Type) := + { + __catch : exc -> A -> B -> C + }. + +Global Instance CatchNotationExpr {S : Set} (F G : Set -> Type) `{AsSynExpr F} `{AsSynExpr G} : CatchNotation (F S) (G (inc S)) (expr S) := + { + __catch err b h := Catch err (__asSynExpr b) (__asSynExpr h) + }. + +Global Instance CatchNotationK {S : Set} (F : Set -> Type) `{AsSynExpr F} : CatchNotation (cont S) (F (inc S)) (cont S) := + { + __catch err K h := CatchK err K (__asSynExpr h) + }. + + +Notation of_val := Val (only parsing). + +Notation "x '⋆' y" := (__app x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope. +Notation "x '+' y" := (__op x%syn Add y%syn) : syn_scope. +Notation "x '-' y" := (__op x%syn Sub y%syn) : syn_scope. +Notation "x '*' y" := (__op x%syn Mult y%syn) : syn_scope. +Notation "'if' x 'then' y 'else' z" := (__if x%syn y%syn z%syn) : syn_scope. +Notation "'#' n" := (LitV n) (at level 60) : syn_scope. +Notation "'rec' e" := (RecV e%syn) (at level 60) : syn_scope. +Notation "'$' fn" := (set_pure_resolver fn) (at level 60) : syn_scope. +Notation "'try' b 'catch' err '=>' h" := + (__catch err b%syn h%syn) (at level 60) : syn_scope. +Notation "'throw' err v" := + (__throw err v%syn) (at level 60) : syn_scope. +Notation "□" := (EmptyK) : syn_scope. +Notation "K '⟪' e '⟫'" := (fill K%syn e%syn) (at level 60) : syn_scope. + +Definition LamV {S : Set} (e : expr (inc S)) : val S := + RecV (shift e). + +Notation "'λ' . e" := (LamV e%syn) (at level 60) : syn_scope. + +Definition LetE {S : Set} (e : expr S) (e' : expr (inc S)) : expr S := + App (LamV e') (e). + +Notation "'let_' e₁ 'in' e₂" := (LetE e₁%syn e₂%syn) (at level 60, right associativity) : syn_scope. + +Definition SeqE {S : Set} (e e' : expr S) : expr S := + App (LamV (shift e)) e'. + +Notation "e₁ ';;' e₂" := (SeqE e₁%syn e₂%syn) : syn_scope. + +Declare Scope typ_scope. +Delimit Scope typ_scope with typ. + +Notation "'ℕ'" := (Tnat) (at level 1) : typ_scope. +Notation "A →ₜ B" := (Tarr A%typ B%typ) + (right associativity, at level 60) : typ_scope. +**) +End Lang. From 1766d81e21060b47f46b0c61da6c261f409148b7 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 28 Jun 2024 15:26:09 +0200 Subject: [PATCH 04/16] Soundness for except_lang --- theories/examples/except_lang/interp.v | 380 +++++++++++++++++++------ theories/examples/except_lang/lang.v | 205 +++++++++++++ 2 files changed, 499 insertions(+), 86 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 0789c17..08e3bb2 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -224,6 +224,23 @@ Module interp (Errors : ExcSig). by rewrite interp_rec_unfold. Qed. + Program Definition interp_handler {S} (h : expr (inc S)) : interp_scope S -n> laterO IT -n> laterO IT := + λne env, laterO_map (λne x, (interp_expr h) (extend_scope env x)). + Next Obligation. + solve_proper_prepare. + f_equiv. + intros []; simpl; solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + repeat f_equiv. + intro. + simpl. + f_equiv. + intros []; + simpl; done. + Qed. + Program Fixpoint split_cont {S} (K : cont S) : interp_scope S → ((IT -n> IT) * (listO (excO * (laterO IT -n> laterO IT) * (laterO IT -n> laterO IT) )))%type := λ env, match K with @@ -245,23 +262,13 @@ Module interp (Errors : ExcSig). (f ◎ (λne t, THROW err t), lst) | CatchK err h K' => let (f, lst) := split_cont K' env in (get_val (λne t, get_val (λne _, t) (_POP err)), (err, - laterO_map - (λne x, (interp_expr h) - (extend_scope env x) - ), laterO_map f) + interp_handler h env , laterO_map f) ::lst) end. Solve All Obligations with try solve_proper. Next Obligation. solve_proper_please. Qed. - Next Obligation. - Proof. - solve_proper_prepare. - f_equiv. - intros []; - done. - Qed. Global Instance split_cont_ne {S} {K : cont S} : NonExpansive (split_cont K). Proof. @@ -624,7 +631,155 @@ Module interp (Errors : ExcSig). by intro. *) Qed. - + Lemma split_cont_decomp {S} K K1 K2 p t p1 t1 env h err f k: + split_cont K env = (p,t) → + split_cont K1 env = (p1,t1) → + K = cont_compose (CatchK err h K1) K2 → + (∀ K4 K3 h', K2 <> @cont_compose S (CatchK err h' K3) K4) → + f = interp_handler h env → + k = laterO_map p1 → + ∃pre, t = pre ++ (err,f,k)::t1 ∧ Forall (λ '(err', _ ,_ ), err <> err' ) pre. + Proof. + generalize dependent K1. + generalize dependent p. + generalize dependent t. + generalize dependent p1. + generalize dependent t1. + generalize dependent K2. + generalize dependent f. + generalize dependent env. + generalize dependent h. + + induction K; intros. + - destruct K2; discriminate. + - destruct K2; try discriminate. + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (IfK e₁ e₂ K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (AppLK v K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (AppRK e K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (NatOpLK op v K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (NatOpRK op e K4)). + simpl. + reflexivity. + - destruct K2; try discriminate. + injection H1 as <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + eapply (IHK h env _ _ _ _ u g _ Heq H0 eq_refl). + Unshelve. + 2, 3 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (ThrowK err0 K4)). + simpl. + reflexivity. + + - destruct K2; try discriminate. + + injection H1 as <- <- ->. + simpl in H. + rewrite H0 in H. + injection H as <- <-. + eexists []. + rewrite H3 H4. + simpl. + done. + + injection H1 as <- <- ->. + simpl in H. + destruct (split_cont (cont_compose (CatchK err h0 K1) K2) env) as [g u] eqn:Heq. + injection H as <- <-. + epose proof (IHK h0 env _ _ _ _ u g _ Heq H0 _ _ _ _) as (pre & -> & Hfall). + eexists. + split. + { rewrite app_comm_cons. done. } + apply Forall_cons. + split; last done. + intros ->. + by eapply (H2 END). + Unshelve. + 2, 4, 5 : done. + intros K4 K3 h' C. + rewrite C in H2. + eapply (H2 (CatchK err0 h K4) _). + simpl. + done. + Qed. + + Lemma unwind_cut_when {S} : ∀ K K' env f t g t' err h, + split_cont K env = (f,t) → + split_cont K' env = (g,t') → + @unwind S err K = Some (h, K') → + cut_when (aux err) t = Some ((err,interp_handler h env,laterO_map g), t'). + Proof. + intros K K' env f t g t' err h HsplitK HsplitK' Hwind. + apply unwind_decompose in Hwind as (K1 & -> & HK1). + pose proof (split_cont_decomp _ _ _ f t g t' env h err _ _ HsplitK HsplitK' eq_refl HK1 eq_refl eq_refl) as (pre & -> & Hfall). + eapply cut_when_first_occ. + { done. } + { simpl. destruct (eq_dec err err); done. }. + eapply Forall_impl. + { exact Hfall. } + intros [[err' ?] ?] ?. + simpl. + destruct (eq_dec err err'); done. + Qed. + Theorem soundness {S} : ∀ c c' e e' σr σ σ' (env : interp_scope S), interp_config c env = (e, σ) → interp_config c' env = (e', σ') → @@ -712,7 +867,7 @@ Module interp (Errors : ExcSig). injection H1 as <- <-. exists 0. by constructor. - - simpl in H0, H1. + - simpl in H0, H1. destruct (split_cont k env) as [f t] eqn:Heq. assert (IT_hom f). { eapply split_cont_left_hom'. apply Heq. } @@ -720,7 +875,7 @@ Module interp (Errors : ExcSig). injection H1 as <- <-. exists 0. by constructor. - - simpl in H0, H1. + - simpl in H0, H1. destruct (split_cont k env) as [g t] eqn:Heq. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } @@ -755,82 +910,135 @@ Module interp (Errors : ExcSig). + destruct i; simpl. * done. * done. - - simpl in H0, H1. - destruct (split_cont k env) as [g t] eqn:Heq. - assert (IT_hom g) as Hg. - { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. - exists 0. - constructor; last done. - f_equiv. - destruct n. - + rewrite IF_False; last lia. - done. - + rewrite IF_True; last lia. - done. - - simpl in H0, H1. - destruct (split_cont k env) as [g t] eqn:Heq. - assert (IT_hom g) as Hg. - { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. - exists 0. - constructor; done. - simpl in H0, H1. - destruct (split_cont k env) as [g t] eqn:Heq. - assert (IT_hom g) as Hg. - { eapply split_cont_left_hom'. apply Heq. } + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. - injection H1 as <- <-. - exists 0. - constructor; last done. - f_equiv. - destruct v1, v2. - 2, 3, 4 : contradict H; done. - simpl in H. - injection H as <-. - simpl. - apply NATOP_Ret. + injection H1 as <- <-. + exists 0. + constructor; last done. + f_equiv. + destruct n. + + rewrite IF_False; last lia. + done. + + rewrite IF_True; last lia. + done. - simpl in H0, H1. - destruct (split_cont k env) as [g t] eqn:Heq. - assert (IT_hom g) as Hg. - { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. - exists 1. - econstructor; last (constructor; done). - rewrite get_val_ITV /= get_val_vis. - eapply sstep_reify; first done. - rewrite reify_vis_eq_ctx_dep. - { rewrite Tick_eq. done. } - epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inl ())) ?[x] (Next _) ?[k] ?[σ] ?[σ'] σr _) as Hry. - match goal with - | |- _ _ _ (_ ?x', (_ _ (_ (_ ?σ2) _)) , ?k1 ◎ (?k2 ◎ _)) ≡ _ => instantiate (x := x'); - instantiate (k := k1 ◎ k2); - instantiate (σ := σ2) - - end. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; done. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 0. + constructor; last done. + f_equiv. + destruct v1, v2. + 2, 3, 4 : contradict H; done. + simpl in H. + injection H as <-. + simpl. + apply NATOP_Ret. + - simpl in H0, H1. + destruct (split_cont k env) as [g t] eqn:Heq. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 1. + econstructor; last (constructor; done). + rewrite get_val_ITV /= get_val_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inl ())) ?[x] (Next _) ?[k] ?[σ] ?[σ'] σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ (_ ?σ2) _)) , ?k1 ◎ (?k2 ◎ _)) ≡ _ => instantiate (x := x'); + instantiate (k := k1 ◎ k2); + instantiate (σ := σ2) + + end. + Unshelve. + 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. }. + 1 : { simpl in Hry|-*. + match goal with + | [Hry : _ ≡ ?r |- _ ] => transitivity r + end. + 2 : { repeat f_equiv. + Transparent laterO_map. + simpl. + Opaque laterO_map. + f_equiv. + apply get_val_ret. + } + + rewrite -Hry. + + repeat f_equiv; first by solve_proper. + intro. simpl. done. + } + - simpl in H0, H1. + (** (interp_expr (subst h (Val v)) env), t) **) + destruct (split_cont k env) as [g t] eqn:Heq. + destruct (split_cont k' env) as [g' t'] eqn:Heq'. + assert (IT_hom g) as Hg. + { eapply split_cont_left_hom'. apply Heq. } + injection H0 as <- <-. + injection H1 as <- <-. + exists 1. + econstructor; last by constructor. + rewrite get_val_ITV hom_vis. + eapply sstep_reify; first done. + rewrite reify_vis_eq_ctx_dep. + { rewrite Tick_eq. done. } + epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inr (inl ()))) ?[x] (Next _) ?[k] ?[σ] t' σr _) as Hry. + match goal with + | |- _ _ _ (_ ?x', (_ _ (_ _ ?σ2)) , _) ≡ _ => + instantiate (x := x'); + instantiate (σ := σ2) + end. + Unshelve. + 4 : { Opaque cut_when. simpl. + apply (unwind_cut_when _ _ env _ _ _ _ _ _ Heq Heq') in H. + rewrite H. + simpl. + f_equiv. + rewrite laterO_map_Next. + simpl. + rewrite pair_equiv. + split; last done. + f_equiv. + trans (g' (interp_expr (subst h (Val v)) env)); last done. + f_equiv. + rewrite interp_expr_subst. + f_equiv. + intros []; done. + } + 1 : { + simpl in Hry. + simpl. + rewrite -Hry. + repeat f_equiv; first solve_proper. + intro. + simpl. + instantiate (k := (laterO_map (λne y, g y)) ◎ (λne x, Empty_set_rect (λ _ : ∅, laterO IT) x)). + simpl. + done. Unshelve. - 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. }. - 1 : { simpl in Hry|-*. - match goal with - | [Hry : _ ≡ ?r |- _ ] => transitivity r - end. - 2 : { repeat f_equiv. - Transparent laterO_map. - simpl. - Opaque laterO_map. - f_equiv. - apply get_val_ret. - } - - rewrite -Hry. - - repeat f_equiv; first by solve_proper. - intro. simpl. done. - } - - (** TODO : THROW **) + intros n []. + } + + Qed. + + diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index 26293bd..fec7a8b 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -318,6 +318,211 @@ Fixpoint unwind {S : Set} (err : exc) (k : cont S) := else unwind err K' end. +Theorem unwind_decompose {S : Set} (err : exc) (K : cont S) (h : expr (inc S)) (K2 : cont S) : unwind err K = Some (h, K2) ↔ ∃ (K1 : cont S), (K = cont_compose (CatchK err h K2) K1 + ∧ (∀ K3 K4 h', K1 ≠ cont_compose (CatchK err h' K4) K3 ) + ). +Proof. + induction K. + - split. + + intros. done. + + intros (? & ? & ?). + destruct x; + done. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (IfK e₁ e₂ K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> -> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (IfK e₁ e₂ K3) K4 h'). + by apply HNC. + + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (AppLK v K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (AppLK v K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (AppRK e K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (AppRK e K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (NatOpLK op v K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> -> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (NatOpLK op v K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (NatOpRK op e K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> -> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (NatOpRK op e K3) K4 h'). + by apply HNC. + - split. + + intros H. + apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (ThrowK err0 K1). + simpl. + rewrite HK1. + split; first done. + intros. + destruct K3; try done. + simpl. + intros [=-> ->]. + specialize (HNC K3 K4 h'). + by apply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + simpl. + apply IHK. + injection HK1 as <- ->. + eexists. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (ThrowK err0 K3) K4 h'). + by apply HNC. + + - split. + + intros H. + simpl in H. + destruct (eq_dec err err0) as [-> | Hdiff]. + * injection H as -> ->. + exists END. + split; first done. + intros K3 K4 h'. + destruct K3, K4; done. + * apply IHK in H. + destruct H as (K1 & HK1 & HNC). + exists (CatchK err0 h0 K1). + simpl. + rewrite HK1. + split; first done. + intros K3 K4 h'. + destruct K3; try done; simpl; intros [=<- <- ->]; first done. + by eapply HNC. + + + intros (K1 & HK1 & HNC). + destruct K1; try done. + * simpl. + destruct (eq_dec err err0) as [-> | C]. + { simpl in HK1. by injection HK1 as -> ->. } + apply IHK. + injection HK1 as <- <-. + by contradict C. + * injection HK1 as <- <- ->. + simpl. + destruct (eq_dec err err0) as [-> | Herr]. + { + exfalso. + specialize (HNC END K1 h0). + by apply HNC. + } + apply IHK. + exists K1. + split; first done. + intros K3 K4 h' ->. + specialize (HNC (CatchK err0 h0 K3)). + by eapply HNC. +Qed. + Variant config {S : Set} : Type := | Cexpr : expr S → config | Ccont : cont S → val S → config From e8c4ab70d9210b4aa51b919657c01835b222d5f5 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 28 Jun 2024 15:30:45 +0200 Subject: [PATCH 05/16] Fixed syntax problem --- theories/examples/except_lang/interp.v | 27 ++++---------------------- 1 file changed, 4 insertions(+), 23 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 08e3bb2..30a6de3 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -772,7 +772,7 @@ Module interp (Errors : ExcSig). pose proof (split_cont_decomp _ _ _ f t g t' env h err _ _ HsplitK HsplitK' eq_refl HK1 eq_refl eq_refl) as (pre & -> & Hfall). eapply cut_when_first_occ. { done. } - { simpl. destruct (eq_dec err err); done. }. + { simpl. destruct (eq_dec err err); done. } eapply Forall_impl. { exact Hfall. } intros [[err' ?] ?] ?. @@ -839,7 +839,7 @@ Module interp (Errors : ExcSig). end. Unshelve. - 6 : { simpl. done. }. + 6 : { simpl. done. } 1 : { simpl in Hry|-*. erewrite <-Hry. repeat f_equiv; first by solve_proper. @@ -967,7 +967,7 @@ Module interp (Errors : ExcSig). end. Unshelve. - 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. }. + 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. } 1 : { simpl in Hry|-*. match goal with | [Hry : _ ≡ ?r |- _ ] => transitivity r @@ -1039,26 +1039,7 @@ Module interp (Errors : ExcSig). Qed. - - - - - - - - - - - - - - - - - - - - + (** BOOKMARK **) (** ** Interpretation of evaluation contexts induces homomorphism *) From 1dfd9e821fcbfddd2be88ec58766f4721a835e5e Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Sat, 29 Jun 2024 02:01:42 +0200 Subject: [PATCH 06/16] Refined semantics for except lang to state soundness more precisely --- theories/examples/except_lang/interp.v | 43 ++++++++------------------ theories/examples/except_lang/lang.v | 40 ++++++++++++------------ 2 files changed, 33 insertions(+), 50 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 30a6de3..9a5859a 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -780,14 +780,13 @@ Module interp (Errors : ExcSig). destruct (eq_dec err err'); done. Qed. - Theorem soundness {S} : ∀ c c' e e' σr σ σ' (env : interp_scope S), + Theorem soundness {S} : ∀ c c' e e' σr σ σ' n (env : interp_scope S), interp_config c env = (e, σ) → interp_config c' env = (e', σ') → - c ===> c' → - ∃ n, - ssteps (gReifiers_sReifier rs) - e (gState_recomp σr (sR_state σ)) - e' (gState_recomp σr (sR_state σ')) n. + c ===> c' / n → + ssteps (gReifiers_sReifier rs) + e (gState_recomp σr (sR_state σ)) + e' (gState_recomp σr (sR_state σ')) n. Proof. intros. revert H H0. @@ -795,30 +794,25 @@ Module interp (Errors : ExcSig). - simpl in H0, H1. injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; done. - simpl in H0, H1. rewrite H0 in H1. injection H1 as <- <-. - exists 0. constructor; done. - simpl in H0, H1. destruct (split_cont k env) as [f t]. injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; done. - simpl in H0, H1. destruct (split_cont k env) as [f t]. injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; done. - simpl in H0, H1. destruct (split_cont k env) as [f t]. injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; done. - simpl in H0, H1. destruct (split_cont k env) as [f t] eqn:Heq. @@ -826,7 +820,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 1. econstructor. + rewrite hom_vis. eapply sstep_reify; first done. @@ -865,7 +858,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 0. by constructor. - simpl in H0, H1. destruct (split_cont k env) as [f t] eqn:Heq. @@ -873,7 +865,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 0. by constructor. - simpl in H0, H1. destruct (split_cont k env) as [g t] eqn:Heq. @@ -881,7 +872,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 1. econstructor; last (econstructor; reflexivity). apply sstep_tick; last done. rewrite -hom_tick. @@ -916,7 +906,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; last done. f_equiv. destruct n. @@ -930,7 +919,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; done. - simpl in H0, H1. destruct (split_cont k env) as [g t] eqn:Heq. @@ -938,7 +926,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 0. constructor; last done. f_equiv. destruct v1, v2. @@ -953,7 +940,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 1. econstructor; last (constructor; done). rewrite get_val_ITV /= get_val_vis. eapply sstep_reify; first done. @@ -961,10 +947,10 @@ Module interp (Errors : ExcSig). { rewrite Tick_eq. done. } epose proof (@subReifier_reify _ _ _ _ _ _ _ (inr (inl ())) ?[x] (Next _) ?[k] ?[σ] ?[σ'] σr _) as Hry. match goal with - | |- _ _ _ (_ ?x', (_ _ (_ (_ ?σ2) _)) , ?k1 ◎ (?k2 ◎ _)) ≡ _ => instantiate (x := x'); - instantiate (k := k1 ◎ k2); - instantiate (σ := σ2) - + | |- _ _ _ (_ ?x', (_ _ (_ (_ ?σ2) _)) , ?k1 ◎ (?k2 ◎ _)) ≡ _ => + instantiate (x := x'); + instantiate (k := k1 ◎ k2); + instantiate (σ := σ2) end. Unshelve. 4 : { simpl. destruct (eq_dec err) as [? | ?]; done. } @@ -993,7 +979,6 @@ Module interp (Errors : ExcSig). { eapply split_cont_left_hom'. apply Heq. } injection H0 as <- <-. injection H1 as <- <-. - exists 1. econstructor; last by constructor. rewrite get_val_ITV hom_vis. eapply sstep_reify; first done. @@ -1038,11 +1023,10 @@ Module interp (Errors : ExcSig). Qed. - (** BOOKMARK **) (** ** Interpretation of evaluation contexts induces homomorphism *) - +(* #[local] Instance interp_cont_hom_emp {S} env : IT_hom (interp_cont (EmptyIK : cont S) env). Proof. @@ -1254,7 +1238,6 @@ Module interp (Errors : ExcSig). rewrite interp_comp. reflexivity. Qed. - *) Example test1 err : expr ∅ := (try @@ -1351,8 +1334,8 @@ Module interp (Errors : ExcSig). rewrite interp_comp /= get_ret_ret hom_OUTPUT_. eauto. Qed. - - + *) *) + (** Section Examples. Context `{!invGS Σ, !stateG rs R Σ}. @@ -1485,6 +1468,6 @@ Module interp (Errors : ExcSig). Qed. End Examples. - +**) End interp. #[global] Opaque INPUT OUTPUT_. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index fec7a8b..5f0f3d0 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -529,36 +529,36 @@ Variant config {S : Set} : Type := | Ceval : expr S → cont S → config | Cret : val S → config. -Reserved Notation "c '===>' c'" +Reserved Notation "c '===>' c' / n" (at level 40, c' at level 30). -Variant Cred {S : Set} : config → config → Prop := - | Cinit e : Cexpr e ===> Ceval e END - | Cval v k : Ceval (Val v) k ===> Ccont k v - | Capp e0 e1 k : Ceval (App e0 e1) k ===> Ceval e1 (AppRK e0 k) - | Cop op e0 e1 k : Ceval (NatOp op e0 e1) k ===> Ceval e1 (NatOpRK op e0 k) - | Cif cd e1 e2 k : Ceval (If cd e1 e2) k ===> Ceval cd (IfK e1 e2 k) - | Ccatch err e h k : Ceval (Catch err e h) k ===> Ceval e (CatchK err h k) - | Cthrow err e k : Ceval (Throw err e) k ===> Ceval e (ThrowK err k) - | Cappr e v k : Ccont (AppRK e k) v ===> Ceval e (AppLK v k) +Variant Cred {S : Set} : config → config → nat → Prop := + | Cinit e : Cexpr e ===> Ceval e END / 0 + | Cval v k : Ceval (Val v) k ===> Ccont k v / 0 + | Capp e0 e1 k : Ceval (App e0 e1) k ===> Ceval e1 (AppRK e0 k) / 0 + | Cop op e0 e1 k : Ceval (NatOp op e0 e1) k ===> Ceval e1 (NatOpRK op e0 k) / 0 + | Cif cd e1 e2 k : Ceval (If cd e1 e2) k ===> Ceval cd (IfK e1 e2 k) / 0 + | Ccatch err e h k : Ceval (Catch err e h) k ===> Ceval e (CatchK err h k) / 1 + | Cthrow err e k : Ceval (Throw err e) k ===> Ceval e (ThrowK err k) / 0 + | Cappr e v k : Ccont (AppRK e k) v ===> Ceval e (AppLK v k) / 0 | Cappl f (v : val S) k : Ccont (AppLK v k) (RecV f) ===> Ceval (subst (Inc := inc) (subst (F := expr) (Inc := inc) f (Val (shift (Inc := inc) v))) - (Val (RecV f))) k - | Cifk n e1 e2 k : Ccont (IfK e1 e2 k) (LitV n) ===> Ceval (if (n =? 0) then e2 else e1) k - | Coprk op v e k : Ccont (NatOpRK op e k) v ===> Ceval e (NatOpLK op v k) + (Val (RecV f))) k / 1 + | Cifk n e1 e2 k : Ccont (IfK e1 e2 k) (LitV n) ===> Ceval (if (n =? 0) then e2 else e1) k / 0 + | Coprk op v e k : Ccont (NatOpRK op e k) v ===> Ceval e (NatOpLK op v k) / 0 | Coplk op v1 v2 v3 k : nat_op_interp op v1 v2 = Some v3 → - Ccont (NatOpLK op v2 k) v1 ===> Ceval (Val v3) k - | Ccatchk err h v k : Ccont (CatchK err h k) v ===> Ceval (Val v) k + Ccont (NatOpLK op v2 k) v1 ===> Ceval (Val v3) k / 0 + | Ccatchk err h v k : Ccont (CatchK err h k) v ===> Ceval (Val v) k / 1 | Cthrowk err h v k k' : unwind err k = Some (h,k') → - Ccont (ThrowK err k) v ===> Ceval (subst (Inc := inc) h (Val v)) k' + Ccont (ThrowK err k) v ===> Ceval (subst (Inc := inc) h (Val v)) k' / 1 -where "c ===> c'" := (Cred c c'). +where "c ===> c' / n" := (Cred c c' n). -Inductive steps {S : Set} : (@config S) → (@config S) → Prop := -| step0 c : steps c c -| step_trans c c' c'' : c ===> c' → steps c' c'' → steps c c'' +Inductive steps {S : Set} : (@config S) → (@config S) → nat → Prop := +| step0 c : steps c c 0 +| step_trans c c' c'' n n' : c ===> c' / n → steps c' c'' n' → steps c c'' (n + n') . (** Carbonara from heap lang *) From 1036fd3c24672a9403b996486ccf1f9f3269c84e Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 11 Jul 2024 15:24:54 +0200 Subject: [PATCH 07/16] Typing system for except lang --- theories/examples/except_lang/interp.v | 34 +- theories/examples/except_lang/lang.v | 20 +- theories/examples/except_lang/typing.v | 953 +++++++++++++++++++++++++ 3 files changed, 998 insertions(+), 9 deletions(-) create mode 100644 theories/examples/except_lang/typing.v diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 9a5859a..3e67cf0 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -239,8 +239,8 @@ Module interp (Errors : ExcSig). f_equiv. intros []; simpl; done. - Qed. - + Qed. + Program Fixpoint split_cont {S} (K : cont S) : interp_scope S → ((IT -n> IT) * (listO (excO * (laterO IT -n> laterO IT) * (laterO IT -n> laterO IT) )))%type := λ env, match K with @@ -1020,12 +1020,33 @@ Module interp (Errors : ExcSig). Unshelve. intros n []. } - + - simpl in H0, H1. + rewrite H0 in H1. + injection H1 as <- <-. + constructor; done. Qed. + Theorem stuck {S} : ∀ c c' e σr σ n (env : interp_scope S), + interp_config c env = (e, σ) → + (∀ m e' σ', m > 0 → ¬ (ssteps (gReifiers_sReifier rs) + e (gState_recomp σr (sR_state σ)) + e' (gState_recomp σr (sR_state σ')) m)) → + c ===> c' / n → + n = 0. + intros c c' e σr σ n env Hc Hst Hred. + destruct n; first done. + exfalso. + destruct (interp_config c' env) as (e', σ') eqn:Hc'. + eapply (soundness _ _ _ _ σr _ _ _ _ Hc Hc') in Hred. + specialize (Hst (Datatypes.S n) e' σ'). + apply Hst; first lia. + apply Hred. + Qed. + (** BOOKMARK **) - (** ** Interpretation of evaluation contexts induces homomorphism *) + + (* #[local] Instance interp_cont_hom_emp {S} env : IT_hom (interp_cont (EmptyIK : cont S) env). @@ -1333,8 +1354,7 @@ Module interp (Errors : ExcSig). Opaque OUTPUT_. rewrite interp_comp /= get_ret_ret hom_OUTPUT_. eauto. - Qed. - *) *) + Qed. *) (** Section Examples. Context `{!invGS Σ, !stateG rs R Σ}. @@ -1468,6 +1488,6 @@ Module interp (Errors : ExcSig). Qed. End Examples. -**) +**) *) End interp. #[global] Opaque INPUT OUTPUT_. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index 5f0f3d0..e19bd79 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -37,6 +37,7 @@ Module Lang (Errors : ExcSig). Arguments val X%bind : clear implicits. Arguments expr X%bind : clear implicits. Arguments cont X%bind : clear implicits. + Local Open Scope bind_scope. @@ -304,7 +305,7 @@ Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S | CatchK err h K => CatchK err h (cont_compose K1 K) end. -Fixpoint unwind {S : Set} (err : exc) (k : cont S) := + Fixpoint unwind {S : Set} (err : exc) (k : cont S) := match k with | END => None | IfK _ _ K' => unwind err K' @@ -522,6 +523,20 @@ Proof. specialize (HNC (CatchK err0 h0 K3)). by eapply HNC. Qed. + +Lemma unwind_decompose_weak {S} : + ∀ (K K1 K2 : cont S) err h, K = cont_compose (CatchK err h K1) K2 → + ∃ h' K3, unwind err K = Some (h', K3). + Proof. + intros K K1 K2. + revert K1. + induction K2; intros K1 err0 h0 ->; try (simpl; by eapply IHK2). + - simpl. destruct (eq_dec err0 err0); last done. + by eexists _,_. + - simpl. destruct (eq_dec err0 err). + + by eexists _,_. + + by eapply IHK2. + Qed. Variant config {S : Set} : Type := | Cexpr : expr S → config @@ -552,7 +567,8 @@ Variant Cred {S : Set} : config → config → nat → Prop := Ccont (NatOpLK op v2 k) v1 ===> Ceval (Val v3) k / 0 | Ccatchk err h v k : Ccont (CatchK err h k) v ===> Ceval (Val v) k / 1 | Cthrowk err h v k k' : unwind err k = Some (h,k') → - Ccont (ThrowK err k) v ===> Ceval (subst (Inc := inc) h (Val v)) k' / 1 + Ccont (ThrowK err k) v ===> Ceval (subst (Inc := inc) h (Val v)) k' / 1 + | Cend v : Ccont END v ===> Cret v / 0 where "c ===> c' / n" := (Cred c c' n). diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v new file mode 100644 index 0000000..87ddc69 --- /dev/null +++ b/theories/examples/except_lang/typing.v @@ -0,0 +1,953 @@ +From gitrees.examples.except_lang Require Import lang. + +Require Import Binding.Lib Binding.Set Binding.Env. +Require Import Coq.Program.Equality. + + +Module Typing (Errors : ExcSig). + Module _LANG := Lang Errors. + Import _LANG. + Import _Exc. + + (** Bare types **) + Inductive bty : Type := + | Bnat : bty + | Barr : bty → bty → bty + . + + + (** Types indicating possible errors raised **) + Inductive pty : Type := + | Tnat : pty + | Tarr : pty → ty → pty + with ty : Type := + Ty : pty → (exc → Prop) → ty. + + Context (ETy : exc → pty). + Notation "'ℕ'" := Tnat. + Notation "σ '⟶' τ" := (Tarr σ τ) + (at level 20). + Notation "τ ⇑ E" := (Ty τ E) + (at level 20, + E at level 20, + no associativity). + Notation "E1 ⪯ E2" := (∀ x, E1 x → E2 x) + (at level 20, + no associativity, + only parsing). + + Notation "⋆" := (λ _, False). + + Reserved Notation "τ '≲' σ" + (at level 20). + + Reserved Notation "τ '⪍' σ" + (at level 20). + + Inductive le_pty : pty → pty → Prop := + | Le_nat : ℕ ≲ ℕ + | Le_arr τ1 τ2 σ1 σ2 : + τ2 ≲ τ1 → + σ1 ⪍ σ2 → + (τ1 ⟶ σ1) ≲ (τ2 ⟶ σ2) + with le_ty : ty → ty → Prop := + Le_Ty τ1 τ2 E1 E2 : + τ1 ≲ τ2 → + E1 ⪯ E2 → + (τ1 ⇑ E1) ⪍ (τ2 ⇑ E2) + where "τ ≲ σ" := (le_pty τ σ) + and "τ ⪍ σ" := (le_ty τ σ). + + Notation "E1 ≋ E2" := (∀ x, E1 x ↔ E2 x) + (at level 20, + no associativity). + + Lemma le_set_trans {A} : ∀ (E1 E2 E3 : A → Prop), E1 ⪯ E2 → E2 ⪯ E3 → E1 ⪯ E3. + Proof. eauto. Qed. + + Lemma le_set_refl {A} : ∀ (E : A → Prop), E ⪯ E. + Proof. eauto. Qed. + + Lemma le_pty_trans : ∀ τ1 τ2 τ3, τ1 ≲ τ2 → τ2 ≲ τ3 → τ1 ≲ τ3 + with le_ty_trans : ∀ τ1 τ2 τ3, τ1 ⪍ τ2 → τ2 ⪍ τ3 → τ1 ⪍ τ3. + Proof. + - intros τ1 τ2. + destruct τ2. + + intros τ3 H1 H2. + inversion H1. subst. + inversion H2. subst. + done. + + intros τ3 H1 H2. + inversion H1. subst. + inversion H2. subst. + constructor. + * by eapply le_pty_trans. + * by eapply le_ty_trans. + - intros τ1 τ2 τ3 H1 H2. + destruct τ1, τ2, τ3. + inversion H1. subst. + inversion H2. subst. + constructor. + + by eapply le_pty_trans. + + by eapply le_set_trans. + Qed. + + Lemma le_pty_refl : ∀ τ, τ ≲ τ + with le_ty_refl : ∀ τ, τ ⪍ τ. + Proof. + - intros τ. + destruct τ; constructor. + + apply le_pty_refl. + + apply le_ty_refl. + - intros [τ E]. + constructor. + + apply le_pty_refl. + + apply le_set_refl. + Qed. + + (** Compatibility between types and bare types **) + + Reserved Notation "τ ≅ σ" + (at level 20). + + Reserved Notation "τ ≈ σ" + (at level 20). + + Inductive compatp : bty → pty → Prop := + | Comp_nat : Bnat ≅ ℕ + | Comp_arr σb σ τb τ : σb ≅ σ → + τb ≈ τ → + Barr σb τb ≅ (σ ⟶ τ) + with compat : bty → ty → Prop := + Compat_Ty τb τ E : τb ≅ τ → + τb ≈ Ty τ E + where "σ ≅ τ" := (compatp σ τ) + and "σ ≈ τ" := (compat σ τ). + + Lemma le_ty_compat τ1 τ2 σ (Hsub : τ1 ⪍ τ2) : (σ ≈ τ1 ↔ σ ≈ τ2) + with le_pty_compat τ1 τ2 σ (Hsub : τ1 ≲ τ2) : (σ ≅ τ1 ↔ σ ≅ τ2). + Proof. + - destruct τ1 as [τ1 E1]. + destruct τ2 as [τ2 E2]. + inversion Hsub. subst. + split; constructor; inversion H; subst; by eapply (le_pty_compat τ1). + - destruct τ1; inversion Hsub; subst; first done. + split; intros Hsim; inversion Hsim; subst; constructor. + + by eapply le_pty_compat. + + by eapply (le_ty_compat t). + + by eapply (le_pty_compat τ3). + + by eapply (le_ty_compat t). + Qed. + + Notation "E ⊕ e" := (λ x, x = e ∨ E x) + (at level 20). + + Notation "E ⊖ e" := (λ x, x <> e ∧ E x) + (at level 20). + + Notation "E1 ⊍ E2" := (λ x, E1 x ∨ E2 x) + (at level 20). + + Reserved Notation "Γ '⊢ₑ' e ':' τ" + (at level 70 + , e at level 60 + , τ at level 20 + , no associativity + ). + + Reserved Notation "Γ '⊢ᵥ' v : τ" + (at level 70 + , v at level 60 + , τ at level 20 + , no associativity + ). + + Inductive typed {S : Set} : (S → pty) → expr S → ty → Prop := + | typed_Var Γ E x τ : Γ x ≲ τ → + (Γ ⊢ₑ (Var x) : τ ⇑ E) + + | typed_Lit Γ E v : (Γ ⊢ᵥ (LitV v) : ℕ ⇑ E) + + | typed_Rec Γ E f σ τ α : + (σ ⟶ τ) ≲ α→ + (Γ ▹ (σ ⟶ τ) ▹ σ ⊢ₑ f : τ) → + (Γ ⊢ᵥ (RecV f) : α ⇑ E) + + (* | typed_wk Γ τ1 τ2 e : + τ1 ⪍ τ2 → + (Γ ⊢ₑ e : τ1) → + (Γ ⊢ₑ e : τ2) *) + + | typed_App E E1 E2 E3 Γ f v σ τ : + (E1 ⊍ E2 ⊍ E3) ⪯ E → + (Γ ⊢ₑ f : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → + (Γ ⊢ₑ v : σ ⇑ E3) → + (Γ ⊢ₑ App f v : τ ⇑ E) + + | typed_Op Γ E E1 E2 op l r : + (E1 ⊍ E2) ⪯ E → + (Γ ⊢ₑ l : ℕ ⇑ E1) → + (Γ ⊢ₑ r : ℕ ⇑ E2) → + (Γ ⊢ₑ NatOp op l r : ℕ ⇑ E) + + | typed_If Γ E E1 E2 E3 c t e τ : + (E1 ⊍ E2 ⊍ E3) ⪯ E→ + (Γ ⊢ₑ c : ℕ ⇑ E1) → + (Γ ⊢ₑ t : τ ⇑ E2) → + (Γ ⊢ₑ e : τ ⇑ E3) → + (Γ ⊢ₑ If c t e : τ ⇑ E) + + | typed_Throw Γ E1 E2 err v σ τ : + σ ≲ ETy err → + (E1 ⊕ err) ⪯ E2 → + (Γ ⊢ₑ v : σ ⇑ E1) → + (Γ ⊢ₑ Throw err v : τ ⇑ E2) + + | typed_Catch Γ E E1 E2 err h v σ τ : + ETy err ≲ σ → + (E1 ⊍ (E2 ⊖ err)) ⪯ E → + (Γ ▹ σ ⊢ₑ h : τ ⇑ E1) → + (Γ ⊢ₑ v : τ ⇑ E2) → + (Γ ⊢ₑ Catch err v h : τ ⇑ E) + + where "Γ ⊢ₑ e : τ" := (typed Γ e τ) + and "Γ ⊢ᵥ v : τ" := (Γ ⊢ₑ (Val v) : τ). + Print cont. + Reserved Notation "Γ '⊢ₖ' K ':' σ ⇒ τ" + (at level 70 + , K at level 60 + , σ at level 20 + , τ at level 20 + , no associativity + ). + + + Inductive typ_cont {S : Set} : (S → pty) → cont S → ty → ty → Prop := + (* | typed_Err_Wk E1 E2 E3 Γ e σ τ : E1 ⪯ E2 → + (Γ ; E1 ⊢ₖ e : σ ; E3 ⇒ τ) → + (Γ ; E2 ⊢ₖ e : σ ; E3 ⇒ τ) + | typed_Err_St E1 E2 E3 Γ e σ τ : E3 ⪯ E2 → + (Γ ; E1 ⊢ₖ e : σ ; E2 ⇒ τ) → + (Γ ; E1 ⊢ₖ e : σ ; E3 ⇒ τ) *) + | typed_END Γ τ1 τ2 : τ1 ⪍ τ2 → + (Γ ⊢ₖ END : τ1 ⇒ τ2) + | typed_IfK Γ e₁ e₂ K E1 E2 E3 E4 τ σ : + (E1 ⊍ E2 ⊍ E3) ⪯ E4 → + (Γ ⊢ₑ e₁ : σ ⇑ E2) → + (Γ ⊢ₑ e₂ : σ ⇑ E3) → + (Γ ⊢ₖ K : σ ⇑ E4 ⇒ τ) → + (Γ ⊢ₖ IfK e₁ e₂ K : ℕ ⇑ E1 ⇒ τ) + | typed_AppLK Γ E1 E2 E3 E4 v K σ τ α : + (E1 ⊍ E2 ⊍ E3) ⪯ E4 → + (Γ ⊢ᵥ v : σ ⇑ E3) → + (Γ ⊢ₖ K : τ ⇑ E4 ⇒ α) → + (Γ ⊢ₖ AppLK v K : ((σ ⟶ (τ ⇑ E1)) ⇑ E2) ⇒ α) + | typed_AppRK Γ E1 E2 E3 E4 e K σ τ α : + (E1 ⊍ E2 ⊍ E3) ⪯ E4 → + (Γ ⊢ₑ e : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → + (Γ ⊢ₖ K : (τ ⇑ E4) ⇒ α) → + (Γ ⊢ₖ AppRK e K : (σ ⇑ E3) ⇒ α) + | typed_NatOpLK Γ E1 E2 E3 op v K τ : + (E1 ⊍ E2) ⪯ E3 → + (Γ ⊢ᵥ v : ℕ ⇑ E1) → + (Γ ⊢ₖ K : (ℕ ⇑ E3) ⇒ τ) → + (Γ ⊢ₖ NatOpLK op v K : (ℕ ⇑ E2) ⇒ τ) + | typed_NatOpRK Γ E1 E2 E3 op e K τ : + (E1 ⊍ E2) ⪯ E3 → + (Γ ⊢ₑ e : ℕ ⇑ E1) → + (Γ ⊢ₖ K : ℕ ⇑ E3 ⇒ τ) → + (Γ ⊢ₖ NatOpRK op e K : (ℕ ⇑ E2) ⇒ τ) + | typed_ThrowK Γ E1 E2 err K σ τ α : + σ ≲ ETy err → + (E1 ⊕ err) ⪯ E2 → + (Γ ⊢ₖ K : (τ ⇑ E2) ⇒ α) → + (Γ ⊢ₖ ThrowK err K : (σ ⇑ E1) ⇒ α) + | typed_CatchK Γ E1 E2 E3 err h K σ τ τ' α : + ETy err ≲ σ → + τ' ≲ τ → + (E1 ⊍ (E2 ⊖ err)) ⪯ E3 → + (Γ ▹ σ ⊢ₑ h : (τ ⇑ E1)) → + (Γ ⊢ₖ K : (τ ⇑ E3) ⇒ α) → + (Γ ⊢ₖ CatchK err h K : (τ' ⇑ E2) ⇒ α) + + where "Γ '⊢ₖ' K ':' σ ⇒ τ" := (typ_cont Γ K σ τ). + + + Definition typedConfig {S : Set} (Γ : S → pty) (c : @config S) (τ : ty) : Prop := + match c with + | Cexpr e => (Γ ⊢ₑ e : τ) + | Ceval e K => (Γ ⊢ₑ (fill K e) : τ) + | Ccont K v => (Γ ⊢ₑ (fill K (Val v)) : τ) + | Cret v => (Γ ⊢ᵥ v : τ) + end. + + Notation "Γ ⊢ᵢ c : τ" := (typedConfig Γ c τ) + (at level 70 + , c at level 60 + , τ at level 20 + , no associativity + ). + + Lemma weakening {S T : Set} : + ∀ (Γ : S → pty) (Δ : T → pty) (δ : S [→] T) (e : expr S) τ, + (Γ ⊢ₑ e : τ) → + (Δ • δ ≡ Γ) → + (Δ ⊢ₑ (fmap δ e) : τ). + Proof. + intros Γ Δ δ e τ Hty Hag. + generalize dependent T. + induction Hty; intros. + + constructor. specialize (Hag x). simpl in Hag. rewrite Hag. done. + + by constructor. + + econstructor; first done. + apply IHHty. + intros [|[|]]. + 1, 2 : done. + simpl. + apply Hag. + (* + econstructor; try done. + by apply IHHty. *) + + eapply typed_App. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + + econstructor. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + + econstructor. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + * by apply IHHty3. + + eapply typed_Throw; try done. + by apply IHHty. + + econstructor; first done. + * eauto. + * apply IHHty1. + intros [|]; first done. + simpl. apply Hag. + * by apply IHHty2. + Qed. + + Lemma weakening_error {S : Set} : + ∀ (Γ : S → pty) (e : expr S) σ τ, + (Γ ⊢ₑ e : σ) → + σ ⪍ τ → + (Γ ⊢ₑ e : τ). + Proof. + intros Γ e [τ Eτ] σ Hty. + generalize dependent σ. + induction Hty; intros [σ' Eσ'] Hsub; inversion Hsub; subst. + + constructor. by eapply le_pty_trans. + + inversion H2. by constructor. + + econstructor; first by eapply le_pty_trans. done. + (* intros [|[|]]. + 1, 2 : done. + simpl. + apply Hag. + + econstruct or; try done. + by apply IHHty. *) + + eapply typed_App. + * eauto. + * apply IHHty1. + constructor; last eauto. + constructor; first apply le_pty_refl. + constructor; last apply le_set_refl. + done. + * apply IHHty2, le_ty_refl. + + inversion H3. subst. + econstructor. + * eauto. + * by apply IHHty1. + * by apply IHHty2. + + econstructor. + * eauto. + * apply IHHty1, le_ty_refl. + * apply IHHty2. + constructor; last apply le_set_refl. + done. + * by apply IHHty3. + + eapply typed_Throw; try done. + eauto. + + econstructor; first done. + * eauto. + * apply IHHty1. + constructor; last apply le_set_refl. + done. + * apply IHHty2. + constructor; last apply le_set_refl. + done. + Qed. +(* + + Lemma weakening_sub {S: Set} : + ∀ (Γ : S → pty) (Δ : S → pty) (e : expr S) τ, + (Γ ⊢ₑ e : τ) → + (∀ x, Δ x ≲ Γ x) → + (Δ ⊢ₑ e : τ). + Proof. + intros Γ Δ e τ Hty Hag. + induction Hty; intros. + + constructor. eapply le_pty_trans; done. + + by constructor. + + constructor. apply IHHty. + intros [|[|]]. + 1, 2 : term_simpl; apply le_pty_refl. + simpl. + apply Hag. + + econstructor; try done. + by apply IHHty. + + eapply typed_App. + * by apply IHHty1. + * by apply IHHty2. + + constructor. + * by apply IHHty1. + * by apply IHHty2. + + constructor. + * by apply IHHty1. + * by apply IHHty2. + * by apply IHHty3. + + eapply typed_Throw; try done. + by apply IHHty. + + econstructor; first done. + * apply IHHty1. + intros [|]. + { term_simpl. apply le_pty_refl. } + simpl. apply Hag. + * by apply IHHty2. + Qed. + *) + (* + Lemma weakening_errors {S} : ∀ Γ τ1 τ2 (e : expr S), + (Γ ⊢ₑ e : τ1) → + τ1 ⪍ τ2 → + (Γ ⊢ₑ e : τ2). + Proof. + intros. by eapply typed_wk. + revert S. + fix IHHty 7. + intros S Γ [τ1 E1] [τ2 E2] e Hty Hle. + inversion Hty; subst. + - constructor. inversion Hle. subst. by eapply le_pty_trans. + - inversion Hle. subst. inversion H2. subst. constructor. + - inversion Hle. subst. inversion H3. subst. + { done. + constructor. + eapply IHHty; last done. + eapply weakening_sub; first done. + intros [|[|]]. + { done. } + { constructor. + + + intros Γ [τ1 E1] τ2 e Hty. + revert τ2. + induction Hty; intros [τ2 E2] Hτ. + - inversion Hτ. subst. constructor. + inversion Hty; subst. + - by constructor. + - by constructor. + - by constructor. + - econstructor. + { inversion H3; subst. + + constructor. + + } (** eapply IHHty; last done. } **) + { by eapply IHHty. } + - constructor. + { by eapply IHHty. } + { by eapply IHHty. } + - constructor. + { by eapply IHHty. } + { by eapply IHHty. } + { by eapply IHHty. } + - econstructor; first done. + { by apply HE. } + by eapply IHHty. + - econstructor; first done. + { by eapply IHHty. } + { eapply IHHty; first done. intros x [|]; auto. } + Qed. + *) + Lemma substitution_lemma {S : Set}: + ∀ (e : expr S) (E : exc → Prop) T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) + → (∀ (x : S), Δ ⊢ₑ γ x : Γ x ⇑ ⋆) + → ( Δ ⊢ₑ bind γ e : τ ⇑ E). + Proof. + - revert S. + intros S e E T Γ Δ γ τ Hty. + generalize dependent T. + induction Hty; intros. + + term_simpl. + subst. + eapply weakening_error; first done. + by constructor. + + term_simpl. constructor. + + term_simpl. econstructor; first done. + * apply IHHty. + intros [|[|]]. + { constructor. simpl. apply le_pty_refl. } + { constructor. apply le_pty_refl. } + term_simpl. + eapply (weakening (Δ ▹ σ ⟶ τ0)). + { eapply weakening; done.} + done. + + term_simpl. + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + + term_simpl. + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + + term_simpl. + econstructor; first done. + * by apply IHHty1. + * by apply IHHty2. + * by apply IHHty3. + + term_simpl. + econstructor; try done. + by apply IHHty. + + term_simpl. + econstructor; try done. + * apply IHHty1. + intros [|]. + { term_simpl. constructor. apply le_pty_refl. } + { term_simpl. eapply weakening; last done. apply H1. } + * by apply IHHty2. + Qed. + + + Lemma weakening_cont {S T : Set} : + ∀ (Γ : S → pty) (Δ : T → pty) (δ : S [→] T) (K : cont S) σ τ, + (Γ ⊢ₖ K : σ ⇒ τ) → + (Δ • δ ≡ Γ) → + (Δ ⊢ₖ (fmap δ K) : σ ⇒ τ). + Proof. + intros Γ Δ δ e σ τ Hty Hag. + generalize dependent T. + induction Hty; intros. + - term_simpl. by constructor. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + change (Val (fmap δ v)) with (fmap δ (Val v)). + by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + change (Val (fmap δ v)) with (fmap δ (Val v)). + by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : by eapply weakening. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + all : done. + - term_simpl. econstructor; last by eapply IHHty. + { eauto. } + { done. } + { done. } + eapply weakening; first done. + intros [|]; first done. + apply Hag. + Qed. + + Lemma weakening_error_cont {S : Set} : + ∀ (Γ : S → pty) (K : cont S) σ1 σ2 τ1 τ2, + (Γ ⊢ₖ K : σ1 ⇒ τ1) → + σ2 ⪍ σ1 → + τ1 ⪍ τ2 → + (Γ ⊢ₖ K : σ2 ⇒ τ2). + Proof. + intros Γ K [σ1 Eσ1] σ2 [τ1 Eτ1] τ2 Hty. + revert σ2 τ2. + induction Hty; intros [σ' Eσ'] [ρ Eρ] Hσ Hτ. + - constructor. eapply le_ty_trans; first done. + by eapply le_ty_trans. + - inversion Hσ. subst. inversion H5. subst. + econstructor; last apply IHHty. + { intros ? [[|]|]; apply H. + * left. left. by apply H7. + * left. right. apply H2. + * right. apply H2. } + all : try done. + constructor; first by apply le_pty_refl. + eauto. + - inversion Hσ. subst. inversion H4. subst. + inversion H7. subst. + econstructor; last apply IHHty. + { intros ? [[|]|]; apply H. + * left. left. by apply H9. + * left. right. by apply H6. + * right. apply H1. } + all : try done. + by eapply weakening_error. + + - inversion Hσ. subst. + econstructor; last eapply IHHty. + { intros ? [[|]|]; apply H. + * left. by left. + * left. by right. + * right. eauto. + } + all : try done. + + eapply weakening_error; first done. + constructor; last by apply le_set_refl. + constructor; first done. + apply le_ty_refl. + + constructor; last by eauto. + apply le_pty_refl. + - inversion Hσ. subst. + inversion H4. subst. + econstructor; last by apply IHHty. + { intros ? [|]; apply H. + * left. apply H1. + * right. eauto. + } + done. + - inversion Hσ. subst. + inversion H4. subst. + econstructor; last by apply IHHty. + { intros ? [|]; apply H. + * left. apply H1. + * right. eauto. + } + done. + - inversion Hσ. subst. + econstructor; first by eapply le_pty_trans. + { intros ? [|]; apply H0. + * by left. + * right. eauto. + } + apply IHHty. + + constructor; first by apply le_pty_refl. + eauto. + + done. + - inversion Hσ. subst. + inversion Hτ. subst. + econstructor. + { done. } + { by eapply le_pty_trans. } + { intros ? [|]; apply H1. + * by left. + * right. destruct H3. split; eauto. + } + { done. } + apply IHHty; last done. + constructor; last by apply le_set_refl. + apply le_pty_refl. + Qed. + + Lemma fill_bind_bind {S T}: ∀ (δ : S [⇒] T) K e, fill (bind δ K) (bind δ e) = bind δ (fill K e). + Proof. + intros δ K. + revert δ. + induction K; first done; + term_simpl; intros; + change (BindCore_expr _ _ δ (fill K ?e) ) with (bind δ (fill K e)); + rewrite -IHK; + done. + Qed. + + Lemma fill_bind_subst {S}: ∀ (K : cont S) e e', fill K (subst e e') = subst (fill (shift K) e) e'. + Proof. + intros K. + induction K; + try done; + term_simpl; intros; + change (BindCore_expr _ _ (mk_subst ?e') (fill (shift K) ?e) ) with (subst (fill (shift K) e) e'); + rewrite -IHK; + term_simpl; try done. + repeat f_equal. + by rewrite subst_shift_id_lifted. + Qed. + + Lemma decomp_types {S} : ∀ (K : cont S) e Γ τ, (Γ ⊢ₑ fill K e : τ) + → ∃ α, (Γ ⊢ₑ e : α) ∧ (Γ ⊢ₖ K : α ⇒ τ). + Proof. + intros K. + induction K; + intros e' Γ τ Hty. + - exists τ. + split; first done. + constructor. + apply le_ty_refl. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + by econstructor. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + by econstructor. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; last done; done. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; last done; last done. intros. apply H3. rewrite or_comm. done. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; last done; done. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + by econstructor. + - simpl in Hty. + apply IHK in Hty as (α & Hα & HK). + inversion Hα; subst. + eexists. + split; first done. + econstructor; try done. + apply le_pty_refl. + Qed. + + Lemma fill_types {S : Set} : + ∀ (K : cont S) e Γ σ τ, + (Γ ⊢ₖ K : σ ⇒ τ ) → + (Γ ⊢ₑ e : σ) → + (Γ ⊢ₑ fill K e : τ). + Proof. + intros K. + induction K; intros e' Γ σ τ HK He'; inversion HK; subst. + { term_simpl. by eapply weakening_error. } + 4 : { simpl. eapply IHK; first done. econstructor; last done; last done. intros. apply H3. by apply or_comm. } + all: simpl; + eapply IHK; try done; + try econstructor; try done. + by eapply weakening_error. + Qed. + + Lemma compose_END_left {S} : ∀ (K : cont S), cont_compose END K = K. + Proof. + intros K. + induction K. + { done. } + all : simpl; by rewrite IHK. + Qed. + + Lemma compose_type {S} : ∀ (K K1 K2 : cont S) Γ σ τ, + (Γ ⊢ₖ K : σ ⇒ τ) → + K = cont_compose K1 K2 → + ∃ α, (Γ ⊢ₖ K1 : α ⇒ τ) ∧ (Γ ⊢ₖ K2 : σ ⇒ α). + Proof. + intros K K1 K2 Γ σ τ HK. + revert K1 K2. + induction HK; intros K1 K2 Heq. + - destruct K1, K2 ; try discriminate. + eexists. split; econstructor; try done. apply le_ty_refl. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α & HK1 & HK2). + eexists. split; first done. by econstructor. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). + eexists. split; first done. by econstructor. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). + eexists. split; first done. by econstructor. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α & HK1 & HK2). + eexists. split; first done. by econstructor. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α & HK1 & HK2). + eexists. split; first done. by econstructor. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). + eexists. split; first done. by econstructor. + - destruct K2; try discriminate. + + simpl in Heq. subst. + eexists. split; econstructor; try done. apply le_ty_refl. + + injection Heq. intros. subst. + destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). + eexists. split; first done. by econstructor. + Qed. + + Lemma less_errors_catch {S} : + ∀ (K : cont S) Γ σ τ E1 E2 err, + (Γ ⊢ₖ K : (σ ⇑ E1) ⇒ (τ ⇑ E2)) → + E1 err ∧ ¬ E2 err → + ∃ K1 K2 h, K = cont_compose (CatchK err h K1) K2. + Proof. + intros K. + induction K; intros Γ σ τ E1 E2 err0 Hty [HE1 HE2]; inversion Hty; subst. + - contradict HE2. inversion H. subst. eauto. + - apply (IHK _ _ _ _ _ err0) in H9 as (K1 & K2 & h & ->); last eauto. + by exists K1, (IfK e₁ e₂ K2), h. + - apply (IHK _ _ _ _ _ err0) in H7 as (K1 & K2 & h & ->); last eauto. + by exists K1, (AppLK v K2), h. + - apply (IHK _ _ _ _ _ err0) in H7 as (K1 & K2 & h & ->); last eauto. + by exists K1, (AppRK e K2), h. + - apply (IHK _ _ _ _ _ err0) in H8 as (K1 & K2 & h & ->); last eauto. + by exists K1, (NatOpLK op v K2), h. + - apply (IHK _ _ _ _ _ err0) in H8 as (K1 & K2 & h & ->); last eauto. + by exists K1, (NatOpRK op e K2), h. + - apply (IHK _ _ _ _ _ err0) in H7 as (K1 & K2 & h & ->); last eauto. + by exists K1, (ThrowK err K2), h. + - destruct (eq_dec err err0) as [-> | Hdiff]. + + by exists K, END, h. + + apply (IHK _ _ _ _ _ err0) in H10 as (K1 & K2 & h0 & ->); last eauto. + by exists K1, (CatchK err h K2), h0. + Qed. + + Lemma preservation {S} : + ∀ Γ τ1 (c c' : @config S) n, + (Γ ⊢ᵢ c : τ1) → + c ===> c' / n → + ∃ τ2, τ2 ⪍ τ1 ∧ (Γ ⊢ᵢ c' : τ2). + Proof. + intros Γ τ c c' n Hty Hred. + revert Γ τ Hty. + induction Hred; intros Γ [τ Eτ] Hty; simpl; eexists; try (split; try done; apply le_ty_refl). + - simpl in *. + split; last first. + + do 2 rewrite fill_bind_subst. + apply decomp_types in Hty as (α & Hα & HK). + inversion Hα. subst. + inversion H3. subst. + inversion H6. subst. + eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1))). + * eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1) ▹ σ0)). + -- eapply fill_types. + { eapply (weakening_cont (Γ ▹ (σ0 ⟶ τ1))). + { eapply weakening_cont. + 2 : instantiate (1 := Γ); done. + apply HK. + } + done. + } + eapply weakening_error; first by apply H7. + eapply le_ty_trans; first done. + constructor; first by apply le_pty_refl. + eauto. + -- intros [|[|]]; term_simpl. + { unfold shift. + change (Val (fmap ?δ ?v)) with (fmap δ (Val v)). + eapply weakening; last by instantiate (1 := Γ). + inversion H5; subst. + + inversion H4. constructor. + + inversion H10. subst. inversion H4. subst. econstructor; last done. + constructor; first by eapply le_pty_trans. + by eapply le_ty_trans. + } + { constructor. apply le_pty_refl. } + { constructor. apply le_pty_refl. } + * intros [|]; term_simpl; first econstructor; try done. + { apply le_pty_refl. } + constructor. apply le_pty_refl. + + apply le_ty_refl. + - apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + split; first last. + + eapply fill_types; first done. + destruct n; simpl; eapply weakening_error; try done; constructor; try apply le_pty_refl; eauto. + + apply le_ty_refl. + - destruct v1, v2; try discriminate. + simpl in H. injection H as <-. + apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + split; first last. + + eapply fill_types; first done. + constructor. + + apply le_ty_refl. + - apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + split; first last. + + eapply fill_types; first done. + inversion Hα; subst. + { inversion H3. constructor. } + { econstructor; last done. by eapply le_pty_trans. } + + apply le_ty_refl. + - apply decomp_types in Hty as [α [Hα HK]]. + inversion HK. subst. + apply unwind_decompose in H as (K1 & Hkcomp & HK1). + destruct (compose_type _ _ _ _ _ _ H7 Hkcomp) as (α & HK2 & HK3). + inversion HK2. subst. + split; first last. + + eapply fill_types; first last. + * eapply substitution_lemma; first done. + -- intros [|]; term_simpl. + { inversion Hα; subst. + - inversion H2. rewrite -H in H3. inversion H3. subst. constructor. + - inversion H9. subst. inversion H2. rewrite -H6 in H3. subst. + inversion H3. subst. + econstructor; last done. + constructor. + + eapply le_pty_trans; first done. + by eapply le_pty_trans. + + eapply le_ty_trans; first done. + by eapply le_ty_trans. + } + constructor. + apply le_pty_refl. + * eapply weakening_error_cont; first done. + { constructor; first by apply le_pty_refl. eauto. } + eapply le_ty_refl. + + eapply le_ty_refl. + Qed. + + Lemma progress : ∀ (c : config) τ, (□ ⊢ᵢ c : τ ⇑ ⋆) → (∃ (v : val ∅), c = Cret v) ∨ (∃ c' n, c ===> c' / n). + Proof. + intros c τ Hty. + destruct c. + - right. eexists _, _. constructor. + - right. destruct c, v; try destruct v0; + try (apply decomp_types in Hty as (α & H1 & H2); + inversion H2; subst; + inversion H1; subst). + 1-3, 5-9,13,17,18 : eexists _, _; by constructor. + 6,7 : eapply less_errors_catch in H8 as (K1 & K2 & h & HK); eauto; + apply unwind_decompose_weak in HK as (? & ? & ?); + eexists _,_; + by constructor. + + inversion H7. + + inversion H8. inversion H6. + + inversion H6. + + inversion H6. + + inversion H6. + - destruct e; right. + 2 : by inversion Hty. + all : eexists _,_ ; try constructor. + - left. eexists. done. + Qed. + + + From cb27c8397da154440c00d8f17e7a07e798ce136f Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 12 Jul 2024 13:43:58 +0200 Subject: [PATCH 08/16] Progress and preservation for except_lang --- theories/examples/except_lang/typing.v | 198 ++++++------------------- 1 file changed, 45 insertions(+), 153 deletions(-) diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index 87ddc69..0116ba8 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -3,7 +3,6 @@ From gitrees.examples.except_lang Require Import lang. Require Import Binding.Lib Binding.Set Binding.Env. Require Import Coq.Program.Equality. - Module Typing (Errors : ExcSig). Module _LANG := Lang Errors. Import _LANG. @@ -15,7 +14,6 @@ Module Typing (Errors : ExcSig). | Barr : bty → bty → bty . - (** Types indicating possible errors raised **) Inductive pty : Type := | Tnat : pty @@ -169,15 +167,10 @@ Module Typing (Errors : ExcSig). | typed_Lit Γ E v : (Γ ⊢ᵥ (LitV v) : ℕ ⇑ E) | typed_Rec Γ E f σ τ α : - (σ ⟶ τ) ≲ α→ + (σ ⟶ τ) ≲ α → (Γ ▹ (σ ⟶ τ) ▹ σ ⊢ₑ f : τ) → (Γ ⊢ᵥ (RecV f) : α ⇑ E) - (* | typed_wk Γ τ1 τ2 e : - τ1 ⪍ τ2 → - (Γ ⊢ₑ e : τ1) → - (Γ ⊢ₑ e : τ2) *) - | typed_App E E1 E2 E3 Γ f v σ τ : (E1 ⊍ E2 ⊍ E3) ⪯ E → (Γ ⊢ₑ f : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → @@ -211,8 +204,8 @@ Module Typing (Errors : ExcSig). (Γ ⊢ₑ Catch err v h : τ ⇑ E) where "Γ ⊢ₑ e : τ" := (typed Γ e τ) - and "Γ ⊢ᵥ v : τ" := (Γ ⊢ₑ (Val v) : τ). - Print cont. + and "Γ ⊢ᵥ v : τ" := (Γ ⊢ₑ (Val v) : τ). + Reserved Notation "Γ '⊢ₖ' K ':' σ ⇒ τ" (at level 70 , K at level 60 @@ -223,12 +216,6 @@ Module Typing (Errors : ExcSig). Inductive typ_cont {S : Set} : (S → pty) → cont S → ty → ty → Prop := - (* | typed_Err_Wk E1 E2 E3 Γ e σ τ : E1 ⪯ E2 → - (Γ ; E1 ⊢ₖ e : σ ; E3 ⇒ τ) → - (Γ ; E2 ⊢ₖ e : σ ; E3 ⇒ τ) - | typed_Err_St E1 E2 E3 Γ e σ τ : E3 ⪯ E2 → - (Γ ; E1 ⊢ₖ e : σ ; E2 ⇒ τ) → - (Γ ; E1 ⊢ₖ e : σ ; E3 ⇒ τ) *) | typed_END Γ τ1 τ2 : τ1 ⪍ τ2 → (Γ ⊢ₖ END : τ1 ⇒ τ2) | typed_IfK Γ e₁ e₂ K E1 E2 E3 E4 τ σ : @@ -305,8 +292,6 @@ Module Typing (Errors : ExcSig). 1, 2 : done. simpl. apply Hag. - (* + econstructor; try done. - by apply IHHty. *) + eapply typed_App. * eauto. * by apply IHHty1. @@ -342,12 +327,6 @@ Module Typing (Errors : ExcSig). + constructor. by eapply le_pty_trans. + inversion H2. by constructor. + econstructor; first by eapply le_pty_trans. done. - (* intros [|[|]]. - 1, 2 : done. - simpl. - apply Hag. - + econstruct or; try done. - by apply IHHty. *) + eapply typed_App. * eauto. * apply IHHty1. @@ -379,7 +358,6 @@ Module Typing (Errors : ExcSig). constructor; last apply le_set_refl. done. Qed. -(* Lemma weakening_sub {S: Set} : ∀ (Γ : S → pty) (Δ : S → pty) (e : expr S) τ, @@ -391,87 +369,34 @@ Module Typing (Errors : ExcSig). induction Hty; intros. + constructor. eapply le_pty_trans; done. + by constructor. - + constructor. apply IHHty. + + econstructor; first done. + apply IHHty. intros [|[|]]. 1, 2 : term_simpl; apply le_pty_refl. simpl. apply Hag. - + econstructor; try done. - by apply IHHty. - + eapply typed_App. + + econstructor; first done. * by apply IHHty1. * by apply IHHty2. - + constructor. + + econstructor; first done. * by apply IHHty1. * by apply IHHty2. - + constructor. + + econstructor; first done. * by apply IHHty1. * by apply IHHty2. * by apply IHHty3. + eapply typed_Throw; try done. by apply IHHty. - + econstructor; first done. + + econstructor; try done. * apply IHHty1. intros [|]. { term_simpl. apply le_pty_refl. } simpl. apply Hag. * by apply IHHty2. Qed. - *) - (* - Lemma weakening_errors {S} : ∀ Γ τ1 τ2 (e : expr S), - (Γ ⊢ₑ e : τ1) → - τ1 ⪍ τ2 → - (Γ ⊢ₑ e : τ2). - Proof. - intros. by eapply typed_wk. - revert S. - fix IHHty 7. - intros S Γ [τ1 E1] [τ2 E2] e Hty Hle. - inversion Hty; subst. - - constructor. inversion Hle. subst. by eapply le_pty_trans. - - inversion Hle. subst. inversion H2. subst. constructor. - - inversion Hle. subst. inversion H3. subst. - { done. - constructor. - eapply IHHty; last done. - eapply weakening_sub; first done. - intros [|[|]]. - { done. } - { constructor. - - - intros Γ [τ1 E1] τ2 e Hty. - revert τ2. - induction Hty; intros [τ2 E2] Hτ. - - inversion Hτ. subst. constructor. - inversion Hty; subst. - - by constructor. - - by constructor. - - by constructor. - - econstructor. - { inversion H3; subst. - + constructor. - - } (** eapply IHHty; last done. } **) - { by eapply IHHty. } - - constructor. - { by eapply IHHty. } - { by eapply IHHty. } - - constructor. - { by eapply IHHty. } - { by eapply IHHty. } - { by eapply IHHty. } - - econstructor; first done. - { by apply HE. } - by eapply IHHty. - - econstructor; first done. - { by eapply IHHty. } - { eapply IHHty; first done. intros x [|]; auto. } - Qed. - *) - Lemma substitution_lemma {S : Set}: - ∀ (e : expr S) (E : exc → Prop) T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) + + Lemma substitution_lemma {S : Set}: + ∀ (e : expr S) (E : exc → Prop) T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) → (∀ (x : S), Δ ⊢ₑ γ x : Γ x ⇑ ⋆) → ( Δ ⊢ₑ bind γ e : τ ⇑ E). Proof. @@ -491,7 +416,7 @@ Module Typing (Errors : ExcSig). { constructor. apply le_pty_refl. } term_simpl. eapply (weakening (Δ ▹ σ ⟶ τ0)). - { eapply weakening; done.} + { eapply weakening; done. } done. + term_simpl. econstructor; first done. @@ -517,7 +442,6 @@ Module Typing (Errors : ExcSig). { term_simpl. eapply weakening; last done. apply H1. } * by apply IHHty2. Qed. - Lemma weakening_cont {S T : Set} : ∀ (Γ : S → pty) (Δ : T → pty) (δ : S [→] T) (K : cont S) σ τ, @@ -755,52 +679,16 @@ Module Typing (Errors : ExcSig). intros K K1 K2 Γ σ τ HK. revert K1 K2. induction HK; intros K1 K2 Heq. - - destruct K1, K2 ; try discriminate. - eexists. split; econstructor; try done. apply le_ty_refl. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α & HK1 & HK2). - eexists. split; first done. by econstructor. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). - eexists. split; first done. by econstructor. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). - eexists. split; first done. by econstructor. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α & HK1 & HK2). - eexists. split; first done. by econstructor. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α & HK1 & HK2). - eexists. split; first done. by econstructor. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). - eexists. split; first done. by econstructor. - - destruct K2; try discriminate. - + simpl in Heq. subst. - eexists. split; econstructor; try done. apply le_ty_refl. - + injection Heq. intros. subst. - destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2). - eexists. split; first done. by econstructor. + { destruct K1, K2 ; try discriminate. + eexists. split; econstructor; try done. apply le_ty_refl. } + all: destruct K2; try discriminate; [ + simpl in Heq; subst; + eexists; split; econstructor; try done; apply le_ty_refl + | injection Heq; intros; subst; + destruct (IHHK K1 K2 eq_refl) as (α0 & HK1 & HK2); + eexists; split; first done; by econstructor]. Qed. - + Lemma less_errors_catch {S} : ∀ (K : cont S) Γ σ τ E1 E2 err, (Γ ⊢ₖ K : (σ ⇑ E1) ⇒ (τ ⇑ E2)) → @@ -808,27 +696,21 @@ Module Typing (Errors : ExcSig). ∃ K1 K2 h, K = cont_compose (CatchK err h K1) K2. Proof. intros K. - induction K; intros Γ σ τ E1 E2 err0 Hty [HE1 HE2]; inversion Hty; subst. - - contradict HE2. inversion H. subst. eauto. - - apply (IHK _ _ _ _ _ err0) in H9 as (K1 & K2 & h & ->); last eauto. - by exists K1, (IfK e₁ e₂ K2), h. - - apply (IHK _ _ _ _ _ err0) in H7 as (K1 & K2 & h & ->); last eauto. - by exists K1, (AppLK v K2), h. - - apply (IHK _ _ _ _ _ err0) in H7 as (K1 & K2 & h & ->); last eauto. - by exists K1, (AppRK e K2), h. - - apply (IHK _ _ _ _ _ err0) in H8 as (K1 & K2 & h & ->); last eauto. - by exists K1, (NatOpLK op v K2), h. - - apply (IHK _ _ _ _ _ err0) in H8 as (K1 & K2 & h & ->); last eauto. - by exists K1, (NatOpRK op e K2), h. - - apply (IHK _ _ _ _ _ err0) in H7 as (K1 & K2 & h & ->); last eauto. - by exists K1, (ThrowK err K2), h. + induction K; intros Γ σ τ E1 E2 err0 Hty [HE1 HE2]; inversion Hty; subst; + match goal with + | H : (Γ ⊢ₖ K : _ ⇒ _) |- ∃ _ _ _, (?C _) = _ => + apply (IHK _ _ _ _ _ err0) in H as (K1 & K2 & h & ->); + [by exists K1, (C K2), h | eauto] + | _ => idtac + end. + - inversion H. subst. contradict HE2. eauto. - destruct (eq_dec err err0) as [-> | Hdiff]. + by exists K, END, h. + apply (IHK _ _ _ _ _ err0) in H10 as (K1 & K2 & h0 & ->); last eauto. by exists K1, (CatchK err h K2), h0. Qed. - Lemma preservation {S} : + Lemma preservation_wk {S} : ∀ Γ τ1 (c c' : @config S) n, (Γ ⊢ᵢ c : τ1) → c ===> c' / n → @@ -924,6 +806,17 @@ Module Typing (Errors : ExcSig). + eapply le_ty_refl. Qed. + Lemma preservation {S} : + ∀ Γ τ1 (c c' : @config S) n, + (Γ ⊢ᵢ c : τ1) → + c ===> c' / n → + (Γ ⊢ᵢ c' : τ1). + Proof. + intros. + apply (preservation_wk _ _ _ _ _ H) in H0 as (? & ? & ?). + destruct c'; by eapply weakening_error. + Qed. + Lemma progress : ∀ (c : config) τ, (□ ⊢ᵢ c : τ ⇑ ⋆) → (∃ (v : val ∅), c = Cret v) ∨ (∃ c' n, c ===> c' / n). Proof. intros c τ Hty. @@ -947,7 +840,6 @@ Module Typing (Errors : ExcSig). 2 : by inversion Hty. all : eexists _,_ ; try constructor. - left. eexists. done. - Qed. - - - + Qed. + +End Typing. From 9b4b1a4193e2742bcc76fcb7be17565390f7c85e Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 12 Jul 2024 14:47:10 +0200 Subject: [PATCH 09/16] Made exception type required to be countable and made use of gsets in except_lang/typing.v --- theories/effects/exceptions.v | 21 ++- theories/examples/except_lang/typing.v | 173 ++++++++++--------------- 2 files changed, 91 insertions(+), 103 deletions(-) diff --git a/theories/effects/exceptions.v b/theories/effects/exceptions.v index 819584d..bcc46b0 100644 --- a/theories/effects/exceptions.v +++ b/theories/effects/exceptions.v @@ -3,7 +3,8 @@ From iris.algebra Require Import list. Module Type ExcSig. Parameter E : Set. - Parameter eq_dec_E : ∀ (x y : E), {x = y} + {x <> y}. + Parameter eq_dec_E : EqDecision E. + Parameter countable_E : @Countable E eq_dec_E. End ExcSig. Module Exc (Errors : ExcSig). @@ -11,12 +12,28 @@ Module Exc (Errors : ExcSig). Structure exc := Exc { value : E }. - Theorem eq_dec : ∀ (x y : exc), {x = y} + {x <> y}. + #[global] Instance eq_dec : EqDecision exc. intros [x] [y]. destruct (eq_dec_E x y) as [<-|HDiff]. - left. reflexivity. - right. intros Heq. injection Heq as <-. apply HDiff. reflexivity. Defined. + + #[global] Instance countable_exc : Countable exc. + Proof. + refine (Build_Countable _ _ ?[encode] ?[decode] _). + [encode] : { intros [e]. + exact ((@encode _ _ countable_E) e). + } + [decode] : { intros p. + destruct ((@decode _ _ countable_E) p) as [e|]. + - exact (Some (Exc e)). + - exact None. + } + intros [e]. + simpl. + by rewrite (@decode_encode _ _ countable_E). + Defined. Canonical Structure excO := leibnizO exc. Definition excOF := constOF exc. diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index 0116ba8..b091683 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -19,7 +19,7 @@ Module Typing (Errors : ExcSig). | Tnat : pty | Tarr : pty → ty → pty with ty : Type := - Ty : pty → (exc → Prop) → ty. + Ty : pty → gmap.gset exc → ty. Context (ETy : exc → pty). Notation "'ℕ'" := Tnat. @@ -29,12 +29,6 @@ Module Typing (Errors : ExcSig). (at level 20, E at level 20, no associativity). - Notation "E1 ⪯ E2" := (∀ x, E1 x → E2 x) - (at level 20, - no associativity, - only parsing). - - Notation "⋆" := (λ _, False). Reserved Notation "τ '≲' σ" (at level 20). @@ -51,21 +45,11 @@ Module Typing (Errors : ExcSig). with le_ty : ty → ty → Prop := Le_Ty τ1 τ2 E1 E2 : τ1 ≲ τ2 → - E1 ⪯ E2 → + E1 ⊆ E2 → (τ1 ⇑ E1) ⪍ (τ2 ⇑ E2) where "τ ≲ σ" := (le_pty τ σ) and "τ ⪍ σ" := (le_ty τ σ). - Notation "E1 ≋ E2" := (∀ x, E1 x ↔ E2 x) - (at level 20, - no associativity). - - Lemma le_set_trans {A} : ∀ (E1 E2 E3 : A → Prop), E1 ⪯ E2 → E2 ⪯ E3 → E1 ⪯ E3. - Proof. eauto. Qed. - - Lemma le_set_refl {A} : ∀ (E : A → Prop), E ⪯ E. - Proof. eauto. Qed. - Lemma le_pty_trans : ∀ τ1 τ2 τ3, τ1 ≲ τ2 → τ2 ≲ τ3 → τ1 ≲ τ3 with le_ty_trans : ∀ τ1 τ2 τ3, τ1 ⪍ τ2 → τ2 ⪍ τ3 → τ1 ⪍ τ3. Proof. @@ -87,7 +71,7 @@ Module Typing (Errors : ExcSig). inversion H2. subst. constructor. + by eapply le_pty_trans. - + by eapply le_set_trans. + + set_solver. Qed. Lemma le_pty_refl : ∀ τ, τ ≲ τ @@ -100,7 +84,7 @@ Module Typing (Errors : ExcSig). - intros [τ E]. constructor. + apply le_pty_refl. - + apply le_set_refl. + + reflexivity. Qed. (** Compatibility between types and bare types **) @@ -137,15 +121,11 @@ Module Typing (Errors : ExcSig). + by eapply (le_ty_compat t). Qed. - Notation "E ⊕ e" := (λ x, x = e ∨ E x) + Notation "E ⊕ e" := (E ∪ {[e]}) (at level 20). - - Notation "E ⊖ e" := (λ x, x <> e ∧ E x) + Notation "E ⊖ e" := (E ∖ {[e]}) (at level 20). - Notation "E1 ⊍ E2" := (λ x, E1 x ∨ E2 x) - (at level 20). - Reserved Notation "Γ '⊢ₑ' e ':' τ" (at level 70 , e at level 60 @@ -159,7 +139,6 @@ Module Typing (Errors : ExcSig). , τ at level 20 , no associativity ). - Inductive typed {S : Set} : (S → pty) → expr S → ty → Prop := | typed_Var Γ E x τ : Γ x ≲ τ → (Γ ⊢ₑ (Var x) : τ ⇑ E) @@ -172,19 +151,19 @@ Module Typing (Errors : ExcSig). (Γ ⊢ᵥ (RecV f) : α ⇑ E) | typed_App E E1 E2 E3 Γ f v σ τ : - (E1 ⊍ E2 ⊍ E3) ⪯ E → + (E1 ∪ E2 ∪ E3) ⊆ E → (Γ ⊢ₑ f : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → (Γ ⊢ₑ v : σ ⇑ E3) → (Γ ⊢ₑ App f v : τ ⇑ E) | typed_Op Γ E E1 E2 op l r : - (E1 ⊍ E2) ⪯ E → + (E1 ∪ E2) ⊆ E → (Γ ⊢ₑ l : ℕ ⇑ E1) → (Γ ⊢ₑ r : ℕ ⇑ E2) → (Γ ⊢ₑ NatOp op l r : ℕ ⇑ E) | typed_If Γ E E1 E2 E3 c t e τ : - (E1 ⊍ E2 ⊍ E3) ⪯ E→ + (E1 ∪ E2 ∪ E3) ⊆ E→ (Γ ⊢ₑ c : ℕ ⇑ E1) → (Γ ⊢ₑ t : τ ⇑ E2) → (Γ ⊢ₑ e : τ ⇑ E3) → @@ -192,13 +171,13 @@ Module Typing (Errors : ExcSig). | typed_Throw Γ E1 E2 err v σ τ : σ ≲ ETy err → - (E1 ⊕ err) ⪯ E2 → + (E1 ⊕ err) ⊆ E2 → (Γ ⊢ₑ v : σ ⇑ E1) → (Γ ⊢ₑ Throw err v : τ ⇑ E2) | typed_Catch Γ E E1 E2 err h v σ τ : ETy err ≲ σ → - (E1 ⊍ (E2 ⊖ err)) ⪯ E → + (E1 ∪ (E2 ⊖ err)) ⊆ E → (Γ ▹ σ ⊢ₑ h : τ ⇑ E1) → (Γ ⊢ₑ v : τ ⇑ E2) → (Γ ⊢ₑ Catch err v h : τ ⇑ E) @@ -219,40 +198,40 @@ Module Typing (Errors : ExcSig). | typed_END Γ τ1 τ2 : τ1 ⪍ τ2 → (Γ ⊢ₖ END : τ1 ⇒ τ2) | typed_IfK Γ e₁ e₂ K E1 E2 E3 E4 τ σ : - (E1 ⊍ E2 ⊍ E3) ⪯ E4 → + (E1 ∪ E2 ∪ E3) ⊆ E4 → (Γ ⊢ₑ e₁ : σ ⇑ E2) → (Γ ⊢ₑ e₂ : σ ⇑ E3) → (Γ ⊢ₖ K : σ ⇑ E4 ⇒ τ) → (Γ ⊢ₖ IfK e₁ e₂ K : ℕ ⇑ E1 ⇒ τ) | typed_AppLK Γ E1 E2 E3 E4 v K σ τ α : - (E1 ⊍ E2 ⊍ E3) ⪯ E4 → + (E1 ∪ E2 ∪ E3) ⊆ E4 → (Γ ⊢ᵥ v : σ ⇑ E3) → (Γ ⊢ₖ K : τ ⇑ E4 ⇒ α) → (Γ ⊢ₖ AppLK v K : ((σ ⟶ (τ ⇑ E1)) ⇑ E2) ⇒ α) | typed_AppRK Γ E1 E2 E3 E4 e K σ τ α : - (E1 ⊍ E2 ⊍ E3) ⪯ E4 → + (E1 ∪ E2 ∪ E3) ⊆ E4 → (Γ ⊢ₑ e : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → (Γ ⊢ₖ K : (τ ⇑ E4) ⇒ α) → (Γ ⊢ₖ AppRK e K : (σ ⇑ E3) ⇒ α) | typed_NatOpLK Γ E1 E2 E3 op v K τ : - (E1 ⊍ E2) ⪯ E3 → + (E1 ∪ E2) ⊆ E3 → (Γ ⊢ᵥ v : ℕ ⇑ E1) → (Γ ⊢ₖ K : (ℕ ⇑ E3) ⇒ τ) → (Γ ⊢ₖ NatOpLK op v K : (ℕ ⇑ E2) ⇒ τ) | typed_NatOpRK Γ E1 E2 E3 op e K τ : - (E1 ⊍ E2) ⪯ E3 → + (E1 ∪ E2) ⊆ E3 → (Γ ⊢ₑ e : ℕ ⇑ E1) → (Γ ⊢ₖ K : ℕ ⇑ E3 ⇒ τ) → (Γ ⊢ₖ NatOpRK op e K : (ℕ ⇑ E2) ⇒ τ) | typed_ThrowK Γ E1 E2 err K σ τ α : σ ≲ ETy err → - (E1 ⊕ err) ⪯ E2 → + (E1 ⊕ err) ⊆ E2 → (Γ ⊢ₖ K : (τ ⇑ E2) ⇒ α) → (Γ ⊢ₖ ThrowK err K : (σ ⇑ E1) ⇒ α) | typed_CatchK Γ E1 E2 E3 err h K σ τ τ' α : ETy err ≲ σ → τ' ≲ τ → - (E1 ⊍ (E2 ⊖ err)) ⪯ E3 → + (E1 ∪ (E2 ⊖ err)) ⊆ E3 → (Γ ▹ σ ⊢ₑ h : (τ ⇑ E1)) → (Γ ⊢ₖ K : (τ ⇑ E3) ⇒ α) → (Γ ⊢ₖ CatchK err h K : (τ' ⇑ E2) ⇒ α) @@ -328,35 +307,31 @@ Module Typing (Errors : ExcSig). + inversion H2. by constructor. + econstructor; first by eapply le_pty_trans. done. + eapply typed_App. - * eauto. + * by etrans. * apply IHHty1. constructor; last eauto. constructor; first apply le_pty_refl. - constructor; last apply le_set_refl. - done. + by constructor. * apply IHHty2, le_ty_refl. + inversion H3. subst. econstructor. - * eauto. + * by etrans. * by apply IHHty1. * by apply IHHty2. + econstructor. - * eauto. + * by etrans. * apply IHHty1, le_ty_refl. * apply IHHty2. - constructor; last apply le_set_refl. - done. + by constructor. * by apply IHHty3. + eapply typed_Throw; try done. - eauto. + by etrans. + econstructor; first done. - * eauto. + * by etrans. * apply IHHty1. - constructor; last apply le_set_refl. - done. + by constructor. * apply IHHty2. - constructor; last apply le_set_refl. - done. + by constructor. Qed. Lemma weakening_sub {S: Set} : @@ -394,10 +369,11 @@ Module Typing (Errors : ExcSig). simpl. apply Hag. * by apply IHHty2. Qed. - + + Lemma substitution_lemma {S : Set}: - ∀ (e : expr S) (E : exc → Prop) T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) - → (∀ (x : S), Δ ⊢ₑ γ x : Γ x ⇑ ⋆) + ∀ (e : expr S) E T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) + → (∀ (x : S), Δ ⊢ₑ γ x : Γ x ⇑ ∅%stdpp) → ( Δ ⊢ₑ bind γ e : τ ⇑ E). Proof. - revert S. @@ -496,75 +472,63 @@ Module Typing (Errors : ExcSig). by eapply le_ty_trans. - inversion Hσ. subst. inversion H5. subst. econstructor; last apply IHHty. - { intros ? [[|]|]; apply H. - * left. left. by apply H7. - * left. right. apply H2. - * right. apply H2. } + { set_solver. } all : try done. constructor; first by apply le_pty_refl. - eauto. + set_solver. - inversion Hσ. subst. inversion H4. subst. inversion H7. subst. econstructor; last apply IHHty. - { intros ? [[|]|]; apply H. - * left. left. by apply H9. - * left. right. by apply H6. - * right. apply H1. } - all : try done. - by eapply weakening_error. + { set_solver. } + 3 : done. + 1 : by eapply weakening_error. + constructor; first done. + set_solver. - inversion Hσ. subst. econstructor; last eapply IHHty. - { intros ? [[|]|]; apply H. - * left. by left. - * left. by right. - * right. eauto. - } + { set_solver. } all : try done. + eapply weakening_error; first done. - constructor; last by apply le_set_refl. + constructor; last done. constructor; first done. apply le_ty_refl. - + constructor; last by eauto. + + constructor; last set_solver. apply le_pty_refl. - inversion Hσ. subst. inversion H4. subst. econstructor; last by apply IHHty. - { intros ? [|]; apply H. - * left. apply H1. - * right. eauto. - } + { by apply union_mono_l. } done. - inversion Hσ. subst. inversion H4. subst. econstructor; last by apply IHHty. - { intros ? [|]; apply H. - * left. apply H1. - * right. eauto. - } + { by apply union_mono_l. } done. - inversion Hσ. subst. econstructor; first by eapply le_pty_trans. - { intros ? [|]; apply H0. - * by left. - * right. eauto. - } + { done. } apply IHHty. + constructor; first by apply le_pty_refl. - eauto. + set_solver. + done. - inversion Hσ. subst. inversion Hτ. subst. econstructor. { done. } { by eapply le_pty_trans. } - { intros ? [|]; apply H1. - * by left. - * right. destruct H3. split; eauto. + { instantiate (1 := E3). + instantiate (1 := E1). + apply union_least. + - set_solver. + - apply (difference_mono_r _ _ (gmap.gset_singleton err)) in H8. + etrans; first apply H8. + etrans; last done. + apply union_subseteq_r. } { done. } apply IHHty; last done. - constructor; last by apply le_set_refl. + constructor; last done. apply le_pty_refl. Qed. @@ -625,7 +589,8 @@ Module Typing (Errors : ExcSig). inversion Hα; subst. eexists. split; first done. - econstructor; last done; last done. intros. apply H3. rewrite or_comm. done. + econstructor; last done; last done. + set_solver. - simpl in Hty. apply IHK in Hty as (α & Hα & HK). inversion Hα; subst. @@ -656,7 +621,7 @@ Module Typing (Errors : ExcSig). intros K. induction K; intros e' Γ σ τ HK He'; inversion HK; subst. { term_simpl. by eapply weakening_error. } - 4 : { simpl. eapply IHK; first done. econstructor; last done; last done. intros. apply H3. by apply or_comm. } + 4 : { simpl. eapply IHK; first done. econstructor; last done; last done. intros. set_solver. } all: simpl; eapply IHK; try done; try econstructor; try done. @@ -692,7 +657,7 @@ Module Typing (Errors : ExcSig). Lemma less_errors_catch {S} : ∀ (K : cont S) Γ σ τ E1 E2 err, (Γ ⊢ₖ K : (σ ⇑ E1) ⇒ (τ ⇑ E2)) → - E1 err ∧ ¬ E2 err → + err ∈ E1 ∧ err ∉ E2 → ∃ K1 K2 h, K = cont_compose (CatchK err h K1) K2. Proof. intros K. @@ -700,14 +665,20 @@ Module Typing (Errors : ExcSig). match goal with | H : (Γ ⊢ₖ K : _ ⇒ _) |- ∃ _ _ _, (?C _) = _ => apply (IHK _ _ _ _ _ err0) in H as (K1 & K2 & h & ->); - [by exists K1, (C K2), h | eauto] + [by exists K1, (C K2), h | set_solver ] | _ => idtac end. - inversion H. subst. contradict HE2. eauto. - destruct (eq_dec err err0) as [-> | Hdiff]. + by exists K, END, h. - + apply (IHK _ _ _ _ _ err0) in H10 as (K1 & K2 & h0 & ->); last eauto. - by exists K1, (CatchK err h K2), h0. + + apply (IHK _ _ _ _ _ err0) in H10 as (K1 & K2 & h0 & ->). + * by exists K1, (CatchK err h K2), h0. + * split; last set_solver. + eapply elem_of_weaken; last done. + apply elem_of_union_r. + rewrite elem_of_difference. + split; first done. + by rewrite elem_of_singleton. Qed. Lemma preservation_wk {S} : @@ -739,7 +710,7 @@ Module Typing (Errors : ExcSig). eapply weakening_error; first by apply H7. eapply le_ty_trans; first done. constructor; first by apply le_pty_refl. - eauto. + set_solver. -- intros [|[|]]; term_simpl. { unfold shift. change (Val (fmap ?δ ?v)) with (fmap δ (Val v)). @@ -760,7 +731,7 @@ Module Typing (Errors : ExcSig). inversion HK. subst. split; first last. + eapply fill_types; first done. - destruct n; simpl; eapply weakening_error; try done; constructor; try apply le_pty_refl; eauto. + destruct n; simpl; eapply weakening_error; try done; constructor; try apply le_pty_refl; set_solver. + apply le_ty_refl. - destruct v1, v2; try discriminate. simpl in H. injection H as <-. @@ -801,7 +772,7 @@ Module Typing (Errors : ExcSig). constructor. apply le_pty_refl. * eapply weakening_error_cont; first done. - { constructor; first by apply le_pty_refl. eauto. } + { constructor; first by apply le_pty_refl. set_solver. } eapply le_ty_refl. + eapply le_ty_refl. Qed. @@ -817,7 +788,7 @@ Module Typing (Errors : ExcSig). destruct c'; by eapply weakening_error. Qed. - Lemma progress : ∀ (c : config) τ, (□ ⊢ᵢ c : τ ⇑ ⋆) → (∃ (v : val ∅), c = Cret v) ∨ (∃ c' n, c ===> c' / n). + Lemma progress : ∀ (c : config) τ, (□ ⊢ᵢ c : τ ⇑ ∅%stdpp) → (∃ (v : val ∅), c = Cret v) ∨ (∃ c' n, c ===> c' / n). Proof. intros c τ Hty. destruct c. @@ -827,7 +798,7 @@ Module Typing (Errors : ExcSig). inversion H2; subst; inversion H1; subst). 1-3, 5-9,13,17,18 : eexists _, _; by constructor. - 6,7 : eapply less_errors_catch in H8 as (K1 & K2 & h & HK); eauto; + 6,7 : eapply (less_errors_catch _ _ _ _ _ _ err) in H8 as (K1 & K2 & h & HK); try (split; set_solver); apply unwind_decompose_weak in HK as (? & ? & ?); eexists _,_; by constructor. From 805d5328906d195e0464fdf0174c16c54932943f Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 19 Jul 2024 19:21:46 +0200 Subject: [PATCH 10/16] Reorganized a few things --- theories/examples/except_lang/interp.v | 2 +- theories/examples/except_lang/lang.v | 42 ----------------- theories/examples/except_lang/typing.v | 64 +++++++++----------------- 3 files changed, 24 insertions(+), 84 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 3e67cf0..758fbc2 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -69,7 +69,7 @@ Module interp (Errors : ExcSig). (body : interp_scope (inc (inc S)) -n> IT) : interp_scope S -n> IT := mmuu (interp_rec_pre body). - + Program Definition ir_unf {S : Set} (body : interp_scope (inc (inc S)) -n> IT) env : IT -n> IT := λne a, body (extend_scope diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index e19bd79..0ab954c 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -638,48 +638,6 @@ Proof. rewrite /Inj; naive_solver. Qed. -(*** Type system *) - - -Inductive ty := - | Tnat : ty | Tarr : ty → ty → ty. - -Context {ETy : exc → ty}. - -Inductive typed {S : Set} (Γ : S -> ty) : expr S → ty → Prop := -| typed_Val (τ : ty) (v : val S) : - typed_val Γ v τ → - typed Γ (Val v) τ -| typed_Var (τ : ty) (v : S) : - Γ v = τ → - typed Γ (Var v) τ -| typed_App (τ1 τ2 : ty) e1 e2 : - typed Γ e1 (Tarr τ1 τ2) → - typed Γ e2 τ1 → - typed Γ (App e1 e2) τ2 -| typed_NatOp e1 e2 op : - typed Γ e1 Tnat → - typed Γ e2 Tnat → - typed Γ (NatOp op e1 e2) Tnat -| typed_If e0 e1 e2 τ : - typed Γ e0 Tnat → - typed Γ e1 τ → - typed Γ e2 τ → - typed Γ (If e0 e1 e2) τ -| typed_Throw err exp τ : - typed Γ exp (ETy err) → typed Γ (Throw err exp) τ -| typed_Catch err exp cexp τ : - typed Γ exp τ → - typed (Γ ▹ (ETy err)) cexp τ → - typed Γ (Catch err exp cexp) τ -with typed_val {S : Set} (Γ : S -> ty) : val S → ty → Prop := -| typed_Lit n : - typed_val Γ (LitV n) Tnat -| typed_RecV (τ1 τ2 : ty) (e : expr (inc (inc S))) : - typed (Γ ▹ (Tarr τ1 τ2) ▹ τ1) e τ2 → - typed_val Γ (RecV e) (Tarr τ1 τ2) -. - (** TODO LATER Declare Scope syn_scope. diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index b091683..cc054af 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -1,19 +1,12 @@ From gitrees.examples.except_lang Require Import lang. Require Import Binding.Lib Binding.Set Binding.Env. -Require Import Coq.Program.Equality. Module Typing (Errors : ExcSig). Module _LANG := Lang Errors. Import _LANG. Import _Exc. - (** Bare types **) - Inductive bty : Type := - | Bnat : bty - | Barr : bty → bty → bty - . - (** Types indicating possible errors raised **) Inductive pty : Type := | Tnat : pty @@ -89,38 +82,6 @@ Module Typing (Errors : ExcSig). (** Compatibility between types and bare types **) - Reserved Notation "τ ≅ σ" - (at level 20). - - Reserved Notation "τ ≈ σ" - (at level 20). - - Inductive compatp : bty → pty → Prop := - | Comp_nat : Bnat ≅ ℕ - | Comp_arr σb σ τb τ : σb ≅ σ → - τb ≈ τ → - Barr σb τb ≅ (σ ⟶ τ) - with compat : bty → ty → Prop := - Compat_Ty τb τ E : τb ≅ τ → - τb ≈ Ty τ E - where "σ ≅ τ" := (compatp σ τ) - and "σ ≈ τ" := (compat σ τ). - - Lemma le_ty_compat τ1 τ2 σ (Hsub : τ1 ⪍ τ2) : (σ ≈ τ1 ↔ σ ≈ τ2) - with le_pty_compat τ1 τ2 σ (Hsub : τ1 ≲ τ2) : (σ ≅ τ1 ↔ σ ≅ τ2). - Proof. - - destruct τ1 as [τ1 E1]. - destruct τ2 as [τ2 E2]. - inversion Hsub. subst. - split; constructor; inversion H; subst; by eapply (le_pty_compat τ1). - - destruct τ1; inversion Hsub; subst; first done. - split; intros Hsim; inversion Hsim; subst; constructor. - + by eapply le_pty_compat. - + by eapply (le_ty_compat t). - + by eapply (le_pty_compat τ3). - + by eapply (le_ty_compat t). - Qed. - Notation "E ⊕ e" := (E ∪ {[e]}) (at level 20). Notation "E ⊖ e" := (E ∖ {[e]}) @@ -654,7 +615,7 @@ Module Typing (Errors : ExcSig). eexists; split; first done; by econstructor]. Qed. - Lemma less_errors_catch {S} : + Lemma fewer_errors_catch {S} : ∀ (K : cont S) Γ σ τ E1 E2 err, (Γ ⊢ₖ K : (σ ⇑ E1) ⇒ (τ ⇑ E2)) → err ∈ E1 ∧ err ∉ E2 → @@ -798,7 +759,7 @@ Module Typing (Errors : ExcSig). inversion H2; subst; inversion H1; subst). 1-3, 5-9,13,17,18 : eexists _, _; by constructor. - 6,7 : eapply (less_errors_catch _ _ _ _ _ _ err) in H8 as (K1 & K2 & h & HK); try (split; set_solver); + 6,7 : eapply (fewer_errors_catch _ _ _ _ _ _ err) in H8 as (K1 & K2 & h & HK); try (split; set_solver); apply unwind_decompose_weak in HK as (? & ? & ?); eexists _,_; by constructor. @@ -813,4 +774,25 @@ Module Typing (Errors : ExcSig). - left. eexists. done. Qed. + Example confEX (err1 : exc) (err2 : exc) : (@config ∅) := + Ceval (Throw err1 (Throw err2 (Val (LitV 5)))) (CatchK err2 (Val (LitV 8)) END) +. +Example typEX (err1 err2 : exc) (Hdiff : err1 <> err2) (Hty : ETy err2 = ℕ) : ∃ τ, (□ ⊢ᵢ (confEX err1 err2) : τ). +Proof. + eexists. + econstructor; first last. + - econstructor; first last. + + econstructor; first last. + * econstructor. + * reflexivity. + * rewrite Hty. apply le_pty_refl. + + reflexivity. + + apply le_pty_refl. + - econstructor. + - reflexivity. + - apply le_pty_refl. + Unshelve. + all : exact (∅%stdpp). +Qed. + End Typing. From 7db44f72f62bc6d2dec3380ddaf57efff70ed38d Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Fri, 19 Jul 2024 20:26:31 +0200 Subject: [PATCH 11/16] Removed undeeded explicit weakening in typing --- theories/examples/except_lang/typing.v | 135 ++++++++++++++----------- 1 file changed, 75 insertions(+), 60 deletions(-) diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index cc054af..70e47c1 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -112,33 +112,33 @@ Module Typing (Errors : ExcSig). (Γ ⊢ᵥ (RecV f) : α ⇑ E) | typed_App E E1 E2 E3 Γ f v σ τ : - (E1 ∪ E2 ∪ E3) ⊆ E → + (E1 ∪ E2 ∪ E3) = E → (Γ ⊢ₑ f : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → (Γ ⊢ₑ v : σ ⇑ E3) → (Γ ⊢ₑ App f v : τ ⇑ E) | typed_Op Γ E E1 E2 op l r : - (E1 ∪ E2) ⊆ E → + (E1 ∪ E2) = E → (Γ ⊢ₑ l : ℕ ⇑ E1) → (Γ ⊢ₑ r : ℕ ⇑ E2) → (Γ ⊢ₑ NatOp op l r : ℕ ⇑ E) | typed_If Γ E E1 E2 E3 c t e τ : - (E1 ∪ E2 ∪ E3) ⊆ E→ + (E1 ∪ E2 ∪ E3) = E→ (Γ ⊢ₑ c : ℕ ⇑ E1) → (Γ ⊢ₑ t : τ ⇑ E2) → (Γ ⊢ₑ e : τ ⇑ E3) → (Γ ⊢ₑ If c t e : τ ⇑ E) | typed_Throw Γ E1 E2 err v σ τ : - σ ≲ ETy err → - (E1 ⊕ err) ⊆ E2 → + σ = ETy err → + (E1 ⊕ err) = E2 → (Γ ⊢ₑ v : σ ⇑ E1) → (Γ ⊢ₑ Throw err v : τ ⇑ E2) | typed_Catch Γ E E1 E2 err h v σ τ : - ETy err ≲ σ → - (E1 ∪ (E2 ⊖ err)) ⊆ E → + ETy err = σ → + (E1 ∪ (E2 ⊖ err)) = E → (Γ ▹ σ ⊢ₑ h : τ ⇑ E1) → (Γ ⊢ₑ v : τ ⇑ E2) → (Γ ⊢ₑ Catch err v h : τ ⇑ E) @@ -159,40 +159,40 @@ Module Typing (Errors : ExcSig). | typed_END Γ τ1 τ2 : τ1 ⪍ τ2 → (Γ ⊢ₖ END : τ1 ⇒ τ2) | typed_IfK Γ e₁ e₂ K E1 E2 E3 E4 τ σ : - (E1 ∪ E2 ∪ E3) ⊆ E4 → + (E1 ∪ E2 ∪ E3) = E4 → (Γ ⊢ₑ e₁ : σ ⇑ E2) → (Γ ⊢ₑ e₂ : σ ⇑ E3) → (Γ ⊢ₖ K : σ ⇑ E4 ⇒ τ) → (Γ ⊢ₖ IfK e₁ e₂ K : ℕ ⇑ E1 ⇒ τ) | typed_AppLK Γ E1 E2 E3 E4 v K σ τ α : - (E1 ∪ E2 ∪ E3) ⊆ E4 → + (E1 ∪ E2 ∪ E3) = E4 → (Γ ⊢ᵥ v : σ ⇑ E3) → (Γ ⊢ₖ K : τ ⇑ E4 ⇒ α) → (Γ ⊢ₖ AppLK v K : ((σ ⟶ (τ ⇑ E1)) ⇑ E2) ⇒ α) | typed_AppRK Γ E1 E2 E3 E4 e K σ τ α : - (E1 ∪ E2 ∪ E3) ⊆ E4 → + (E1 ∪ E2 ∪ E3) = E4 → (Γ ⊢ₑ e : (σ ⟶ (τ ⇑ E1)) ⇑ E2) → (Γ ⊢ₖ K : (τ ⇑ E4) ⇒ α) → (Γ ⊢ₖ AppRK e K : (σ ⇑ E3) ⇒ α) | typed_NatOpLK Γ E1 E2 E3 op v K τ : - (E1 ∪ E2) ⊆ E3 → + (E1 ∪ E2) = E3 → (Γ ⊢ᵥ v : ℕ ⇑ E1) → (Γ ⊢ₖ K : (ℕ ⇑ E3) ⇒ τ) → (Γ ⊢ₖ NatOpLK op v K : (ℕ ⇑ E2) ⇒ τ) | typed_NatOpRK Γ E1 E2 E3 op e K τ : - (E1 ∪ E2) ⊆ E3 → + (E1 ∪ E2) = E3 → (Γ ⊢ₑ e : ℕ ⇑ E1) → (Γ ⊢ₖ K : ℕ ⇑ E3 ⇒ τ) → (Γ ⊢ₖ NatOpRK op e K : (ℕ ⇑ E2) ⇒ τ) | typed_ThrowK Γ E1 E2 err K σ τ α : σ ≲ ETy err → - (E1 ⊕ err) ⊆ E2 → + (E1 ⊕ err) = E2 → (Γ ⊢ₖ K : (τ ⇑ E2) ⇒ α) → (Γ ⊢ₖ ThrowK err K : (σ ⇑ E1) ⇒ α) | typed_CatchK Γ E1 E2 E3 err h K σ τ τ' α : ETy err ≲ σ → τ' ≲ τ → - (E1 ∪ (E2 ⊖ err)) ⊆ E3 → + (E1 ∪ (E2 ⊖ err)) = E3 → (Γ ▹ σ ⊢ₑ h : (τ ⇑ E1)) → (Γ ⊢ₖ K : (τ ⇑ E3) ⇒ α) → (Γ ⊢ₖ CatchK err h K : (τ' ⇑ E2) ⇒ α) @@ -267,30 +267,40 @@ Module Typing (Errors : ExcSig). + constructor. by eapply le_pty_trans. + inversion H2. by constructor. + econstructor; first by eapply le_pty_trans. done. - + eapply typed_App. - * by etrans. + + econstructor. + * instantiate (3 := E1). + instantiate (2 := E2). + instantiate (1 := Eσ'). + set_solver. * apply IHHty1. constructor; last eauto. constructor; first apply le_pty_refl. by constructor. - * apply IHHty2, le_ty_refl. + * apply IHHty2. constructor; first apply le_pty_refl. + set_solver. + inversion H3. subst. econstructor. - * by etrans. + * instantiate (2 := E1). instantiate (1 := Eσ'). set_solver. * by apply IHHty1. - * by apply IHHty2. + * apply IHHty2. constructor; first by apply le_pty_refl. set_solver. + econstructor. - * by etrans. + * instantiate (3 := E1). + instantiate (2 := E2). + instantiate (1 := Eσ'). + set_solver. * apply IHHty1, le_ty_refl. * apply IHHty2. by constructor. - * by apply IHHty3. - + eapply typed_Throw; try done. - by etrans. + * apply IHHty3. constructor; first done. set_solver. + + econstructor. + * done. + * instantiate (1 := Eσ'). set_solver. + * apply IHHty. constructor; first apply le_pty_refl. set_solver. + econstructor; first done. - * by etrans. + * instantiate (1 := E2). instantiate (1 := Eσ'). set_solver. * apply IHHty1. - by constructor. + constructor; first done. + set_solver. * apply IHHty2. by constructor. Qed. @@ -438,7 +448,7 @@ Module Typing (Errors : ExcSig). constructor; first by apply le_pty_refl. set_solver. - inversion Hσ. subst. inversion H4. subst. - inversion H7. subst. + inversion H5. subst. econstructor; last apply IHHty. { set_solver. } 3 : done. @@ -459,13 +469,17 @@ Module Typing (Errors : ExcSig). - inversion Hσ. subst. inversion H4. subst. econstructor; last by apply IHHty. - { by apply union_mono_l. } - done. + { instantiate (1 := E1 ∪ E2). set_solver. } + eapply weakening_error; first done. + constructor; first by apply le_pty_refl. + set_solver. - inversion Hσ. subst. inversion H4. subst. econstructor; last by apply IHHty. - { by apply union_mono_l. } - done. + { instantiate (1 := E1 ∪ E2). set_solver. } + eapply weakening_error; first done. + constructor; first by apply le_pty_refl. + set_solver. - inversion Hσ. subst. econstructor; first by eapply le_pty_trans. { done. } @@ -473,24 +487,17 @@ Module Typing (Errors : ExcSig). + constructor; first by apply le_pty_refl. set_solver. + done. - - inversion Hσ. subst. + - Print typed_CatchK. + inversion Hσ. subst. inversion Hτ. subst. econstructor. { done. } { by eapply le_pty_trans. } - { instantiate (1 := E3). - instantiate (1 := E1). - apply union_least. - - set_solver. - - apply (difference_mono_r _ _ (gmap.gset_singleton err)) in H8. - etrans; first apply H8. - etrans; last done. - apply union_subseteq_r. - } + { done. } { done. } apply IHHty; last done. - constructor; last done. - apply le_pty_refl. + constructor; first apply le_pty_refl. + set_solver. Qed. Lemma fill_bind_bind {S T}: ∀ (δ : S [⇒] T) K e, fill (bind δ K) (bind δ e) = bind δ (fill K e). @@ -562,15 +569,19 @@ Module Typing (Errors : ExcSig). apply IHK in Hty as (α & Hα & HK). inversion Hα; subst. eexists. - split; first done. - by econstructor. + split. + + done. + + econstructor. + * apply le_pty_refl. + * reflexivity. + * done. - simpl in Hty. apply IHK in Hty as (α & Hα & HK). inversion Hα; subst. eexists. split; first done. econstructor; try done. - apply le_pty_refl. + all: apply le_pty_refl. Qed. Lemma fill_types {S : Set} : @@ -582,11 +593,14 @@ Module Typing (Errors : ExcSig). intros K. induction K; intros e' Γ σ τ HK He'; inversion HK; subst. { term_simpl. by eapply weakening_error. } - 4 : { simpl. eapply IHK; first done. econstructor; last done; last done. intros. set_solver. } + 4 : { simpl. eapply IHK; first done. econstructor; last done; last done. set_solver. } all: simpl; eapply IHK; try done; try econstructor; try done. - by eapply weakening_error. + 2 : { eapply weakening_sub; first done. intros [|]; first done. + apply le_pty_refl. + } + all : by eapply weakening_error. Qed. Lemma compose_END_left {S} : ∀ (K : cont S), cont_compose END K = K. @@ -657,7 +671,7 @@ Module Typing (Errors : ExcSig). apply decomp_types in Hty as (α & Hα & HK). inversion Hα. subst. inversion H3. subst. - inversion H6. subst. + inversion H4. subst. eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1))). * eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1) ▹ σ0)). -- eapply fill_types. @@ -668,7 +682,7 @@ Module Typing (Errors : ExcSig). } done. } - eapply weakening_error; first by apply H7. + eapply weakening_error; first by apply H6. eapply le_ty_trans; first done. constructor; first by apply le_pty_refl. set_solver. @@ -677,8 +691,8 @@ Module Typing (Errors : ExcSig). change (Val (fmap ?δ ?v)) with (fmap δ (Val v)). eapply weakening; last by instantiate (1 := Γ). inversion H5; subst. - + inversion H4. constructor. - + inversion H10. subst. inversion H4. subst. econstructor; last done. + + inversion H2. constructor. + + inversion H9. subst. inversion H2. subst. econstructor; last done. constructor; first by eapply le_pty_trans. by eapply le_ty_trans. } @@ -721,7 +735,7 @@ Module Typing (Errors : ExcSig). -- intros [|]; term_simpl. { inversion Hα; subst. - inversion H2. rewrite -H in H3. inversion H3. subst. constructor. - - inversion H9. subst. inversion H2. rewrite -H6 in H3. subst. + - inversion H6. subst. inversion H2. rewrite -H5 in H3. subst. inversion H3. subst. econstructor; last done. constructor. @@ -763,11 +777,11 @@ Module Typing (Errors : ExcSig). apply unwind_decompose_weak in HK as (? & ? & ?); eexists _,_; by constructor. - + inversion H7. - + inversion H8. inversion H6. - + inversion H6. - + inversion H6. - + inversion H6. + + inversion H5. + + inversion H8. inversion H5. + + inversion H5. + + inversion H5. + + inversion H5. - destruct e; right. 2 : by inversion Hty. all : eexists _,_ ; try constructor. @@ -785,14 +799,15 @@ Proof. + econstructor; first last. * econstructor. * reflexivity. - * rewrite Hty. apply le_pty_refl. + * done. + + reflexivity. + reflexivity. - + apply le_pty_refl. - econstructor. - reflexivity. - - apply le_pty_refl. + - reflexivity. Unshelve. all : exact (∅%stdpp). + Show Proof. Qed. End Typing. From 4017ea5dbbabe0911e63fb62fc014998f56b5b2a Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Mon, 22 Jul 2024 15:03:42 +0200 Subject: [PATCH 12/16] Removed a useless induction in except_lang/interp.v --- _CoqProject | 3 +- theories/examples/except_lang/interp.v | 100 ++++++++++++------------- theories/examples/except_lang/typing.v | 4 +- 3 files changed, 52 insertions(+), 55 deletions(-) diff --git a/_CoqProject b/_CoqProject index aba5faf..943359b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -60,8 +60,7 @@ theories/examples/input_lang/logrel.v theories/examples/except_lang/lang.v theories/examples/except_lang/interp.v -theories/examples/except_lang/logpred.v -theories/examples/except_lang/logrel.v +theories/examples/except_lang/typing.v theories/examples/affine_lang/lang.v theories/examples/affine_lang/logrel1.v diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 758fbc2..3c6f07c 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -790,36 +790,36 @@ Module interp (Errors : ExcSig). Proof. intros. revert H H0. - induction H1; intros H0 H1. - - simpl in H0, H1. - injection H0 as <- <-. - injection H1 as <- <-. + inversion H1; intros HE0 HE1. + - simpl in HE0, HE1. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; done. - - simpl in H0, H1. - rewrite H0 in H1. - injection H1 as <- <-. + - simpl in HE0, HE1. + rewrite HE0 in HE1. + injection HE1 as <- <-. constructor; done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [f t]. - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [f t]. - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [f t]. - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [f t] eqn:Heq. assert (IT_hom f). { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. econstructor. + rewrite hom_vis. eapply sstep_reify; first done. @@ -852,31 +852,31 @@ Module interp (Errors : ExcSig). intro; simpl; done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [f t] eqn:Heq. assert (IT_hom f). { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. by constructor. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [f t] eqn:Heq. assert (IT_hom f). { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. by constructor. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [g t] eqn:Heq. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. econstructor; last (econstructor; reflexivity). apply sstep_tick; last done. rewrite -hom_tick. f_equiv. - pose (interp_rec_unfold (interp_expr f) env) as H. + pose (interp_rec_unfold (interp_expr f) env) as HEq. assert (∀ x y z : IT, x ≡ y → x ⊙ z ≡ y ⊙ z) as APP'_equiv. { intros x y z Hxy. Transparent APP APP'. @@ -887,7 +887,7 @@ Module interp (Errors : ExcSig). f_equiv. done. } - rewrite (APP'_equiv _ _ _ H) APP_APP'_ITV APP_Fun Tick_eq /=. + rewrite (APP'_equiv _ _ _ HEq) APP_APP'_ITV APP_Fun Tick_eq /=. do 2 rewrite interp_expr_subst. do 3 f_equiv. intros []. @@ -900,32 +900,32 @@ Module interp (Errors : ExcSig). + destruct i; simpl. * done. * done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [g t] eqn:Heq. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; last done. f_equiv. - destruct n. + destruct n0. + rewrite IF_False; last lia. done. + rewrite IF_True; last lia. done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [g t] eqn:Heq. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; done. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [g t] eqn:Heq. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. constructor; last done. f_equiv. destruct v1, v2. @@ -934,12 +934,12 @@ Module interp (Errors : ExcSig). injection H as <-. simpl. apply NATOP_Ret. - - simpl in H0, H1. + - simpl in HE0, HE1. destruct (split_cont k env) as [g t] eqn:Heq. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. econstructor; last (constructor; done). rewrite get_val_ITV /= get_val_vis. eapply sstep_reify; first done. @@ -971,14 +971,14 @@ Module interp (Errors : ExcSig). repeat f_equiv; first by solve_proper. intro. simpl. done. } - - simpl in H0, H1. + - simpl in HE0, HE1. (** (interp_expr (subst h (Val v)) env), t) **) destruct (split_cont k env) as [g t] eqn:Heq. destruct (split_cont k' env) as [g' t'] eqn:Heq'. assert (IT_hom g) as Hg. { eapply split_cont_left_hom'. apply Heq. } - injection H0 as <- <-. - injection H1 as <- <-. + injection HE0 as <- <-. + injection HE1 as <- <-. econstructor; last by constructor. rewrite get_val_ITV hom_vis. eapply sstep_reify; first done. @@ -1018,11 +1018,11 @@ Module interp (Errors : ExcSig). simpl. done. Unshelve. - intros n []. + intros n0 []. } - - simpl in H0, H1. - rewrite H0 in H1. - injection H1 as <- <-. + - simpl in HE0, HE1. + rewrite HE0 in HE1. + injection HE1 as <- <-. constructor; done. Qed. diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index 70e47c1..51fc99e 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -487,8 +487,7 @@ Module Typing (Errors : ExcSig). + constructor; first by apply le_pty_refl. set_solver. + done. - - Print typed_CatchK. - inversion Hσ. subst. + - inversion Hσ. subst. inversion Hτ. subst. econstructor. { done. } @@ -807,7 +806,6 @@ Proof. - reflexivity. Unshelve. all : exact (∅%stdpp). - Show Proof. Qed. End Typing. From 5e7f4947b7ada99c97fcb07703570fe0922a6b79 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Tue, 23 Jul 2024 00:28:44 +0200 Subject: [PATCH 13/16] Added subtyping lemma for continuations --- theories/examples/except_lang/typing.v | 28 ++++++++++++++++++++++---- 1 file changed, 24 insertions(+), 4 deletions(-) diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index 51fc99e..8b08728 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -340,7 +340,27 @@ Module Typing (Errors : ExcSig). simpl. apply Hag. * by apply IHHty2. Qed. - + + Lemma weakening_sub_cont {S: Set} : + ∀ (Γ : S → pty) (Δ : S → pty) (K : cont S) σ τ, + (Γ ⊢ₖ K : σ ⇒ τ) → + (∀ x, Δ x ≲ Γ x) → + (Δ ⊢ₖ K : σ ⇒ τ). + Proof. + intros Γ Δ K σ τ Hty Hag. + induction Hty; intros. + + by constructor. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto; by eapply weakening_sub. + + econstructor; eauto. eapply weakening_sub; first done. + intros [|]; term_simpl. + { apply le_pty_refl. } + { apply Hag. } + Qed. Lemma substitution_lemma {S : Set}: ∀ (e : expr S) E T Γ Δ (γ : S [⇒] T) τ, (Γ ⊢ₑ e : τ ⇑ E) @@ -787,9 +807,9 @@ Module Typing (Errors : ExcSig). - left. eexists. done. Qed. - Example confEX (err1 : exc) (err2 : exc) : (@config ∅) := - Ceval (Throw err1 (Throw err2 (Val (LitV 5)))) (CatchK err2 (Val (LitV 8)) END) -. +Example confEX (err1 : exc) (err2 : exc) : (@config ∅) := + Ceval (Throw err1 (Throw err2 (Val (LitV 5)))) (CatchK err2 (Val (LitV 8)) END). + Example typEX (err1 err2 : exc) (Hdiff : err1 <> err2) (Hty : ETy err2 = ℕ) : ∃ τ, (□ ⊢ᵢ (confEX err1 err2) : τ). Proof. eexists. From df0417f16a8255ef7d155a06bfc55a27fe595d17 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Tue, 23 Jul 2024 00:41:03 +0200 Subject: [PATCH 14/16] Removed useless induction in typing and useless assert in soundness for except_lang --- theories/examples/except_lang/interp.v | 2 -- theories/examples/except_lang/typing.v | 19 +++++++++---------- 2 files changed, 9 insertions(+), 12 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 3c6f07c..844d502 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -936,8 +936,6 @@ Module interp (Errors : ExcSig). apply NATOP_Ret. - simpl in HE0, HE1. destruct (split_cont k env) as [g t] eqn:Heq. - assert (IT_hom g) as Hg. - { eapply split_cont_left_hom'. apply Heq. } injection HE0 as <- <-. injection HE1 as <- <-. econstructor; last (constructor; done). diff --git a/theories/examples/except_lang/typing.v b/theories/examples/except_lang/typing.v index 8b08728..df8c504 100644 --- a/theories/examples/except_lang/typing.v +++ b/theories/examples/except_lang/typing.v @@ -683,14 +683,14 @@ Module Typing (Errors : ExcSig). Proof. intros Γ τ c c' n Hty Hred. revert Γ τ Hty. - induction Hred; intros Γ [τ Eτ] Hty; simpl; eexists; try (split; try done; apply le_ty_refl). + inversion Hred; intros Γ [τ Eτ] Hty; simpl; eexists; try (split; try done; apply le_ty_refl). - simpl in *. split; last first. + do 2 rewrite fill_bind_subst. apply decomp_types in Hty as (α & Hα & HK). inversion Hα. subst. + inversion H6. subst. inversion H3. subst. - inversion H4. subst. eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1))). * eapply (substitution_lemma _ _ _ (Γ ▹ (σ0 ⟶ τ1) ▹ σ0)). -- eapply fill_types. @@ -701,7 +701,7 @@ Module Typing (Errors : ExcSig). } done. } - eapply weakening_error; first by apply H6. + eapply weakening_error; first by apply H4. eapply le_ty_trans; first done. constructor; first by apply le_pty_refl. set_solver. @@ -709,7 +709,7 @@ Module Typing (Errors : ExcSig). { unfold shift. change (Val (fmap ?δ ?v)) with (fmap δ (Val v)). eapply weakening; last by instantiate (1 := Γ). - inversion H5; subst. + inversion H8; subst. + inversion H2. constructor. + inversion H9. subst. inversion H2. subst. econstructor; last done. constructor; first by eapply le_pty_trans. @@ -725,7 +725,7 @@ Module Typing (Errors : ExcSig). inversion HK. subst. split; first last. + eapply fill_types; first done. - destruct n; simpl; eapply weakening_error; try done; constructor; try apply le_pty_refl; set_solver. + destruct n0; simpl; eapply weakening_error; try done; constructor; try apply le_pty_refl; set_solver. + apply le_ty_refl. - destruct v1, v2; try discriminate. simpl in H. injection H as <-. @@ -740,22 +740,21 @@ Module Typing (Errors : ExcSig). split; first last. + eapply fill_types; first done. inversion Hα; subst. - { inversion H3. constructor. } + { inversion H6. constructor. } { econstructor; last done. by eapply le_pty_trans. } + apply le_ty_refl. - apply decomp_types in Hty as [α [Hα HK]]. inversion HK. subst. apply unwind_decompose in H as (K1 & Hkcomp & HK1). - destruct (compose_type _ _ _ _ _ _ H7 Hkcomp) as (α & HK2 & HK3). + destruct (compose_type _ _ _ _ _ _ H10 Hkcomp) as (α & HK2 & HK3). inversion HK2. subst. split; first last. + eapply fill_types; first last. * eapply substitution_lemma; first done. -- intros [|]; term_simpl. { inversion Hα; subst. - - inversion H2. rewrite -H in H3. inversion H3. subst. constructor. - - inversion H6. subst. inversion H2. rewrite -H5 in H3. subst. - inversion H3. subst. + - inversion H5. rewrite -H in H2. inversion H2. subst. constructor. + - inversion H6. subst. inversion H5. rewrite -H4 in H2. subst. inversion H2. subst. econstructor; last done. constructor. + eapply le_pty_trans; first done. From fd13f96c97736cd14216f8b94d7757a7ec1ef626 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 1 Aug 2024 11:59:21 +0200 Subject: [PATCH 15/16] Minor fixes in except lang --- theories/examples/except_lang/interp.v | 8 ++++---- theories/examples/except_lang/lang.v | 2 +- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 844d502..2df5c3b 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -1,14 +1,15 @@ From gitrees Require Import gitree lang_generic. From iris.algebra Require Import list. From gitrees.effects Require Export exceptions. -From gitrees.examples.except_lang Require Import lang. +From gitrees.examples.except_lang Require Import lang typing. Require Import Binding.Lib Binding.Set. Module interp (Errors : ExcSig). - - Module _LANG := Lang Errors. + + Module _TYP := Typing Errors. + Import _TYP. Import _LANG. Import _Exc. @@ -1488,4 +1489,3 @@ Module interp (Errors : ExcSig). End Examples. **) *) End interp. -#[global] Opaque INPUT OUTPUT_. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index 0ab954c..fe0c89f 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -1,4 +1,4 @@ -From gitrees Require Export prelude effects.io_tape effects.exceptions. +From gitrees Require Export prelude effects.exceptions. Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. Module Lang (Errors : ExcSig). From 41a300e4605f2cc9520028199a727cff9bd61415 Mon Sep 17 00:00:00 2001 From: Virgil Marionneau Date: Thu, 1 Aug 2024 12:03:52 +0200 Subject: [PATCH 16/16] Cleaned up the files in except lang --- theories/examples/except_lang/interp.v | 527 +------------------------ theories/examples/except_lang/lang.v | 132 ------- 2 files changed, 2 insertions(+), 657 deletions(-) diff --git a/theories/examples/except_lang/interp.v b/theories/examples/except_lang/interp.v index 2df5c3b..2584395 100644 --- a/theories/examples/except_lang/interp.v +++ b/theories/examples/except_lang/interp.v @@ -471,9 +471,6 @@ Module interp (Errors : ExcSig). with interp_val_ren {S S'} env (δ : S [→] S') (e : val S) : interp_val (fmap δ e) env ≡ interp_val e (ren_scope δ env). - (** with interp_cont_ren {S S'} env - (δ : S [→] S') (e : cont S) : - interp_cont (fmap δ e) env ≡ interp_cont e (ren_scope δ env). **) Proof. - destruct e; simpl. + by apply interp_val_ren. @@ -506,40 +503,8 @@ Module interp (Errors : ExcSig). destruct y' as [| [| y]]; simpl; first done. * by iRewrite - "IH". * done. - (* - destruct e; simpl; intros ?; simpl. - + reflexivity. - + repeat f_equiv; [by apply interp_cont_ren | by apply interp_expr_ren | by apply interp_expr_ren]. - + repeat f_equiv; [by apply interp_cont_ren | by apply interp_val_ren]. - + repeat f_equiv; [by apply interp_expr_ren | by apply interp_cont_ren]. - + repeat f_equiv; [by apply interp_expr_ren | by apply interp_cont_ren]. - + repeat f_equiv; [by apply interp_cont_ren | by apply interp_val_ren]. - + repeat f_equiv. by apply interp_cont_ren. - + repeat f_equiv; last done. - intro. - simpl. - destruct x0. - do 2 rewrite laterO_map_Next. - f_equiv. - simpl. - rewrite interp_expr_ren. - f_equiv. - intro. - destruct x0; done. *) Qed. -(* - Lemma interp_comp {S} (e : expr S) (env : interp_scope S) (K : cont S): - interp_expr (fill K e) env ≡ (interp_cont K) env ((interp_expr e) env). - Proof. - revert env. - induction K; simpl; intros env; first reflexivity; try (by rewrite IHK). - - repeat f_equiv. - by rewrite IHK. - - repeat f_equiv. - by rewrite IHK. - - repeat f_equiv. - by rewrite IHK. - Qed. -*) + Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') : interp_scope S := λne x, interp_expr (δ x) env. @@ -562,9 +527,6 @@ Module interp (Errors : ExcSig). with interp_val_subst {S S'} (env : interp_scope S') (δ : S [⇒] S') e : interp_val (bind δ e) env ≡ interp_val e (sub_scope δ env). -(* with interp_cont_subst {S S'} (env : interp_scope S') - (δ : S [⇒] S') e : - interp_cont (bind δ e) env ≡ interp_cont e (sub_scope δ env). *) Proof. - destruct e; simpl. + by apply interp_val_subst. @@ -610,26 +572,6 @@ Module interp (Errors : ExcSig). iApply internal_eq_pointwise. iIntros (z). done. - (* - destruct e; simpl; intros ?; simpl. - + reflexivity. - + repeat f_equiv; [by apply interp_cont_subst | by apply interp_expr_subst | by apply interp_expr_subst]. - + repeat f_equiv; [by apply interp_cont_subst | by apply interp_val_subst]. - + repeat f_equiv; [by apply interp_expr_subst | by apply interp_cont_subst]. - + repeat f_equiv; [by apply interp_expr_subst | by apply interp_cont_subst]. - + repeat f_equiv; [by apply interp_cont_subst | by apply interp_val_subst]. - + repeat f_equiv. - by apply interp_cont_subst. - + repeat f_equiv; last done. - intros []. simpl. - do 2 rewrite laterO_map_Next. - f_equiv. simpl. - rewrite interp_expr_subst. - f_equiv. - intros []; simpl. - * done. - * rewrite interp_expr_ren. - f_equiv. - by intro. *) Qed. Lemma split_cont_decomp {S} K K1 K2 p t p1 t1 env h err f k: @@ -842,8 +784,7 @@ Module interp (Errors : ExcSig). + constructor. * repeat f_equiv. intro. simpl. - f_equiv. - f_equiv. (* Reflexivity doesn't work here, really funny, show Sergei *) + do 2 f_equiv. intro. simpl. done. @@ -971,7 +912,6 @@ Module interp (Errors : ExcSig). intro. simpl. done. } - simpl in HE0, HE1. - (** (interp_expr (subst h (Val v)) env), t) **) destruct (split_cont k env) as [g t] eqn:Heq. destruct (split_cont k' env) as [g' t'] eqn:Heq'. assert (IT_hom g) as Hg. @@ -1025,467 +965,4 @@ Module interp (Errors : ExcSig). constructor; done. Qed. - Theorem stuck {S} : ∀ c c' e σr σ n (env : interp_scope S), - interp_config c env = (e, σ) → - (∀ m e' σ', m > 0 → ¬ (ssteps (gReifiers_sReifier rs) - e (gState_recomp σr (sR_state σ)) - e' (gState_recomp σr (sR_state σ')) m)) → - c ===> c' / n → - n = 0. - intros c c' e σr σ n env Hc Hst Hred. - destruct n; first done. - exfalso. - destruct (interp_config c' env) as (e', σ') eqn:Hc'. - eapply (soundness _ _ _ _ σr _ _ _ _ Hc Hc') in Hred. - specialize (Hst (Datatypes.S n) e' σ'). - apply Hst; first lia. - apply Hred. - Qed. - - (** BOOKMARK **) - (** ** Interpretation of evaluation contexts induces homomorphism *) - - -(* - #[local] Instance interp_cont_hom_emp {S} env : - IT_hom (interp_cont (EmptyIK : cont S) env). - Proof. - simple refine (IT_HOM _ _ _ _ _); intros; auto. - simpl. fold (@idfun IT). f_equiv. intro. simpl. - by rewrite laterO_map_id. - Qed. - - #[local] Instance interp_cont_hom_if {S} - (K : cont S) (e1 e2 : expr S) env : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (IfIK K e1 e2) env). - Proof. - intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -IF_Tick. do 3 f_equiv. apply hom_tick. - - assert ((interp_cont K env (Vis op i ko)) ≡ - (Vis op i (laterO_map (λne y, interp_cont K env y) ◎ ko))). - { by rewrite hom_vis. } - trans (IF (Vis op i (laterO_map (λne y : IT, interp_cont K env y) ◎ ko)) - (interp_expr e1 env) (interp_expr e2 env)). - { do 3 f_equiv. by rewrite hom_vis. } - rewrite IF_Vis. f_equiv. simpl. - intro. simpl. by rewrite -laterO_map_compose. - - trans (IF (Err e) (interp_expr e1 env) (interp_expr e2 env)). - { repeat f_equiv. apply hom_err. } - apply IF_Err. - Qed. - - #[local] Instance interp_cont_hom_appr {S} (K : cont S) - (e : expr S) env : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (AppRIK e K) env). - Proof. - intros. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by rewrite !hom_tick. - - rewrite !hom_vis. f_equiv. intro x. simpl. - by rewrite laterO_map_compose. - - by rewrite !hom_err. - Qed. - - #[local] Instance interp_cont_hom_appl {S} (K : cont S) - (v : val S) (env : interp_scope S) : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (AppLIK K v) env). - Proof. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -APP'_Tick_l. do 2 f_equiv. apply hom_tick. - - trans (APP' (Vis op i (laterO_map (interp_cont K env) ◎ ko)) - (interp_val v env)). - + do 2f_equiv. rewrite hom_vis. do 3 f_equiv. by intro. - + rewrite APP'_Vis_l. f_equiv. intro x. simpl. - by rewrite -laterO_map_compose. - - trans (APP' (Err e) (interp_val v env)). - { do 2f_equiv. apply hom_err. } - apply APP'_Err_l, interp_val_asval. - Qed. - - #[local] Instance interp_cont_hom_natopr {S} (K : cont S) - (e : expr S) op env : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (NatOpRIK op e K) env). - Proof. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by rewrite !hom_tick. - - rewrite !hom_vis. f_equiv. intro x. simpl. - by rewrite laterO_map_compose. - - by rewrite !hom_err. - Qed. - - #[local] Instance interp_cont_hom_natopl {S} (K : cont S) - (v : val S) op (env : interp_scope S) : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (NatOpLIK op K v) env). - Proof. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -NATOP_ITV_Tick_l. do 2 f_equiv. apply hom_tick. - - trans (NATOP (do_natop op) - (Vis op0 i (laterO_map (interp_cont K env) ◎ ko)) - (interp_val v env)). - { do 2 f_equiv. rewrite hom_vis. f_equiv. by intro. } - rewrite NATOP_ITV_Vis_l. f_equiv. intro x. simpl. - by rewrite -laterO_map_compose. - - trans (NATOP (do_natop op) (Err e) (interp_val v env)). - + do 2 f_equiv. apply hom_err. - + by apply NATOP_Err_l, interp_val_asval. - Qed. - - #[local] Instance interp_cont_hom_throw {S} (K : cont S) err (env : interp_scope S) : - IT_hom (interp_cont K env) -> - IT_hom (interp_cont (ThrowIK err K) env). - Proof. - Opaque THROW. - intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - by do 2 rewrite hom_tick. - - do 2 rewrite hom_vis. f_equiv. by intro. - - by do 2 rewrite hom_err. - Qed. - - - #[global] Instance interp_cont_hom {S} (IK : cont S) env : - (∃ K, IK = cont_of_cont K) → - IT_hom (interp_cont IK env). - Proof. - intros [K ->]. - induction K; try apply _. - Qed. - - (** ** Finally, preservation of reductions *) - Lemma interp_expr_head_step {S : Set} (env : interp_scope S) (e : expr S) e' n : - head_step e e' (n, 0) → - interp_expr e env ≡ Tick_n n $ interp_expr e' env. - Proof. - inversion 1; cbn-[IF APP' INPUT Tick get_ret2]. - - (* app lemma *) - subst. - erewrite APP_APP'_ITV; last apply _. - trans (APP (Fun (Next (ir_unf (interp_expr e1) env))) (Next $ interp_val v2 env)). - { repeat f_equiv. apply interp_rec_unfold. } - rewrite APP_Fun. simpl. rewrite Tick_eq. do 2 f_equiv. - simplify_eq. - rewrite !interp_expr_subst. - f_equiv. - intros [| [| x]]; simpl; [| reflexivity | reflexivity]. - rewrite interp_val_ren. - f_equiv. - intros ?; simpl; reflexivity. - - (* the natop stuff *) - simplify_eq. - destruct v1,v2; try naive_solver. simpl in *. - rewrite NATOP_Ret. - destruct op; simplify_eq/=; done. - - rewrite IF_True; last lia. - reflexivity. - - rewrite IF_False; last lia. - reflexivity. - Qed. - - Lemma interp_expr_fill_no_reify {S} K (env : interp_scope S) (e e' : expr S) n : - head_step e e' (n, 0) → - interp_expr (fill (cont_of_cont K) e) env - ≡ - Tick_n n $ interp_expr (fill (cont_of_cont K) e') env. - Proof. - intros He. - rewrite !interp_comp. - erewrite <-hom_tick_n. - - apply (interp_expr_head_step env) in He. - rewrite He. - reflexivity. - - apply interp_cont_hom. exists K. done. - Qed. - - Opaque extend_scope. - Opaque Ret. - (** - Lemma interp_expr_fill_yes_reify {S} K env (e e' : expr S) - (σ σ' : stateO) (σr : gState_rest sR_idx rs ♯ IT) n : - head_step e e' (n, 1) → - reify (gReifiers_sReifier rs) - (interp_expr (fill K e) env) (gState_recomp σr (sR_state σ)) - ≡ (gState_recomp σr (sR_state σ'), Tick_n n $ interp_expr (fill K e') env). - Proof. - intros Hst. - trans (reify (gReifiers_sReifier rs) (interp_cont K env (interp_expr e env)) - (gState_recomp σr (sR_state σ))). - { f_equiv. by rewrite interp_comp. } - inversion Hst; simplify_eq; cbn-[gState_recomp]. - - trans (reify (gReifiers_sReifier rs) (INPUT (interp_cont K env ◎ Ret)) (gState_recomp σr (sR_state σ))). - { - repeat f_equiv; eauto. - rewrite hom_INPUT. - do 2 f_equiv. by intro. - } - rewrite reify_vis_eq_ctx_indep //; first last. - { - epose proof (@subReifier_reify sz NotCtxDep reify_io rs _ IT _ (inl ()) () _ σ σ' σr) as H. - simpl in H. - simpl. - erewrite <-H; last first. - - rewrite H4. reflexivity. - - f_equiv; - solve_proper. - } - repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. - rewrite interp_comp. - rewrite ofe_iso_21. - simpl. - reflexivity. - - trans (reify (gReifiers_sReifier rs) (interp_cont K env (OUTPUT n0)) (gState_recomp σr (sR_state σ))). - { - do 3 f_equiv; eauto. - rewrite get_ret_ret//. - } - trans (reify (gReifiers_sReifier rs) (OUTPUT_ n0 (interp_cont K env (Ret 0))) (gState_recomp σr (sR_state σ))). - { - do 2 f_equiv; eauto. - by rewrite hom_OUTPUT_. - } - rewrite reify_vis_eq_ctx_indep //; last first. - { - epose proof (@subReifier_reify sz _ reify_io rs _ IT _ (inr (inl ())) n0 _ σ (update_output n0 σ) σr) as H. - simpl in H. - simpl. - erewrite <-H; last reflexivity. - f_equiv. - intros ???. by rewrite /prod_map H0. - } - repeat f_equiv. rewrite Tick_eq/=. repeat f_equiv. - rewrite interp_comp. - reflexivity. - Qed. - - Example test1 err : expr ∅ := - (try - (#4) + #5 - catch err => #1 - )%syn. - - Example test2 err : expr ∅ := - (try - #9 - catch err => #1 - )%syn. - - Example uu err σr : ∃ n m σ t, - ssteps (gReifiers_sReifier rs) - (interp_expr (test1 err) (λne (x : leibnizO ∅), match x with end) : IT) - (gState_recomp σr (sR_state σ)) - t - (gState_recomp σr (sR_state σ)) n ∧ - ssteps (gReifiers_sReifier rs) - (interp_expr (test2 err) (λne (x : leibnizO ∅), match x with end) : IT) - (gState_recomp σr (sR_state σ)) - t - (gState_recomp σr (sR_state σ)) m. - Proof. - rewrite /test1 /test2. - simpl. - do 2 eexists. - exists []. - eexists. - split. - - eapply ssteps_many. - + eapply sstep_reify. - { f_equiv. rewrite /ccompose /compose /=. reflexivity. }. - Check reify_vis_eq_ctx_dep. - apply reify_vis_eq_ctx_dep. - - - - Proof. - intros H. - unfold test1 in H. - unfold test2 in H. - simpl in H. - - Compute . - - Lemma soundness {S} (e1 e2 : expr S) (σr : gState_rest sR_idx rs ♯ IT) n m (env : interp_scope S) : - prim_step e1 e2 (n,m) → ∀ σ1, ∃ σ2, - ssteps (gReifiers_sReifier rs) - (interp_expr e1 env) (gState_recomp σr (sR_state σ1)) - (interp_expr e2 env) (gState_recomp σr (sR_state σ2)) n. - Proof. - Opaque gState_decomp gState_recomp. - intros Hstep. - inversion Hstep;simplify_eq/=. - - intros σ1. - eexists. - rewrite !interp_comp. - - - - unshelve eapply (interp_expr_fill_no_reify K) in H2; first apply env. - rewrite H2. - rewrite interp_comp. - eapply ssteps_tick_n. - + inversion H2;subst. - * eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. - rewrite interp_comp. - rewrite hom_INPUT. - change 1 with (Nat.add 1 0). econstructor; last first. - { apply ssteps_zero; reflexivity. } - eapply sstep_reify. - { Transparent INPUT. unfold INPUT. simpl. - f_equiv. reflexivity. } - simpl in H2. - rewrite -H2. - repeat f_equiv; eauto. - rewrite interp_comp hom_INPUT. - eauto. - * eapply (interp_expr_fill_yes_reify K env _ _ _ _ σr) in H2. - rewrite interp_comp. simpl. - rewrite get_ret_ret. - rewrite hom_OUTPUT_. - change 1 with (Nat.add 1 0). econstructor; last first. - { apply ssteps_zero; reflexivity. } - eapply sstep_reify. - { Transparent OUTPUT_. unfold OUTPUT_. simpl. - f_equiv. reflexivity. } - simpl in H2. - rewrite -H2. - repeat f_equiv; eauto. - Opaque OUTPUT_. - rewrite interp_comp /= get_ret_ret hom_OUTPUT_. - eauto. - Qed. *) - (** - Section Examples. - Context `{!invGS Σ, !stateG rs R Σ}. - - Opaque CATCH. - - Example prog1 (err : exc) (n : nat) : expr ∅ := - (try - if #n then - throw err #5 - else #4 - catch err => ($0) * $0 - )%syn. - - Example wp_prog1 (err : exc) (n : nat) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ (⌜n = 0⌝ -∗ Φ (RetV 4)) ∗ (⌜n > 0⌝ -∗ Φ (RetV 25))) -∗ - WP@{rs} (interp_expr (prog1 err n) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - iIntros "Hσ H▷". - simpl. - destruct n. - - rewrite IF_False; last lia. - iApply (wp_catch_v _ _ (Ret 4) _ _ _ idfun with "Hσ"). - + by simpl. - + iIntros "!> H£ Hσ". - iPoseProof ("H▷" with "H£ Hσ") as "[HΦ _]". - iApply wp_val. - iModIntro. - by iApply "HΦ". - - rewrite IF_True; last lia. - iApply (wp_catch_throw _ _ (Ret 5) idfun idfun with "Hσ"). - + simpl. - rewrite laterO_map_Next. - simpl. - rewrite NATOP_Ret. - by simpl. - + simpl. - iIntros "!> H£ Hσ". - iPoseProof ("H▷" with "H£ Hσ") as "[_ HΦ]". - iApply wp_val. - iModIntro. - iApply "HΦ". - iPureIntro. - lia. - Qed. - - Example prog2 (err : exc) : expr ∅ := - (if ( - try - throw err #3 - catch err => ($0) * #4 - ) - then #1 - else #0 - )%syn. - - Example wp_prog2 (err : exc) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ Φ (RetV 1)) -∗ - WP@{rs} (interp_expr (prog2 err) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - Proof. - iIntros "Hσ H▷". - simpl. - iApply (wp_catch_throw _ _ (Ret 3) idfun (λne x, IF x (Ret 1) (Ret 0)) with "Hσ"). - - simpl. - rewrite laterO_map_Next /=. - rewrite NATOP_Ret. - by simpl. - - simpl. - iIntros "!>H£ Hσ". - rewrite IF_True; last lia. - iApply wp_val. - iModIntro. - iApply ("H▷" with "H£ Hσ"). - Qed. - - Example prog3 (err : exc) : expr ∅ := - (try - (if ( - throw err #3 - ) - then #1 - else #0) - catch err => ($0) * #4 - )%syn. - - Example wp_prog3 (err : exc) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ Φ (RetV 12)) -∗ - WP@{rs} (interp_expr (prog3 err) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - Proof. - iIntros "Hσ H▷". - simpl. - iApply (wp_catch_throw _ _ (Ret 3) (λne x, IF x (Ret 1) (Ret 0)) idfun with "Hσ"). - - by rewrite laterO_map_Next /= NATOP_Ret /=. - - iIntros "!> H£ Hσ". - iApply wp_val. - by iApply ("H▷" with "H£ Hσ"). - Qed. - - Example prog4 (err1 err2 : exc) : expr ∅ := - (try - try - throw err1 #3 - catch err2 => ($0) + $0 - catch err1 => ($0) * $0 - )%syn. - - Example wp_prog4 (err1 err2 : exc) (Herr : err1 <> err2) (σ : stateF ♯ IT) Φ : - has_substate σ -∗ - ▷(£1 -∗ has_substate σ -∗ Φ (RetV 9)) -∗ - WP@{rs} (interp_expr (prog4 err1 err2) (λne (x : leibnizO ∅), match x with end) : IT) {{ Φ }}. - Proof. - Opaque _REG. - iIntros "Hσ H▷". - simpl. - iApply (wp_reg _ _ err1 _ idfun with "Hσ"). - { reflexivity. } - iIntros "!> H£ Hσ". - iApply (wp_reg _ _ _ _ (get_val _) with "Hσ"). - { reflexivity. } - iIntros "!> H£' Hσ". - iApply (wp_throw _ _ _ _ _ _ _ (get_val _) with "Hσ"). - 3: change (?a :: ?b :: σ) with ([a] ++ b::σ); reflexivity. - { constructor; first done. constructor. } - { by rewrite laterO_map_Next /= NATOP_Ret /=. } - iIntros "!> H£'' Hσ". - iApply wp_val. - iModIntro. - iApply ("H▷" with "H£ Hσ"). - Qed. - - End Examples. -**) *) End interp. diff --git a/theories/examples/except_lang/lang.v b/theories/examples/except_lang/lang.v index fe0c89f..682bf42 100644 --- a/theories/examples/except_lang/lang.v +++ b/theories/examples/except_lang/lang.v @@ -638,136 +638,4 @@ Proof. rewrite /Inj; naive_solver. Qed. -(** TODO LATER - -Declare Scope syn_scope. -Delimit Scope syn_scope with syn. - -Coercion Val : val >-> expr. - -Coercion App : expr >-> Funclass. -Coercion AppLK : val >-> Funclass. -Coercion AppRK : expr >-> Funclass. - - -(* XXX: We use these typeclasses to share the notation between the -expressions and the evaluation contexts, for readability. It will be -good to also share the notation between different languages. *) - -Class AsSynExpr (F : Set -> Type) := { __asSynExpr : ∀ S, F S -> expr S }. - -Arguments __asSynExpr {_} {_} {_}. - -Global Instance AsSynExprValue : AsSynExpr val := { - __asSynExpr _ v := Val v - }. -Global Instance AsSynExprExpr : AsSynExpr expr := { - __asSynExpr _ e := e - }. - -Class OpNotation (A B C D : Type) := { __op : A -> B -> C -> D }. - -Global Instance OpNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : OpNotation (F S) nat_op (G S) (expr S) := { - __op e₁ op e₂ := NatOp op (__asSynExpr e₁) (__asSynExpr e₂) - }. - -Global Instance OpNotationLK {S : Set} : OpNotation (cont S) (nat_op) (val S) (cont S) := { - __op K op v := NatOpRK op K v - }. - -Global Instance OpNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : OpNotation (F S) (nat_op) (cont S) (cont S) := { - __op e op K := NatOpLK op (__asSynExpr e) K - }. - -Class IfNotation (A B C D : Type) := { __if : A -> B -> C -> D }. - -Global Instance IfNotationExpr {S : Set} {F G H : Set -> Type} `{AsSynExpr F, AsSynExpr G, AsSynExpr H} : IfNotation (F S) (G S) (H S) (expr S) := { - __if e₁ e₂ e₃ := If (__asSynExpr e₁) (__asSynExpr e₂) (__asSynExpr e₃) - }. - -Global Instance IfNotationK {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : IfNotation (cont S) (F S) (G S) (cont S) := { - __if K e₂ e₃ := IfK K (__asSynExpr e₂) (__asSynExpr e₃) - }. - -Class AppNotation (A B C : Type) := { __app : A -> B -> C }. - -Global Instance AppNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : AppNotation (F S) (G S) (expr S) := { - __app e₁ e₂ := App (__asSynExpr e₁) (__asSynExpr e₂) - }. - -Global Instance AppNotationLK {S : Set} : AppNotation (cont S) (val S) (cont S) := { - __app K v := AppLK K v - }. - -Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (cont S) (cont S) := { - __app e K := AppRK (__asSynExpr e) K - }. - -Class ThrowNotation (A B : Type) := { __throw : exc -> A -> B}. - -Global Instance ThrowNotationExpr {S : Set} {F: Set -> Type} `{AsSynExpr F} : ThrowNotation (F S) (expr S) := - { - __throw e v := Throw e (__asSynExpr v) - }. - -Global Instance ThrowNotationK {S : Set} : ThrowNotation (cont S) (cont S) := - { - __throw e K := ThrowK e K - }. - -Class CatchNotation (A B C : Type) := - { - __catch : exc -> A -> B -> C - }. - -Global Instance CatchNotationExpr {S : Set} (F G : Set -> Type) `{AsSynExpr F} `{AsSynExpr G} : CatchNotation (F S) (G (inc S)) (expr S) := - { - __catch err b h := Catch err (__asSynExpr b) (__asSynExpr h) - }. - -Global Instance CatchNotationK {S : Set} (F : Set -> Type) `{AsSynExpr F} : CatchNotation (cont S) (F (inc S)) (cont S) := - { - __catch err K h := CatchK err K (__asSynExpr h) - }. - - -Notation of_val := Val (only parsing). - -Notation "x '⋆' y" := (__app x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope. -Notation "x '+' y" := (__op x%syn Add y%syn) : syn_scope. -Notation "x '-' y" := (__op x%syn Sub y%syn) : syn_scope. -Notation "x '*' y" := (__op x%syn Mult y%syn) : syn_scope. -Notation "'if' x 'then' y 'else' z" := (__if x%syn y%syn z%syn) : syn_scope. -Notation "'#' n" := (LitV n) (at level 60) : syn_scope. -Notation "'rec' e" := (RecV e%syn) (at level 60) : syn_scope. -Notation "'$' fn" := (set_pure_resolver fn) (at level 60) : syn_scope. -Notation "'try' b 'catch' err '=>' h" := - (__catch err b%syn h%syn) (at level 60) : syn_scope. -Notation "'throw' err v" := - (__throw err v%syn) (at level 60) : syn_scope. -Notation "□" := (EmptyK) : syn_scope. -Notation "K '⟪' e '⟫'" := (fill K%syn e%syn) (at level 60) : syn_scope. - -Definition LamV {S : Set} (e : expr (inc S)) : val S := - RecV (shift e). - -Notation "'λ' . e" := (LamV e%syn) (at level 60) : syn_scope. - -Definition LetE {S : Set} (e : expr S) (e' : expr (inc S)) : expr S := - App (LamV e') (e). - -Notation "'let_' e₁ 'in' e₂" := (LetE e₁%syn e₂%syn) (at level 60, right associativity) : syn_scope. - -Definition SeqE {S : Set} (e e' : expr S) : expr S := - App (LamV (shift e)) e'. - -Notation "e₁ ';;' e₂" := (SeqE e₁%syn e₂%syn) : syn_scope. - -Declare Scope typ_scope. -Delimit Scope typ_scope with typ. - -Notation "'ℕ'" := (Tnat) (at level 1) : typ_scope. -Notation "A →ₜ B" := (Tarr A%typ B%typ) - (right associativity, at level 60) : typ_scope. -**) End Lang.