Add Lam, Letin, and Seq in F_mu_ref_conc, add factorial example

_CoqProject

@@ -70,6 +70,7 @@ theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
 theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
 theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
 theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
+theories/logrel/F_mu_ref_conc/examples/fact.v
 
 theories/hocap/abstract_bag.v
 theories/hocap/cg_bag.v

theories/logrel/F_mu_ref_conc/examples/fact.v

+From iris.proofmode Require Import tactics.
+From iris_examples.logrel.F_mu_ref_conc Require Import
+     soundness_binary rules rules_binary.
+From iris.program_logic Require Import adequacy.
+
+Fixpoint mathfact n :=
+  match n with
+  | O => 1
+  | S m => n * (mathfact m)
+  end.
+
+Definition fact : expr :=
+  Rec (If (BinOp Eq (Var 1) (#n 0))
+          (#n 1)
+          (BinOp Mult (Var 1) (App (Var 0) (BinOp Sub (Var 1) (#n 1))))).
+
+Lemma fact_typed : [] ⊢ₜ fact : TArrow TNat TNat.
+Proof. repeat econstructor. Qed.
+
+Definition fact_acc_body : expr :=
+  Rec (Lam
+         (If (BinOp Eq (Var 2) (#n 0))
+             (Var 0)
+             (LetIn
+                (BinOp Mult (Var 2) (Var 0))
+                (LetIn
+                   (BinOp Sub (Var 3) (#n 1))
+                   (App (App (Var 3) (Var 0)) (Var 1))
+                )
+             )
+         )
+      ).
+
+Lemma fact_acc_body_typed : [] ⊢ₜ fact_acc_body : TArrow TNat (TArrow TNat TNat).
+Proof. repeat econstructor. Qed.
+
+Lemma fact_acc_body_subst f : fact_acc_body.[f] = fact_acc_body.
+Proof. by asimpl. Qed.
+
+Hint Rewrite fact_acc_body_subst : autosubst.
+
+Lemma fact_acc_body_unfold :
+  fact_acc_body =
+  Rec (Lam
+         (If (BinOp Eq (Var 2) (#n 0))
+             (Var 0)
+             (LetIn
+                (BinOp Mult (Var 2) (Var 0))
+                (LetIn
+                   (BinOp Sub (Var 3) (#n 1))
+                   (App (App (Var 3) (Var 0)) (Var 1))
+                )
+             )
+         )
+      ).
+Proof. trivial. Qed.
+
+Global Typeclasses Opaque fact_acc_body.
+Global Opaque fact_acc_body.
+
+Definition fact_acc : expr :=
+  Lam (App (App fact_acc_body (Var 0)) (#n 1)).
+
+Lemma fact_acc_typed : [] ⊢ₜ fact_acc : TArrow TNat TNat.
+Proof.
+  repeat econstructor.
+  apply (closed_context_weakening [_] []); eauto.
+  apply fact_acc_body_typed.
+Qed.
+
+Section fact_equiv.
+  Context `{heapIG Σ, cfgSG Σ}.
+
+  Lemma fact_fact_acc_refinement :
+    [] ⊨ fact ≤log≤ fact_acc : (TArrow TNat TNat).
+  Proof.
+    iIntros (? vs ρ _) "[#HE HΔ]".
+    iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
+    rewrite !empty_env_subst.
+    iClear "HΔ". simpl.
+    iIntros (j K) "Hj"; simpl.
+    iApply wp_value; iExists (LamV _); iFrame.
+    rewrite /= -/fact.
+    iAlways. iIntros ([? ?] [n [? ?]]); simpl in *; simplify_eq; simpl.
+    clear j K.
+    iIntros (j K) "Hj"; simpl.
+    iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+    asimpl.
+    iApply (wp_mono _ _ _ (λ v, j ⤇ fill K (#n (mathfact n)) ∗ ⌜v = #nv (mathfact n)⌝))%I.
+    { iIntros (?) "[? %]"; iExists (#nv _); iFrame; eauto. }
+    replace (fill K (#n mathfact n)) with (fill K (#n (1 * mathfact n)))
+      by by repeat f_equal; lia.
+    generalize 1 as l => l.
+    iInduction n as [|n] "IH" forall (l).
+    - iApply wp_pure_step_later; auto.
+      iNext; simpl; asimpl.
+      rewrite fact_acc_body_unfold.
+      iMod (do_step_pure _ _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+      rewrite -fact_acc_body_unfold.
+      simpl; asimpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      iApply (wp_bind (fill [IfCtx _ _])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iApply wp_value. simpl.
+      iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      iApply wp_value.
+      replace (l * 1) with l by lia.
+      auto.
+    - iApply wp_pure_step_later; auto.
+      iNext; simpl; asimpl.
+      rewrite fact_acc_body_unfold.
+      iMod (do_step_pure _ _ _ (AppLCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+      rewrite -fact_acc_body_unfold.
+      simpl; asimpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      iApply (wp_bind (fill [IfCtx _ _])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iApply wp_value. simpl.
+      iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      asimpl.
+      iApply (wp_bind (fill [BinOpRCtx _ (#nv _)])).
+      iApply (wp_bind (fill [AppRCtx (RecV _)])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl; iApply wp_value; simpl.
+      iMod (do_step_pure _ _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      asimpl.
+      iMod (do_step_pure _ _ _ (LetInCtx _ :: _) with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      asimpl.
+      replace (n -0) with n by lia.
+      iApply wp_wand_r; iSplitL; first iApply ("IH" with "[Hj]"); eauto.
+      iIntros (v) "[H %]"; simplify_eq.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl; iApply wp_value.
+      replace (l * (mathfact n + n * mathfact n)) with ((l + n * l) * mathfact n)
+        by lia.
+      iFrame; auto.
+  Qed.
+
+  Lemma fact_acc_fact_refinement :
+    [] ⊨ fact_acc ≤log≤ fact : (TArrow TNat TNat).
+  Proof.
+    iIntros (? vs ρ _) "[#HE HΔ]".
+    iDestruct (interp_env_length with "HΔ") as %?; destruct vs; simplify_eq.
+    rewrite !empty_env_subst.
+    iClear "HΔ". simpl.
+    iIntros (j K) "Hj"; simpl.
+    iApply wp_value; iExists (RecV _); iFrame.
+    iAlways. iIntros ([? ?] [n [? ?]]); simpl in *; simplify_eq; simpl.
+    clear j K.
+    iIntros (j K) "Hj"; simpl.
+    iApply wp_pure_step_later; auto.
+    iNext; asimpl.
+    rewrite -/fact.
+    iApply (wp_mono _ _ _ (λ v, j ⤇ fill K (#n (mathfact n)) ∗ ⌜v = #nv (1 * mathfact n)⌝))%I.
+    { replace (1 * mathfact n) with (mathfact n) by lia.
+      iIntros (?) "[? %]"; iExists (#nv _); iFrame; eauto. }
+    generalize 1 as l => l.
+    iInduction n as [|n] "IH" forall (K l).
+    - rewrite fact_acc_body_unfold.
+      iApply (wp_bind (fill [AppLCtx _])).
+      iApply wp_pure_step_later; auto.
+      rewrite -fact_acc_body_unfold.
+      iNext; simpl; asimpl.
+      iApply wp_value; simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl; asimpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      simpl; asimpl.
+      iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+      iApply (wp_bind (fill [IfCtx _ _])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iApply wp_value. simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iApply wp_value.
+      replace (l * 1) with l by lia; auto.
+    - rewrite {2}fact_acc_body_unfold.
+      iApply (wp_bind (fill [AppLCtx _])).
+      iApply wp_pure_step_later; auto.
+      rewrite -fact_acc_body_unfold.
+      iNext; simpl; asimpl.
+      iApply wp_value; simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl; asimpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iApply (wp_bind (fill [IfCtx _ _])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iApply wp_value. simpl.
+      iMod (do_step_pure _ _ _ (IfCtx _ _ :: _) with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      iMod (do_step_pure _ _ _ (AppRCtx (RecV _):: BinOpRCtx _ (#nv _) :: _)
+              with "[$Hj]") as "Hj"; eauto.
+      simpl.
+      iApply (wp_bind (fill [LetInCtx _])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl; iApply wp_value; simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl. asimpl.
+      iApply (wp_bind (fill [LetInCtx _])).
+      iApply wp_pure_step_later; auto.
+      iNext; simpl; iApply wp_value; simpl.
+      iApply wp_pure_step_later; auto.
+      iNext; simpl. asimpl.
+      replace (n -0) with n by lia.
+      iApply wp_fupd.
+      iApply wp_wand_r; iSplitL;
+        first iApply ("IH" $! (BinOpRCtx _ (#nv _) :: K) with "[$Hj]"); eauto.
+      iIntros (v) "[Hj %]"; simplify_eq.
+      simpl.
+      iMod (do_step_pure with "[$Hj]") as "Hj"; auto.
+      simpl.
+      iModIntro. iFrame.
+      eauto with lia.
+  Qed.
+
+End fact_equiv.
+
+Theorem fact_ctx_equiv :
+  [] ⊨ fact ≤ctx≤ fact_acc : (TArrow TNat TNat) ∧
+  [] ⊨ fact_acc ≤ctx≤ fact : (TArrow TNat TNat).
+Proof.
+  set (Σ := #[invΣ ; gen_heapΣ loc val ; GFunctor (auth.authR cfgUR)]).
+  set (HG := soundness_unary.HeapPreIG Σ _ _).
+  split.
+  - eapply (binary_soundness Σ _); auto using fact_acc_typed, fact_typed.
+    intros; apply fact_fact_acc_refinement.
+  -  eapply (binary_soundness Σ _); auto using fact_acc_typed, fact_typed.
+    intros; apply fact_acc_fact_refinement.
+Qed.

theories/logrel/F_mu_ref_conc/fundamental_binary.v

@@ -220,6 +220,60 @@ Section fundamental.
     rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto.
   Qed.
 
+  Lemma bin_log_related_lam Γ (e e' : expr) τ1 τ2
+      (Hclosed : ∀ f, e.[upn (S (length Γ)) f] = e)
+      (Hclosed' : ∀ f, e'.[upn (S (length Γ)) f] = e')
+      (IHHtyped : τ1 :: Γ ⊨ e ≤log≤ e' : τ2) :
+    Γ ⊨ Lam e ≤log≤ Lam e' : TArrow τ1 τ2.
+  Proof.
+    iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iApply wp_value. iExists (LamV _). iIntros "{$Hj} !#".
+    iIntros ([v v']) "#Hiv". iIntros (j' K') "Hj".
+    iDestruct (interp_env_length with "HΓ") as %?.
+    iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
+    iApply fupd_wp.
+    iMod (step_lam _ _ j' K' _ (of_val v') v' with "* [-]") as "Hz"; eauto.
+    asimpl. iFrame "#". change (Lam ?e) with (of_val (LamV e)).
+    erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
+    iApply ('`IHHtyped _  ((v,v') :: vvs)); repeat iSplit; eauto.
+    iModIntro.
+    rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto.
+  Qed.
+
+  Lemma bin_log_related_letin Γ (e1 e2 e1' e2' : expr) τ1 τ2
+      (Hclosed2 : ∀ f, e2.[upn (S (length Γ)) f] = e2)
+      (Hclosed2' : ∀ f, e2'.[upn (S (length Γ)) f] = e2')
+      (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : τ1)
+      (IHHtyped2 : τ1 :: Γ ⊨ e2 ≤log≤ e2' : τ2) :
+    Γ ⊨ LetIn e1 e2 ≤log≤ LetIn e1' e2': τ2.
+  Proof.
+    iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iDestruct (interp_env_length with "HΓ") as %?.
+    smart_wp_bind (LetInCtx _) v v' "[Hv #Hiv]"
+      ('`IHHtyped1 _ _ _ j ((LetInCtx _) :: K)); cbn.
+    iMod (step_letin _ _ j K with "[-]") as "Hz"; eauto.
+    iApply wp_pure_step_later; auto. iModIntro.
+    asimpl.
+    erewrite !n_closed_subst_head_simpl by (rewrite ?fmap_length; eauto).
+    iApply ('`IHHtyped2 _ ((v, v') :: vvs)); repeat iSplit; eauto.
+    rewrite !interp_env_cons; iSplit; try iApply interp_env_cons; auto.
+  Qed.
+
+  Lemma bin_log_related_seq Γ (e1 e2 e1' e2' : expr) τ1 τ2
+      (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : τ1)
+      (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ2) :
+    Γ ⊨ Seq e1 e2 ≤log≤ Seq e1' e2': τ2.
+  Proof.
+    iIntros (Δ vvs ρ ?) "#(Hs & HΓ)"; iIntros (j K) "Hj /=".
+    iDestruct (interp_env_length with "HΓ") as %?.
+    smart_wp_bind (SeqCtx _) v v' "[Hv #Hiv]"
+      ('`IHHtyped1 _ _ _ j ((SeqCtx _) :: K)); cbn.
+    iMod (step_seq _ _ j K with "[-]") as "Hz"; eauto.
+    iApply wp_pure_step_later; auto. iModIntro.
+    asimpl.
+    iApply '`IHHtyped2; repeat iSplit; eauto.
+  Qed.
+
   Lemma bin_log_related_app Γ e1 e2 e1' e2' τ1 τ2
       (IHHtyped1 : Γ ⊨ e1 ≤log≤ e1' : TArrow τ1 τ2)
       (IHHtyped2 : Γ ⊨ e2 ≤log≤ e2' : τ1) :
@@ -429,6 +483,11 @@ Section fundamental.
     - eapply bin_log_related_if; eauto.
     - eapply bin_log_related_rec; eauto;
         match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
+    - eapply bin_log_related_lam; eauto;
+        match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
+    - eapply bin_log_related_letin; eauto;
+        match goal with H : _ |- _ => eapply (typed_n_closed _ _ _ H) end.
+    - eapply bin_log_related_seq; eauto.
     - eapply bin_log_related_app; eauto.
     - eapply bin_log_related_tlam; eauto with typeclass_instances.
     - eapply bin_log_related_tapp; eauto.

theories/logrel/F_mu_ref_conc/fundamental_unary.v

@@ -75,6 +75,25 @@ Section typed_interp.
       erewrite typed_subst_head_simpl_2 by naive_solver.
       iApply (IHtyped Δ (_ :: w :: vs)).
       iApply interp_env_cons; iSplit; [|iApply interp_env_cons]; auto.
+    - (* Lam *)
+      iApply wp_value. simpl. iAlways. iIntros (w) "#Hw".
+      iDestruct (interp_env_length with "HΓ") as %?.
+      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
+      asimpl.
+      erewrite typed_subst_head_simpl by naive_solver.
+      iApply (IHtyped Δ (w :: vs)); auto.
+      iApply interp_env_cons; iSplit; auto.
+    - (* LetIn *)
+      smart_wp_bind (LetInCtx _) v "#Hv" IHtyped1; cbn.
+      iDestruct (interp_env_length with "HΓ") as %?.
+      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
+      asimpl. erewrite typed_subst_head_simpl by naive_solver.
+      iApply (IHtyped2 Δ (v :: vs)).
+      iApply interp_env_cons; iSplit; eauto.
+    - (* Seq *)
+      smart_wp_bind (SeqCtx _) v "#Hv" IHtyped1; cbn.
+      iApply wp_pure_step_later; auto 1 using to_of_val. iNext.
+      by iApply IHtyped2.
     - (* app *)
       smart_wp_bind (AppLCtx (e2.[env_subst vs])) v "#Hv" IHtyped1.
       smart_wp_bind (AppRCtx v) w "#Hw" IHtyped2.
@@ -124,7 +143,7 @@ Section typed_interp.
       iDestruct "Hv" as (l) "[% #Hv]"; subst.
       iApply wp_atomic.
       iInv (logN .@ l) as (z) "[Hz1 #Hz2]" "Hclose".
-      iApply (wp_store with "Hz1"); auto using to_of_val. 
+      iApply (wp_store with "Hz1"); auto using to_of_val.
       iModIntro. iNext.
       iIntros "Hz1". iMod ("Hclose" with "[Hz1 Hz2]"); eauto.
     - (* CAS *)

theories/logrel/F_mu_ref_conc/lang.v

@@ -8,7 +8,7 @@ Module F_mu_ref_conc.
 
   Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.
 
-  Inductive binop := Add | Sub | Eq | Le | Lt.
+  Inductive binop := Add | Sub | Mult | Eq | Le | Lt.
 
   Instance binop_dec_eq (op op' : binop) : Decision (op = op').
   Proof. solve_decision. Defined.
@@ -17,6 +17,9 @@ Module F_mu_ref_conc.
   | Var (x : var)
   | Rec (e : {bind 2 of expr})
   | App (e1 e2 : expr)
+  | Lam (e : {bind expr})
+  | LetIn (e1 : expr) (e2 : {bind expr})
+  | Seq (e1 e2 : expr)
   (* Base Types *)
   | Unit
   | Nat (n : nat)
@@ -62,6 +65,7 @@ Module F_mu_ref_conc.
 
   Inductive val :=
   | RecV (e : {bind 1 of expr})
+  | LamV (e : {bind expr})
   | TLamV (e : {bind 1 of expr})
   | UnitV
   | NatV (n : nat)
@@ -80,6 +84,7 @@ Module F_mu_ref_conc.
     match op with
     | Add => λ a b, #nv(a + b)
     | Sub => λ a b, #nv(a - b)
+    | Mult => λ a b, #nv(a * b)
     | Eq => λ a b, if (eq_nat_dec a b) then #♭v true else #♭v false
     | Le => λ a b, if (le_dec a b) then #♭v true else #♭v false
     | Lt => λ a b, if (lt_dec a b) then #♭v true else #♭v false
@@ -93,6 +98,7 @@ Module F_mu_ref_conc.
   Fixpoint of_val (v : val) : expr :=
     match v with
     | RecV e => Rec e
+    | LamV e => Lam e
     | TLamV e => TLam e
     | UnitV => Unit
     | NatV v => Nat v
@@ -107,6 +113,7 @@ Module F_mu_ref_conc.
   Fixpoint to_val (e : expr) : option val :=
     match e with
     | Rec e => Some (RecV e)
+    | Lam e => Some (LamV e)
     | TLam e => Some (TLamV e)
     | Unit => Some UnitV
     | Nat n => Some (NatV n)
@@ -123,6 +130,8 @@ Module F_mu_ref_conc.
   Inductive ectx_item :=
   | AppLCtx (e2 : expr)
   | AppRCtx (v1 : val)
+  | LetInCtx (e2 : expr)
+  | SeqCtx (e2 : expr)
   | TAppCtx
   | PairLCtx (e2 : expr)
   | PairRCtx (v1 : val)
@@ -148,6 +157,8 @@ Module F_mu_ref_conc.
     match Ki with
     | AppLCtx e2 => App e e2
     | AppRCtx v1 => App (of_val v1) e
+    | LetInCtx e2 => LetIn e e2
+    | SeqCtx e2 => Seq e e2
     | TAppCtx => TApp e
     | PairLCtx e2 => Pair e e2
     | PairRCtx v1 => Pair (of_val v1) e
@@ -177,6 +188,18 @@ Module F_mu_ref_conc.
   | BetaS e1 e2 v2 σ :
       to_val e2 = Some v2 →
       head_step (App (Rec e1) e2) σ [] e1.[(Rec e1), e2/] σ []
+  (* Lam-β *)
+  | LamBetaS e1 e2 v2 σ :
+      to_val e2 = Some v2 →
+      head_step (App (Lam e1) e2) σ [] e1.[e2/] σ []
+  (* LetIn-β *)
+  | LetInBetaS e1 e2 v2 σ :
+      to_val e1 = Some v2 →
+      head_step (LetIn e1 e2) σ [] e2.[e1/] σ []
+  (* Seq-β *)
+  | SeqBetaS e1 e2 v2 σ :
+      to_val e1 = Some v2 →
+      head_step (Seq e1 e2) σ [] e2 σ []
   (* Products *)
   | FstS e1 v1 e2 v2 σ :
       to_val e1 = Some v1 → to_val e2 = Some v2 →

theories/logrel/F_mu_ref_conc/rules.v

@@ -133,6 +133,18 @@ Section lang_rules.
     PureExec True 1 (App (Rec e1) e2) e1.[(Rec e1), e2 /].
   Proof. solve_pure_exec. Qed.
 
+  Global Instance pure_lam e1 e2 `{!AsVal e2} :
+    PureExec True 1 (App (Lam e1) e2) e1.[e2 /].
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_LetIn e1 e2 `{!AsVal e1} :
+    PureExec True 1 (LetIn e1 e2) e2.[e1 /].
+  Proof. solve_pure_exec. Qed.
+
+  Global Instance pure_seq e1 e2 `{!AsVal e1} :
+    PureExec True 1 (Seq e1 e2) e2.
+  Proof. solve_pure_exec. Qed.
+
   Global Instance pure_tlam e : PureExec True 1 (TApp (TLam e)) e.
   Proof. solve_pure_exec. Qed.
 

theories/logrel/F_mu_ref_conc/rules_binary.v

+From iris.program_logic Require Export language ectx_language ectxi_language.
 From iris.program_logic Require Import lifting.
 From iris.algebra Require Import auth frac agree gmap list.
 From iris_examples.logrel.F_mu_ref_conc Require Export rules.
@@ -151,23 +152,67 @@ Section cfg.
     erased_step (tp, σ) (<[j:=fill K e']> tp, σ').
   Proof. rewrite -(right_id_L [] (++) (<[_:=_]>_)). by apply step_insert. Qed.
 
-  Lemma step_pure E ρ j K e e' :
-    (∀ σ, head_step e σ [] e' σ []) →
+  Lemma nsteps_inv_r {A} n (R : A → A → Prop) x y :
+    nsteps R (S n) x y → ∃ z, nsteps R n x z ∧ R z y.
+  Proof.
+    revert x y; induction n; intros x y.
+    - inversion 1; subst.
+      match goal with H : nsteps _ 0 _ _ |- _ => inversion H end; subst.
+      eexists; repeat econstructor; eauto.
+    - inversion 1; subst.
+      edestruct IHn as [z [? ?]]; eauto.
+      exists z; split; eauto using nsteps_l.
+  Qed.
+
+  Lemma step_pure' E ρ j K e e' (P : Prop) n :
+    P →
+    PureExec P n e e' →
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
   Proof.
-    iIntros (??) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
-    iInv specN as (tp σ) ">[Hown %]" "Hclose".
+    iIntros (HP Hex ?) "[#Hspec Hj]". rewrite /spec_ctx /tpool_mapsto.
+    iInv specN as (tp σ) ">[Hown Hrtc]" "Hclose".
+    iDestruct "Hrtc" as %Hrtc.
     iDestruct (own_valid_2 with "Hown Hj")
-      as %[[?%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
+      as %[[Htpj%tpool_singleton_included' _]%prod_included ?]%auth_valid_discrete_2.
     iMod (own_update_2 with "Hown Hj") as "[Hown Hj]".
     { by eapply auth_update, prod_local_update_1,
         singleton_local_update, (exclusive_local_update _ (Excl (fill K e'))). }
     iFrame "Hj". iApply "Hclose". iNext. iExists (<[j:=fill K e']> tp), σ.
     rewrite to_tpool_insert'; last eauto.
-    iFrame. iPureIntro. eapply rtc_r, step_insert_no_fork; eauto.
+    iFrame. iPureIntro.
+    apply rtc_nsteps in Hrtc; destruct Hrtc as [m Hrtc].
+    specialize (Hex HP). apply (nsteps_rtc (m + n)).
+    eapply nsteps_trans; eauto.
+    revert e e' Htpj Hex.
+    induction n => e e' Htpj Hex.
+    - inversion Hex; subst.
+      rewrite list_insert_id; eauto. econstructor.
+    - apply nsteps_inv_r in Hex.
+      destruct Hex as [z [Hex1 Hex2]].
+      specialize (IHn _ _ Htpj Hex1).
+      eapply nsteps_r; eauto.
+      replace (<[j:=fill K e']> tp) with
+          (<[j:=fill K e']> (<[j:=fill K z]> tp)); last first.
+      { clear. revert tp; induction j; intros tp.
+        - destruct tp; trivial.
+        - destruct tp; simpl; auto. by rewrite IHj. }
+      destruct Hex2 as [Hexs Hexd].
+      specialize (Hexs σ). destruct Hexs as [e'' [σ' [efs Hexs]]].
+      specialize (Hexd σ [] e'' σ' efs Hexs); destruct Hexd as [? [? [? ?]]];
+        subst.
+      inversion Hexs; simpl in *; subst.
+      rewrite -!fill_app.
+      eapply step_insert_no_fork; eauto.
+      { apply list_lookup_insert. apply lookup_lt_is_Some; eauto. }
   Qed.
 
+
+  Lemma do_step_pure E ρ j K e e' `{!PureExec True 1 e e'}:
+    nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K e ={E}=∗ j ⤇ fill K e'.
+  Proof. by eapply step_pure'; last eauto. Qed.
+
   Lemma step_alloc E ρ j K e v:
     to_val e = Some v → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Alloc e) ={E}=∗ ∃ l, j ⤇ fill K (Loc l) ∗ l ↦ₛ v.
@@ -285,55 +330,73 @@ Section cfg.
     to_val e2 = Some v → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (App (Rec e1) e2)
     ={E}=∗ j ⤇ fill K (e1.[Rec e1,e2/]).
-  Proof. intros ?; apply step_pure => σ; econstructor; eauto. Qed.
+  Proof. by intros ?; apply: do_step_pure. Qed.
+
+  Lemma step_lam E ρ j K e1 e2 v :
+    to_val e2 = Some v → nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K (App (Lam e1) e2)
+    ={E}=∗ j ⤇ fill K (e1.[e2/]).
+  Proof. by intros ?; apply: do_step_pure. Qed.
+
+  Lemma step_letin E ρ j K e1 e2 v :
+    to_val e1 = Some v → nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K (LetIn e1 e2)
+    ={E}=∗ j ⤇ fill K (e2.[e1/]).
+  Proof. by intros ?; apply: do_step_pure. Qed.
+
+  Lemma step_seq E ρ j K e1 e2 v :
+    to_val e1 = Some v → nclose specN ⊆ E →
+    spec_ctx ρ ∗ j ⤇ fill K (Seq e1 e2)
+    ={E}=∗ j ⤇ fill K e2.
+  Proof. by intros ?; apply: do_step_pure. Qed.
 
   Lemma step_tlam E ρ j K e :
     nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (TApp (TLam e)) ={E}=∗ j ⤇ fill K e.
-  Proof. apply step_pure => σ; econstructor; eauto. Qed.
+  Proof. by intros ?; apply: do_step_pure. Qed.
 
   Lemma step_Fold E ρ j K e v :
     to_val e = Some v → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Unfold (Fold e)) ={E}=∗ j ⤇ fill K e.
-  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.
+  Proof. by intros ?; apply: do_step_pure. Qed.
 
   Lemma step_fst E ρ j K e1 v1 e2 v2 :
     to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Fst (Pair e1 e2)) ={E}=∗ j ⤇ fill K e1.
-  Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.
+  Proof. by intros; apply: do_step_pure. Qed.
 
   Lemma step_snd E ρ j K e1 v1 e2 v2 :
     to_val e1 = Some v1 → to_val e2 = Some v2 → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Snd (Pair e1 e2)) ={E}=∗ j ⤇ fill K e2.
-  Proof. intros H1 H2; apply step_pure => σ; econstructor; eauto. Qed.
+  Proof. by intros; apply: do_step_pure. Qed.
 
   Lemma step_case_inl E ρ j K e0 v0 e1 e2 :
     to_val e0 = Some v0 → nclose specN ⊆ E →
     spec_ctx ρ ∗ j ⤇ fill K (Case (InjL e0) e1 e2)
       ={E}=∗ j ⤇ fill K (e1.[e0/]).
-  Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.