diff --git a/README.md b/README.md index c74eddd..0724d9a 100644 --- a/README.md +++ b/README.md @@ -30,7 +30,7 @@ to the code structure. - `examples/input_lang/` -- formalization of the language with io, the soundness and adequacy - `examples/affine_lang/` -- formalization of the affine language, type safety of the language interoperability - `examples/input_lang_callcc/` -- formalization of the language with io, throw and call/cc, the soundness and adequacy -- `examples/delim_lang/` -- formalization shift/reset effects, of a language with delimited continuations and its soundness +- `examples/delim_lang/` -- formalization of the language with shift/reset and its soundness/adequacy wrt abstract machine semantics - `prelude.v` -- some stuff that is missing from Iris - `lang_generic.v` -- generic facts about languages with binders and their interpretations, shared by `input_lang` and `affine_lang` diff --git a/_CoqProject b/_CoqProject index 02dc8bc..0359382 100644 --- a/_CoqProject +++ b/_CoqProject @@ -24,6 +24,7 @@ theories/gitree/reify.v theories/gitree/greifiers.v theories/gitree/reductions.v theories/gitree/weakestpre.v +theories/hom.v theories/gitree.v theories/program_logic.v @@ -31,15 +32,20 @@ theories/program_logic.v theories/effects/store.v theories/effects/callcc.v theories/effects/io_tape.v +theories/effects/delim.v theories/lib/pairs.v theories/lib/while.v theories/lib/factorial.v - theories/lib/iter.v +theories/lib/iter.v theories/examples/delim_lang/lang.v +theories/examples/delim_lang/typing.v theories/examples/delim_lang/interp.v +theories/examples/delim_lang/hom.v theories/examples/delim_lang/example.v +theories/examples/delim_lang/logpred.v +theories/examples/delim_lang/logrel.v theories/examples/input_lang_callcc/lang.v theories/examples/input_lang_callcc/interp.v diff --git a/theories/effects/delim.v b/theories/effects/delim.v new file mode 100644 index 0000000..5862e8e --- /dev/null +++ b/theories/effects/delim.v @@ -0,0 +1,299 @@ +(** * Representation of delimited continuations *) +From gitrees Require Import prelude gitree. +From iris.algebra Require Import list. + +(** * State, corresponding to a meta-continuation *) +Definition stateF : oFunctor := (listOF (▶ ∙ -n> ▶ ∙))%OF. + +#[local] Instance state_inhabited : Inhabited (stateF ♯ unitO). +Proof. apply _. Qed. + +#[local] Instance state_cofe X `{!Cofe X} : Cofe (stateF ♯ X). +Proof. apply _. Qed. + +(* We store a list of meta continuations in the state. *) + +(** * Signatures *) + +(** Bind the innermost continuation *) +Program Definition shiftE : opInterp := + {| + Ins := ((▶ ∙ -n> ▶ ∙) -n> ▶ ∙); + Outs := (▶ ∙); + |}. + +(** Delimit the continuation *) +Program Definition resetE : opInterp := + {| + Ins := (▶ ∙); + Outs := (▶ ∙); + |}. + +(** Explicitly pop a continuation from the meta-continuation and jump +to it *) +Program Definition popE : opInterp := + {| + Ins := (▶ ∙); + Outs := Empty_setO; + |}. + +(** Applies continuation, pushes outer context in meta *) +Program Definition appContE : opInterp := + {| + Ins := (▶ ∙ * (▶ (∙ -n> ∙))); + Outs := ▶ ∙; + |} . + +Definition delimE := @[shiftE; resetE; popE;appContE]. + +Notation op_shift := (inl ()). +Notation op_reset := (inr (inl ())). +Notation op_pop := (inr (inr (inl ()))). +Notation op_app_cont := (inr (inr (inr (inl ())))). + +Section reifiers. + Context {X} `{!Cofe X}. + Notation state := (stateF ♯ X). + + Definition reify_shift : ((laterO X -n> laterO X) -n> laterO X) * + state * (laterO X -n> laterO X) → + option (laterO X * state) := + λ '(f, σ, k), Some ((f k): laterO X, σ : state). + #[export] Instance reify_shift_ne : + NonExpansive (reify_shift : + prodO (prodO ((laterO X -n> laterO X) -n> laterO X) state) + (laterO X -n> laterO X) → + optionO (prodO (laterO X) state)). + Proof. intros ?[[]][[]][[]]. simpl in *. repeat f_equiv; auto. Qed. + + Definition reify_reset : (laterO X) * state * (laterO X -n> laterO X) → + option (laterO X * state) := + λ '(e, σ, k), Some (e, (k :: σ)). + #[export] Instance reify_reset_ne : + NonExpansive (reify_reset : + prodO (prodO (laterO X) state) (laterO X -n> laterO X) → + optionO (prodO (laterO X) state)). + Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed. + + + Definition reify_pop : (laterO X) * state * (Empty_setO -n> laterO X) → + option (laterO X * state) := + λ '(e, σ, _), + match σ with + | [] => Some (e, σ) + | k' :: σ' => Some (k' e, σ') + end. + #[export] Instance reify_pop_ne : + NonExpansive (reify_pop : + prodO (prodO (laterO X) state) (Empty_setO -n> laterO X) → + optionO (prodO (laterO X) state)). + Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed. + + + Definition reify_app_cont : ((laterO X * (laterO (X -n> X))) * state * (laterO X -n> laterO X)) → + option (laterO X * state) := + λ '((e, k'), σ, k), + Some (((laterO_ap k' : laterO X -n> laterO X) e : laterO X), k::σ : state). + #[export] Instance reify_app_cont_ne : + NonExpansive (reify_app_cont : + prodO (prodO (prodO (laterO X) (laterO (X -n> X))) state) + (laterO X -n> laterO X) → + optionO (prodO (laterO X) (state))). + Proof. + intros ?[[[]]][[[]]]?. rewrite /reify_app_cont. + repeat f_equiv; apply H. + Qed. + +End reifiers. + +Canonical Structure reify_delim : sReifier CtxDep. +Proof. + simple refine {| + sReifier_ops := delimE; + sReifier_state := stateF + |}. + intros X HX op. + destruct op as [ | [ | [ | [| []]]]]; simpl. + - simple refine (OfeMor (reify_shift)). + - simple refine (OfeMor (reify_reset)). + - simple refine (OfeMor (reify_pop)). + - simple refine (OfeMor (reify_app_cont)). +Defined. + +Section constructors. + Context {E : opsInterp} {A} `{!Cofe A}. + Context {subEff0 : subEff delimE E}. + Context {subOfe0 : SubOfe natO A}. + Context {subOfe1 : SubOfe unitO A}. + Notation IT := (IT E A). + Notation ITV := (ITV E A). + + (** ** POP *) + + Program Definition POP : IT -n> IT := + λne e, Vis (E:=E) (subEff_opid op_pop) + (subEff_ins (F:=delimE) (op:=op_pop) (Next e)) + (Empty_setO_rec _ ◎ (subEff_outs (F:=delimE) (op:=op_pop))^-1). + Solve All Obligations with solve_proper. + + Notation 𝒫 := (get_val POP). + + (** ** RESET *) + + Program Definition RESET_ : (laterO IT -n> laterO IT) -n> + laterO IT -n> + IT := + λne k e, Vis (E:=E) (subEff_opid op_reset) + (subEff_ins (F := delimE) (op := op_reset) (laterO_map 𝒫 e)) + (k ◎ subEff_outs (F := delimE) (op := op_reset)^-1). + Solve Obligations with solve_proper. + + Program Definition RESET : laterO IT -n> IT := + RESET_ idfun. + + (** ** SHIFT *) + + Program Definition SHIFT_ : ((laterO IT -n> laterO IT) -n> laterO IT) -n> + (laterO IT -n> laterO IT) -n> + IT := + λne f k, Vis (E:=E) (subEff_opid op_shift) + (subEff_ins (F:=delimE) (op:=op_shift) ((laterO_map $ 𝒫) ◎ f)) + (k ◎ (subEff_outs (F:=delimE) (op:=op_shift))^-1). + Solve All Obligations with solve_proper. + + Program Definition SHIFT : ((laterO IT -n> laterO IT) -n> laterO IT) -n> IT := + λne f, SHIFT_ f (idfun). + Solve Obligations with solve_proper. + + Lemma hom_SHIFT_ k e f `{!IT_hom f} : + f (SHIFT_ e k) ≡ SHIFT_ e (laterO_map (OfeMor f) ◎ k). + Proof. + unfold SHIFT_. + rewrite hom_vis/=. + f_equiv. by intro. + Qed. + + (** ** APP_CONT *) + + Program Definition APP_CONT_ : laterO IT -n> (laterO (IT -n> IT)) -n> + (laterO IT -n> laterO IT) -n> + IT := + λne e k k', Vis (E := E) (subEff_opid op_app_cont) + (subEff_ins (F:=delimE) (op:=op_app_cont) (e, k)) + (k' ◎ (subEff_outs (F:=delimE) (op:=op_app_cont))^-1). + Solve All Obligations with solve_proper. + + Program Definition APP_CONT : laterO IT -n> (laterO (IT -n> IT)) -n> + IT := + λne e k, APP_CONT_ e k idfun. + Solve All Obligations with solve_proper. + +End constructors. + +Notation 𝒫 := (get_val POP). + +Section weakestpre. + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {subR : subReifier reify_delim rs}. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R}. + Context `{!SubOfe unitO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Notation state := (stateF ♯ IT). + Context `{!invGS Σ, !stateG rs R Σ}. + Notation iProp := (iProp Σ). + + (** * The symbolic execution rules *) + + (** ** SHIFT *) + + Lemma wp_shift (σ : state) (f : (laterO IT -n> laterO IT) -n> laterO IT) + (k : IT -n> IT) β {Hk : IT_hom k} Φ s : + laterO_map 𝒫 (f (laterO_map k)) ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β @ s {{ Φ }}) -∗ + WP@{rs} (k (SHIFT f)) @ s {{ Φ }}. + Proof. + iIntros (Hp) "Hs Ha". + unfold SHIFT. simpl. + rewrite hom_vis. + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (laterO_map 𝒫 $ f (laterO_map k)) with "Hs"). + { + simpl. do 2 f_equiv; last done. do 2 f_equiv. + rewrite ccompose_id_l. intro. simpl. by rewrite ofe_iso_21. + } + { exact Hp. } + iModIntro. + iApply "Ha". + Qed. + + Lemma wp_reset (σ : state) (e : IT) (k : IT -n> IT) {Hk : IT_hom k} + Φ s : + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ + WP@{rs} 𝒫 e @ s {{ Φ }}) -∗ + WP@{rs} k $ (RESET (Next e)) @ s {{ Φ }}. + Proof. + iIntros "Hs Ha". + unfold RESET. simpl. rewrite hom_vis. + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next $ 𝒫 e) with "Hs"). + - simpl. repeat f_equiv. rewrite ccompose_id_l. + trans ((laterO_map k) :: σ); last reflexivity. + f_equiv. intro. simpl. by rewrite ofe_iso_21. + - reflexivity. + - iApply "Ha". + Qed. + + Lemma wp_pop_end (v : IT) + {HV : AsVal v} + Φ s : + has_substate [] -∗ + ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} v @ s {{ Φ }}) -∗ + WP@{rs} 𝒫 v @ s {{ Φ }}. + Proof. + iIntros "Hs Ha". + rewrite get_val_ITV. simpl. + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next v)) with "Hs"). + - simpl. reflexivity. + - reflexivity. + - done. + Qed. + + Lemma wp_pop_cons (σ : state) (v : IT) (k : IT -n> IT) + {HV : AsVal v} + Φ s : + has_substate ((laterO_map k) :: σ) -∗ + ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ v @ s {{ Φ }}) -∗ + WP@{rs} 𝒫 v @ s {{ Φ }}. + Proof. + iIntros "Hs Ha". + rewrite get_val_ITV. simpl. + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next v))) with "Hs"). + - simpl. reflexivity. + - reflexivity. + - done. + Qed. + + Lemma wp_app_cont (σ : state) (e : laterO IT) (k' : laterO (IT -n> IT)) + (k : IT -n> IT) β {Hk : IT_hom k} + Φ s : + laterO_ap k' e ≡ Next β → + has_substate σ -∗ + ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ + WP@{rs} β @ s {{ Φ }}) -∗ + WP@{rs} k (APP_CONT e k') @ s {{ Φ }}. + Proof. + iIntros (Hb) "Hs Ha". + unfold APP_CONT. simpl. rewrite hom_vis. + iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next β) with "Hs"). + - cbn-[laterO_ap]. rewrite Hb. do 2 f_equiv. + trans (laterO_map k :: σ); last reflexivity. + rewrite ccompose_id_l. f_equiv. intro. simpl. by rewrite ofe_iso_21. + - reflexivity. + - iApply "Ha". + Qed. + +End weakestpre. diff --git a/theories/effects/io_tape.v b/theories/effects/io_tape.v index fd34746..3436566 100644 --- a/theories/effects/io_tape.v +++ b/theories/effects/io_tape.v @@ -1,4 +1,4 @@ -(** I/O on a tape effect *) +(** * I/O on a tape effect *) From gitrees Require Import prelude gitree. Record state := State { diff --git a/theories/examples/delim_lang/example.v b/theories/examples/delim_lang/example.v index 60d32fc..2885340 100644 --- a/theories/examples/delim_lang/example.v +++ b/theories/examples/delim_lang/example.v @@ -1,109 +1,113 @@ +(** * Example of a program in delim_lang and its symbolic execution *) From gitrees Require Import gitree lang_generic. +From gitrees.effects Require Import delim. From gitrees.examples.delim_lang Require Import lang interp. From iris.proofmode Require Import base classes tactics environments. From iris.base_logic Require Import algebra. Open Scope syn_scope. +(** The program captures the inner continuation, invokes it with 5 and +6, and adds the results to 1. The result is 1+(3+5)+(3+6)=18 *) Example p : expr Empty_set := ((#1) + (reset ((#3) + (shift/cc ((($0) @k #5) + (($0) @k #6)))))). -Local Definition rs : gReifiers _ _ := gReifiers_cons reify_delim gReifiers_nil. -(* Local Definition Hrs : subReifier reify_delim rs. *) -(* Proof. unfold rs. apply subReifier_here. Qed. *) -Notation F := (gReifiers_ops rs). -Context {R} `{!Cofe R}. -Context `{!SubOfe natO R, !SubOfe unitO R}. -Notation IT := (IT F R). -Notation ITV := (ITV F R). -Context (env : @interp_scope F R _ Empty_set). +Section example. + Local Definition rs : gReifiers _ _ := gReifiers_cons reify_delim gReifiers_nil. + Notation F := (gReifiers_ops rs). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R, !SubOfe unitO R}. + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context (env : @interp_scope F R _ Empty_set). -Example ts := interp_config rs (Cexpr p) env. -Definition t := fst ts. -Definition σ := snd ts. + Definition ts := interp_config rs (Cexpr p) env. + Definition t := fst ts. + Definition σ := snd ts. -Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}. -Notation iProp := (iProp Σ). + Context `{!invGS Σ, !stateG rs R Σ, !heapG rs R Σ}. + Notation iProp := (iProp Σ). -Ltac shift_hom := - match goal with - | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) _ _ _) => - assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t)) ≡ (λne x, k1 (k2 x)) t) as -> by done - | |- envs_entails _ (wp _ (?k ?t) _ _ _) => - assert (k t ≡ (λne x, k x) t) as -> by done - end. + Ltac shift_hom := + match goal with + | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) (?k2 ?t)) _ _ _) => + assert ((ofe_mor_car _ _ (λne x, k1 x) (k2 t)) ≡ (λne x, k1 (k2 x)) t) as -> by done + | |- envs_entails _ (wp _ (?k ?t) _ _ _) => + assert (k t ≡ (λne x, k x) t) as -> by done + end. -Ltac shift_natop_l := - match goal with - | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) - (ofe_mor_car _ _ - (ofe_mor_car _ _ - (NATOP (do_natop lang.Add)) ?t) (IT_of_V ?e))) _ _ _) => - assert ((ofe_mor_car _ _ (λne x, k1 x) (NATOP (do_natop lang.Add) t (IT_of_V e))) ≡ - (λne x, k1 (NATOP (do_natop lang.Add) x (IT_of_V e))) t) as -> by done - end. + Ltac shift_natop_l := + match goal with + | |- envs_entails _ (wp _ (ofe_mor_car _ _ (λne x, ?k1 x) + (ofe_mor_car _ _ + (ofe_mor_car _ _ + (NATOP (do_natop lang.Add)) ?t) (IT_of_V ?e))) _ _ _) => + assert ((ofe_mor_car _ _ (λne x, k1 x) (NATOP (do_natop lang.Add) t (IT_of_V e))) ≡ + (λne x, k1 (NATOP (do_natop lang.Add) x (IT_of_V e))) t) as -> by done + end. -Lemma wp_t (s : gitree.weakestpre.stuckness) : - has_substate σ -∗ - WP@{rs} t @ s {{βv, βv ≡ RetV 18}}. -Proof. - Opaque SHIFT APP_CONT. - iIntros "Hσ". - cbn. - (* first, reset *) - do 2 shift_hom. - iApply (wp_reset with "Hσ"). - iIntros "!> _ Hσ". simpl. + Lemma wp_t (s : gitree.weakestpre.stuckness) : + has_substate σ -∗ + WP@{rs} t @ s {{βv, βv ≡ RetV 18}}. + Proof. + Opaque SHIFT APP_CONT. + iIntros "Hσ". + cbn. + (* first, reset *) + do 2 shift_hom. + iApply (wp_reset with "Hσ"). + iIntros "!> _ Hσ". simpl. - (* then, shift *) - do 2 shift_hom. - iApply (wp_shift with "Hσ"). - { rewrite laterO_map_Next. done. } - iIntros "!>_ Hσ". - simpl. + (* then, shift *) + do 2 shift_hom. + iApply (wp_shift with "Hσ"). + { rewrite laterO_map_Next. done. } + iIntros "!>_ Hσ". + simpl. - (* the rest *) - rewrite -(IT_of_V_Ret 6) get_val_ITV'. simpl. - rewrite get_fun_fun. simpl. - do 2 shift_hom. - iApply (wp_app_cont with "Hσ"); first done. - iIntros "!> _ Hσ". simpl. - rewrite later_map_Next -Tick_eq. - iApply wp_tick. iNext. - shift_hom. - rewrite IT_of_V_Ret NATOP_Ret. simpl. - rewrite -(IT_of_V_Ret 9). - iApply (wp_pop_cons with "Hσ"). - iIntros "!> _ Hσ". - simpl. + (* the rest *) + rewrite -(IT_of_V_Ret 6) get_val_ITV'. simpl. + rewrite get_fun_fun. simpl. + do 2 shift_hom. + iApply (wp_app_cont with "Hσ"); first done. + iIntros "!> _ Hσ". simpl. + rewrite later_map_Next -Tick_eq. + iApply wp_tick. iNext. + shift_hom. + rewrite IT_of_V_Ret NATOP_Ret. simpl. + rewrite -(IT_of_V_Ret 9). + iApply (wp_pop_cons with "Hσ"). + iIntros "!> _ Hσ". + simpl. - shift_hom. shift_natop_l. - rewrite -(IT_of_V_Ret 5) get_val_ITV'. simpl. - shift_hom. shift_natop_l. - rewrite get_fun_fun. simpl. - shift_hom. shift_natop_l. - iApply (wp_app_cont with "Hσ"); first done. - iIntros "!> _ Hσ". simpl. - rewrite later_map_Next -Tick_eq. - iApply wp_tick. iNext. - rewrite (IT_of_V_Ret 5) NATOP_Ret. simpl. - rewrite -(IT_of_V_Ret 8). - iApply (wp_pop_cons with "Hσ"). - iIntros "!> _ Hσ". - simpl. - shift_hom. - shift_natop_l. - rewrite (IT_of_V_Ret 8). - simpl. rewrite IT_of_V_Ret NATOP_Ret. - simpl. rewrite -(IT_of_V_Ret 17). - iApply (wp_pop_cons with "Hσ"). - iIntros "!> _ Hσ". simpl. - rewrite IT_of_V_Ret NATOP_Ret. - simpl. rewrite -(IT_of_V_Ret 18). - iApply (wp_pop_end with "Hσ"). - iIntros "!> _ _". - iApply wp_val. done. -Qed. + shift_hom. shift_natop_l. + rewrite -(IT_of_V_Ret 5) get_val_ITV'. simpl. + shift_hom. shift_natop_l. + rewrite get_fun_fun. simpl. + shift_hom. shift_natop_l. + iApply (wp_app_cont with "Hσ"); first done. + iIntros "!> _ Hσ". simpl. + rewrite later_map_Next -Tick_eq. + iApply wp_tick. iNext. + rewrite (IT_of_V_Ret 5) NATOP_Ret. simpl. + rewrite -(IT_of_V_Ret 8). + iApply (wp_pop_cons with "Hσ"). + iIntros "!> _ Hσ". + simpl. + shift_hom. + shift_natop_l. + rewrite (IT_of_V_Ret 8). + simpl. rewrite IT_of_V_Ret NATOP_Ret. + simpl. rewrite -(IT_of_V_Ret 17). + iApply (wp_pop_cons with "Hσ"). + iIntros "!> _ Hσ". simpl. + rewrite IT_of_V_Ret NATOP_Ret. + simpl. rewrite -(IT_of_V_Ret 18). + iApply (wp_pop_end with "Hσ"). + iIntros "!> _ _". + iApply wp_val. done. + Qed. +End example. diff --git a/theories/examples/delim_lang/hom.v b/theories/examples/delim_lang/hom.v new file mode 100644 index 0000000..7aad45a --- /dev/null +++ b/theories/examples/delim_lang/hom.v @@ -0,0 +1,113 @@ +From gitrees Require Import gitree lang_generic hom. +From gitrees.effects Require Import delim. +From gitrees.examples.delim_lang Require Import lang interp. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Open Scope stdpp_scope. + +Section hom. + Context {sz : nat}. + Context {rs : gReifiers CtxDep sz}. + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R}. + Context `{!subReifier reify_delim rs}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + + Program Definition 𝒫_HOM : HOM (A:=natO) := exist _ 𝒫 _. + Next Obligation. + apply _. + Qed. + + Program Definition AppContRSCtx_HOM {S : Set} + (α : @interp_scope F R _ S -n> IT) + (env : @interp_scope F R _ S) + : HOM := exist _ (interp_app_contrk rs α (λne env, idfun) env) _. + Next Obligation. + intros; simpl. + apply _. + Qed. + + Program Definition AppContLSCtx_HOM {S : Set} + (β : IT) (env : @interp_scope F R _ S) + (Hv : AsVal β) + : HOM := exist _ (interp_app_contlk rs (constO β) (λne env, idfun) env) _. + Next Obligation. + intros; simpl. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - solve_proper_please. + - rewrite get_val_ITV. + rewrite get_val_ITV. + simpl. + rewrite get_fun_tick. + reflexivity. + - rewrite get_val_ITV. + simpl. rewrite get_fun_vis. simpl. + f_equiv. + intros ?; simpl. + apply later_map_ext. + intros ?; simpl. + rewrite get_val_ITV. + simpl. + reflexivity. + - rewrite get_val_ITV. simpl. rewrite get_fun_err. reflexivity. + Qed. + + Program Definition NatOpRSCtx_HOM {S : Set} (op : nat_op) + (α : @interp_scope F R _ S -n> IT) (env : @interp_scope F R _ S) + : HOM := exist _ (interp_natoprk rs op α (λne env, idfun) env) _. + Next Obligation. + intros; simpl. + apply _. + Qed. + + Program Definition NatOpLSCtx_HOM {S : Set} (op : nat_op) + (α : IT) (env : @interp_scope F R _ S) + (Hv : AsVal α) + : HOM := exist _ (interp_natoplk rs op (constO α) (λne env, idfun) env) _. + Next Obligation. + intros; simpl. + apply _. + Qed. + + Program Definition AppLSCtx_HOM {S : Set} + (α : @interp_scope F R _ S -n> IT) + (env : @interp_scope F R _ S) + : HOM := exist _ (interp_applk rs α (λne env, idfun) env) _. + Next Obligation. + intros; simpl. + apply _. + Qed. + + Transparent LET. + Program Definition AppRSCtx_HOM {S : Set} + (β : IT) (env : @interp_scope F R _ S) + (Hv : AsVal β) + : HOM := exist _ (interp_apprk rs (constO β) (λne env, idfun) env) _. + Next Obligation. + intros; simpl. + simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - solve_proper_please. + - rewrite get_val_ITV. + simpl. + rewrite get_val_ITV. + simpl. + rewrite get_val_tick. + reflexivity. + - rewrite get_val_ITV. + simpl. + rewrite get_val_vis. + do 3 f_equiv. + intro; simpl. + rewrite get_val_ITV. + simpl. + reflexivity. + - rewrite get_val_ITV. + simpl. + rewrite get_val_err. + reflexivity. + Qed. + Opaque LET. +End hom. diff --git a/theories/examples/delim_lang/interp.v b/theories/examples/delim_lang/interp.v index 5578614..c049041 100644 --- a/theories/examples/delim_lang/interp.v +++ b/theories/examples/delim_lang/interp.v @@ -1,5 +1,6 @@ -(* From Equations Require Import Equations. *) +(** Interpretation of delim_lang into gitrees *) From gitrees Require Import gitree lang_generic. +From gitrees.effects Require Import delim. From gitrees.examples.delim_lang Require Import lang. From iris.algebra Require Import list. From iris.proofmode Require Import classes tactics. @@ -7,311 +8,6 @@ From iris.base_logic Require Import algebra. Require Import Binding.Lib Binding.Set. - -(** * State, corresponding to a meta-continuation *) -Definition stateF : oFunctor := (listOF (▶ ∙ -n> ▶ ∙))%OF. - -#[local] Instance state_inhabited : Inhabited (stateF ♯ unitO). -Proof. apply _. Qed. - -#[local] Instance state_cofe X `{!Cofe X} : Cofe (stateF ♯ X). -Proof. apply _. Qed. - -(* We store a list of meta continuations in the state. *) - - -(** * Signatures *) - -Program Definition shiftE : opInterp := - {| - Ins := ((▶ ∙ -n> ▶ ∙) -n> ▶ ∙); - Outs := (▶ ∙); - |}. - -Program Definition resetE : opInterp := - {| - Ins := (▶ ∙); - Outs := (▶ ∙); - |}. - -(* to apply the head of the meta continuation *) -Program Definition popE : opInterp := - {| - Ins := (▶ ∙); - Outs := Empty_setO; - |}. - -(* apply continuation, pushes outer context in meta *) -Program Definition appContE : opInterp := - {| - Ins := (▶ ∙ * (▶ (∙ -n> ∙))); - Outs := ▶ ∙; - |} . - -Definition delimE := @[shiftE; resetE; popE;appContE]. - - - -Notation op_shift := (inl ()). -Notation op_reset := (inr (inl ())). -Notation op_pop := (inr (inr (inl ()))). -Notation op_app_cont := (inr (inr (inr (inl ())))). - - - -Section reifiers. - - Context {X} `{!Cofe X}. - Notation state := (stateF ♯ X). - - - Definition reify_shift : ((laterO X -n> laterO X) -n> laterO X) * - state * (laterO X -n> laterO X) → - option (laterO X * state) := - λ '(f, σ, k), Some ((f k): laterO X, σ : state). - #[export] Instance reify_shift_ne : - NonExpansive (reify_shift : - prodO (prodO ((laterO X -n> laterO X) -n> laterO X) state) - (laterO X -n> laterO X) → - optionO (prodO (laterO X) state)). - Proof. intros ?[[]][[]][[]]. simpl in *. repeat f_equiv; auto. Qed. - - Definition reify_reset : (laterO X) * state * (laterO X -n> laterO X) → - option (laterO X * state) := - λ '(e, σ, k), Some (e, (k :: σ)). - #[export] Instance reify_reset_ne : - NonExpansive (reify_reset : - prodO (prodO (laterO X) state) (laterO X -n> laterO X) → - optionO (prodO (laterO X) state)). - Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed. - - - Definition reify_pop : (laterO X) * state * (Empty_setO -n> laterO X) → - option (laterO X * state) := - λ '(e, σ, _), - match σ with - | [] => Some (e, σ) - | k' :: σ' => Some (k' e, σ') - end. - #[export] Instance reify_pop_ne : - NonExpansive (reify_pop : - prodO (prodO (laterO X) state) (Empty_setO -n> laterO X) → - optionO (prodO (laterO X) state)). - Proof. intros ?[[]][[]][[]]. simpl in *. by repeat f_equiv. Qed. - - - Definition reify_app_cont : ((laterO X * (laterO (X -n> X))) * state * (laterO X -n> laterO X)) → - option (laterO X * state) := - λ '((e, k'), σ, k), - Some (((laterO_ap k' : laterO X -n> laterO X) e : laterO X), k::σ : state). - #[export] Instance reify_app_cont_ne : - NonExpansive (reify_app_cont : - prodO (prodO (prodO (laterO X) (laterO (X -n> X))) state) - (laterO X -n> laterO X) → - optionO (prodO (laterO X) (state))). - Proof. - intros ?[[[]]][[[]]]?. rewrite /reify_app_cont. - repeat f_equiv; apply H. - Qed. - -End reifiers. - -Canonical Structure reify_delim : sReifier CtxDep. -Proof. - simple refine {| - sReifier_ops := delimE; - sReifier_state := stateF - |}. - intros X HX op. - destruct op as [ | [ | [ | [| []]]]]; simpl. - - simple refine (OfeMor (reify_shift)). - - simple refine (OfeMor (reify_reset)). - - simple refine (OfeMor (reify_pop)). - - simple refine (OfeMor (reify_app_cont)). -Defined. - - - -Section constructors. - Context {E : opsInterp} {A} `{!Cofe A}. - Context {subEff0 : subEff delimE E}. - Context {subOfe0 : SubOfe natO A}. - Context {subOfe1 : SubOfe unitO A}. - Notation IT := (IT E A). - Notation ITV := (ITV E A). - - - - (** ** POP *) - - Program Definition POP : IT -n> IT := - λne e, Vis (E:=E) (subEff_opid op_pop) - (subEff_ins (F:=delimE) (op:=op_pop) (Next e)) - (Empty_setO_rec _ ◎ (subEff_outs (F:=delimE) (op:=op_pop))^-1). - Solve All Obligations with solve_proper. - - Notation 𝒫 := (get_val POP). - - (** ** RESET *) - - Program Definition RESET_ : (laterO IT -n> laterO IT) -n> - laterO IT -n> - IT := - λne k e, Vis (E:=E) (subEff_opid op_reset) - (subEff_ins (F := delimE) (op := op_reset) (laterO_map 𝒫 e)) - (k ◎ subEff_outs (F := delimE) (op := op_reset)^-1). - Solve Obligations with solve_proper. - - Program Definition RESET : laterO IT -n> IT := - RESET_ idfun. - - (** ** SHIFT *) - - Program Definition SHIFT_ : ((laterO IT -n> laterO IT) -n> laterO IT) -n> - (laterO IT -n> laterO IT) -n> - IT := - λne f k, Vis (E:=E) (subEff_opid op_shift) - (subEff_ins (F:=delimE) (op:=op_shift) ((laterO_map $ 𝒫) ◎ f)) - (k ◎ (subEff_outs (F:=delimE) (op:=op_shift))^-1). - Solve All Obligations with solve_proper. - - Program Definition SHIFT : ((laterO IT -n> laterO IT) -n> laterO IT) -n> IT := - λne f, SHIFT_ f (idfun). - Solve Obligations with solve_proper. - - Lemma hom_SHIFT_ k e f `{!IT_hom f} : - f (SHIFT_ e k) ≡ SHIFT_ e (laterO_map (OfeMor f) ◎ k). - Proof. - unfold SHIFT_. - rewrite hom_vis/=. - f_equiv. by intro. - Qed. - - - (** ** APP_CONT *) - - Program Definition APP_CONT_ : laterO IT -n> (laterO (IT -n> IT)) -n> - (laterO IT -n> laterO IT) -n> - IT := - λne e k k', Vis (E := E) (subEff_opid op_app_cont) - (subEff_ins (F:=delimE) (op:=op_app_cont) (e, k)) - (k' ◎ (subEff_outs (F:=delimE) (op:=op_app_cont))^-1). - Solve All Obligations with solve_proper. - - Program Definition APP_CONT : laterO IT -n> (laterO (IT -n> IT)) -n> - IT := - λne e k, APP_CONT_ e k idfun. - Solve All Obligations with solve_proper. - -End constructors. - -Notation 𝒫 := (get_val POP). - -Section weakestpre. - Context {sz : nat}. - Variable (rs : gReifiers CtxDep sz). - Context {subR : subReifier reify_delim rs}. - Notation F := (gReifiers_ops rs). - Context {R} `{!Cofe R}. - Context `{!SubOfe natO R}. - Context `{!SubOfe unitO R}. - Notation IT := (IT F R). - Notation ITV := (ITV F R). - Notation state := (stateF ♯ IT). - Context `{!invGS Σ, !stateG rs R Σ}. - Notation iProp := (iProp Σ). - - (** * The symbolic execution rules *) - - (** ** SHIFT *) - - Lemma wp_shift (σ : state) (f : (laterO IT -n> laterO IT) -n> laterO IT) - (k : IT -n> IT) β {Hk : IT_hom k} Φ s : - laterO_map 𝒫 (f (laterO_map k)) ≡ Next β → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} β @ s {{ Φ }}) -∗ - WP@{rs} (k (SHIFT f)) @ s {{ Φ }}. - Proof. - iIntros (Hp) "Hs Ha". - unfold SHIFT. simpl. - rewrite hom_vis. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (laterO_map 𝒫 $ f (laterO_map k)) with "Hs"). - { - simpl. do 2 f_equiv; last done. do 2 f_equiv. - rewrite ccompose_id_l. intro. simpl. by rewrite ofe_iso_21. - } - { exact Hp. } - iModIntro. - iApply "Ha". - Qed. - - Lemma wp_reset (σ : state) (e : IT) (k : IT -n> IT) {Hk : IT_hom k} - Φ s : - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ - WP@{rs} 𝒫 e @ s {{ Φ }}) -∗ - WP@{rs} k $ (RESET (Next e)) @ s {{ Φ }}. - Proof. - iIntros "Hs Ha". - unfold RESET. simpl. rewrite hom_vis. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next $ 𝒫 e) with "Hs"). - - simpl. repeat f_equiv. rewrite ccompose_id_l. - trans ((laterO_map k) :: σ); last reflexivity. - f_equiv. intro. simpl. by rewrite ofe_iso_21. - - reflexivity. - - iApply "Ha". - Qed. - - (** XXX: Formulate the rules using AsVal *) - Lemma wp_pop_end (v : ITV) - Φ s : - has_substate [] -∗ - ▷ (£ 1 -∗ has_substate [] -∗ WP@{rs} IT_of_V v @ s {{ Φ }}) -∗ - WP@{rs} 𝒫 (IT_of_V v) @ s {{ Φ }}. - Proof. - iIntros "Hs Ha". - rewrite get_val_ITV. simpl. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((Next $ IT_of_V v)) with "Hs"). - - simpl. reflexivity. - - reflexivity. - - done. - Qed. - - Lemma wp_pop_cons (σ : state) (v : ITV) (k : IT -n> IT) - Φ s : - has_substate ((laterO_map k) :: σ) -∗ - ▷ (£ 1 -∗ has_substate σ -∗ WP@{rs} k $ IT_of_V v @ s {{ Φ }}) -∗ - WP@{rs} 𝒫 (IT_of_V v) @ s {{ Φ }}. - Proof. - iIntros "Hs Ha". - rewrite get_val_ITV. simpl. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ ((laterO_map k (Next $ IT_of_V v))) with "Hs"). - - simpl. reflexivity. - - reflexivity. - - done. - Qed. - - Lemma wp_app_cont (σ : state) (e : laterO IT) (k' : laterO (IT -n> IT)) - (k : IT -n> IT) β {Hk : IT_hom k} - Φ s : - laterO_ap k' e ≡ Next β → - has_substate σ -∗ - ▷ (£ 1 -∗ has_substate ((laterO_map k) :: σ) -∗ - WP@{rs} β @ s {{ Φ }}) -∗ - WP@{rs} k (APP_CONT e k') @ s {{ Φ }}. - Proof. - iIntros (Hb) "Hs Ha". - unfold APP_CONT. simpl. rewrite hom_vis. - iApply (wp_subreify_ctx_dep _ _ _ _ _ _ _ (Next β) with "Hs"). - - cbn-[laterO_ap]. rewrite Hb. do 2 f_equiv. - trans (laterO_map k :: σ); last reflexivity. - rewrite ccompose_id_l. f_equiv. intro. simpl. by rewrite ofe_iso_21. - - reflexivity. - - iApply "Ha". - Qed. - -End weakestpre. - Section interp. Context {sz : nat}. Variable (rs : gReifiers CtxDep sz). @@ -326,11 +22,9 @@ Section interp. Context `{!invGS Σ, !stateG rs R Σ}. Notation iProp := (iProp Σ). - Global Instance denot_cont_ne (κ : IT -n> IT) : - NonExpansive (λ x : IT, Tau (laterO_map κ (Next x))). - Proof. - solve_proper. - Qed. + Global Instance denot_cont_ne (κ : later IT -n> later IT) : + NonExpansive (λ x : IT, Tau (κ (Next x))). + Proof. solve_proper. Defined. (** * Interpreting individual operators *) @@ -346,7 +40,7 @@ Section interp. interp_scope S -n> IT := λne env, SHIFT (λne (k : laterO IT -n> laterO IT), Next (e (extend_scope env (λit x, Tau (k (Next x)))))). - Next Obligation. solve_proper. Qed. + Next Obligation. intros; apply denot_cont_ne. Defined. Next Obligation. solve_proper_prepare. repeat f_equiv. @@ -362,7 +56,6 @@ Section interp. repeat f_equiv. Qed. - (** ** NATOP *) 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). @@ -419,13 +112,22 @@ Section interp. simpl. unfold ir_unf. intro. simpl. reflexivity. Qed. - (** ** APP *) 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 ]. + λne env, + LET (t1 env) $ λne f, + LET (t2 env) $ λne x, + APP' f x. + Solve All Obligations with solve_proper_please. + Global Instance interp_app_ne A : NonExpansive2 (@interp_app A). - Proof. solve_proper. Qed. + Proof. + solve_proper_prepare. + f_equiv. + - by f_equiv. + - intro; simpl. + by do 2 f_equiv. + Qed. Typeclasses Opaque interp_app. (** ** APP_CONT *) @@ -470,12 +172,37 @@ Section interp. Program Definition interp_apprk {A} (q : A -n> IT) (K : A -n> IT -n> IT) : A -n> IT -n> IT := λne env t, (K env) $ interp_app q (λne env, t) env. - Solve All Obligations with solve_proper. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + do 2 f_equiv. + intro; simpl. + by do 2 f_equiv. + Qed. + Next Obligation. + solve_proper_prepare. + f_equiv; first solve_proper. + f_equiv; first solve_proper. + intro; simpl. + solve_proper. + Qed. Program Definition interp_applk {A} (q : A -n> IT) (K : A -n> IT -n> IT) : A -n> IT -n> IT := λne env t, (K env) $ interp_app (λne env, t) q env. - Solve All Obligations with solve_proper. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper. + Qed. + Next Obligation. + solve_proper_prepare. + f_equiv; first solve_proper. + f_equiv; first solve_proper. + Qed. Program Definition interp_app_contrk {A} (q : A -n> IT) (K : A -n> IT -n> IT) : A -n> IT -n> IT := @@ -538,8 +265,8 @@ Section interp. match K with | END => λne env x, x | IfK e1 e2 K => interp_ifk (interp_expr e1) (interp_expr e2) (interp_cont K) - | AppLK v K => interp_applk (interp_val v) (interp_cont K) - | AppRK e K => interp_apprk (interp_expr e) (interp_cont K) + | AppLK e K => interp_applk (interp_expr e) (interp_cont K) + | AppRK v K => interp_apprk (interp_val v) (interp_cont K) | AppContLK v K => interp_app_contlk (interp_val v) (interp_cont K) | AppContRK e K => interp_app_contrk (interp_expr e) (interp_cont K) | NatOpLK op v K => interp_natoplk op (interp_val v) (interp_cont K) @@ -619,12 +346,18 @@ Section interp. interp_cont (fmap δ K) env ≡ interp_cont K (ren_scope δ env). Proof. - destruct e; simpl; try by repeat f_equiv. + + f_equiv; first by rewrite interp_expr_ren. + intro; simpl. + f_equiv; by rewrite interp_expr_ren. + f_equiv; last by rewrite interp_expr_ren. f_equiv. intro. simpl. by f_equiv. - + repeat f_equiv. intro; simpl; repeat f_equiv. - rewrite interp_expr_ren. f_equiv. - intros [|a]; simpl; last done. - by repeat f_equiv. + + f_equiv; last eauto. f_equiv. intro. simpl. + rewrite !laterO_map_Next. + repeat f_equiv. + rewrite interp_expr_ren. + f_equiv. + intros [| ?]; simpl; first done. + reflexivity. - destruct e; simpl. + reflexivity. + clear -interp_expr_ren. @@ -646,17 +379,28 @@ Section interp. apply interp_cont_ren. - destruct K; try solve [simpl; repeat f_equiv; intro; simpl; repeat f_equiv; (apply interp_expr_ren || apply interp_val_ren || apply interp_cont_ren)]. - + intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. - intro. simpl. by repeat f_equiv. - + intro. simpl. f_equiv; eauto. do 2 f_equiv. - intro. simpl. by repeat f_equiv. + + intro. simpl. f_equiv; eauto. + f_equiv; first by rewrite interp_val_ren. + intro; simpl. + reflexivity. + + intro. simpl. f_equiv; eauto. + f_equiv. + intro; simpl. + f_equiv. + by rewrite interp_expr_ren. + + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv. + + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv. 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. elim : K e env; eauto. - intros. simpl. rewrite H. f_equiv. simpl. - do 2 f_equiv. intro. simpl. by repeat f_equiv. + - intros. simpl. rewrite H. f_equiv. simpl. + f_equiv. + intro; simpl. + reflexivity. + - intros. simpl. rewrite H. f_equiv. simpl. + do 2 f_equiv. intro. simpl. by repeat f_equiv. Qed. Program Definition sub_scope {S S'} (δ : S [⇒] S') (env : interp_scope S') @@ -686,11 +430,19 @@ Section interp. interp_cont (bind δ K) env ≡ interp_cont K (sub_scope δ env). Proof. - destruct e; simpl; try by repeat f_equiv. + + f_equiv; first by rewrite interp_expr_subst. + intro; simpl. + f_equiv; first by rewrite interp_expr_subst. + f_equiv; last eauto. f_equiv. intro. simpl. by repeat f_equiv. - + repeat f_equiv. repeat (intro; simpl; repeat f_equiv). - rewrite interp_expr_subst. f_equiv. - intros [|a]; simpl; repeat f_equiv. rewrite interp_expr_ren. - f_equiv. intro. done. + + f_equiv; last eauto. f_equiv. intro. simpl. + rewrite !laterO_map_Next. + repeat f_equiv. + rewrite interp_expr_subst. + f_equiv. + intros [| ?]; simpl; first done. + rewrite interp_expr_ren. + f_equiv. + intros ?; simpl; done. - destruct e; simpl. + reflexivity. + clear -interp_expr_subst. @@ -716,12 +468,19 @@ Section interp. by rewrite interp_cont_subst. - destruct K; try solve [simpl; repeat f_equiv; intro; simpl; repeat f_equiv; (apply interp_expr_subst || apply interp_val_subst || apply interp_cont_subst)]. + + intro; simpl. + f_equiv; first by rewrite interp_cont_subst. + f_equiv; first by rewrite interp_val_subst. + intro; simpl; reflexivity. + + intro; simpl. + f_equiv; first by rewrite interp_cont_subst. + f_equiv. + intro; simpl. + f_equiv; first by rewrite interp_expr_subst. + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv. + simpl. intro. simpl. f_equiv; eauto. f_equiv; eauto. f_equiv. intro. simpl. by repeat f_equiv. Qed. - - (** ** Interpretation of continuations is a homormophism *) #[local] Instance interp_cont_hom_emp {S} env : @@ -748,36 +507,63 @@ Section interp. apply hom_err. Qed. - + Transparent LET. #[local] Instance interp_cont_hom_appr {S} (K : cont S) - (e : expr S) env : + (v : val S) (env : interp_scope S) : IT_hom (interp_cont K env) -> - IT_hom (interp_cont (AppRK e K) env). + IT_hom (interp_cont (AppRK v 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. + pose proof (interp_val_asval v (D := env)) as HHH. + intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. + - rewrite <-hom_tick. + f_equiv. + rewrite ->2 get_val_ITV. + simpl. + rewrite get_val_tick. + reflexivity. + - rewrite get_val_ITV. + simpl. + rewrite ->2 hom_vis. + f_equiv. + intro; simpl. + rewrite <-laterO_map_compose. + do 2 f_equiv. + intro; simpl. + rewrite get_val_ITV. + simpl. + reflexivity. + - rewrite <-hom_err. + rewrite get_val_ITV. + simpl. + f_equiv. + rewrite get_val_err. + reflexivity. Qed. + Opaque LET. + Transparent LET. #[local] Instance interp_cont_hom_appl {S} (K : cont S) - (v : val S) (env : interp_scope S) : + (e : expr S) env : IT_hom (interp_cont K env) -> - IT_hom (interp_cont (AppLK v K) env). + IT_hom (interp_cont (AppLK e K) env). Proof. intros H. simple refine (IT_HOM _ _ _ _ _); intros; simpl. - - rewrite -hom_tick. f_equiv. apply APP'_Tick_l. apply interp_val_asval. - - trans (Vis op i (laterO_map (λne y, - (λne t : IT, interp_cont K env (t ⊙ (interp_val v env))) - y) ◎ ko)); - last (simpl; do 3 f_equiv; by intro). - by rewrite -hom_vis. - - trans (interp_cont K env (Err e)); - first (f_equiv; apply APP'_Err_l; apply interp_val_asval). - apply hom_err. + - rewrite <-hom_tick. + f_equiv. + rewrite get_val_tick. + reflexivity. + - rewrite !hom_vis. + f_equiv. + intro; simpl. + rewrite <-laterO_map_compose. + reflexivity. + - rewrite <-hom_err. + f_equiv. + rewrite hom_err. + rewrite get_val_err. + reflexivity. Qed. - + Opaque LET. #[local] Instance interp_cont_hom_app_contr {S} (K : cont S) (e : expr S) env : @@ -807,7 +593,6 @@ Section interp. - rewrite get_val_ITV. simpl. rewrite get_fun_err. apply hom_err. Qed. - #[local] Instance interp_cont_hom_natopr {S} (K : cont S) (e : expr S) op env : IT_hom (interp_cont K env) -> @@ -841,7 +626,8 @@ Section interp. (K : cont S) env : IT_hom (interp_cont K env). Proof. - induction K; simpl; apply _. + induction K; simpl; try apply _. + by apply interp_cont_hom_appr. Qed. (** ** Finally, preservation of reductions *) @@ -852,15 +638,34 @@ Section interp. (interp_config C' env) = (t', σ') -> t ≡ Tick_n n $ t'. Proof. - inversion 1; cbn-[IF APP' Tick get_ret2]; intros Ht Ht'; inversion Ht; inversion Ht'; try done. + inversion 1; cbn-[IF LET APP' Tick get_ret2]; intros Ht Ht'; inversion Ht; inversion Ht'; try done. + - do 3 f_equiv. + intro; simpl. + reflexivity. - do 4 f_equiv. intro. simpl. by repeat f_equiv. - rewrite -hom_tick. f_equiv. - erewrite APP_APP'_ITV; last apply _. - trans (interp_cont k env (APP (Fun (Next (ir_unf (interp_expr e) env))) (Next $ interp_val v env))). - { repeat f_equiv. apply interp_rec_unfold. } - rewrite APP_Fun. simpl. rewrite hom_tick. do 2 f_equiv. + match goal with + | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] => + set (F := b) + end. + trans (interp_cont k env (LET (Fun (Next (ir_unf (interp_expr e) env))) F)). + { + do 3 f_equiv. + apply interp_rec_unfold. + } + subst F. + rewrite LET_Val. + simpl. + rewrite LET_Val. + simpl. + rewrite APP'_Fun_l. + rewrite laterO_map_Next. + rewrite <-Tick_eq. + rewrite hom_tick. + do 2 f_equiv. simplify_eq. rewrite !interp_expr_subst. + simpl. f_equiv. intros [| [| x]]; simpl; [| reflexivity | reflexivity]. rewrite interp_val_ren. @@ -954,10 +759,11 @@ Section interp. | |- context G [ofe_mor_car _ _ (get_fun _) (ofe_mor_car _ _ Fun ?f)] => set (fin := f) end. + trans (reify (gReifiers_sReifier rs) (APP_CONT_ (Next (interp_val v env)) fin kk) - (gState_recomp σr (sR_state (σ)))). + (gState_recomp σr (sR_state σ))). { repeat f_equiv. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl. rewrite !hom_vis. f_equiv. subst kk. rewrite ccompose_id_l. intro. simpl. @@ -1034,20 +840,20 @@ Section interp. assert ((n', m').1 = n') as Hn' by done. rewrite <-Heqc2 in IHs. specialize (IHs s n' t2 t' σ2 σ' Hn' Heqc2 Ht'). - inversion H0; subst; - try solve [specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H0 Ht Heqc2) as Heq; - specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H0 Ht Heqc2) as <-; + inversion H2; subst; + try solve [specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H2 Ht Heqc2) as Heq; + specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H2 Ht Heqc2) as <-; simpl in Heq|-*; rewrite Heq; eapply IHs]; try solve [eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done; - specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq; + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq; cbn in Ht; eapply sstep_reify; last done; inversion Ht; rewrite !hom_vis; done]. + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. - specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H0 Ht Heqc2) as Heq. - specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H0 Ht Heqc2) as <-. + specialize (interp_cred_no_reify env _ _ _ _ _ _ _ H2 Ht Heqc2) as Heq. + specialize (interp_cred_no_reify_state env _ _ _ _ _ _ _ H2 Ht Heqc2) as <-. simpl in Heq|-*; rewrite Heq. constructor; eauto. - + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq. + + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq. simpl in Heq|-*. change (2+n') with (1+(1+n')). eapply ssteps_many; last first. @@ -1058,13 +864,13 @@ Section interp. rewrite get_val_ITV. simpl. rewrite get_fun_fun. simpl. rewrite !hom_vis. done. + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. - specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq. + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq. cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl. eapply sstep_reify; simpl in Heq; last first. * rewrite -Heq. f_equiv. f_equiv. rewrite get_val_ITV. simpl. done. * f_equiv. reflexivity. + eapply ssteps_many with t2 (gState_recomp σr (sR_state σ2)); last done. - specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H0 Ht Heqc2) as Heq. + specialize (interp_cred_yes_reify env _ _ _ _ _ _ σr _ H2 Ht Heqc2) as Heq. cbn in Ht; inversion Ht. subst. rewrite get_val_ITV. simpl. eapply sstep_reify; simpl in Heq; last first. * rewrite -Heq. repeat f_equiv. by rewrite get_val_ITV. diff --git a/theories/examples/delim_lang/lang.v b/theories/examples/delim_lang/lang.v index dbd9688..0a1daf9 100644 --- a/theories/examples/delim_lang/lang.v +++ b/theories/examples/delim_lang/lang.v @@ -1,7 +1,11 @@ -From gitrees Require Export prelude. +(** * delim-lang: a language with shift/reset and the abstract machine semantics +Based on Malgorzata Biernacka; Dariusz Biernacki; Olivier Danvy +An Operational Foundation for Delimited Continuations in the CPS Hierarchy + *) +From gitrees Require Export prelude. +From stdpp Require Import gmap. Require Import Binding.Resolver Binding.Lib Binding.Set Binding.Auto Binding.Env. -(* Require Import FunctionalExtensionality. *) Variant nat_op := Add | Sub | Mult. @@ -26,17 +30,16 @@ with val {X : Set} := with cont {X : Set} := | END : cont | IfK (e1 : expr) (e2 : expr) : cont -> cont -| AppLK (v : val) : cont -> cont (* ◻ v *) -| AppRK (e : expr) : cont -> cont (* e ◻ *) +| AppRK (v : val) : cont -> cont (* v ◻ *) +| AppLK (e : expr) : cont -> cont (* ◻ e *) | AppContLK (v : val) : cont -> cont (* ◻ v *) | AppContRK (e : expr) : cont -> cont (* e ◻ *) | NatOpLK (op : nat_op) (v : val) : cont -> cont (* ◻ + v *) -| NatOpRK (op : nat_op) (e : expr) : cont -> cont. (* e + ◻ *) - +| NatOpRK (op : nat_op) (e : expr) : cont -> cont (* e + ◻ *) +. (* conts are inside-out contexts: eg IfK e1 e2 (AppLK v ◻) ==> App (if ◻ then e1 else e2) v*) - Arguments val X%bind : clear implicits. Arguments expr X%bind : clear implicits. Arguments cont X%bind : clear implicits. @@ -65,8 +68,8 @@ with kmap {A B : Set} (f : A [→] B) (K : cont A) : cont B := match K with | END => END | IfK e1 e2 k => IfK (emap f e1) (emap f e2) (kmap f k) - | AppLK v k => AppLK (vmap f v) (kmap f k) - | AppRK e k => AppRK (emap f e) (kmap f k) + | AppLK v k => AppLK (emap f v) (kmap f k) + | AppRK e k => AppRK (vmap f e) (kmap f k) | AppContLK v k => AppContLK (vmap f v) (kmap f k) | AppContRK e k => AppContRK (emap f e) (kmap f k) | NatOpLK op v k => NatOpLK op (vmap f v) (kmap f k) @@ -102,8 +105,8 @@ with kbind {A B : Set} (f : A [⇒] B) (K : cont A) : cont B := match K with | END => END | IfK e1 e2 k => IfK (ebind f e1) (ebind f e2) (kbind f k) - | AppLK v k => AppLK (vbind f v) (kbind f k) - | AppRK e k => AppRK (ebind f e) (kbind f k) + | AppLK v k => AppLK (ebind f v) (kbind f k) + | AppRK e k => AppRK (vbind f e) (kbind f k) | AppContLK v k => AppContLK (vbind f v) (kbind f k) | AppContRK e k => AppContRK (ebind f e) (kbind f k) | NatOpLK op v k => NatOpLK op (vbind f v) (kbind f k) @@ -281,15 +284,14 @@ Fixpoint fill {X : Set} (K : cont X) (e : expr X) : expr X := match K with | IfK e1 e2 K => fill K (If e e1 e2) | END => e - | AppLK v K => fill K (App e (Val v)) - | AppRK el K => fill K (App el e) + | AppRK v K => fill K (App (Val v) e) + | AppLK el K => fill K (App e el) | AppContLK v K => fill K (AppCont e (Val v)) | AppContRK el K => fill K (AppCont el e) | NatOpLK op v K => fill K (NatOp op e (Val v)) | NatOpRK op el K => fill K (NatOp op el e) end. - (*** Continuation operations *) @@ -308,8 +310,8 @@ Fixpoint cont_compose {S} (K1 K2 : cont S) : cont S := match K2 with | END => K1 | IfK e1 e2 K => IfK e1 e2 (cont_compose K1 K) - | AppLK v K => AppLK v (cont_compose K1 K) - | AppRK e K => AppRK e (cont_compose K1 K) + | AppLK e K => AppLK e (cont_compose K1 K) + | AppRK v K => AppRK v (cont_compose K1 K) | AppContLK v K => AppContLK v (cont_compose K1 K) | AppContRK e K => AppContRK e (cont_compose K1 K) | NatOpLK op v K => NatOpLK op v (cont_compose K1 K) @@ -322,20 +324,18 @@ Proof. intros H K1 e; simpl; by rewrite H. 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. - (*** Abstract Machine semantics *) Definition Mcont {S} := list $ cont S. Variant config {S} : Type := - | Ceval : expr S -> cont S -> @Mcont S -> config + | Ceval : expr S -> cont S -> @Mcont S → config | Ccont : cont S -> val S -> @Mcont S -> config | Cmcont : @Mcont S -> val S -> config | Cexpr : expr S -> config @@ -345,76 +345,73 @@ Reserved Notation "c '===>' c' / nm" (at level 40, c', nm at level 30). Variant Cred {S : Set} : config -> config -> (nat * nat) -> Prop := +(* init *) +| Ceval_init : forall (e : expr S), + (Cexpr e) ===> (Ceval e END []) / (0,0) - (* init *) - | Ceval_init : forall (e : expr S), - Cexpr e ===> Ceval e END [] / (0,0) - - (* eval *) - | Ceval_val : forall v k mk, - Ceval (Val v) k mk ===> Ccont k v mk / (0,0) +(* eval *) +| Ceval_val : forall v k mk, + (Ceval (Val v) k mk) ===> (Ccont k v mk) / (0,0) - | Ceval_app : forall e0 e1 k mk, - Ceval (App e0 e1) k mk ===> Ceval e1 (AppRK e0 k) mk / (0,0) +| Ceval_app : forall e0 e1 k mk, + (Ceval (App e0 e1) k mk) ===> (Ceval e0 (AppLK e1 k) mk) / (0,0) - | Ceval_app_cont : forall e0 e1 k mk, - Ceval (AppCont e0 e1) k mk ===> Ceval e1 (AppContRK e0 k) mk / (0,0) +| Ceval_app_cont : forall e0 e1 k mk, + (Ceval (AppCont e0 e1) k mk) ===> (Ceval e1 (AppContRK e0 k) mk) / (0,0) - | Ceval_natop : forall op e0 e1 k mk, - Ceval (NatOp op e0 e1) k mk ===> Ceval e1 (NatOpRK op e0 k) mk / (0,0) +| Ceval_natop : forall op e0 e1 k mk, + (Ceval (NatOp op e0 e1) k mk) ===> (Ceval e1 (NatOpRK op e0 k) mk) / (0,0) - | Ceval_if : forall eb et ef k mk, - Ceval (If eb et ef) k mk ===> Ceval eb (IfK et ef k) mk / (0,0) +| Ceval_if : forall eb et ef k mk, + (Ceval (If eb et ef) k mk) ===> (Ceval eb (IfK et ef k) mk) / (0,0) - | Ceval_reset : forall e k mk, - Ceval (Reset e) k mk ===> Ceval e END (k :: mk) / (1, 1) +| Ceval_reset : forall e k mk, + (Ceval (Reset e) k mk) ===> (Ceval e END (k :: mk)) / (1, 1) - | Ceval_shift : forall (e : expr $ inc S) k mk, - Ceval (Shift e) k mk ===> - Ceval (subst (Inc := inc) e (Val $ ContV k)) - END mk / (1, 1) +| Ceval_shift : forall (e : expr $ inc S) k mk, + (Ceval (Shift e) k mk) ===> + (Ceval (subst (Inc := inc) e (Val $ ContV k)) END mk) / (1, 1) - (* cont *) - | Ccont_end : forall v mk, - Ccont END v mk ===> Cmcont mk v / (0,0) +(* cont *) +| Ccont_end : forall v mk, + (Ccont END v mk) ===> (Cmcont mk v) / (0,0) - | Ccont_appr : forall e v k mk, - Ccont (AppRK e k) v mk ===> Ceval e (AppLK v k) mk / (0, 0) +| Ccont_appl : forall e v k mk, + (Ccont (AppLK e k) v mk) ===> (Ceval e (AppRK v k) mk) / (0, 0) - | Ccont_app_contr : forall e v k mk, - Ccont (AppContRK e k) v mk ===> Ceval e (AppContLK v k) mk / (0, 0) +| Ccont_app_contr : forall e v k mk, + (Ccont (AppContRK e k) v mk) ===> (Ceval e (AppContLK v k) mk) / (0, 0) - | Ccont_appl : forall e v k mk, - Ccont (AppLK v k) (RecV e) mk ===> - Ceval (subst (Inc := inc) - (subst (F := expr) (Inc := inc) e - (Val (shift (Inc := inc) v))) - (Val (RecV e))) k mk / (1, 0) +| Ccont_appr : forall e v k mk, + (Ccont (AppRK (RecV e) k) v mk) ===> + (Ceval (subst (Inc := inc) + (subst (F := expr) (Inc := inc) e + (Val (shift (Inc := inc) v))) + (Val (RecV e))) k mk) / (1, 0) - | Ccont_cont : forall v k k' mk, - Ccont (AppContLK v k) (ContV k') mk ===> - Ccont k' v (k :: mk) / (2, 1) +| Ccont_cont : forall v k k' mk, + (Ccont (AppContLK v k) (ContV k') mk) ===> + (Ccont k' v (k :: mk)) / (2, 1) - | Ccont_if : forall et ef n k mk, - Ccont (IfK et ef k) (LitV n) mk ===> - Ceval (if (n =? 0) then ef else et) k mk / (0, 0) +| Ccont_if : forall et ef n k mk, + (Ccont (IfK et ef k) (LitV n) mk) ===> + (Ceval (if (n =? 0) then ef else et) k mk) / (0, 0) - | Ccont_natopr : forall op e v k mk, - Ccont (NatOpRK op e k) v mk ===> - Ceval e (NatOpLK op v k) mk / (0, 0) +| Ccont_natopr : forall op e v k mk, + (Ccont (NatOpRK op e k) v mk) ===> + (Ceval e (NatOpLK op v k) mk) / (0, 0) - | Ccont_natopl : forall op v0 v1 v2 k mk, - nat_op_interp op v0 v1 = Some v2 -> - Ccont (NatOpLK op v1 k) v0 mk ===> - Ceval (Val v2) k mk / (0,0) +| Ccont_natopl : forall op v0 v1 v2 k mk, + nat_op_interp op v0 v1 = Some v2 -> + (Ccont (NatOpLK op v1 k) v0 mk) ===> + (Ceval (Val v2) k mk) / (0,0) - (* meta-cont *) - | Cmcont_cont : forall k mk v, - Cmcont (k :: mk) v ===> Ccont k v mk / (1,1) - - | Cmcont_ret : forall v, - Cmcont [] v ===> Cret v / (1, 1) +(* meta-cont *) +| Cmcont_cont : forall k mk v, + (Cmcont (k :: mk) v) ===> (Ccont k v mk) / (1,1) +| Cmcont_ret : forall v, + (Cmcont [] v) ===> (Cret v) / (1, 1) where "c ===> c' / nm" := (Cred c c' nm). Arguments Mcont S%bind : clear implicits. @@ -422,105 +419,85 @@ Arguments config S%bind : clear implicits. Inductive steps {S} : config S -> config S -> (nat * nat) -> Prop := | steps_zero : forall c, - steps c c (0,0) -| steps_many : forall c1 c2 c3 n m n' m', - c1 ===> c2 / (n,m) -> - steps c2 c3 (n',m') -> - steps c1 c3 (n+n',m+m'). + steps c c (0, 0) +| steps_many : forall c1 c2 c3 n m n' m' n'' m'', + n'' = n + n' -> m'' = m + m' -> + c1 ===> c2 / (n, m) -> + steps c2 c3 (n', m') -> + steps c1 c3 (n'', m''). + +Definition stepEx {S} : config S → config S → Prop := + λ a b, ∃ nm, Cred a b nm. + +Definition stepsEx {S} : config S → config S → Prop := + λ a b, ∃ nm, steps a b nm. + +Lemma stepsExNow {S} : ∀ (a : config S), stepsEx a a. +Proof. + intros a. + exists (0, 0). + constructor. +Qed. + +Lemma stepsExCons {S} (a b c : config S) : + stepEx a b → stepsEx b c → stepsEx a c. +Proof. + intros [[n m] H] [[n' m'] G]. + exists (n + n', m + m'). + econstructor; + [reflexivity | reflexivity | |]. + - apply H. + - apply G. +Qed. + +Lemma step_pack {S : Set} (a b : config S) : + ∀ nm, Cred a b nm → stepEx a b. +Proof. + intros nm H. + by exists nm. +Qed. + +Lemma steps_pack {S : Set} (a b : config S) : + ∀ nm, steps a b nm → stepsEx a b. +Proof. + intros nm H. + by exists nm. +Qed. + +Lemma step_det {S : Set} (c c' c'' : config S) + : stepEx c c' → stepEx c c'' → c' = c''. +Proof. + intros [nm H]. + revert c''. + inversion H; subst; intros c'' [nm' G]; + inversion G; subst; simplify_eq; reflexivity. +Qed. + +Lemma steps_det_val {S : Set} (c c' : config S) (v : val S) + : stepsEx c (Cret v) → stepEx c c' → stepsEx c' (Cret v). +Proof. + intros [n H]. + revert c'. + inversion H; subst; intros c' G. + - destruct G as [? G]. + inversion G. + - erewrite (step_det c c' c2). + + by eapply steps_pack. + + assumption. + + by eapply step_pack. +Qed. Definition meta_fill {S} (mk : Mcont S) e := fold_left (λ e k, fill k e) mk e. -(*** Type system *) -(* Type system from [Filinski, Danvy 89] : A Functional Abstraction of Typed Contexts *) - Coercion Val : val >-> expr. -Inductive ty := -| Tnat : ty -| Tarr : ty -> ty -> ty -> ty -> ty -| TarrCont : ty -> ty -> ty -> ty -> ty. - - -(* Notation "'T' τ '/' α '->' σ '/' β" := (Tarr τ α σ β) (at level 99, only parsing). *) -(* Notation "τ '/' α '→k' σ '/' β" := (TarrCont τ α σ β) (at level 60). *) - -(* Reserved Notation " Γ , α ⊢ e : τ , β" *) -(* (at level 90, e at next level, τ at level 20, no associativity). *) - -(* Inductive typed {S : Set} (Γ : S -> ty) : ty -> expr S -> ty -> ty -> Prop := *) - -(* | typed_Lit α n : *) -(* Γ, α ⊢ (LitV n) : Tnat, α *) - -(* | typed_Rec (δ σ τ α β : ty) (e : expr (inc (inc S))) : *) -(* (Γ ▹ (Tarr σ α τ β) ▹ σ) , α ⊢ e : τ , β -> *) -(* Γ,δ ⊢ (RecV e) : (Tarr σ α τ β) , δ *) - -(* | typed_Cont (δ σ τ α : ty) (k : cont S) : *) -(* typed_cont Γ α k (TarrCont σ α τ α) α -> *) -(* Γ,δ ⊢ (ContV k) : (TarrCont σ α τ α) , δ *) - -(* with typed_cont {S : Set} (Γ : S -> ty) : ty -> cont S -> ty -> ty -> Prop := *) - -(* | typed_END τ α δ : *) -(* typed_cont Γ δ END (TarrCont τ α τ α) δ *) - -(* | typed_IfK τ τ' α ε e1 e2 : *) -(* Γ, α ⊢ e1 : τ, α -> *) -(* Γ, α ⊢ e2 : τ, α -> *) -(* typed_cont Γ α K *) -(* typed_cont Γ α (IfK e1 e2 K) (TarrCont Tnat ε τ' ε) α *) - -(* where "Γ , α ⊢ e : τ , β" := (typed Γ α e τ β). *) - -(* | 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_Shift (e : expr (inc S)) τ : *) -(* typed (Γ ▹ Tcont τ) e τ -> *) -(* typed Γ (Shift e) τ *) -(* | typed_App_Cont (τ τ' : ty) e1 e2 : *) -(* typed Γ e1 (Tcont τ) -> *) -(* typed Γ e2 τ -> *) -(* typed Γ (App e1 e2) τ' *) -(* | type_Reset e τ : *) -(* typed Γ e τ -> *) -(* typed Γ (Reset e) τ *) -(* (* CHECK *) *) -(* with typed_val {S : Set} (Γ : S -> ty) : ty -> val S -> ty -> ty -> Prop := *) -(* | typed_Lit n : *) -(* typed_val Γ (LitV n) Tnat *) -(* | typed_RecV (τ1 τ2 : ty) (e : expr (inc (inc S))) : *) -(* typed (Γ ▹ (Tarr τ1 τ2) ▹ σ) e τ2 → *) -(* typed_val Γ (RecV e) (Tarr τ1 τ2) *) -(* . *) - (*** Notations *) Declare Scope syn_scope. Delimit Scope syn_scope with syn. - Coercion App : expr >-> Funclass. -(* Coercion AppLK : expr >-> Funclass. *) -(* Coercion AppRK : expr >-> Funclass. *) Class AsSynExpr (F : Set -> Type) := { __asSynExpr : ∀ S, F S -> expr S }. @@ -535,254 +512,103 @@ Global Instance AsSynExprExpr : AsSynExpr expr := { 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) := { +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) := { +Global Instance OpNotationLK {S : Set} : + OpNotation (cont S) (nat_op) (val S) (cont S) := { __op K op v := cont_compose K (NatOpLK op v END) }. -Global Instance OpNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : OpNotation (F S) (nat_op) (cont S) (cont S) := { +Global Instance OpNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : + OpNotation (F S) (nat_op) (cont S) (cont S) := { __op e op K := cont_compose K (NatOpRK op (__asSynExpr e) END) }. 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) := { +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} : +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₃ := cont_compose K (IfK (__asSynExpr e₂) (__asSynExpr e₃) END) }. - -(* Class OutputNotation (A B : Type) := { __output : A -> B }. *) - -(* Global Instance OutputNotationExpr {S : Set} {F : Set -> Type} `{AsSynExpr F} : OutputNotation (F S) (expr S) := { *) -(* __output e := Output (__asSynExpr e) *) -(* }. *) - -(* Global Instance OutputNotationK {S : Set} : OutputNotation (cont S) (cont S) := { *) -(* __output K := cont_compose K (OutputK END) *) -(* }. *) - Class ResetNotation (A B : Type) := { __reset : A -> B }. Global Instance ResetNotationExpr {S : Set} {F : Set -> Type} `{AsSynExpr F} : ResetNotation (F S) (expr S) := { __reset e := Reset (__asSynExpr e) }. -(* Global Instance ResetNotationK {S : Set} : ResetNotation (cont S) (cont S) := *) -(* { __reset K := cont_compose K (ResetK END) }. *) - -(* Class ThrowNotation (A B C : Type) := { __throw : A -> B -> C }. *) - -(* Global Instance ThrowNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : ThrowNotation (F S) (G S) (expr S) := { *) -(* __throw e₁ e₂ := Throw (__asSynExpr e₁) (__asSynExpr e₂) *) -(* }. *) - -(* Global Instance ThrowNotationLK {S : Set} {F : Set -> Type} `{AsSynExpr F} : ThrowNotation (cont S) (F S) (cont S) := { *) -(* __throw K e₂ := ThrowLK K (__asSynExpr e₂) *) -(* }. *) - -(* Global Instance ThrowNotationRK {S : Set} : ThrowNotation (val S) (cont S) (cont S) := { *) -(* __throw v K := ThrowRK v K *) -(* }. *) - 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) := { +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 := cont_compose K (AppLK v END) +Global Instance AppNotationRK {S : Set} : + AppNotation (cont S) (val S) (cont S) := { + __app K v := cont_compose K (AppRK v END) }. -Global Instance AppNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppNotation (F S) (cont S) (cont S) := { - __app e K := cont_compose K (AppRK (__asSynExpr e) END) +Global Instance AppNotationLK {S : Set} {F : Set -> Type} `{AsSynExpr F} : + AppNotation (F S) (cont S) (cont S) := { + __app e K := cont_compose K (AppLK (__asSynExpr e) END) }. Class AppContNotation (A B C : Type) := { __app_cont : A -> B -> C }. -Global Instance AppContNotationExpr {S : Set} {F G : Set -> Type} `{AsSynExpr F, AsSynExpr G} : AppContNotation (F S) (G S) (expr S) := { +Global Instance AppContNotationExpr {S : Set} {F G : Set -> Type} + `{AsSynExpr F, AsSynExpr G} : AppContNotation (F S) (G S) (expr S) := { __app_cont e₁ e₂ := AppCont (__asSynExpr e₁) (__asSynExpr e₂) }. -Global Instance AppContNotationLK {S : Set} : AppContNotation (cont S) (val S) (cont S) := { +Global Instance AppContNotationLK {S : Set} : + AppContNotation (cont S) (val S) (cont S) := { __app_cont K v := cont_compose K (AppContLK v END) }. -Global Instance AppContNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : AppContNotation (F S) (cont S) (cont S) := { +Global Instance AppContNotationRK {S : Set} {F : Set -> Type} `{AsSynExpr F} : + AppContNotation (F S) (cont S) (cont S) := { __app_cont e K := cont_compose K (AppContRK (__asSynExpr e) END) }. 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 '@k' y" := (__app_cont x%syn y%syn) (at level 40, y at next level, left associativity) : syn_scope. +Notation "x '⋆' y" := (__app x%syn y%syn) (at level 40, y at next level + , left associativity) : syn_scope. +Notation "x '@k' y" := (__app_cont 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 "'output' x" := (__output x%syn) (at level 60) : syn_scope. *) -(* Notation "'throw' e₁ e₂" := (__throw e₁%syn e₂%syn) (at level 60) : syn_scope. *) Notation "'#' n" := (LitV n) (at level 60) : syn_scope. -(* Notation "'input'" := (Input) : syn_scope. *) Notation "'rec' e" := (RecV e%syn) (at level 60) : syn_scope. Notation "'shift/cc' e" := (Shift e%syn) (at level 60) : syn_scope. Notation "'reset' e" := (Reset e%syn) (at level 60) : syn_scope. -(* Notation "'cont' K" := (ContV K%syn) (at level 60) : syn_scope. *) Notation "'$' fn" := (set_pure_resolver fn) (at level 60) : syn_scope. -(* Notation "□" := (EmptyK) : syn_scope. *) Notation "K '⟪' e '⟫'" := (fill K%syn e%syn) (at level 60) : syn_scope. - -(* Notation "'lam' 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. -(* Notation "A 'Cont'" := (Tcont A%typ) *) -(* (at level 60) : typ_scope. *) - -Declare Scope typing_scope. -Delimit Scope typing_scope with typing. - -Class TypingNotation (A B C : Type) := { __typing : A -> B -> C -> Prop }. - -Notation "Γ ⊢ e : τ" := (__typing Γ e%syn τ%typ) (at level 70, e at level 60) : typing_scope. - -(* Global Instance TypingNotationExpr {S : Set} {F : Set -> Type} `{AsSynExpr F} : TypingNotation (S -> ty) (F S) ty := { *) -(* __typing Γ e τ := typed Γ (__asSynExpr e) τ *) -(* }. *) - -(* Global Instance TypingNotationVal {S : Set} : TypingNotation (S -> ty) (val S) ty := { *) -(* __typing Γ e τ := typed_val Γ e τ *) -(* }. *) - Module SynExamples. - Open Scope syn_scope. - Example test1 : expr (inc ∅) := ($ 0). - Example test2 : val ∅ := (rec (if ($ 1) then # 1 else # 0)). - (* Example test21 : val ∅ := (lam (if ($ 0) then # 1 else #0)). *) - Example test3 : expr ∅ := (shift/cc (rec ($ 0))). - Example test4 : expr ∅ := ((# 1) + (# 0)). - Example test5 : val ∅ := (rec (if ($ 1) then # 1 else (($ 0) ⋆ (($ 1) - (# 1))))). - Example test6 : expr (inc (inc ∅)) := ($ 0) ⋆ ($ 1). - (* Example test7 : expr ∅ := (let_ ((rec (if ($ 1) then # 1 else (($ 0) ⋆ (($ 1) - (# 1))))) ⋆ (# 5)) in (output ($ 0))). *) - - Open Scope typing_scope. - - (* Example test8 : Prop := (empty_env ⊢ (# 0) : ℕ). *) + Example test1 : expr (inc ∅) := $0. + Example test2 : expr (inc (inc ∅)) := ($0) ⋆ $1. + Example test3 : expr ∅ := (rec (reset (shift/cc (($0) @k $1)))). + Example test4 : expr ∅ := + (rec (if ($0) then #1 else (($0) ⋆ (($0) - #1)))). + Example test8 : expr (inc ∅) := ($ 0). + Example test9 : val ∅ := (rec (if ($ 1) then # 1 else # 0)). + Example test10 : expr ∅ := (shift/cc (rec ($ 0))). + Example test11 : expr ∅ := ((# 1) + (# 0)). + Example test12 : val ∅ := (rec (if ($ 1) then # 1 else (($ 0) ⋆ (($ 1) - (# 1))))). + Example test13 : expr (inc (inc ∅)) := ($ 0) ⋆ ($ 1). End SynExamples. - -(* Definition compute_head_step {S} *) -(* (e : expr S) (K : cont S) : *) -(* option (expr S * cont S * (nat * nat)) := *) -(* match e with *) -(* | (App (Val (RecV e1)) (Val v2)) => *) -(* Some ((subst (Inc := inc) ((subst (F := expr) (Inc := inc) e1) *) -(* (Val (shift (Inc := inc) v2))) *) -(* (Val (RecV e1))), K, (1,0)) *) -(* (* | Input => *) *) -(* (* let '(n, σ') := update_input σ in *) *) -(* (* Some ((Val (LitV n)), σ', K, (1, 1)) *) *) -(* (* | Output (Val (LitV n)) => *) *) -(* (* (* let := update_output n σ in *) *) *) -(* (* Some ((Val (LitV 0)), σ', K, (1, 1)) *) *) -(* | (NatOp op (Val v1) (Val v2)) => *) -(* let res := nat_op_interp op v1 v2 in *) -(* option_rect (fun _ => option _) (fun v3 => Some ((Val v3), K, (0, 0))) None res *) -(* | (If (Val (LitV n)) e1 e2) => *) -(* if (decide (0 < n)) *) -(* then Some (e1, K, (0, 0)) *) -(* else *) -(* if (decide (n = 0)) *) -(* then Some (e2, K, (0, 0)) *) -(* else None *) -(* (* | (Shift e) => *) *) -(* (* let (Ki, Ko) := shift_context K in *) *) -(* (* let f := cont_to_rec Ki in *) *) -(* (* Some ((subst (Inc := inc) e (Val f)), Ko, (1, 1)) *) *) -(* | (Reset (Val v)) => Some (Val v, K, (1, 1)) *) -(* (* | (Reset (fill E (Shift e))) => None *) *) -(* | _ => None *) -(* end. *) -(* (* CHECK *) *) - -(* Example test21 : val ∅ := (rec (if ($ 0) then # 1 else #0))%syn. *) - - -(* Example testc : option (expr (inc ∅) * cont (inc ∅) * (nat * nat)) := *) -(* (compute_head_step (App (Val test1) (Val $ LitV 5)) []). *) -(* Eval compute in testc. *) - - -(* Lemma head_step_reflect {S : Set} (e : expr S) (K Ko : cont S) *) -(* : option_reflect (fun '(e', K', nm) => head_step e K e' K' Ko nm) *) -(* True *) -(* (compute_head_step e K). *) -(* Proof. *) -(* destruct e; try (by constructor). *) -(* - destruct e1; try (by constructor). *) -(* destruct v; try (by constructor). *) -(* destruct e2; try (by constructor). *) -(* constructor. *) -(* constructor. *) -(* - destruct e1; try (by constructor). *) -(* destruct e2; try (by constructor). *) -(* destruct (nat_op_interp op v v0) eqn:Heqn. *) -(* + simpl; rewrite Heqn. *) -(* simpl. *) -(* constructor. *) -(* by constructor. *) -(* + simpl; rewrite Heqn. *) -(* simpl. *) -(* constructor. *) -(* constructor. *) -(* - destruct e1; try (by constructor). *) -(* destruct v; try (by constructor). *) -(* simpl. *) -(* case_match; simpl. *) -(* + constructor. *) -(* constructor. *) -(* assumption. *) -(* + case_match; simpl. *) -(* * constructor. *) -(* constructor. *) -(* assumption. *) -(* * constructor. *) -(* constructor. *) -(* (* - simpl. *) *) -(* (* destruct (update_input σ) eqn:Heqn. *) *) -(* (* by do 2 constructor. *) *) -(* (* - simpl. *) *) -(* (* destruct e; try (by constructor). *) *) -(* (* destruct v; try (by constructor). *) *) -(* (* destruct (update_output n σ) eqn:Heqn. *) *) -(* (* by do 2 constructor. *) *) -(* (* - simpl. *) *) -(* (* destruct (shift_context K) as [Ki Ko] eqn:HK. *) *) -(* (* constructor. apply ShiftS with Ki =>//=. *) *) -(* - simpl. *) -(* destruct e; try (by constructor). *) -(* do 2 constructor. *) -(* Qed. *) diff --git a/theories/examples/delim_lang/logpred.v b/theories/examples/delim_lang/logpred.v new file mode 100644 index 0000000..f1ae73e --- /dev/null +++ b/theories/examples/delim_lang/logpred.v @@ -0,0 +1,750 @@ +From gitrees Require Import gitree lang_generic hom. +From gitrees.effects Require Import delim. +From gitrees.examples.delim_lang Require Import lang interp typing hom. +From iris.algebra Require Import list. +From iris.proofmode Require Import classes tactics. +From iris.base_logic Require Import algebra. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Open Scope stdpp_scope. + +Section logrel. + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R}. + Context `{!subReifier reify_delim rs}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!invGS Σ}. + Context `{!stateG rs R Σ}. + Notation iProp := (iProp Σ). + Notation restO + := (gState_rest + (@sR_idx _ _ + (sReifier_NotCtxDep_CtxDep reify_delim)) rs ♯ IT). + + Canonical Structure exprO S := leibnizO (expr S). + Canonical Structure valO S := leibnizO (val S). + Canonical Structure contO S := leibnizO (cont S). + Canonical Structure mcontO S := leibnizO (Mcont S). + + Notation "'WP' α {{ β , Φ } }" + := (wp rs α notStuck ⊤ (λ β, Φ)) + (at level 20, α, Φ at level 200, + format "'WP' α {{ β , Φ } }") + : bi_scope. + + Notation "'WP' α {{ Φ } }" + := (wp rs α notStuck ⊤ Φ) + (at level 20, α, Φ at level 200, + format "'WP' α {{ Φ } }") : bi_scope. + + Definition logrel_nat' (βv : ITV) : iProp := + (∃ (n : natO), βv ≡ RetV n)%I. + Local Instance logrel_nat_ne : NonExpansive logrel_nat'. + Proof. solve_proper. Qed. + Definition logrel_nat : ITV -n> iProp := λne x, logrel_nat' x. + + Definition obs_ref' + (t : IT) (κ : HOM) (σ : stateF ♯ IT) + : iProp := + (has_substate σ -∗ WP (𝒫 (`κ t)) {{ βv, has_substate [] }})%I. + Local Instance obs_ref_ne : NonExpansive3 obs_ref'. + Proof. solve_proper. Qed. + Program Definition obs_ref : IT -n> HOM -n> (stateF ♯ IT) -n> iProp := + λne x y z, obs_ref' x y z. + Solve All Obligations with solve_proper. + + Definition logrel_mcont' (P : ITV -n> iProp) (F : stateF ♯ IT) := + (∀ αv, P αv -∗ obs_ref (IT_of_V αv) HOM_id F)%I. + Local Instance logrel_mcont_ne : NonExpansive2 logrel_mcont'. + Proof. solve_proper. Qed. + Program Definition logrel_mcont : (ITV -n> iProp) -n> (stateF ♯ IT) -n> iProp + := λne x y, logrel_mcont' x y. + Solve All Obligations with solve_proper. + + Program Definition logrel_ectx' + (Pτ Pα : ITV -n> iProp) (κ : HOM) + : iProp := + (□ ∀ αv, Pτ αv -∗ ∀ σ, logrel_mcont Pα σ -∗ obs_ref (IT_of_V αv) κ σ)%I. + Local Instance logrel_ectx_ne : NonExpansive3 logrel_ectx'. + Proof. solve_proper. Qed. + Program Definition logrel_ectx + : (ITV -n> iProp) -n> (ITV -n> iProp) -n> HOM -n> iProp + := λne x y z, logrel_ectx' x y z. + Solve All Obligations with solve_proper. + + Program Definition logrel_cont' V W (βv : ITV) : iProp := + (∃ (κ : HOM), (IT_of_V βv) ≡ + (Fun (Next (λne x, Tau (laterO_map (𝒫 ◎ `κ) (Next x))))) + ∧ □ logrel_ectx V W κ)%I. + Local Instance logrel_cont_ne : NonExpansive3 logrel_cont'. + Proof. solve_proper. Qed. + Program Definition logrel_cont + : (ITV -n> iProp) -n> (ITV -n> iProp) -n> ITV -n> iProp + := λne x y z, logrel_cont' x y z. + Solve All Obligations with solve_proper. + + Program Definition logrel_arr' (Pτ Pα Pσ Pβ : ITV -n> iProp) (f : ITV) : iProp + := (∃ f', IT_of_V f ≡ Fun f' + ∧ □ ∀ (βv : ITV), + Pτ βv -∗ ∀ (κ : HOM), + logrel_ectx Pσ Pα κ -∗ ∀ σ, + logrel_mcont Pβ σ -∗ obs_ref (APP' (Fun f') (IT_of_V βv)) κ σ)%I. + Local Instance logrel_arr_ne + : (∀ n, Proper (dist n + ==> dist n + ==> dist n + ==> dist n + ==> dist n + ==> dist n) + logrel_arr'). + Proof. solve_proper. Qed. + Program Definition logrel_arr + : (ITV -n> iProp) + -n> (ITV -n> iProp) + -n> (ITV -n> iProp) + -n> (ITV -n> iProp) -n> ITV -n> iProp := + λne x y z w v, logrel_arr' x y z w v. + Solve All Obligations with solve_proper. + + Fixpoint interp_ty (τ : ty) : ITV -n> iProp := + match τ with + | Tnat => logrel_nat + | Tcont α β => logrel_cont (interp_ty α) (interp_ty β) + | Tarr τ α σ β => logrel_arr (interp_ty τ) (interp_ty α) + (interp_ty σ) (interp_ty β) + end. + + Local Instance interp_ty_persistent (τ : ty) α : + Persistent (interp_ty τ α). + Proof. + revert α. induction τ=> α; simpl. + - unfold logrel_nat. apply _. + - unfold logrel_arr. apply _. + - unfold logrel_cont. apply _. + Qed. + + Program Definition logrel_expr (τ α δ : ITV -n> iProp) : IT -n> iProp + := λne e, (∀ E, logrel_ectx τ α E + -∗ ∀ F, logrel_mcont δ F + -∗ obs_ref e E F)%I. + Solve All Obligations with solve_proper. + + Definition logrel (τ α β : ty) : IT -n> iProp + := logrel_expr (interp_ty τ) (interp_ty α) (interp_ty β). + + Program Definition ssubst_valid {S : Set} + (Γ : S -> ty) + (ss : interp_scope S) : iProp := + (∀ x τ, □ logrel (Γ x) τ τ (ss x))%I. + + Program Definition valid {S : Set} + (Γ : S -> ty) + (e : interp_scope S -n> IT) + (τ α σ : ty) : iProp := + (□ ∀ γ, ssubst_valid Γ γ + -∗ logrel τ α σ (e γ))%I. + + Lemma compat_HOM_id P : + ⊢ logrel_ectx P P HOM_id. + Proof. + iIntros (v). + iModIntro. + iIntros "Pv". + iIntros (σ) "Hσ HH". + iApply ("Hσ" with "Pv HH"). + Qed. + + Lemma logrel_of_val τ α v : + interp_ty α v -∗ logrel α τ τ (IT_of_V v). + Proof. + iIntros "#H". + iIntros (κ) "Hκ". + iIntros (σ) "Hσ Hown". + iApply ("Hκ" with "H Hσ Hown"). + Qed. + + Lemma compat_var {S : Set} (Γ : S -> ty) (x : S) : + ⊢ (∀ α, valid Γ (interp_var x) (Γ x) α α). + Proof. + iIntros (α). + iModIntro. + iIntros (γ) "#Hss". + iIntros (E) "HE". + iIntros (F) "HF". + iIntros "Hσ". + iApply ("Hss" with "HE HF Hσ"). + Qed. + + Lemma compat_reset {S : Set} (Γ : S -> ty) e σ τ : + ⊢ valid Γ e σ σ τ -∗ (∀ α, valid Γ (interp_reset rs e) τ α α). + Proof. + iIntros "#H". + iIntros (α). + iModIntro. + iIntros (γ) "Hγ". + iIntros (κ) "Hκ". + iIntros (m) "Hm Hst". + assert (𝒫 ((`κ) (interp_reset rs e γ)) + ≡ (𝒫 ◎ `κ) (interp_reset rs e γ)) as ->. + { reflexivity. } + iApply (wp_reset with "Hst"). + iNext. + iIntros "_ Hst". + iSpecialize ("H" $! γ with "Hγ"). + iSpecialize ("H" $! HOM_id (compat_HOM_id _) (laterO_map (𝒫 ◎ `κ) :: m)). + iAssert (logrel_mcont (interp_ty τ) (laterO_map (𝒫 ◎ `κ) :: m)) + with "[Hm Hκ]" as "Hm". + { + iIntros (v) "Hv Hst". + iApply (wp_pop_cons with "Hst"). + iNext. + iIntros "_ Hst". + iSpecialize ("Hκ" $! v with "Hv"). + iSpecialize ("Hκ" $! m with "Hm"). + iSpecialize ("Hκ" with "Hst"). + iApply "Hκ". + } + iSpecialize ("H" with "Hm Hst"). + iApply "H". + Qed. + + Lemma compat_shift {S : Set} (Γ : S -> ty) e σ α τ β : + ⊢ valid (Γ ▹ (Tcont τ α)) e σ σ β -∗ valid Γ (interp_shift _ e) τ α β. + Proof. + iIntros "#H". + iModIntro. + iIntros (γ) "#Hγ". + iIntros (κ) "#Hκ". + iIntros (m) "Hm Hst". + assert (𝒫 ((`κ) (interp_shift rs e γ)) + ≡ (𝒫 ◎ `κ) (interp_shift rs e γ)) as ->. + { reflexivity. } + iApply (wp_shift with "Hst"). + { rewrite laterO_map_Next; reflexivity. } + iNext. + iIntros "_ Hst". + match goal with + | |- context G [ofe_mor_car _ _ e ?a] => + set (γ' := a) + end. + iAssert (ssubst_valid (Γ ▹ Tcont τ α) γ') with "[Hγ Hκ]" as "Hγ'". + { + iIntros (x τ'). + destruct x as [| x]. + - iModIntro. + subst γ'. + iIntros (E) "HE". + iIntros (F) "HF Hst". + simpl. + match goal with + | |- context G [ofe_mor_car _ _ (`E) (ofe_mor_car _ _ Fun ?a)] => + set (f := a) + end. + iApply ("HE" $! (FunV f) with "[Hκ] HF Hst"). + iExists κ. + iSplit. + + subst f; iPureIntro. + reflexivity. + + iApply "Hκ". + - iApply "Hγ". + } + iSpecialize ("H" $! γ' with "Hγ'"). + iSpecialize ("H" $! HOM_id (compat_HOM_id _) m with "Hm Hst"). + iApply "H". + Qed. + + Lemma compat_nat {S : Set} (Γ : S → ty) n α : + ⊢ valid Γ (interp_nat rs n) Tnat α α. + Proof. + iModIntro. + iIntros (γ) "#Hγ". + assert ((interp_nat rs n γ) ≡ IT_of_V (RetV n)) as ->. + { reflexivity. } + iApply logrel_of_val. + iExists _; by iPureIntro. + Qed. + + Lemma compat_recV {S : Set} (Γ : S -> ty) + τ1 α τ2 β e : + ⊢ valid ((Γ ▹ (Tarr τ1 α τ2 β) ▹ τ1)) e τ2 α β + -∗ (∀ θ, valid Γ (interp_rec rs e) (Tarr τ1 α τ2 β) θ θ). + Proof. + iIntros "#H". + iIntros (θ). + iModIntro. + iIntros (γ) "#Hγ". + set (f := (ir_unf rs e γ)). + iAssert (interp_rec rs e γ ≡ IT_of_V $ FunV (Next f))%I as "Hf". + { iPureIntro. apply interp_rec_unfold. } + iRewrite "Hf". + Opaque IT_of_V. + iApply logrel_of_val; term_simpl. + iExists _. iSplit. + { iPureIntro. apply into_val. } + iModIntro. + iLöb as "IH". + iIntros (v) "#Hw". + iIntros (κ) "#Hκ". + iIntros (σ) "Hσ Hst". + rewrite APP_APP'_ITV APP_Fun laterO_map_Next -Tick_eq. + pose (γ' := + (extend_scope (extend_scope γ (interp_rec rs e γ)) (IT_of_V v))). + rewrite /logrel. + Opaque extend_scope. + simpl. + rewrite hom_tick. + rewrite hom_tick. + iApply wp_tick. + iNext. + iSpecialize ("H" $! γ' with "[Hw]"). + { + iIntros (x). + destruct x as [| [| x]]; iIntros (ξ); iModIntro. + * iApply logrel_of_val. + iApply "Hw". + * iIntros (κ') "Hκ'". + iIntros (σ') "Hσ' Hst". + Transparent extend_scope. + simpl. + iRewrite "Hf". + iSpecialize ("Hκ'" $! (FunV (Next f)) with "[IH]"). + { + iExists (Next f). + iSplit; first done. + iModIntro. + iIntros (βv) "Hβv". + iIntros (κ'') "Hκ''". + iIntros (σ'') "Hσ'' Hst". + iApply ("IH" $! βv with "Hβv Hκ'' Hσ'' Hst"). + } + iApply ("Hκ'" $! σ' with "Hσ' Hst"). + * iApply "Hγ". + } + subst γ'. + iApply ("H" with "Hκ Hσ Hst"). + Qed. + + Lemma compat_nat_op {S : Set} (Γ : S → ty) + D E F e1 e2 op : + ⊢ valid Γ e1 Tnat E F + -∗ valid Γ e2 Tnat F D + -∗ valid Γ (interp_natop rs op e1 e2) Tnat E D. + Proof. + iIntros "#H #G". + iModIntro. + iIntros (γ) "#Hγ". + iIntros (κ) "#Hκ". + iIntros (m) "Hm Hst". + rewrite /interp_natop //=. + + set (κ' := (NatOpRSCtx_HOM op e1 γ)). + assert ((NATOP (do_natop op) (e1 γ) (e2 γ)) = ((`κ') (e2 γ))) as -> by done. + rewrite HOM_ccompose. + pose (sss := (HOM_compose κ κ')). rewrite (HOM_compose_ccompose κ κ' sss)//. + + iSpecialize ("G" $! γ with "Hγ"). + iSpecialize ("G" $! sss). + iApply ("G" with "[H] Hm Hst"). + + iIntros (w). + iModIntro. + iIntros "#Hw". + iIntros (m') "Hm Hst". + subst sss. + subst κ'. + simpl. + + pose (κ' := (NatOpLSCtx_HOM op (IT_of_V w) γ _)). + assert ((NATOP (do_natop op) (e1 γ) (IT_of_V w)) = ((`κ') (e1 γ))) + as -> by done. + rewrite HOM_ccompose. + pose (sss := (HOM_compose κ κ')). rewrite (HOM_compose_ccompose κ κ' sss)//. + + iSpecialize ("H" $! γ with "Hγ"). + iSpecialize ("H" $! sss). + iApply ("H" with "[] Hm Hst"). + + iIntros (v). + iModIntro. + iIntros "#Hv". + iIntros (m'') "Hm Hst". + subst sss. + subst κ'. + simpl. + + iDestruct "Hw" as "(%n & #HEQ1)". + iDestruct "Hv" as "(%n' & #HEQ2)". + iSpecialize ("Hκ" $! (RetV (do_natop op n' n)) with "[]"). + { + iExists _. + iPureIntro. + reflexivity. + } + iSpecialize ("Hκ" $! m'' with "Hm Hst"). + rewrite IT_of_V_Ret. + + iAssert ((NATOP (do_natop op) (IT_of_V v) (IT_of_V w)) + ≡ (Ret (do_natop op n' n)))%I as "#HEQ". + { + iRewrite "HEQ1". + rewrite IT_of_V_Ret. + iAssert ((IT_of_V v) ≡ IT_of_V (RetV n'))%I as "#HEQ2'". + { + iApply f_equivI. + iApply "HEQ2". + } + rewrite IT_of_V_Ret. + iAssert (NATOP (do_natop op) (IT_of_V v) (Ret n) + ≡ NATOP (do_natop op) (Ret n') (Ret n))%I as "#HEQ2''". + { + unshelve iApply (f_equivI (λne x, NATOP (do_natop op) x (Ret n))). + { solve_proper. } + { solve_proper. } + iApply "HEQ2'". + } + iRewrite "HEQ2''". + rewrite NATOP_Ret. + done. + } + iRewrite "HEQ". + iApply "Hκ". + Qed. + + Lemma compat_app {S : Set} (Γ : S → ty) + ξ α β δ η τ e1 e2 : + ⊢ valid Γ e1 (Tarr η α τ β) ξ δ + -∗ valid Γ e2 η β ξ + -∗ valid Γ (interp_app rs e1 e2) τ α δ. + Proof. + iIntros "#H #G". + iModIntro. + iIntros (γ) "#Hγ". + iIntros (κ) "#Hκ". + iIntros (σ) "Hσ Hst". + rewrite /interp_app //=. + + pose (κ' := (AppLSCtx_HOM e2 γ)). + match goal with + | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] => + set (F := b) + end. + assert (LET (e1 γ) F = ((`κ') (e1 γ))) as ->. + { simpl; unfold AppLSCtx. reflexivity. } + clear F. + assert ((`κ) ((`κ') (e1 γ)) = ((`κ) ◎ (`κ')) (e1 γ)) as ->. + { reflexivity. } + pose (sss := (HOM_compose κ κ')). + assert ((`κ ◎ `κ') = (`sss)) as ->. + { reflexivity. } + + iSpecialize ("H" $! γ with "Hγ"). + iSpecialize ("H" $! sss). + iApply ("H" with "[H] Hσ Hst"). + + iIntros (w). + iModIntro. + iIntros "#Hw". + iIntros (m') "Hm Hst". + subst sss. + subst κ'. + simpl. + rewrite LET_Val. + cbn [ofe_mor_car]. + + match goal with + | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] => + set (F := b) + end. + pose (κ'' := exist _ (LETCTX F) (LETCTX_Hom F) : HOM). + assert (((`κ) (LET (e2 γ) F)) = (((`κ) ◎ (`κ'')) (e2 γ))) as ->. + { reflexivity. } + pose (sss := (HOM_compose κ κ'')). + assert ((`κ ◎ `κ'') = (`sss)) as ->. + { reflexivity. } + iSpecialize ("G" $! γ with "Hγ"). + iSpecialize ("G" $! sss). + iApply ("G" with "[H] Hm Hst"). + iIntros (v). + iModIntro. + iIntros "#Hv". + iIntros (m'') "Hm Hst". + subst sss. + subst κ''. + simpl. + rewrite LET_Val. + subst F. + cbn [ofe_mor_car]. + + iDestruct "Hw" as "(%n' & #HEQ & Hw)". + iSpecialize ("Hw" $! v with "Hv"). + iSpecialize ("Hw" $! κ with "Hκ"). + iSpecialize ("Hw" $! m'' with "Hm Hst"). + iAssert ((IT_of_V w ⊙ (IT_of_V v)) + ≡ (Fun n' ⊙ (IT_of_V v)))%I as "#HEQ'". + { + iApply (f_equivI (λne x, (x ⊙ (IT_of_V v)))). + iApply "HEQ". + } + iRewrite "HEQ'". + iApply "Hw". + Qed. + + Lemma compat_appcont {S : Set} (Γ : S -> ty) e1 e2 τ α δ β σ : + valid Γ e1 (Tcont τ α) σ δ + -∗ valid Γ e2 τ δ β + -∗ valid Γ (interp_app_cont _ e1 e2) α σ β. + Proof. + iIntros "#H #G". + iModIntro. + iIntros (γ) "#Henv". + iIntros (κ) "#Hκ". + iIntros (σ') "Hm Hst". + + pose (κ' := (AppContRSCtx_HOM e1 γ)). + assert ((interp_app_cont rs e1 e2 γ) = ((`κ') (e2 γ))) as ->. + { simpl. reflexivity. } + assert ((`κ) ((`κ') (e2 γ)) = ((`κ) ◎ (`κ')) (e2 γ)) as ->. + { reflexivity. } + pose (sss := (HOM_compose κ κ')). + assert ((`κ ◎ `κ') = (`sss)) as ->. + { reflexivity. } + + iSpecialize ("G" $! γ with "Henv"). + iSpecialize ("G" $! sss). + iApply ("G" with "[H] Hm Hst"). + + iIntros (w). + iModIntro. + iIntros "#Hw". + iIntros (m') "Hm Hst". + subst sss. + subst κ'. + Opaque interp_app_cont. + simpl. + + pose (κ'' := (AppContLSCtx_HOM (IT_of_V w) γ _)). + set (F := (`κ) _). + assert (F ≡ (((`κ) ◎ (`κ'')) (e1 γ))) as ->. + { + subst F. simpl. Transparent interp_app_cont. simpl. + f_equiv. + rewrite ->2 get_val_ITV. + simpl. + reflexivity. + } + pose (sss := (HOM_compose κ κ'')). + assert ((`κ ◎ `κ'') = (`sss)) as ->. + { reflexivity. } + + iSpecialize ("H" $! γ with "Henv"). + iSpecialize ("H" $! sss). + iApply ("H" with "[] Hm Hst"). + + iIntros (v). + iModIntro. + iIntros "#Hv". + iIntros (m'') "Hm Hst". + subst sss. + subst κ''. + Opaque APP_CONT. + simpl. + + rewrite get_val_ITV. + simpl. + + iDestruct "Hv" as "(%n' & #HEQ & #Hv)". + iRewrite "HEQ". + rewrite get_fun_fun. + simpl. + + match goal with + | |- context G [ofe_mor_car _ _ + (ofe_mor_car _ _ APP_CONT ?a) ?b] => + set (T := APP_CONT a b) + end. + iAssert (𝒫 ((`κ) T) ≡ (𝒫 ◎ (`κ)) T)%I as "HEQ'". + { iPureIntro. reflexivity. } + iRewrite "HEQ'"; iClear "HEQ'". + subst T. + + iApply (wp_app_cont with "[Hst]"). + { reflexivity. } + - iFrame "Hst". + - simpl. + iNext. + iIntros "_ Hst". + rewrite later_map_Next. + rewrite <-Tick_eq. + iApply wp_tick. + iNext. + iSpecialize ("Hv" $! w with "Hw"). + + iApply ("Hv" $! (laterO_map (𝒫 ◎ `κ) :: m'') with "[Hm] Hst"). + { + iIntros (p) "#Hp Hst". + iApply (wp_pop_cons with "Hst"). + iNext. + iIntros "_ Hst". + iApply ("Hκ" with "Hp Hm Hst"). + } + Qed. + + Lemma compat_if {S : Set} (Γ : S -> ty) e e₁ e₂ τ σ α β : + ⊢ valid Γ e Tnat β α + -∗ valid Γ e₁ τ σ β + -∗ valid Γ e₂ τ σ β + -∗ valid Γ (interp_if rs e e₁ e₂) τ σ α. + Proof. + iIntros "#H #G #J". + iModIntro. + iIntros (γ) "#Henv". + iIntros (κ) "#Hκ". + iIntros (σ') "Hm Hst". + unfold interp_if. + cbn [ofe_mor_car]. + pose (κ' := (IFSCtx_HOM (e₁ γ) (e₂ γ))). + assert ((IF (e γ) (e₁ γ) (e₂ γ)) = ((`κ') (e γ))) as -> by reflexivity. + assert ((`κ) ((`κ') (e γ)) = ((`κ) ◎ (`κ')) (e γ)) + as -> by reflexivity. + pose (sss := (HOM_compose κ κ')). + rewrite (HOM_compose_ccompose κ κ' sss)//. + + iSpecialize ("H" $! γ with "Henv"). + iSpecialize ("H" $! sss). + iApply ("H" with "[] Hm Hst"). + + iIntros (v). + iModIntro. + iIntros "#Hv". + iIntros (σ'') "Hm Hst". + iDestruct "Hv" as "(%n & #Hv)". + iRewrite "Hv". + rewrite IT_of_V_Ret. + subst sss. + subst κ'. + simpl. + unfold IFSCtx. + destruct (decide (0 < n)) as [H|H]. + - rewrite IF_True//. + iApply ("G" $! γ with "Henv [Hκ] Hm Hst"). + iIntros (w). + iModIntro. + iIntros "#Hw". + iIntros (σ''') "Hm Hst". + iApply ("Hκ" with "Hw Hm Hst"). + - rewrite IF_False//; last lia. + iApply ("J" $! γ with "Henv [Hκ] Hm Hst"). + iIntros (w). + iModIntro. + iIntros "#Hw". + iIntros (σ''') "Hm Hst". + iApply ("Hκ" with "Hw Hm Hst"). + Qed. + + Open Scope types. + + Lemma fundamental_expr {S : Set} (Γ : S -> ty) τ α β e : + Γ; α ⊢ₑ e : τ; β → ⊢ valid Γ (interp_expr rs e) τ α β + with fundamental_val {S : Set} (Γ : S -> ty) τ α β v : + Γ; α ⊢ᵥ v : τ; β → ⊢ valid Γ (interp_val rs v) τ α β. + Proof. + - intros H. + destruct H. + + by apply fundamental_val. + + subst; iApply compat_var. + + iApply compat_app; + by iApply fundamental_expr. + + iApply compat_appcont; + by iApply fundamental_expr. + + iApply compat_nat_op; + by iApply fundamental_expr. + + iApply compat_if; + by iApply fundamental_expr. + + iApply compat_shift; + by iApply fundamental_expr. + + iApply (compat_reset with "[]"); + by iApply fundamental_expr. + - intros H. + destruct H. + + iApply compat_nat. + + iApply (compat_recV with "[]"); + by iApply fundamental_expr. + Qed. + +End logrel. + +Local Definition rs : gReifiers CtxDep 1 := gReifiers_cons reify_delim gReifiers_nil. + +Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. + +Lemma logpred_adequacy cr Σ R `{!Cofe R, SubOfe natO R} + `{!invGpreS Σ} `{!statePreG rs R Σ} τ + (α : interp_scope ∅ -n> IT (gReifiers_ops rs) R) + (e : IT (gReifiers_ops rs) R) st' k : + (∀ `{H1 : !invGS Σ} `{H2: !stateG rs R Σ}, + (£ cr ⊢ valid rs □ α τ τ τ)%I) → + ssteps (gReifiers_sReifier rs) (𝒫 (α ı_scope)) ([], ()) e st' k → + (∃ β1 st1, sstep (gReifiers_sReifier rs) e st' β1 st1) + ∨ (∃ βv, IT_of_V βv ≡ e). +Proof. + intros Hlog Hst. + destruct (IT_to_V e) as [βv|] eqn:Hb. + { right. exists βv. apply IT_of_to_V'. rewrite Hb; eauto. } + left. + cut ((∃ β1 st1, sstep (gReifiers_sReifier rs) e st' β1 st1) + ∨ (∃ e', e ≡ Err e' ∧ notStuck e')). + { intros [?|He]; first done. + destruct He as [? [? []]]. } + eapply (wp_safety cr); eauto. + { apply Hdisj. } + { by rewrite Hb. } + intros H1 H2. + exists (λ _, True)%I. split. + { apply _. } + iIntros "[Hcr Hst]". + iPoseProof (Hlog with "Hcr") as "Hlog". + match goal with + | |- context G [has_full_state (?a, _)] => + set (st := a) + end. + simpl in st. + iAssert (has_substate _) with "[Hst]" as "Hs". + { unfold has_substate, has_full_state. + eassert (of_state rs (IT (gReifiers_ops rs) _) (_,()) ≡ + of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state _)) as ->; last done. + intro j. unfold sR_idx. simpl. + unfold of_state, of_idx. + destruct decide as [Heq|]; last first. + { inv_fin j; first done. + intros i. inversion i. } + inv_fin j; last done. + intros Heq. + rewrite (eq_pi _ _ Heq eq_refl)//. + simpl. + unfold iso_ofe_refl. + cbn. + reflexivity. + } + iSpecialize ("Hlog" $! ı_scope with "[]"). + { iIntros ([]). } + iSpecialize ("Hlog" $! HOM_id (compat_HOM_id _ _) [] with "[]"). + { + iIntros (αv) "HHH GGG". + iApply (wp_pop_end with "GGG"). + iNext. + iIntros "_ GGG". + iApply wp_val. + by iModIntro. + } + subst st. + iSpecialize ("Hlog" with "Hs"). + iApply (wp_wand with "Hlog"). + iIntros (βv). simpl. + iIntros "_". + done. +Qed. diff --git a/theories/examples/delim_lang/logrel.v b/theories/examples/delim_lang/logrel.v new file mode 100644 index 0000000..5d29269 --- /dev/null +++ b/theories/examples/delim_lang/logrel.v @@ -0,0 +1,1241 @@ +From gitrees Require Import gitree lang_generic hom. +From gitrees.effects Require Import delim. +From gitrees.examples.delim_lang Require Import lang interp typing hom. +From iris.algebra Require Import list. +From iris.proofmode Require Import classes tactics. +From iris.base_logic Require Import algebra. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Open Scope syn. +Open Scope stdpp_scope. + +Section logrel. + Context {sz : nat}. + Variable (rs : gReifiers CtxDep sz). + Context {R} `{!Cofe R}. + Context `{!SubOfe natO R}. + Context `{!subReifier reify_delim rs}. + Notation F := (gReifiers_ops rs). + Notation IT := (IT F R). + Notation ITV := (ITV F R). + Context `{!invGS Σ}. + Context `{!stateG rs R Σ}. + Notation iProp := (iProp Σ). + Notation restO + := (gState_rest + (@sR_idx _ _ + (sReifier_NotCtxDep_CtxDep reify_delim)) rs ♯ IT). + + Canonical Structure exprO S := leibnizO (expr S). + Canonical Structure valO S := leibnizO (val S). + Canonical Structure contO S := leibnizO (cont S). + Canonical Structure mcontO S := leibnizO (Mcont S). + + Notation "'WP' α {{ β , Φ } }" + := (wp rs α notStuck ⊤ (λ β, Φ)) + (at level 20, α, Φ at level 200, + format "'WP' α {{ β , Φ } }") + : bi_scope. + + Notation "'WP' α {{ Φ } }" + := (wp rs α notStuck ⊤ Φ) + (at level 20, α, Φ at level 200, + format "'WP' α {{ Φ } }") : bi_scope. + + Definition logrel_nat' {S : Set} (βv : ITV) (v : valO S) : iProp := + (∃ (n : natO), βv ≡ RetV n ∧ v ≡ LitV n)%I. + Local Instance logrel_nat_ne {S : Set} : NonExpansive2 (@logrel_nat' S). + Proof. solve_proper. Qed. + Program Definition logrel_nat {S : Set} : ITV -n> valO S -n> iProp := + λne x y, @logrel_nat' S x y. + Solve All Obligations with solve_proper. + Fail Next Obligation. + + (** The configuration of the abstract machine (e, k, m) corresponds + to the "denotational configuration" tuple (t, κ, σ). + + The meta-continuation is stored in the state and the top-level + current continuation is explicitly invoked. + + At the top-level the refinement is explicitly about fully-evaluated + terms which compute to natural numbers. *) + + Definition obs_ref' {S : Set} + (t : IT) (κ : HOM) (σ : stateF ♯ IT) + (e : exprO S) (k : contO S) (m : mcontO S) + : iProp := + (has_substate σ + -∗ WP (𝒫 (`κ t)) {{ βv, has_substate [] + ∗ ∃ (v : valO S), + ⌜∃ (nm : nat * nat), steps (Ceval e k m) (Cret v) nm⌝ + ∗ logrel_nat βv v }})%I. + Local Instance obs_ref_ne {S : Set} : + ∀ n, Proper (dist n ==> dist n ==> dist n ==> + dist n ==> dist n ==> dist n ==> dist n) + (@obs_ref' S). + Proof. solve_proper. Qed. + Local Instance obs_ref_proper {S : Set} : + Proper ((≡) ==> (≡) ==> (≡) ==> + (≡) ==> (≡) ==> (≡) ==> (≡)) + (@obs_ref' S). + Proof. solve_proper. Qed. + + Program Definition obs_ref {S : Set} + : IT -n> HOM -n> (stateF ♯ IT) + -n> exprO S -n> contO S -n> mcontO S -n> iProp := + λne x y z a b c, obs_ref' x y z a b c. + Solve All Obligations with try solve_proper. + Next Obligation. solve_proper_please. Qed. + + + Definition logrel_mcont' {S : Set} + (P : ITV -n> valO S -n> iProp) (F : stateF ♯ IT) (m : mcontO S) := + (∀ αv v, P αv v -∗ obs_ref (IT_of_V αv) HOM_id F (Val v) END m)%I. + Local Instance logrel_mcont_ne {S : Set} : + NonExpansive3 (@logrel_mcont' S). + Proof. solve_proper. Qed. + Local Instance logrel_mcont_proper {S : Set} : + Proper ((≡) ==> (≡) ==> (≡) ==> (≡)) + (@logrel_mcont' S). + Proof. solve_proper. Qed. + Program Definition logrel_mcont {S : Set} : + (ITV -n> valO S -n> iProp) + -n> (stateF ♯ IT) -n> mcontO S -n> iProp + := λne x y z, logrel_mcont' x y z. + Solve All Obligations with solve_proper. + + Program Definition logrel_ectx' {S : Set} + (Pτ Pα : ITV -n> valO S -n> iProp) (κ : HOM) (k : cont S) + : iProp := + (□ ∀ αv v, Pτ αv v -∗ ∀ σ (m : mcontO S), + logrel_mcont Pα σ m -∗ obs_ref (IT_of_V αv) κ σ (Val v) k m)%I. + Local Instance logrel_ectx_ne {S : Set} : + NonExpansive4 (@logrel_ectx' S). + Proof. solve_proper. Qed. + Local Instance logrel_ectx_proper {S : Set} : + Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) + (@logrel_ectx' S). + Proof. solve_proper. Qed. + Program Definition logrel_ectx {S : Set} + : (ITV -n> valO S -n> iProp) -n> (ITV -n> valO S -n> iProp) + -n> HOM -n> cont S -n> iProp + := λne x y z w, logrel_ectx' x y z w. + Solve All Obligations with solve_proper. + + Program Definition logrel_cont' {S : Set} + (V W : ITV -n> valO S -n> iProp) (βv : ITV) (v : valO S) : iProp := + (∃ (κ : HOM) K, (IT_of_V βv) ≡ + (Fun (Next (λne x, Tau (laterO_map (𝒫 ◎ `κ) (Next x))))) + ∧ ⌜v = ContV K⌝ + ∧ □ logrel_ectx V W κ K)%I. + Local Instance logrel_cont_ne {S : Set} : NonExpansive4 (@logrel_cont' S). + Proof. solve_proper. Qed. + Local Instance logrel_cont_proper {S : Set} : + Proper ((≡) ==> (≡) ==> (≡) ==> (≡) ==> (≡)) + (@logrel_cont' S). + Proof. solve_proper. Qed. + Program Definition logrel_cont {S : Set} + : (ITV -n> valO S -n> iProp) -n> (ITV -n> valO S -n> iProp) + -n> ITV -n> valO S -n> iProp + := λne x y z w, logrel_cont' x y z w. + Solve All Obligations with solve_proper. + + Program Definition logrel_arr' {S : Set} + (Pτ Pα Pσ Pβ : ITV -n> valO S -n> iProp) (f : ITV) (vf : valO S) + : iProp + := (∃ f', IT_of_V f ≡ Fun f' + ∧ ⌜(∃ f'', vf = RecV f'')⌝ + ∧ □ ∀ (βv : ITV) (v : valO S), + Pτ βv v -∗ ∀ (κ : HOM) (K : cont S), + logrel_ectx Pσ Pα κ K -∗ ∀ σ m, + logrel_mcont Pβ σ m + -∗ obs_ref (APP' (Fun f') (IT_of_V βv)) κ σ + (App (Val vf) (Val v)) K m)%I. + Local Instance logrel_arr_ne {S : Set} + : (∀ n, Proper (dist n + ==> dist n + ==> dist n + ==> dist n + ==> dist n + ==> dist n + ==> dist n) + (@logrel_arr' S)). + Proof. solve_proper. Qed. + Local Instance logrel_arr_proper {S : Set} : + Proper ((≡) ==> (≡) ==> (≡) ==> + (≡) ==> (≡) ==> (≡) ==> (≡)) + (@logrel_arr' S). + Proof. solve_proper. Qed. + Program Definition logrel_arr {S : Set} + : (ITV -n> valO S -n> iProp) + -n> (ITV -n> valO S -n> iProp) + -n> (ITV -n> valO S -n> iProp) + -n> (ITV -n> valO S -n> iProp) -n> ITV -n> valO S -n> iProp := + λne x y z w v t, logrel_arr' x y z w v t. + Solve All Obligations with try solve_proper. + Next Obligation. + intros; intros ????????; simpl. + solve_proper. + Qed. + + Fixpoint interp_ty {S : Set} (τ : ty) : ITV -n> valO S -n> iProp := + match τ with + | Tnat => logrel_nat + | Tcont α β => logrel_cont (interp_ty α) (interp_ty β) + | Tarr τ α σ β => logrel_arr (interp_ty τ) (interp_ty α) + (interp_ty σ) (interp_ty β) + end. + + Local Instance interp_ty_persistent {S : Set} (τ : ty) α v : + Persistent (@interp_ty S τ α v). + Proof. + revert α. induction τ=> α; simpl. + - unfold logrel_nat. apply _. + - unfold logrel_arr. apply _. + - unfold logrel_cont. apply _. + Qed. + + Program Definition logrel_expr {S : Set} + (τ α δ : ITV -n> valO S -n> iProp) : IT -n> exprO S -n> iProp + := λne e e', (∀ E E', logrel_ectx τ α E E' + -∗ ∀ F F', logrel_mcont δ F F' + -∗ obs_ref e E F e' E' F')%I. + Solve All Obligations with try solve_proper. + Next Obligation. solve_proper_please. Qed. + + Definition logrel {S : Set} (τ α β : ty) : IT -n> exprO S -n> iProp + := logrel_expr (interp_ty τ) (interp_ty α) (interp_ty β). + + Program Definition ssubst_valid {S : Set} + (Γ : S -> ty) + (ss : interp_scope S) (γ : S [⇒] Empty_set) : iProp := + (∀ x τ, □ logrel (Γ x) τ τ (ss x) (γ x))%I. + + Program Definition valid {S : Set} + (Γ : S -> ty) + (e : interp_scope S -n> IT) + (e' : exprO S) + (τ α σ : ty) : iProp := + (□ ∀ γ (γ' : S [⇒] Empty_set), ssubst_valid Γ γ γ' + -∗ logrel τ α σ (e γ) (bind (F := expr) γ' e'))%I. + + Lemma compat_HOM_id {S : Set} P : + ⊢ @logrel_ectx S P P HOM_id END. + Proof. + iIntros (v v'). + iModIntro. + iIntros "Pv". + iIntros (σ m) "Hσ HH". + iApply ("Hσ" with "Pv HH"). + Qed. + + Lemma logrel_of_val {S : Set} τ α v (v' : valO S) : + interp_ty α v v' -∗ logrel α τ τ (IT_of_V v) (Val v'). + Proof. + iIntros "#H". + iIntros (κ K) "Hκ". + iIntros (σ m) "Hσ Hown". + iApply ("Hκ" with "H Hσ Hown"). + Qed. + + Lemma compat_var {S : Set} (Γ : S -> ty) (x : S) : + ⊢ (∀ α, valid Γ (interp_var x) (Var x) (Γ x) α α). + Proof. + iIntros (α). + iModIntro. + iIntros (γ γ') "#Hss". + iIntros (E E') "HE". + iIntros (F F') "HF". + iIntros "Hσ". + iApply ("Hss" with "HE HF Hσ"). + Qed. + + Lemma compat_reset {S : Set} (Γ : S -> ty) e (e' : exprO S) σ τ : + ⊢ valid Γ e e' σ σ τ -∗ (∀ α, valid Γ (interp_reset rs e) (reset e') τ α α). + Proof. + iIntros "#H". + iIntros (α). + iModIntro. + iIntros (γ γ') "Hγ". + iIntros (κ κ') "Hκ". + iIntros (m m') "Hm Hst". + assert (𝒫 ((`κ) (interp_reset rs e γ)) + ≡ (𝒫 ◎ `κ) (interp_reset rs e γ)) as ->. + { reflexivity. } + iApply (wp_reset with "Hst"). + iNext. + iIntros "_ Hst". + iSpecialize ("H" $! γ with "Hγ"). + unshelve iSpecialize ("H" $! HOM_id END (compat_HOM_id _) + (laterO_map (𝒫 ◎ `κ) :: m) (κ' :: m')); + first apply _. + iAssert (logrel_mcont (interp_ty τ) (laterO_map (𝒫 ◎ `κ) :: m) (κ' :: m')) + with "[Hm Hκ]" as "Hm". + { + iIntros (v v') "Hv Hst". + iApply (wp_pop_cons with "Hst"). + iNext. + iIntros "_ Hst". + iSpecialize ("Hκ" $! v with "Hv"). + iSpecialize ("Hκ" $! m with "Hm"). + iSpecialize ("Hκ" with "Hst"). + iApply (wp_wand with "Hκ"). + iIntros (?) "(H1 & (%w & %H2 & #H3))". + iModIntro. + iFrame "H1". + iExists w. + iFrame "H3". + iPureIntro. + edestruct (steps_det_val _ (Ccont κ' v' m') _ H2) as [[a b] H]; + first eapply step_pack; first econstructor. + exists (a + 1, b + 1)%nat. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat (b + 1)%nat _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat (b + 1)%nat _ _); + [ lia | lia | apply Ccont_end |]. + eapply (steps_many _ _ _ 1 1 a b (a + 1)%nat (b + 1)%nat); + [ lia | lia | apply Cmcont_cont |]. + apply H. + } + iSpecialize ("H" with "Hm Hst"). + iApply (wp_wand with "H"). + iIntros (?) "(H1 & (%w & %H2 & #H3))". + destruct H2 as [[a b] H2]. + iModIntro. + iFrame "H1". + iExists w. + iFrame "H3". + iPureIntro. + exists ((a + 1)%nat, (b + 1)%nat). + term_simpl. + eapply (steps_many _ _ _ 1 1 a b (a + 1)%nat (b + 1)%nat); + [ lia | lia | apply Ceval_reset |]. + assumption. + Qed. + + Lemma compat_shift {S : Set} (Γ : S -> ty) e (e' : exprO (inc S)) σ α τ β : + ⊢ valid (Γ ▹ (τ ⤑ α)) e e' σ σ β -∗ valid Γ (interp_shift _ e) (shift/cc e') τ α β. + Proof. + iIntros "#H". + iModIntro. + iIntros (γ γ') "#Hγ". + iIntros (κ κ') "#Hκ". + iIntros (m m') "Hm Hst". + assert (𝒫 ((`κ) (interp_shift rs e γ)) + ≡ (𝒫 ◎ `κ) (interp_shift rs e γ)) as ->. + { reflexivity. } + iApply (wp_shift with "Hst"). + { rewrite laterO_map_Next; reflexivity. } + iNext. + iIntros "_ Hst". + match goal with + | |- context G [ofe_mor_car _ _ e ?a] => + set (γ_ := a) + end. + pose (γ_' := ((mk_subst (Val (ContV κ')%syn)) ∘ (γ' ↑)%bind)%bind : inc S [⇒] ∅). + iAssert (ssubst_valid (Γ ▹ Tcont τ α) γ_ γ_') with "[Hγ Hκ]" as "Hγ'". + { + iIntros (x τ'). + destruct x as [| x]. + - iModIntro. + subst γ_'. + iIntros (E E') "HE". + iIntros (F F') "HF Hst". + simpl. + match goal with + | |- context G [ofe_mor_car _ _ (`E) (ofe_mor_car _ _ Fun ?a)] => + set (f := a) + end. + iApply ("HE" $! (FunV f) with "[Hκ] HF Hst"). + iExists κ, κ'. + iSplit. + + subst f; iPureIntro. + reflexivity. + + iSplit; first done. + iApply "Hκ". + - subst γ_'. + term_simpl. + iApply "Hγ". + } + iSpecialize ("H" $! γ_ with "Hγ'"). + iSpecialize ("H" $! HOM_id END (compat_HOM_id _) m with "Hm Hst"). + iApply (wp_wand with "H"). + iIntros (?) "(H1 & (%w & %H2 & #H3))". + destruct H2 as [[a b] H2]. + iModIntro. + iFrame "H1". + iExists w. + iFrame "H3". + iPureIntro. + exists ((a + 1)%nat, (b + 1)%nat). + term_simpl. + eapply (steps_many _ _ _ 1 1 a b (a + 1)%nat (b + 1)%nat); + [ lia | lia | apply Ceval_shift |]. + subst γ_'. + match goal with + | H2 : ?G |- ?H => + assert (H = G) as -> + end; last done. + do 2 f_equal. + unfold subst. + erewrite bind_bind_comp; + first reflexivity. + reflexivity. + Qed. + + Lemma compat_nat {S : Set} (Γ : S → ty) n α : + ⊢ valid Γ (interp_nat rs n) (#n) ℕ α α. + Proof. + iModIntro. + iIntros (γ γ') "#Hγ". + assert ((interp_nat rs n γ) = IT_of_V (RetV n)) as ->. + { reflexivity. } + iApply logrel_of_val. + by iExists n. + Qed. + + Lemma compat_recV {S : Set} (Γ : S -> ty) + τ1 α τ2 β e (e' : expr (inc (inc S))) : + ⊢ valid (Γ ▹ τ1 ∕ α → τ2 ∕ β ▹ τ1) e e' τ2 α β + -∗ (∀ θ, valid Γ (interp_rec rs e) (rec e') (τ1 ∕ α → τ2 ∕ β) θ θ). + Proof. + iIntros "#H". + iIntros (θ). + iModIntro. + iIntros (γ γ') "#Hγ". + set (f := (ir_unf rs e γ)). + iAssert (interp_rec rs e γ ≡ IT_of_V $ FunV (Next f))%I as "Hf". + { iPureIntro. apply interp_rec_unfold. } + iAssert (logrel (Tarr τ1 α τ2 β) θ θ (interp_rec rs e γ) + (bind (F := expr) γ' (rec e')) + ≡ logrel (Tarr τ1 α τ2 β) θ θ (IT_of_V (FunV (Next f))) + (bind (F := expr) γ' (rec e')))%I as "Hf'". + { + iPureIntro. + do 2 f_equiv. + apply interp_rec_unfold. + } + iRewrite "Hf'". + Opaque IT_of_V. + iApply logrel_of_val; term_simpl. + iExists _. iSplit. + { iPureIntro. apply into_val. } + iSplit. + { iPureIntro. + eexists _. + reflexivity. + } + iModIntro. + iLöb as "IH". + iIntros (v v') "#Hw". + iIntros (κ κ') "#Hκ". + iIntros (σ σ') "Hσ Hst". + rewrite APP_APP'_ITV APP_Fun laterO_map_Next -Tick_eq. + pose (γ'' := + (extend_scope (extend_scope γ (interp_rec rs e γ)) (IT_of_V v))). + rewrite /logrel. + Opaque extend_scope. + simpl. + rewrite hom_tick. + rewrite hom_tick. + iApply wp_tick. + iNext. + set (γ_' := ((mk_subst (Val (rec bind ((γ' ↑) ↑)%bind e')%syn)) + ∘ ((mk_subst (shift (Val v'))) ∘ ((γ' ↑) ↑)))%bind). + iSpecialize ("H" $! γ'' γ_' with "[Hw]"). + { + iIntros (x). + destruct x as [| [| x]]; iIntros (ξ); iModIntro. + * subst γ''. + iApply logrel_of_val. + term_simpl. + rewrite subst_shift_id. + iApply "Hw". + * iIntros (K' K'') "Hκ'". + iIntros (M' σ'') "Hσ' Hst". + Transparent extend_scope. + simpl. + iRewrite "Hf". + iSpecialize ("Hκ'" $! (FunV (Next f)) (bind (BindCore := BindCore_val) γ' (RecV e')) with "[IH]"). + { + iExists (Next f). + iSplit; first done. + iSplit. + { + iPureIntro. + eexists (bind (F := expr) (lift (G := inc) (lift γ'))%bind e'). + term_simpl. + reflexivity. + } + iModIntro. + iIntros (βv v'') "Hβv". + iIntros (κ'' P'') "Hκ''". + iIntros (σ''' M'') "Hσ'' Hst". + iApply ("IH" $! βv with "Hβv Hκ'' Hσ'' Hst"). + } + iApply ("Hκ'" with "Hσ' Hst"). + * subst γ_'. + term_simpl. + iApply "Hγ". + } + subst γ_'. + iSpecialize ("H" with "Hκ Hσ Hst"). + iApply (wp_wand with "H"). + iIntros (?) "(? & HHH)". + iModIntro. + iFrame. + iDestruct "HHH" as "(%v1 & %HHH & #GGG)". + iExists v1. + iFrame "GGG". + iPureIntro. + destruct HHH as [nm HHH]. + destruct nm as [a b]. + exists (a + 1, b)%nat. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat b _ _); + [ reflexivity | reflexivity | apply Ceval_app |]. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat b _ _); + [ lia | lia | apply Ccont_appl |]. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 1 0 a b (a + 1)%nat b); + [ lia | lia | apply Ccont_appr |]. + unfold subst. + rewrite !bind_bind_comp'. + match goal with + | HHH : ?T |- ?Q => + assert (Q = T) as -> + end; last done. + do 2 f_equal. + fold_bind. + rewrite -!bind_bind_comp'. + reflexivity. + Qed. + + Lemma compat_nat_op {S : Set} (Γ : S → ty) + D E F e1 e2 (e1' e2' : expr S) op : + ⊢ valid Γ e1 e1' ℕ E F + -∗ valid Γ e2 e2' ℕ F D + -∗ valid Γ (interp_natop rs op e1 e2) (NatOp op e1' e2') ℕ E D. + Proof. + iIntros "#H #G". + iModIntro. + iIntros (γ γ') "#Hγ". + iIntros (κ κ') "#Hκ". + iIntros (m m') "Hm Hst". + rewrite /interp_natop //=. + + set (K' := (NatOpRSCtx_HOM op e1 γ)). + assert ((NATOP (do_natop op) (e1 γ) (e2 γ)) = ((`K') (e2 γ))) as -> by done. + rewrite HOM_ccompose. + pose (sss := (HOM_compose κ K')). rewrite (HOM_compose_ccompose κ K' sss)//. + + iSpecialize ("G" $! γ with "Hγ"). + iSpecialize ("G" $! sss). + iSpecialize ("G" $! (NatOpRK op (bind (F := expr) (BindCore := BindCore_expr) γ' e1' : exprO Empty_set) κ') with "[H] Hm Hst"). + { + iIntros (w w'). + iModIntro. + iIntros "#Hw". + iIntros (M M') "Hm Hst". + subst sss. + subst K'. + simpl. + + pose (K' := (NatOpLSCtx_HOM op (IT_of_V w) γ _)). + assert ((NATOP (do_natop op) (e1 γ) (IT_of_V w)) = ((`K') (e1 γ))) + as -> by done. + rewrite HOM_ccompose. + pose (sss := (HOM_compose κ K')). rewrite (HOM_compose_ccompose κ K' sss)//. + + iSpecialize ("H" $! γ with "Hγ"). + iSpecialize ("H" $! sss). + iSpecialize ("H" $! (NatOpLK op w' κ') with "[] Hm Hst"). + { + iIntros (v v'). + iModIntro. + iIntros "#Hv". + iIntros (m'' M'') "Hm Hst". + subst sss. + subst K'. + simpl. + + iDestruct "Hw" as "(%n & #HEQ1 & #HEQ1')". + iDestruct "Hv" as "(%n' & #HEQ2 & #HEQ2')". + iSpecialize ("Hκ" $! (RetV (do_natop op n' n)) with "[]"). + { + iExists _. + iPureIntro. + split; reflexivity. + } + iSpecialize ("Hκ" $! m'' with "Hm Hst"). + rewrite IT_of_V_Ret. + + iAssert ((NATOP (do_natop op) (IT_of_V v) (IT_of_V w)) + ≡ (Ret (do_natop op n' n)))%I as "#HEQ". + { + iRewrite "HEQ1". + rewrite IT_of_V_Ret. + iAssert ((IT_of_V v) ≡ IT_of_V (RetV n'))%I as "#HEQ2''". + { + iApply f_equivI. + iApply "HEQ2". + } + rewrite IT_of_V_Ret. + iAssert (NATOP (do_natop op) (IT_of_V v) (Ret n) + ≡ NATOP (do_natop op) (Ret n') (Ret n))%I as "#HEQ2'''". + { + unshelve iApply (f_equivI (λne x, NATOP (do_natop op) x (Ret n))). + { solve_proper. } + { solve_proper. } + iApply "HEQ2''". + } + iRewrite "HEQ2'''". + rewrite NATOP_Ret. + done. + } + iRewrite "HEQ". + iApply (wp_wand with "Hκ"). + iIntros (?) "(H1 & (%t & %H2 & #H3))". + iModIntro. + iFrame "H1". + iRewrite "HEQ2'". + iRewrite "HEQ1'". + iExists t. + iFrame "H3". + iPureIntro. + destruct H2 as [nm H2]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 a b _ _); + [ lia | lia | apply Ccont_natopl |]. + - reflexivity. + - apply H2. + } + iApply (wp_wand with "H"). + iIntros (?) "(H1 & (%t & %H2 & #H3))". + iModIntro. + iFrame "H1". + iExists t. + iFrame "H3". + iPureIntro. + destruct H2 as [nm H2]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 a b _ _); + [ lia | lia | apply Ccont_natopr |]. + assumption. + } + iApply (wp_wand with "G"). + iIntros (?) "(H1 & (%t & %H2 & #H3))". + iModIntro. + iFrame "H1". + iExists t. + iFrame "H3". + iPureIntro. + destruct H2 as [nm H2]. + destruct nm as [a b]. + exists (a, b). + term_simpl. + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_natop |]. + assumption. + Qed. + + Lemma compat_app {S : Set} (Γ : S → ty) + ξ α β δ η τ e1 e2 (e1' e2' : expr S) : + ⊢ valid Γ e1 e1' (η ∕ α → τ ∕ β) ξ δ + -∗ valid Γ e2 e2' η β ξ + -∗ valid Γ (interp_app rs e1 e2) (e1' e2') τ α δ. + Proof. + iIntros "#H #G". + iModIntro. + iIntros (γ γ') "#Hγ". + iIntros (κ κ') "#Hκ". + iIntros (σ σ') "Hσ Hst". + rewrite /interp_app //=. + + pose (K' := (AppLSCtx_HOM e2 γ)). + match goal with + | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] => + set (F := b) + end. + assert (LET (e1 γ) F = ((`K') (e1 γ))) as ->. + { simpl; unfold AppLSCtx. reflexivity. } + clear F. + assert ((`κ) ((`K') (e1 γ)) = ((`κ) ◎ (`K')) (e1 γ)) as ->. + { reflexivity. } + pose (sss := (HOM_compose κ K')). + assert ((`κ ◎ `K') = (`sss)) as ->. + { reflexivity. } + + iSpecialize ("H" $! γ with "Hγ"). + iSpecialize ("H" $! sss). + iSpecialize ("H" $! (AppLK (bind (F := expr) γ' e2') κ') with "[] Hσ Hst"). + { + iIntros (w w'). + iModIntro. + iIntros "#Hw". + iIntros (m' M') "Hm Hst". + subst sss. + subst K'. + simpl. + rewrite LET_Val. + cbn [ofe_mor_car]. + match goal with + | |- context G [ofe_mor_car _ _ (ofe_mor_car _ _ LET ?a) ?b] => + set (F := b) + end. + pose (κ'' := exist _ (LETCTX F) (LETCTX_Hom F) : HOM). + assert (((`κ) (LET (e2 γ) F)) = (((`κ) ◎ (`κ'')) (e2 γ))) as ->. + { reflexivity. } + pose (sss := (HOM_compose κ κ'')). + assert ((`κ ◎ `κ'') = (`sss)) as ->. + { reflexivity. } + iSpecialize ("G" $! γ with "Hγ"). + iSpecialize ("G" $! sss). + + iSpecialize ("G" $! (AppRK w' κ') with "[] Hm Hst"). + { + iIntros (v v'). + iModIntro. + iIntros "#Hv". + iIntros (m'' M'') "Hm Hst". + subst sss. + subst κ''. + simpl. + rewrite LET_Val. + subst F. + cbn [ofe_mor_car]. + + iDestruct "Hw" as "(%n' & #HEQ & %HEQ_ & Hw)". + iSpecialize ("Hw" $! v with "Hv"). + iSpecialize ("Hw" $! κ with "Hκ"). + iSpecialize ("Hw" $! m'' with "Hm Hst"). + iAssert ((IT_of_V w ⊙ (IT_of_V v)) + ≡ (Fun n' ⊙ (IT_of_V v)))%I as "#HEQ'". + { + iApply (f_equivI (λne x, (x ⊙ (IT_of_V v)))). + iApply "HEQ". + } + iRewrite "HEQ'". + iApply (wp_wand with "Hw"). + iIntros (u) "(Hst & (%y & %H1 & H2))". + iModIntro. + iFrame "Hst". + iExists y. + iFrame "H2". + iPureIntro. + unshelve epose proof (steps_det_val _ (Ceval w' (AppLK v' κ') M'') _ H1 _) as H. + { eapply step_pack; first econstructor. } + unshelve epose proof (steps_det_val _ (Ccont (AppLK v' κ') w' M'') _ H _) as H'. + { eapply step_pack; first econstructor. } + unshelve epose proof (steps_det_val _ (Ceval v' (AppRK w' κ') M'') _ H' _) as H''. + { eapply step_pack; first econstructor. } + apply H''. + } + iApply (wp_wand with "G"). + iIntros (u) "(Hst & (%y & %H1 & H2))". + iModIntro. + iFrame "Hst". + iExists y. + iFrame "H2". + iPureIntro. + destruct H1 as [nm H1]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ccont_appl |]. + apply H1. + } + iApply (wp_wand with "H"). + iIntros (u) "(Hst & (%y & %H1 & H2))". + iModIntro. + iFrame "Hst". + iExists y. + iFrame "H2". + iPureIntro. + destruct H1 as [nm H1]. + destruct nm as [a b]. + term_simpl. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_app |]. + apply H1. + Qed. + + Lemma compat_appcont {S : Set} (Γ : S -> ty) e1 e2 (e1' e2' : expr S) τ α δ β σ : + valid Γ e1 e1' (τ ⤑ α) σ δ + -∗ valid Γ e2 e2' τ δ β + -∗ valid Γ (interp_app_cont _ e1 e2) (e1' @k e2') α σ β. + Proof. + iIntros "#H #G". + iModIntro. + iIntros (γ γ') "#Henv". + iIntros (κ κ') "#Hκ". + iIntros (σ' M') "Hm Hst". + + pose (K' := (AppContRSCtx_HOM e1 γ)). + assert ((interp_app_cont rs e1 e2 γ) = ((`K') (e2 γ))) as ->. + { simpl. reflexivity. } + assert ((`κ) ((`K') (e2 γ)) = ((`κ) ◎ (`K')) (e2 γ)) as ->. + { reflexivity. } + pose (sss := (HOM_compose κ K')). + assert ((`κ ◎ `K') = (`sss)) as ->. + { reflexivity. } + + iSpecialize ("G" $! γ with "Henv"). + iSpecialize ("G" $! sss). + iSpecialize ("G" $! (AppContRK (bind (F := expr) (BindCore := BindCore_expr) γ' e1') κ') with "[H] Hm Hst"). + { + iIntros (w w'). + iModIntro. + iIntros "#Hw". + iIntros (m' m'') "Hm Hst". + subst sss. + subst K'. + Opaque interp_app_cont. + simpl. + + pose (κ'' := (AppContLSCtx_HOM (IT_of_V w) γ _)). + set (F := (`κ) _). + assert (F ≡ (((`κ) ◎ (`κ'')) (e1 γ))) as ->. + { + subst F. simpl. Transparent interp_app_cont. simpl. + f_equiv. + rewrite ->2 get_val_ITV. + simpl. + reflexivity. + } + pose (sss := (HOM_compose κ κ'')). + assert ((`κ ◎ `κ'') = (`sss)) as ->. + { reflexivity. } + iSpecialize ("H" $! γ with "Henv"). + iSpecialize ("H" $! sss). + iSpecialize ("H" $! (AppContLK w' κ') with "[] Hm Hst"). + { + iIntros (v v'). + iModIntro. + iIntros "#Hv". + iIntros (σ'' M'') "Hm Hst". + subst sss. + subst κ''. + Opaque APP_CONT. + simpl. + + rewrite get_val_ITV. + simpl. + iDestruct "Hv" as "(%n' & %K'' & #HEQ & %HK & #Hv)". + iRewrite "HEQ". + rewrite get_fun_fun. + simpl. + + match goal with + | |- context G [ofe_mor_car _ _ + (ofe_mor_car _ _ APP_CONT ?a) ?b] => + set (T := APP_CONT a b) + end. + iAssert (𝒫 ((`κ) T) ≡ (𝒫 ◎ (`κ)) T)%I as "HEQ'". + { iPureIntro. reflexivity. } + iRewrite "HEQ'"; iClear "HEQ'". + subst T. + + iApply (wp_app_cont with "[Hst]"). + { reflexivity. } + - iFrame "Hst". + - simpl. + iNext. + iIntros "_ Hst". + rewrite later_map_Next. + rewrite <-Tick_eq. + iApply wp_tick. + iNext. + iSpecialize ("Hv" $! w with "Hw"). + + iSpecialize ("Hv" $! (laterO_map (𝒫 ◎ `κ) :: σ'') (κ' :: M'') with "[Hm] Hst"). + { + iIntros (p p') "#Hp Hst". + iApply (wp_pop_cons with "Hst"). + iNext. + iIntros "_ Hst". + iSpecialize ("Hκ" with "Hp Hm Hst"). + iApply (wp_wand with "Hκ"). + iIntros (?) "(T & (%v1 & %Q & R))". + iModIntro. + iFrame "T". + iExists v1. + iFrame "R". + iPureIntro. + unshelve epose proof (steps_det_val _ (Ccont κ' p' M'') _ Q _) as Q'. + { eapply step_pack; first econstructor. } + destruct Q' as [nm Q']. + destruct nm as [a b]. + exists ((a + 1)%nat, (b + 1)%nat). + eapply (steps_many _ _ _ 0 0 (a + 1)%nat (b + 1)%nat _ _); + [done | done | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 (a + 1)%nat (b + 1)%nat _ _); + [done | done | apply Ccont_end |]. + eapply (steps_many _ _ _ 1 1 a b _ _); + [lia | lia | apply Cmcont_cont |]. + apply Q'. + } + iApply (wp_wand with "Hv"). + iIntros (?) "(T & (%v1 & %Q & R))". + iModIntro. + iFrame "T". + iExists v1. + iFrame "R". + iPureIntro. + unshelve epose proof (steps_det_val _ (Ccont K'' w' (κ' :: M'')) _ Q _) as Q'. + { eapply step_pack; first econstructor. } + destruct Q' as [nm Q']. + destruct nm as [a b]. + exists ((a + 2)%nat, (b + 1)%nat). + eapply (steps_many _ _ _ 0 0 (a + 2)%nat (b + 1)%nat _ _); + [done | done | apply Ceval_val |]. + rewrite HK. + eapply (steps_many _ _ _ 2 1 a b _ _); + [lia | lia | apply Ccont_cont |]. + apply Q'. + } + iApply (wp_wand with "H"). + iIntros (?) "(T & (%v1 & %Q & R))". + iModIntro. + iFrame "T". + iExists v1. + iFrame "R". + iPureIntro. + destruct Q as [nm Q]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [done | done | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 a b _ _); + [done | done | apply Ccont_app_contr |]. + apply Q. + } + iApply (wp_wand with "G"). + iIntros (?) "(T & (%v1 & %Q & R))". + iModIntro. + iFrame "T". + iExists v1. + iFrame "R". + iPureIntro. + destruct Q as [nm Q]. + destruct nm as [a b]. + exists (a, b). + term_simpl. + eapply (steps_many _ _ _ 0 0 a b _ _); + [done | done | apply Ceval_app_cont |]. + apply Q. + Qed. + + Lemma compat_if {S : Set} (Γ : S -> ty) e e₁ e₂ (e' e₁' e₂' : expr S) τ σ α β : + ⊢ valid Γ e e' ℕ β α + -∗ valid Γ e₁ e₁' τ σ β + -∗ valid Γ e₂ e₂' τ σ β + -∗ valid Γ (interp_if rs e e₁ e₂) + (if e' then e₁' else e₂') τ σ α. + Proof. + iIntros "#H #G #J". + iModIntro. + iIntros (γ γ') "#Henv". + iIntros (κ K) "#Hκ". + iIntros (σ' M) "Hm Hst". + unfold interp_if. + cbn [ofe_mor_car]. + pose (κ' := (IFSCtx_HOM (e₁ γ) (e₂ γ))). + assert ((IF (e γ) (e₁ γ) (e₂ γ)) = ((`κ') (e γ))) as -> by reflexivity. + assert ((`κ) ((`κ') (e γ)) = ((`κ) ◎ (`κ')) (e γ)) + as -> by reflexivity. + pose (sss := (HOM_compose κ κ')). + rewrite (HOM_compose_ccompose κ κ' sss)//. + + iSpecialize ("H" $! γ with "Henv"). + iSpecialize ("H" $! sss). + + iSpecialize ("H" $! (IfK (bind (F := expr) (BindCore := BindCore_expr) γ' e₁') + (bind (F := expr) (BindCore := BindCore_expr) γ' e₂') K) + with "[] Hm Hst"). + { + iIntros (v v'). + iModIntro. + iIntros "#Hv". + iIntros (σ'' M'') "Hm Hst". + iDestruct "Hv" as "(%n & #Hv & #Hv')". + iRewrite "Hv". + rewrite IT_of_V_Ret. + subst sss. + subst κ'. + simpl. + unfold IFSCtx. + destruct (decide (0 < n)) as [H|H]. + - rewrite IF_True//. + iSpecialize ("G" $! γ with "Henv [Hκ] Hm Hst"). + { + iIntros (w w'). + iModIntro. + iIntros "#Hw". + iIntros (σ''' M''') "Hm Hst". + iApply ("Hκ" with "Hw Hm Hst"). + } + iApply (wp_wand with "G"). + iIntros (q) "(H1 & H2)". + iModIntro. + iFrame "H1". + iDestruct "H2" as "(%p & %H2 & H3)". + iExists p. + iFrame "H3". + iRewrite "Hv'". + iPureIntro. + destruct H2 as [nm H2]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ccont_if |]. + assert ((n =? 0)%nat = false) as ->. + { + apply Nat.eqb_neq. + lia. + } + assumption. + - rewrite IF_False//; last lia. + iSpecialize ("J" $! γ with "Henv [Hκ] Hm Hst"). + { + iIntros (w w'). + iModIntro. + iIntros "#Hw". + iIntros (σ''' M''') "Hm Hst". + iApply ("Hκ" with "Hw Hm Hst"). + } + iApply (wp_wand with "J"). + iIntros (q) "(H1 & H2)". + iModIntro. + iFrame "H1". + iDestruct "H2" as "(%p & %H2 & H3)". + iExists p. + iFrame "H3". + iRewrite "Hv'". + iPureIntro. + destruct H2 as [nm H2]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ccont_if |]. + assert ((n =? 0)%nat = true) as ->. + { + apply Nat.eqb_eq. + lia. + } + assumption. + } + iApply (wp_wand with "H"). + iIntros (q) "(H1 & H2)". + iModIntro. + iFrame "H1". + iDestruct "H2" as "(%p & %H2 & H3)". + iExists p. + iFrame "H3". + iPureIntro. + term_simpl. + destruct H2 as [nm H2]. + destruct nm as [a b]. + exists (a, b). + eapply (steps_many _ _ _ 0 0 a b _ _); + [ reflexivity | reflexivity | apply Ceval_if |]. + apply H2. + Qed. + + Open Scope types. + + Lemma fundamental_expr {S : Set} (Γ : S -> ty) τ α β e : + Γ; α ⊢ₑ e : τ; β → ⊢ valid Γ (interp_expr rs e) e τ α β + with fundamental_val {S : Set} (Γ : S -> ty) τ α β v : + Γ; α ⊢ᵥ v : τ; β → ⊢ valid Γ (interp_val rs v) v τ α β. + Proof. + - intros H. + destruct H. + + by apply fundamental_val. + + subst; iApply compat_var. + + iApply compat_app; + by iApply fundamental_expr. + + iApply compat_appcont; + by iApply fundamental_expr. + + iApply compat_nat_op; + by iApply fundamental_expr. + + iApply compat_if; + by iApply fundamental_expr. + + iApply compat_shift; + by iApply fundamental_expr. + + iApply (compat_reset with "[]"); + by iApply fundamental_expr. + - intros H. + destruct H. + + iApply compat_nat. + + iApply (compat_recV with "[]"); + by iApply fundamental_expr. + Qed. + +End logrel. + +Definition κ {S} {E} : ITV E natO → val S := λ x, + match x with + | core.RetV n => LitV n + | _ => LitV 0 + end. +Lemma κ_Ret {S} {E} n : κ ((RetV n) : ITV E natO) = (LitV n : val S). +Proof. + Transparent RetV. unfold RetV. simpl. done. Opaque RetV. +Qed. + +Local Definition rs : gReifiers CtxDep 1 := + gReifiers_cons reify_delim gReifiers_nil. + +Variable Hdisj : ∀ (Σ : gFunctors) (P Q : iProp Σ), disjunction_property P Q. + +Lemma logrel_nat_adequacy Σ `{!invGpreS Σ} `{!statePreG rs natO Σ} {S} + (α : IT (gReifiers_ops rs) natO) + (e : expr S) (n : nat) σ k : + (∀ `{H1 : !invGS Σ} `{H2: !stateG rs natO Σ}, + (⊢ logrel rs Tnat Tnat Tnat α e)%I) → + ssteps (gReifiers_sReifier rs) (𝒫 α) ([], ()) (Ret n) σ k → + ∃ m, steps (Cexpr e) (Cret (LitV n)) m. +Proof. + intros Hlog Hst. + pose (ϕ := λ (βv : ITV (gReifiers_ops rs) natO), + ∃ m, steps (Cexpr e) (Cret $ κ βv) m). + cut (ϕ (RetV n)). + { + destruct 1 as ( m' & Hm). + exists m'. revert Hm. by rewrite κ_Ret. + } + eapply (wp_adequacy 0); eauto. + Unshelve. + 2: { + intros ?. + apply False. + } + intros Hinv1 Hst1. + pose (Φ := (λ (βv : ITV (gReifiers_ops rs) natO), + ∃ n, interp_ty rs (Σ := Σ) (S := S) Tnat βv (LitV n) + ∗ ⌜∃ m, steps (Cexpr e) (Cret $ LitV n) m⌝ + ∗ logrel_nat rs (Σ := Σ) (S := S) βv (LitV n))%I). + assert (NonExpansive Φ). + { + unfold Φ. + intros l a1 a2 Ha. repeat f_equiv; done. + } + exists Φ. split; first assumption. split. + - iIntros (βv). iDestruct 1 as (n'') "(H & %H' & #H'')". + iDestruct "H" as (n') "[#H %]". simplify_eq/=. + iAssert (IT_of_V βv ≡ Ret n')%I as "#Hb". + { iRewrite "H". iPureIntro. by rewrite IT_of_V_Ret. } + iAssert (⌜βv = RetV n'⌝)%I with "[-]" as %Hfoo. + { destruct βv as [r|f]; simpl. + - iPoseProof (Ret_inj' with "Hb") as "%Hr". + fold_leibniz. eauto. + - iExFalso. iApply (IT_ret_fun_ne). + iApply internal_eq_sym. iExact "Hb". } + iPureIntro. rewrite Hfoo. unfold ϕ. + eauto. + - iIntros "[_ Hs]". + iPoseProof (Hlog _ _) as "Hlog". + iAssert (has_substate _)%I with "[Hs]" as "Hs". + { + unfold has_substate, has_full_state. + eassert (of_state rs (IT (gReifiers_ops rs) _) (_,()) + ≡ of_idx rs (IT (gReifiers_ops rs) _) sR_idx (sR_state _)) as -> + ; last done. + intro j. unfold sR_idx. simpl. + unfold of_state, of_idx. + destruct decide as [Heq|]; last first. + { inv_fin j; first done. + intros i. inversion i. } + inv_fin j; last done. + intros Heq. + rewrite (eq_pi _ _ Heq eq_refl)//. + simpl. + unfold iso_ofe_refl. + cbn. + reflexivity. + } + iSpecialize ("Hlog" $! HOM_id END (compat_HOM_id _ _) [] [] with "[]"). + { + iIntros (αv v) "HHH GGG". + iApply (wp_pop_end with "GGG"). + iNext. + iIntros "_ GGG". + iApply wp_val. + iModIntro. + iFrame "GGG". + iExists v. + iSplitR "HHH". + - iPureIntro. + exists (1, 1). + eapply (steps_many _ _ _ 0 0 1 1 1 1); + [done | done | apply Ceval_val |]. + eapply (steps_many _ _ _ 0 0 1 1 1 1); + [done | done | apply Ccont_end |]. + eapply (steps_many _ _ _ 1 1 0 0 1 1); + [done | done | apply Cmcont_ret |]. + constructor. + - iApply "HHH". + } + simpl. + unfold obs_ref'. + iSpecialize ("Hlog" with "Hs"). + iApply (wp_wand with "Hlog"). + iIntros ( βv). iIntros "H". + iDestruct "H" as "[Hi Hsts]". + subst Φ. + iModIntro. + iDestruct "Hsts" as "(%w & %p & Hsts)". + iDestruct "Hsts" as "(%w' & #HEQ1 & #HEQ2)". + iExists w'. + iSplit. + + iExists _. + iSplit; done. + + iSplit. + * iRewrite - "HEQ2". + iPureIntro. + destruct p as [nm p]. + exists nm. + destruct nm as [a b]. + eapply (steps_many _ _ _ 0 0 a b a b); + [done | done | apply Ceval_init |]. + done. + * iExists _. + iSplit; done. +Qed. + +Theorem adequacy (e : expr ∅) (k : nat) σ n : + (empty_env; ℕ ⊢ₑ e : ℕ; ℕ)%type → + ssteps (gReifiers_sReifier rs) (𝒫 (interp_expr rs e ı_scope)) ([], ()) + (Ret k : IT _ natO) σ n → + ∃ mm, steps (Cexpr e) (Cret $ LitV k) mm. +Proof. + intros Hty Hst. + pose (Σ := gFunctors.app invΣ (gFunctors.app (stateΣ rs natO) gFunctors.nil)). + eapply (logrel_nat_adequacy Σ (interp_expr rs e ı_scope)); last eassumption. + intros ? ?. + iPoseProof (fundamental_expr rs _ _ _ _ _ Hty) as "#H". + unfold valid. + unshelve iSpecialize ("H" $! ı_scope _ with "[]"). + { apply ı%bind. } + { iIntros (x); destruct x. } + rewrite ebind_id; first last. + { intros ?; reflexivity. } + iApply "H". +Qed. diff --git a/theories/examples/delim_lang/typing.v b/theories/examples/delim_lang/typing.v new file mode 100644 index 0000000..fa98b2a --- /dev/null +++ b/theories/examples/delim_lang/typing.v @@ -0,0 +1,100 @@ +(** * Type sytem for delim-lang + +The system is based on + O. Danvy and A. Filinski. A functional abstraction of typed contexts. +*) +From gitrees.examples.delim_lang Require Import lang. + +Require Import Binding.Lib Binding.Set Binding.Env. + +Open Scope syn. + +Inductive ty := +| Tnat : ty +| Tarr : ty -> ty -> ty -> ty -> ty +| Tcont : ty → ty → ty. + +Declare Scope types. + +Notation "'ℕ'" := (Tnat) : types. +Notation "τ '∕' α '→' σ '∕' β" := + (Tarr τ α σ β) + (at level 15 + , σ, α, β at level 10 + , no associativity) : types. +Notation "τ '⤑' σ" := (Tcont τ σ) (at level 10, left associativity) : types. + +Reserved Notation "Γ ';' α '⊢ₑ' e ':' τ ';' β" + (at level 70 + , e at level 60 + , τ, α, β at level 20 + , no associativity). + +Reserved Notation "Γ ';' α '⊢ᵥ' e ':' τ ';' β" + (at level 70 + , e at level 60 + , τ, α, β at level 20 + , no associativity). + +Open Scope types. + +Inductive typed_expr {S : Set} (Γ : S -> ty) : ty -> expr S -> ty -> ty -> Prop := +| typed_Val v α τ β : + (Γ; α ⊢ᵥ v : τ; β) → + (Γ; α ⊢ₑ v : τ; β) +| typed_Var x τ α : + (Γ x = τ) → + (Γ; α ⊢ₑ (Var x) : τ; α) +| typed_App e₁ e₂ γ α β δ σ τ : + (Γ; γ ⊢ₑ e₁ : σ ∕ α → τ ∕ β; δ) → + (Γ; β ⊢ₑ e₂ : σ; γ) → + (Γ; α ⊢ₑ e₁ ⋆ e₂ : τ; δ) +| typed_AppCont e₁ e₂ α β δ σ τ : + (Γ; σ ⊢ₑ e₁ : τ ⤑ α; δ) → + (Γ; δ ⊢ₑ e₂ : τ; β) → + (Γ; σ ⊢ₑ e₁ @k e₂ : α; β) +| typed_NatOp o e₁ e₂ α β γ : + (Γ; α ⊢ₑ e₁ : ℕ; β) → + (Γ; β ⊢ₑ e₂ : ℕ; γ) → + (Γ; α ⊢ₑ NatOp o e₁ e₂ : ℕ; γ) +| typed_If e e₁ e₂ α β σ τ : + (Γ; β ⊢ₑ e : ℕ; α) → + (Γ; σ ⊢ₑ e₁ : τ; β) → + (Γ; σ ⊢ₑ e₂ : τ; β) → + (Γ; σ ⊢ₑ (if e then e₁ else e₂) : τ; α) +| typed_Shift (e : @expr (inc S)) τ α σ β : + (Γ ▹ τ ⤑ α; σ ⊢ₑ e : σ; β) → + (Γ; α ⊢ₑ shift/cc e : τ; β) +| typed_Reset e α σ τ : + (Γ; σ ⊢ₑ e : σ; τ) → + (Γ; α ⊢ₑ reset e : τ; α) +where "Γ ';' α '⊢ₑ' e ':' τ ';' β" := (typed_expr Γ α e τ β) : types +with typed_val {S : Set} (Γ : S -> ty) : ty -> val S -> ty -> ty -> Prop := +| typed_LitV n α : + (Γ; α ⊢ᵥ #n : ℕ; α) +| typed_RecV (e : expr (inc (inc S))) (δ σ τ α β : ty) : + (Γ ▹ (σ ∕ α → τ ∕ β) ▹ σ; α ⊢ₑ e : τ; β) -> + (Γ; δ ⊢ᵥ rec e : σ ∕ α → τ ∕ β; δ) +where "Γ ';' α '⊢ᵥ' e ':' τ ';' β" := (typed_val Γ α e τ β) : types +. + +Module Example. + Open Scope types. + + Lemma typ_example1 α : + □; α ⊢ₑ ((#1) + (reset ((#3) + (shift/cc ((($0) @k #5) + (($0) @k #6)))))) : Tnat; α. + Proof. + econstructor. + - do 2 constructor. + - do 2 econstructor. + + do 2 constructor. + + do 2 econstructor. + * econstructor. + -- by constructor. + -- do 2 constructor. + * econstructor. + -- by constructor. + -- do 2 constructor. + Qed. + +End Example. diff --git a/theories/examples/input_lang_callcc/hom.v b/theories/examples/input_lang_callcc/hom.v index 17d197e..0b5e227 100644 --- a/theories/examples/input_lang_callcc/hom.v +++ b/theories/examples/input_lang_callcc/hom.v @@ -1,6 +1,6 @@ -(** In this module, we package up IT homomorphism in a sigma type, and -we will use it as a domain for logical relations on continuations *) +(** Particular homomorphisms for the call/cc lang *) From gitrees Require Import gitree lang_generic. +From gitrees Require Export hom. From gitrees.examples.input_lang_callcc Require Import lang interp. Require Import Binding.Lib Binding.Set Binding.Env. @@ -9,50 +9,19 @@ Open Scope stdpp_scope. Section hom. Context {sz : nat}. Context {rs : gReifiers CtxDep sz}. + Context {A : ofe}. + Context {CA : Cofe A}. + Context `{SubOfe natO A}. Context `{!subReifier reify_cont rs}. Context `{!subReifier (sReifier_NotCtxDep_CtxDep reify_io) rs}. Notation F := (gReifiers_ops rs). Notation IT := (IT F natO). Notation ITV := (ITV F natO). - Definition HOM : ofe := @sigO (IT -n> IT) IT_hom. - - Global Instance HOM_hom (κ : HOM) : IT_hom (`κ). - Proof. - apply (proj2_sig κ). - Qed. - - Program Definition HOM_id : HOM := exist _ idfun _. - Next Obligation. - apply _. - Qed. - - Lemma HOM_ccompose (f g : HOM) : - ∀ α, `f (`g α) = (`f ◎ `g) α. - Proof. - intro; reflexivity. - Qed. - - Program Definition HOM_compose (f g : HOM) : HOM := exist _ (`f ◎ `g) _. - Next Obligation. - intros f g; simpl. - apply _. - Qed. - - Lemma HOM_compose_ccompose (f g h : HOM) : - h = HOM_compose f g -> - `f ◎ `g = `h. - Proof. intros ->. done. Qed. - (** Specific packaged homomorphisms *) - Program Definition IFSCtx_HOM α β : HOM := exist _ (λne x, IFSCtx α β x) _. - Next Obligation. - intros; simpl. - apply _. - Qed. Program Definition NatOpRSCtx_HOM {S : Set} (op : nat_op) - (α : @interp_scope F natO _ S -n> IT) (env : @interp_scope F natO _ S) + (α : @interp_scope F A _ S -n> IT) (env : @interp_scope F A _ S) : HOM := exist _ (interp_natoprk rs op α (λne env, idfun) env) _. Next Obligation. intros; simpl. @@ -60,7 +29,7 @@ Section hom. Qed. Program Definition NatOpLSCtx_HOM {S : Set} (op : nat_op) - (α : IT) (env : @interp_scope F natO _ S) + (α : IT) (env : @interp_scope F A _ S) (Hv : AsVal α) : HOM := exist _ (interp_natoplk rs op (λne env, idfun) (constO α) env) _. Next Obligation. @@ -69,8 +38,8 @@ Section hom. Qed. Program Definition ThrowLSCtx_HOM {S : Set} - (α : @interp_scope F natO _ S -n> IT) - (env : @interp_scope F natO _ S) + (α : @interp_scope F A _ S -n> IT) + (env : @interp_scope F A _ S) : HOM := exist _ ((interp_throwlk rs (λne env, idfun) α env)) _. Next Obligation. intros; simpl. @@ -78,7 +47,7 @@ Section hom. Qed. Program Definition ThrowRSCtx_HOM {S : Set} - (β : IT) (env : @interp_scope F natO _ S) + (β : IT) (env : @interp_scope F A _ S) (Hv : AsVal β) : HOM := exist _ (interp_throwrk rs (constO β) (λne env, idfun) env) _. Next Obligation. @@ -104,16 +73,16 @@ Section hom. Qed. Program Definition OutputSCtx_HOM {S : Set} - (env : @interp_scope F natO _ S) - : HOM := exist _ ((interp_outputk rs (λne env, idfun) env)) _. + (env : @interp_scope F A _ S) : HOM (A:=natO) + := exist _ ((interp_outputk rs (λne env, idfun) env)) _. Next Obligation. intros; simpl. apply _. Qed. Program Definition AppRSCtx_HOM {S : Set} - (α : @interp_scope F natO _ S -n> IT) - (env : @interp_scope F natO _ S) + (α : @interp_scope F A _ S -n> IT) + (env : @interp_scope F A _ S) : HOM := exist _ (interp_apprk rs α (λne env, idfun) env) _. Next Obligation. intros; simpl. @@ -121,7 +90,7 @@ Section hom. Qed. Program Definition AppLSCtx_HOM {S : Set} - (β : IT) (env : @interp_scope F natO _ S) + (β : IT) (env : @interp_scope F A _ S) (Hv : AsVal β) : HOM := exist _ (interp_applk rs (λne env, idfun) (constO β) env) _. Next Obligation. diff --git a/theories/gitree/weakestpre.v b/theories/gitree/weakestpre.v index e6e343f..494fd16 100644 --- a/theories/gitree/weakestpre.v +++ b/theories/gitree/weakestpre.v @@ -146,6 +146,32 @@ Section weakestpre. Definition has_substate {sR : sReifier a} `{!stateG Σ} `{!subReifier sR rs} (σ : sReifier_state sR ♯ IT) : iProp Σ := (own stateG_name (◯ (of_idx sR_idx (sR_state σ))))%I. + #[export] Instance has_substate_ne {sR : sReifier a} `{!stateG Σ} + `{!subReifier sR rs} : NonExpansive (has_substate). + Proof. + intros ????. + unfold has_substate. + do 2 f_equiv. + intros i. + unfold of_idx, weakestpre.of_idx. + destruct (decide (i = sR_idx)). + - subst; simpl. + now do 3 f_equiv. + - reflexivity. + Qed. + #[export] Instance has_substate_proper {sR : sReifier a} `{!stateG Σ} + `{!subReifier sR rs} : Proper ((≡) ==> (≡)) (has_substate). + Proof. + intros ???. + unfold has_substate. + do 2 f_equiv. + intros i. + unfold of_idx, weakestpre.of_idx. + destruct (decide (i = sR_idx)). + - subst; simpl. + now do 3 f_equiv. + - reflexivity. + Qed. #[export] Instance state_interp_ne `{!stateG Σ} : NonExpansive state_interp. Proof. solve_proper. Qed. diff --git a/theories/hom.v b/theories/hom.v new file mode 100644 index 0000000..178179b --- /dev/null +++ b/theories/hom.v @@ -0,0 +1,49 @@ +(** In this module, we package up IT homomorphism in a sigma type, and +we will use it as a domain for logical relations on continuations *) +From gitrees Require Import gitree lang_generic. +Require Import Binding.Lib Binding.Set Binding.Env. + +Open Scope stdpp_scope. + +Section hom. + Context {A : ofe}. + Context {CA : Cofe A}. + Context {F : opsInterp}. + Notation IT := (IT F A). + Notation ITV := (ITV F A). + + Definition HOM : ofe := @sigO (IT -n> IT) IT_hom. + + Global Instance HOM_hom (κ : HOM) : IT_hom (`κ). + Proof. + apply (proj2_sig κ). + Qed. + + Program Definition HOM_id : HOM := exist _ idfun _. + Next Obligation. + apply _. + Qed. + + Lemma HOM_ccompose (f g : HOM) : + ∀ α, `f (`g α) = (`f ◎ `g) α. + Proof. + intro; reflexivity. + Qed. + + Program Definition HOM_compose (f g : HOM) : HOM := exist _ (`f ◎ `g) _. + Next Obligation. + intros f g; simpl. + apply _. + Qed. + + Lemma HOM_compose_ccompose (f g h : HOM) : + h = HOM_compose f g -> + `f ◎ `g = `h. + Proof. intros ->. done. Qed. + + Program Definition IFSCtx_HOM `{!SubOfe natO A} α β : HOM := exist _ (λne x, IFSCtx α β x) _. + Next Obligation. + intros; simpl. + apply _. + Qed. +End hom.