Add types Nat and Bool to Fμ,ref,par

9f324536 · Amin Timany · 16093667 · 9f324536 · 9f324536 · 9f324536
Commit 9f324536 authored May 24, 2016 by Amin Timany
9 changed files
--- a/F_mu_ref_par/fundamental_binary.v
+++ b/F_mu_ref_par/fundamental_binary.v
@@ -184,6 +184,48 @@ Section typed_interp.
      Unshelve. all: eauto using to_of_val.
  Qed.

+  Lemma typed_binary_interp_If Δ Γ e0 e1 e2 e0' e1' e2' τ {HΔ : ✓✓ Δ}
+        (IHHtyped1 : Δ ∥ Γ ⊩ e0 ≤log≤ e0' ∷ TBool)
+        (IHHtyped2 : Δ ∥ Γ ⊩ e1 ≤log≤ e1' ∷ τ)
+        (IHHtyped3 : Δ ∥ Γ ⊩ e2 ≤log≤ e2' ∷ τ)
+    :
+      Δ ∥ Γ ⊩ If e0 e1 e2 ≤log≤ If e0' e1' e2' ∷ τ.
+  Proof.
+    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
+    smart_wp_bind (IfCtx _ _) v v' "[Hv #Hiv]"
+                  (IHHtyped1 _ _ _ j (K ++ [IfCtx _ _])); cbn.
+    iDestruct "Hiv" as {b} "[% %]"; subst; destruct b; simpl.
+    + iPvs (step_if_true _ _ _ j K _ _ _ with "* -") as "Hz".
+      iFrame "Hspec Hv"; trivial. iApply wp_if_true. iNext.
+      iApply IHHtyped2; trivial. iFrame "Hheap Hspec HΓ"; trivial.
+    + iPvs (step_if_false _ _ _ j K _ _ _ with "* -") as "Hz".
+      iFrame "Hspec Hv"; trivial. iApply wp_if_false. iNext.
+      iApply IHHtyped3; trivial. iFrame "Hheap Hspec HΓ"; trivial.
+      (* unshelving *)
+      Unshelve. all: eauto using to_of_val.
+  Qed.
+
+  Lemma typed_binary_interp_nat_bin_op Δ Γ op e1 e2 e1' e2' {HΔ : ✓✓ Δ}
+        (IHHtyped1 : Δ ∥ Γ ⊩ e1 ≤log≤ e1' ∷ TNat)
+        (IHHtyped2 : Δ ∥ Γ ⊩ e2 ≤log≤ e2' ∷ TNat)
+    :
+      Δ ∥ Γ ⊩ NBOP op e1 e2 ≤log≤ NBOP op e1' e2' ∷ (NatBinOP_res_type op).
+  Proof.
+    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
+    smart_wp_bind (NBOPLCtx _ _) v v' "[Hv #Hiv]"
+                  (IHHtyped1 _ _ _ j (K ++ [NBOPLCtx _ _])); cbn.
+    smart_wp_bind (NBOPRCtx _ _) w w' "[Hw #Hiw]"
+                  (IHHtyped2 _ _ _ j (K ++ [NBOPRCtx _ _])); cbn.
+    iDestruct "Hiv" as {n} "[% %]"; subst; simpl.
+    iDestruct "Hiw" as {n'} "[% %]"; subst; simpl.
+    iPvs (step_nat_bin_op _ _ _ j K _ _ _ _ with "* -") as "Hz".
+    iFrame "Hspec Hw"; trivial. iApply wp_nat_bin_op. iNext.
+    iExists _; iSplitL; eauto.
+    destruct op; simpl; try destruct eq_nat_dec; try destruct le_dec;
+      try destruct lt_dec; iExists _; iSplit; trivial.
+    (* unshelving *)
+    Unshelve. all: eauto using to_of_val.
+  Qed.

  Lemma typed_binary_interp_Lam Δ Γ e e' τ1 τ2 {HΔ : ✓✓ Δ}
        (Htyped : typed (TArrow τ1 τ2 :: τ1 :: Γ) e τ2)
@@ -444,7 +486,7 @@ Section typed_interp.
        (IHHtyped2 : Δ ∥ Γ ⊩ e2 ≤log≤ e2' ∷ τ)
        (IHHtyped3 : Δ ∥ Γ ⊩ e3 ≤log≤ e3' ∷ τ)
    :
-      Δ ∥ Γ ⊩ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' ∷ TBOOL.
+      Δ ∥ Γ ⊩ CAS e1 e2 e3 ≤log≤ CAS e1' e2' e3' ∷ TBool.
  Proof.
    intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
    smart_wp_bind (CasLCtx _ _) v v' "[Hv #Hiv]"
@@ -475,8 +517,7 @@ Section typed_interp.
      iNext. iIntros "Hw1".
      iSplitL "Hw1 Hw2".
      * iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
-      * iPvsIntro. iExists TRUEV; iFrame "Hw".
-        iLeft; iExists (UnitV, UnitV); repeat iSplit; trivial.
+      * iPvsIntro. iExists (♭v true); iFrame "Hw". iExists _; iSplit; trivial.
    + iPvs (step_cas_fail _ _ _ j K (l.2) 1 (z2) (# w') w' (# u') u' _ _ _
            with "[Hu Hw2]") as "[Hw Hw2]"; simpl.
      { iFrame "Hspec Hu Hw2". iNext.
@@ -489,15 +530,13 @@ Section typed_interp.
      iNext. iIntros "Hw1".
      iSplitL "Hw1 Hw2".
      * iNext; iExists (_, _); iFrame "Hw1 Hw2"; trivial.
-      * iPvsIntro. iExists FALSEV; iFrame "Hw".
-        iRight; iExists (UnitV, UnitV); repeat iSplit; trivial.
+      * iPvsIntro. iExists (♭v false); iFrame "Hw". iExists _; iSplit; trivial.
        (* unshelving *)
        Unshelve. all: eauto using to_of_val. all: SolveDisj 3 l.
  Qed.

  Lemma typed_binary_interp Δ Γ e τ {HΔ : context_interp_Persistent Δ}
-        (Htyped : typed Γ e τ)
-    : Δ ∥ Γ ⊩ e ≤log≤ e ∷ τ.
+        (Htyped : typed Γ e τ) : Δ ∥ Γ ⊩ e ≤log≤ e ∷ τ.
  Proof.
    revert Δ HΔ; induction Htyped; intros Δ HΔ.
    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
@@ -511,12 +550,18 @@ Section typed_interp.
      rewrite lookup_zip_with; simplify_option_eq; destruct v; trivial.
    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
      value_case. iExists UnitV; iFrame "Htr"; iSplit; trivial.
+    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
+      value_case. iExists (♯v _); iFrame "Htr"; iExists _; iSplit; trivial.
+    - intros vs Hlen ρ j K. iIntros "[#Hheap [#Hspec [#HΓ Htr]]]"; cbn.
+      value_case. iExists (♭v _); iFrame "Htr"; iExists _; iSplit; trivial.
+    - apply typed_binary_interp_nat_bin_op; trivial.
    - apply typed_binary_interp_Pair; trivial.
    - eapply typed_binary_interp_Fst; trivial.
    - eapply typed_binary_interp_Snd; trivial.
    - eapply typed_binary_interp_InjL; trivial.
    - eapply typed_binary_interp_InjR; trivial.
    - eapply typed_binary_interp_Case; eauto.
+    - eapply typed_binary_interp_If; eauto.
    - eapply typed_binary_interp_Lam; eauto.
    - eapply typed_binary_interp_App; trivial.
    - eapply typed_binary_interp_TLam; trivial.

--- a/F_mu_ref_par/fundamental_unary.v
+++ b/F_mu_ref_par/fundamental_unary.v
@@ -74,6 +74,15 @@ Section typed_interp.
      apply elem_of_list_lookup_2 with x.
      rewrite lookup_zip_with; simplify_option_eq; trivial.
    - (* unit *) value_case; trivial.
+    - (* nat *) value_case; iExists _ ; trivial.
+    - (* bool *) value_case; iExists _ ; trivial.
+    - (* nat bin op *)
+      smart_wp_bind (NBOPLCtx _ e2.[env_subst vs]) v "#Hv" IHHtyped1.
+      smart_wp_bind (NBOPRCtx _ v) v' "# Hv'" IHHtyped2.
+      iDestruct "Hv" as {n} "%"; iDestruct "Hv'" as {n'} "%"; subst. simpl.
+      iApply wp_nat_bin_op. iNext; destruct op; simpl;
+      try destruct eq_nat_dec; try destruct le_dec; try destruct lt_dec;
+        eauto 10 with itauto.
    - (* pair *)
      smart_wp_bind (PairLCtx e2.[env_subst vs]) v "#Hv" IHHtyped1.
      smart_wp_bind (PairRCtx v) v' "# Hv'" IHHtyped2.
@@ -105,6 +114,11 @@ Section typed_interp.
         specialize (IHHtyped3 Δ HΔ (w::vs))];
        erewrite <- ?typed_subst_head_simpl in * by (cbn; eauto); iNext;
          [iApply IHHtyped2 | iApply IHHtyped3]; cbn; auto with itauto.
+    - (* If *)
+      smart_wp_bind (IfCtx _ _) v "#Hv" IHHtyped1; cbn.
+      iDestruct "Hv" as {b} "%"; subst; destruct b; simpl;
+        [iApply wp_if_true| iApply wp_if_false]; iNext;
+      [iApply IHHtyped2| iApply IHHtyped3]; auto with itauto.
    - (* lam *)
      value_case. iApply löb. rewrite -always_later.
      iIntros "#Hlat". iAlways. iIntros {w} "#Hw".
@@ -223,7 +237,7 @@ Section typed_interp.
        iNext. iIntros "Hw1".
        iSplitL.
        * iNext; iExists _; iSplitL; trivial.
-        * iPvsIntro. iLeft; iExists _; auto with itauto.
+        * iPvsIntro. iExists _; auto with itauto.
      + iApply (wp_cas_fail N); eauto using to_of_val.
        clear Hneq. specialize (HNLdisj l); set_solver_ndisj.
        (* Weird that Hneq above makes set_solver_ndisj diverge or
@@ -232,7 +246,7 @@ Section typed_interp.
        iNext. iIntros "Hw1".
        iSplitL.
        * iNext; iExists _; iSplitL; trivial.
-        * iPvsIntro. iRight; iExists _; auto with itauto.
+        * iPvsIntro. iExists _; auto with itauto.
      (* unshelving *)
      Unshelve.
      cbn; typeclasses eauto.

--- a/F_mu_ref_par/lang.v
+++ b/F_mu_ref_par/lang.v
@@ -8,12 +8,27 @@ Module lang.

  Global Instance loc_dec_eq (l l' : loc) : Decision (l = l') := _.

+  Inductive NatBinOP :=
+  | Add
+  | Sub
+  | Eq
+  | Le
+  | Lt.
+
+  Global Instance Natbinop_dec_eq (op op' : NatBinOP) : Decision (op = op').
+  Proof. unfold Decision. decide equality. Qed.
+
  Inductive expr :=
  | Var (x : var)
  | Lam (e : {bind 2 of expr})
  | App (e1 e2 : expr)
-  (* Unit *)
+  (* Base Types *)
  | Unit
+  | Nat (n : nat)
+  | Bool (b : bool)
+  | NBOP (op : NatBinOP) (e1 e2 : expr)
+  (* If then else *)
+  | If (e0 e1 e2 : expr)
  (* Products *)
  | Pair (e1 e2 : expr)
  | Fst (e : expr)
@@ -43,26 +58,47 @@ Module lang.
  Instance Subst_expr : Subst expr. derive. Defined.
  Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.

+  (* Notation for bool and nat *)
+  Notation "♭ b" := (Bool b) (at level 200).
+  Notation "♯ n" := (Nat n) (at level 200).

  Global Instance expr_dec_eq (e e' : expr) : Decision (e = e').
  Proof.
-    unfold Decision.
-    decide equality; [apply eq_nat_dec | apply loc_dec_eq].
+    unfold Decision; decide equality;
+      solve [apply eq_nat_dec | apply loc_dec_eq |
+             apply bool_eq_dec | apply Natbinop_dec_eq].
  Defined.

  Inductive val :=
  | LamV (e : {bind 1 of expr})
  | TLamV (e : {bind 1 of expr})
  | UnitV
+  | NatV (n : nat)
+  | BoolV (b : bool)
  | PairV (v1 v2 : val)
  | InjLV (v : val)
  | InjRV (v : val)
  | FoldV (v : val)
  | LocV (l : loc).

+  (* Notation for bool and nat *)
+  Notation "'♭v' b" := (BoolV b) (at level 200).
+  Notation "'♯v' n" := (NatV n) (at level 200).
+
+  Fixpoint NatBinOP_meaning (op : NatBinOP) : nat → nat → val :=
+    match op with
+    | Add => λ a b, ♯v(a + b)
+    | Sub => λ a b, ♯v(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
+    end.
+
  Global Instance val_dec_eq (v v' : val) : Decision (v = v').
  Proof.
-    unfold Decision; decide equality; try apply expr_dec_eq; apply loc_dec_eq.
+    unfold Decision; decide equality;
+      try solve [apply expr_dec_eq | apply eq_nat_dec |
+                 apply loc_dec_eq | apply bool_eq_dec].
  Defined.

  Global Instance val_inh : Inhabited val.
@@ -73,6 +109,8 @@ Module lang.
    | LamV e => Lam e
    | TLamV e => TLam e
    | UnitV => Unit
+    | NatV v => Nat v
+    | BoolV v => Bool v
    | PairV v1 v2 => Pair (of_val v1) (of_val v2)
    | InjLV v => InjL (of_val v)
    | InjRV v => InjR (of_val v)
@@ -85,6 +123,8 @@ Module lang.
    | Lam e => Some (LamV e)
    | TLam e => Some (TLamV e)
    | Unit => Some UnitV
+    | Nat n => Some (NatV n)
+    | Bool b => Some (BoolV b)
    | Pair e1 e2 => v1 ← to_val e1; v2 ← to_val e2; Some (PairV v1 v2)
    | InjL e => InjLV <$> to_val e
    | InjR e => InjRV <$> to_val e
@@ -100,11 +140,14 @@ Module lang.
  | TAppCtx
  | PairLCtx (e2 : expr)
  | PairRCtx (v1 : val)
+  | NBOPLCtx (op : NatBinOP) (e2 : expr)
+  | NBOPRCtx (op : NatBinOP) (v1 : val)
  | FstCtx
  | SndCtx
  | InjLCtx
  | InjRCtx
  | CaseCtx (e1 : {bind expr}) (e2 : {bind expr})
+  | IfCtx (e1 : {bind expr}) (e2 : {bind expr})
  | FoldCtx
  | UnfoldCtx
  | AllocCtx
@@ -124,11 +167,14 @@ Module lang.
    | TAppCtx => TApp e
    | PairLCtx e2 => Pair e e2
    | PairRCtx v1 => Pair (of_val v1) e
+    | NBOPLCtx op e2 => NBOP op e e2
+    | NBOPRCtx op v1 => NBOP op (of_val v1) e
    | FstCtx => Fst e
    | SndCtx => Snd e
    | InjLCtx => InjL e
    | InjRCtx => InjR e
    | CaseCtx e1 e2 => Case e e1 e2
+    | IfCtx e1 e2 => If e e1 e2
    | FoldCtx => Fold e
    | UnfoldCtx => Unfold e
    | AllocCtx => Alloc e
@@ -144,13 +190,6 @@ Module lang.

  Definition state : Type := gmap loc val.

-  (** Abbreviation for true and false -- we don't want to add a primitive boolean type
-      and its terms *)
-  Notation TRUE := (InjL Unit).
-  Notation FALSE := (InjR Unit).
-  Notation TRUEV := (InjLV UnitV).
-  Notation FALSEV := (InjRV UnitV).
-
  Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
  (* β *)
  | BetaS e1 e2 v2 σ :
@@ -170,6 +209,14 @@ Module lang.
  | CaseRS e0 v0 e1 e2 σ :
      to_val e0 = Some v0 →
      head_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
+    (* nat bin op *)
+  | NBOPS op a b σ :
+      head_step (NBOP op (♯ a) (♯b)) σ (of_val (NatBinOP_meaning op a b)) σ None
+  (* If then else *)
+  | IfFalse e1 e2 σ :
+      head_step (If (♭ false) e1 e2) σ e2 σ None
+  | IfTrue e1 e2 σ :
+      head_step (If (♭ true) e1 e2) σ e1 σ None
  (* Recursive Types *)
  | Unfold_Fold e v σ :
      to_val e = Some v →
@@ -194,11 +241,11 @@ Module lang.
  | CasFailS l e1 v1 e2 v2 vl σ :
     to_val e1 = Some v1 → to_val e2 = Some v2 →
     σ !! l = Some vl → vl ≠ v1 →
-     head_step (CAS (Loc l) e1 e2) σ FALSE σ None
+     head_step (CAS (Loc l) e1 e2) σ (♭ false) σ None
  | CasSucS l e1 v1 e2 v2 σ :
     to_val e1 = Some v1 → to_val e2 = Some v2 →
     σ !! l = Some v1 →
-     head_step (CAS (Loc l) e1 e2) σ TRUE (<[l:=v2]>σ) None.
+     head_step (CAS (Loc l) e1 e2) σ (♭ true) (<[l:=v2]>σ) None.

  (** Atomic expressions: we don't consider any atomic operations. *)
  Definition atomic (e: expr) :=

--- a/F_mu_ref_par/logrel_binary.v
+++ b/F_mu_ref_par/logrel_binary.v
@@ -94,6 +94,20 @@ Section logrel.
  Next Obligation.
  Proof. intros n x y [H1 H2]; rewrite H1 H2; trivial. Qed.

+  Program Definition interp_nat : bivalC -n> iPropG lang Σ :=
+    {|
+      cofe_mor_car := λ w, (∃ n, w.1 = (♯v n) ∧ w.2 = (♯v n))%I
+    |}.
+  Next Obligation.
+  Proof. intros n x y [H1 H2]; rewrite H1 H2; trivial. Qed.
+
+  Program Definition interp_bool : bivalC -n> iPropG lang Σ :=
+    {|
+      cofe_mor_car := λ w, (∃ b, w.1 = (♭v b) ∧ w.2 = (♭v b))%I
+    |}.
+  Next Obligation.
+  Proof. intros n x y [H1 H2]; rewrite H1 H2; trivial. Qed.
+
  Program Definition interp_prod :
    (bivalC -n> iPropG lang Σ) -n> (bivalC -n> iPropG lang Σ) -n>
    bivalC -n> iPropG lang Σ :=
@@ -328,6 +342,8 @@ Section logrel.
                     bivalC -n> iPropG lang Σ
      with
      | TUnit => {| cofe_mor_car := λ Δ, interp_unit |}
+      | TNat => {| cofe_mor_car := λ Δ, interp_nat |}
+      | TBool => {| cofe_mor_car := λ Δ, interp_bool |}
      | TProd τ1 τ2 =>
        {| cofe_mor_car := λ Δ, interp_prod (interp τ1 Δ) (interp τ2 Δ)|}
      | TSum τ1 τ2 =>
@@ -673,8 +689,10 @@ Section logrel.
        {HΔ : context_interp_Persistent Δ} :
    interp τ Δ (v, v') ⊢ ■ (v = v').
  Proof.
-      revert v v'; induction H => v v'; iIntros "#H1".
+    revert v v'; induction H => v v'; iIntros "#H1".
    - simpl; iDestruct "H1" as "[% %]"; subst; trivial.
+    - simpl; iDestruct "H1" as {n} "[% %]"; subst; trivial.
+    - simpl; iDestruct "H1" as {b} "[% %]"; subst; trivial.
    - iDestruct "H1" as {w1 w2} "[% [H1 H2]]".
      destruct w1; destruct w2; simpl in *.
      inversion H1; subst.

--- a/F_mu_ref_par/logrel_unary.v
+++ b/F_mu_ref_par/logrel_unary.v
@@ -87,6 +87,16 @@ Section logrel.
      cofe_mor_car := λ w, (w = UnitV)%I
    |}.

+  Definition interp_nat : valC -n> iPropG lang Σ :=
+    {|
+      cofe_mor_car := λ w, (∃ n, w = (♯v n))%I
+    |}.
+
+  Definition interp_bool : valC -n> iPropG lang Σ :=
+    {|
+      cofe_mor_car := λ w, (∃ n, w = (♭v n))%I
+    |}.
+
  Program Definition interp_prod :
    (valC -n> iPropG lang Σ) -n> (valC -n> iPropG lang Σ) -n>
    valC -n> iPropG lang Σ :=
@@ -262,9 +272,14 @@ Section logrel.
                     valC -n> iPropG lang Σ
      with
      | TUnit => {| cofe_mor_car := λ Δ, interp_unit |}
-      | TProd τ1 τ2 => {| cofe_mor_car := λ Δ, interp_prod (interp τ1 Δ) (interp τ2 Δ)|}
-      | TSum τ1 τ2 => {| cofe_mor_car := λ Δ, interp_sum(interp τ1 Δ) (interp τ2 Δ)|}
-      | TArrow τ1 τ2 => {|cofe_mor_car := λ Δ, interp_arrow (interp τ1 Δ) (interp τ2 Δ)|}
+      | TNat => {| cofe_mor_car := λ Δ, interp_nat |}
+      | TBool => {| cofe_mor_car := λ Δ, interp_bool |}
+      | TProd τ1 τ2 =>
+        {| cofe_mor_car := λ Δ, interp_prod (interp τ1 Δ) (interp τ2 Δ)|}
+      | TSum τ1 τ2 =>
+        {| cofe_mor_car := λ Δ, interp_sum(interp τ1 Δ) (interp τ2 Δ)|}
+      | TArrow τ1 τ2 =>
+        {|cofe_mor_car := λ Δ, interp_arrow (interp τ1 Δ) (interp τ2 Δ)|}
      | TVar v => {| cofe_mor_car :=
                      λ Δ : (varC -n> (valC -n> iPropG lang Σ)), (Δ v)  |}
      | TForall τ' =>

--- a/F_mu_ref_par/rules.v
+++ b/F_mu_ref_par/rules.v
@@ -268,21 +268,21 @@ Section lang_rules.

    Lemma wp_cas_fail_pst E σ l e1 v1 e2 v2 v' Φ :
      to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v' → v' ≠ v1 →
-      (▷ ownP σ ★ ▷ (ownP σ -★ Φ (FALSEV)))
+      (▷ ownP σ ★ ▷ (ownP σ -★ Φ (♭v false)))
        ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
    Proof.
-      intros. rewrite -(wp_lift_atomic_det_step σ (FALSEV) σ None)
+      intros. rewrite -(wp_lift_atomic_det_step σ (♭v false) σ None)
                         ?right_id //; last (by intros; inv_step; eauto);
                simpl; by eauto 10.
    Qed.

    Lemma wp_cas_suc_pst E σ l e1 v1 e2 v2 Φ :
      to_val e1 = Some v1 → to_val e2 = Some v2 → σ !! l = Some v1 →
-      (▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (TRUEV)))
+      (▷ ownP σ ★ ▷ (ownP (<[l:=v2]>σ) -★ Φ (♭v true)))
        ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
    Proof.
      intros. rewrite -(wp_lift_atomic_det_step
-                          σ (TRUEV)  (<[l:=v2]>σ) None)
+                          σ (♭v true)  (<[l:=v2]>σ) None)
                         ?right_id //; last (by intros; inv_step; eauto);
                simpl; by eauto 10.
    Qed.
@@ -336,7 +336,7 @@ Section lang_rules.

    Lemma wp_cas_fail N E l q v' e1 v1 e2 v2 Φ :
      to_val e1 = Some v1 → to_val e2 = Some v2 → v' ≠ v1 → nclose N ⊆ E →
-      (heapI_ctx N ★ ▷ l ↦ᵢ{q} v' ★ ▷ (l ↦ᵢ{q} v' -★ Φ (FALSEV)))
+      (heapI_ctx N ★ ▷ l ↦ᵢ{q} v' ★ ▷ (l ↦ᵢ{q} v' -★ Φ (♭v false)))
        ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
    Proof.
      iIntros {????} "[#Hh [Hl HΦ]]". rewrite /heapI_ctx /heapI_mapsto.
@@ -350,7 +350,7 @@ Section lang_rules.

    Lemma wp_cas_suc N E l e1 v1 e2 v2 Φ :
      to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
-      (heapI_ctx N ★ ▷ l ↦ᵢ v1 ★ ▷ (l ↦ᵢ v2 -★ Φ (TRUEV)))
+      (heapI_ctx N ★ ▷ l ↦ᵢ v1 ★ ▷ (l ↦ᵢ v2 -★ Φ (♭v true)))
        ⊢ WP CAS (Loc l) e1 e2 @ E {{ Φ }}.
    Proof.
      iIntros {???} "[#Hh [Hl HΦ]]". rewrite /heapI_ctx /heapI_mapsto.
@@ -418,7 +418,8 @@ Section lang_rules.
      ▷ WP e1.[e0/] @ E {{Φ}} ⊢ WP (Case (InjL e0) e1 e2) @ E {{Φ}}.
    Proof.
      intros <-%of_to_val.
-      rewrite -(wp_lift_pure_det_step (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=.
+      rewrite -(wp_lift_pure_det_step
+                  (Case (InjL _) _ _) (e1.[of_val v0/]) None) //=.
      - rewrite right_id; auto using uPred.later_mono, wp_value'.
      - intros. inv_step; auto.
    Qed.
@@ -428,7 +429,8 @@ Section lang_rules.
      ▷ WP e2.[e0/] @ E {{Φ}} ⊢ WP (Case (InjR e0) e1 e2) @ E {{Φ}}.
    Proof.
      intros <-%of_to_val.
-      rewrite -(wp_lift_pure_det_step (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=.
+      rewrite -(wp_lift_pure_det_step
+                  (Case (InjR _) _ _) (e2.[of_val v0/]) None) //=.
      - rewrite right_id; auto using uPred.later_mono, wp_value'.
      - intros. inv_step; auto.
    Qed.
@@ -441,6 +443,31 @@ Section lang_rules.
      rewrite later_sep -(wp_value _ _ (Unit)) //.
    Qed.

+    Lemma wp_if_false E e1 e2 Φ :
+      ▷ WP e2 @ E {{Φ}} ⊢ WP (If (♭ false) e1 e2) @ E {{Φ}}.
+    Proof.
+      rewrite -(wp_lift_pure_det_step (If (♭ false) _ _) (e2) None) //=.
+      - rewrite right_id; auto using uPred.later_mono, wp_value'.
+      - intros. inv_step; auto.
+    Qed.
+
+    Lemma wp_if_true E e1 e2 Φ :
+      ▷ WP e1 @ E {{Φ}} ⊢ WP (If (♭ true) e1 e2) @ E {{Φ}}.
+    Proof.
+      rewrite -(wp_lift_pure_det_step (If (♭ true) _ _) (e1) None) //=.
+      - rewrite right_id; auto using uPred.later_mono, wp_value'.
+      - intros. inv_step; auto.
+    Qed.
+
+    Lemma wp_nat_bin_op E op a b Φ :
+      ▷ Φ (NatBinOP_meaning op a b) ⊢ WP (NBOP op (♯ a) (♯ b)) @ E {{Φ}}.
+    Proof.
+      rewrite -(wp_lift_pure_det_step
+                  (NBOP _ _ _) (of_val (NatBinOP_meaning op a b)) None) //=.
+      - rewrite right_id; auto using uPred.later_mono, wp_value'.
+      - intros. inv_step; auto.
+    Qed.
+
  End heap.

 End lang_rules.

--- a/F_mu_ref_par/rules_binary.v
+++ b/F_mu_ref_par/rules_binary.v
@@ -676,7 +676,7 @@ Section lang_rules.
      step
        (of_cfg (({[j := Frac 1 (DecAgree (fill K (CAS (Loc l) e1 e2)))]}, ∅)
                   ⋅ (∅, {[l := Frac q (DecAgree v')]}) ⋅ ρ))
-        (of_cfg (({[j := Frac 1 (DecAgree (fill K FALSE))]}, ∅)
+        (of_cfg (({[j := Frac 1 (DecAgree (fill K (♭ false)))]}, ∅)
                   ⋅ (∅, {[l := Frac q (DecAgree v')]}) ⋅ ρ)).
    Proof.
      destruct ρ as [tp th]; simpl.
@@ -695,7 +695,7 @@ Section lang_rules.
      to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
      ((Spec_ctx N ρ ★ j ⤇ (fill K (CAS (Loc l) e1 e2))
                 ★ ▷ (■ (v' ≠ v1)) ★ l ↦ₛ{q} v')%I)
-        ⊢ |={E}=>(j ⤇ (fill K (FALSE)) ★ l ↦ₛ{q} v')%I.
+        ⊢ |={E}=>(j ⤇ (fill K (♭ false)) ★ l ↦ₛ{q} v')%I.
    Proof.
      iIntros {H1 H2 H3} "[#Hinv [Hj [#Hneq Hl]]]".
      unfold Spec_ctx, auth_ctx, tpool_mapsto, heapS_mapsto, auth_own.
@@ -712,7 +712,7 @@ Section lang_rules.
      iPvs (own_update with "Hown") as "Hown".
      rewrite assoc -auth_frag_op.
      rewrite -cfg_split; rewrite cmra_comm.
-      apply (thread_update _ _ (fill K FALSE)). revert H.
+      apply (thread_update _ _ (fill K (♭ false))). revert H.
      rewrite cfg_combine; first by rewrite !left_id !right_id.
      rewrite own_op; iDestruct "Hown" as "[H1 H2]".
      iSplitR "H2".
@@ -730,7 +730,7 @@ Section lang_rules.
      step
        (of_cfg (({[j := Frac 1 (DecAgree (fill K (CAS (Loc l) e1 e2)))]}, ∅)
                   ⋅ (∅, {[l := Frac 1 (DecAgree v1)]}) ⋅ ρ))
-        (of_cfg (({[j := Frac 1 (DecAgree (fill K TRUE))]}, ∅)
+        (of_cfg (({[j := Frac 1 (DecAgree (fill K (♭ true)))]}, ∅)
                   ⋅ (∅, {[l := Frac 1 (DecAgree v2)]}) ⋅ ρ)).
    Proof.
      destruct ρ as [tp th]; simpl.
@@ -751,7 +751,7 @@ Section lang_rules.
      to_val e1 = Some v1 → to_val e2 = Some v2 → nclose N ⊆ E →
      ((Spec_ctx N ρ ★ j ⤇ (fill K (CAS (Loc l) e1 e2))
                 ★ ▷ (■ (v1 = v1')) ★ l ↦ₛ v1')%I)
-        ⊢ |={E}=>(j ⤇ (fill K (TRUE)) ★ l ↦ₛ v2)%I.
+        ⊢ |={E}=>(j ⤇ (fill K (♭ true)) ★ l ↦ₛ v2)%I.
    Proof.
      iIntros {H1 H2 H3} "[#Hinv [Hj [#Heq Hl]]]".
      unfold Spec_ctx, auth_ctx, tpool_mapsto, heapS_mapsto, auth_own.
@@ -768,7 +768,7 @@ Section lang_rules.
      iPvs (own_update with "Hown") as "Hown".
      rewrite assoc -auth_frag_op.
      rewrite -cfg_split; rewrite cmra_comm.
-      apply (thread_update _ _ (fill K TRUE)). revert H.
+      apply (thread_update _ _ (fill K (♭ true))). revert H.
      rewrite cfg_combine; first by rewrite !left_id !right_id.
      iPvs (own_update with "Hown") as "Hown".
      apply (cfg_heap_update _ _ v2). revert H.
@@ -825,6 +825,24 @@ Section lang_rules.
        ⊢ |={E}=>(j ⤇ (fill K (e2.[e0/])))%I.
    Proof. intros H1; apply step_pure => σ; econstructor; eauto. Qed.

+    Lemma step_if_false N E ρ j K e1 e2 :
+      nclose N ⊆ E →
+      ((Spec_ctx N ρ ★ j ⤇ (fill K (If (♭ false) e1 e2)))%I)
+        ⊢ |={E}=>(j ⤇ (fill K e2))%I.
+    Proof. apply step_pure => σ; econstructor. Qed.
+
+    Lemma step_if_true N E ρ j K e1 e2 :
+      nclose N ⊆ E →
+      ((Spec_ctx N ρ ★ j ⤇ (fill K (If (♭ true) e1 e2)))%I)
+        ⊢ |={E}=>(j ⤇ (fill K e1))%I.
+    Proof. apply step_pure => σ; econstructor. Qed.
+
+    Lemma step_nat_bin_op N E ρ j K op a b :
+      nclose N ⊆ E →
+      ((Spec_ctx N ρ ★ j ⤇ (fill K (NBOP op (♯ a) (♯ b))))%I)
+        ⊢ |={E}=>(j ⤇ (fill K (of_val (NatBinOP_meaning op a b))))%I.
+    Proof. apply step_pure => σ; econstructor. Qed.
+
    Lemma step_fork_base k j K e h ρ :
      k > j → k > List.length (ρ.1) →
      ✓ (({[j := Frac 1 (DecAgree (fill K (Fork e)))]}, h) ⋅ ρ) →

--- a/F_mu_ref_par/soundness_binary.v
+++ b/F_mu_ref_par/soundness_binary.v
@@ -26,6 +26,13 @@ Inductive context_item : Type :=
 | CTX_CaseL (e1 : expr) (e2 : expr)
 | CTX_CaseM (e0 : expr) (e2 : expr)
 | CTX_CaseR (e0 : expr) (e1 : expr)
+(* Nat bin op *)
+| CTX_NBOPL (op : NatBinOP) (e2 : expr)
+| CTX_NBOPR (op : NatBinOP) (e1 : expr)
+(* If *)