start showing that we can implement the predecessor function

barrier/heap_lang.v

@@ -38,10 +38,10 @@ Instance Rename_expr : Rename expr. derive. Defined.
 Instance Subst_expr : Subst expr. derive. Defined.
 Instance SubstLemmas_expr : SubstLemmas expr. derive. Qed.
 
-Definition Lam (e : {bind expr}) := Rec (e.[ren(+1)]).
+Definition Lam (e : {bind expr}) := Rec e.[ren(+1)].
 Definition Let (e1 : expr) (e2: {bind expr}) := App (Lam e2) e1.
-Definition Seq (e1 e2 : expr) := Let e1 (e2.[ren(+1)]).
-Definition If (e0 e1 e2 : expr) := Case e0 (e1.[ren(+1)]) (e2.[ren(+1)]).
+Definition Seq (e1 e2 : expr) := Let e1 e2.[ren(+1)].
+Definition If (e0 e1 e2 : expr) := Case e0 e1.[ren(+1)] e2.[ren(+1)].
 
 Inductive value :=
 | RecV (e : {bind 2 of expr})
@@ -53,7 +53,7 @@ Inductive value :=
 | LocV (l : loc)
 .
 
-Definition LamV (e : {bind expr}) := RecV (e.[ren(+1)]).
+Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
 
 Definition LitTrue := InjL LitUnit.
 Definition LitTrueV := InjLV LitUnitV.
@@ -245,7 +245,7 @@ Qed.
 (** The stepping relation *)
 Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
 | BetaS e1 e2 v2 σ (Hv2 : e2v e2 = Some v2):
-    prim_step (App (Rec e1) e2) σ (e1.[(Rec e1),e2/]) σ None
+    prim_step (App (Rec e1) e2) σ e1.[(Rec e1),e2/] σ None
 | PlusS n1 n2 σ:
     prim_step (Plus (LitNat n1) (LitNat n2)) σ (LitNat (n1 + n2)) σ None
 | LeTrueS n1 n2 σ (Hle : n1 ≤ n2):
@@ -257,9 +257,9 @@ Inductive prim_step : expr -> state -> expr -> state -> option expr -> Prop :=
 | SndS e1 v1 e2 v2 σ (Hv1 : e2v e1 = Some v1) (Hv2 : e2v e2 = Some v2):
     prim_step (Snd (Pair e1 e2)) σ e2 σ None
 | CaseLS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
-    prim_step (Case (InjL e0) e1 e2) σ (e1.[e0/]) σ None
+    prim_step (Case (InjL e0) e1 e2) σ e1.[e0/] σ None
 | CaseRS e0 v0 e1 e2 σ (Hv0 : e2v e0 = Some v0):
-    prim_step (Case (InjR e0) e1 e2) σ (e2.[e0/]) σ None
+    prim_step (Case (InjR e0) e1 e2) σ e2.[e0/] σ None
 | ForkS e σ:
     prim_step (Fork e) σ LitUnit σ (Some e)
 | AllocS e v σ l (Hv : e2v e = Some v) (Hfresh : σ !! l = None):

barrier/lifting.v

@@ -11,9 +11,7 @@ Proof.
   by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
 Qed.
 
-(** Base axioms for core primitives of the language: Stateful reductions.
-    These are the lemmas basd on the physical state; we will derive versions
-    based on a ghost "mapsto"-predicate later. *)
+(** Base axioms for core primitives of the language: Stateful reductions. *)
 
 Lemma wp_lift_step E1 E2 (φ : expr → state → Prop) Q e1 σ1 :
   E1 ⊆ E2 → to_val e1 = None →
@@ -209,22 +207,24 @@ Proof.
     rewrite right_id. done.
 Qed.
 
-Lemma wp_rec E e v Q :
-  ▷wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
+Lemma wp_rec E ef e v Q :
+  e2v e = Some v →
+  ▷wp (Σ:=Σ) E ef.[Rec ef, e /] Q ⊑ wp (Σ:=Σ) E (App (Rec ef) e) Q.
 Proof.
   etransitivity; last eapply wp_lift_pure_step with
-    (φ := λ e', e' = e.[Rec e, v2e v /]); last first.
+    (φ := λ e', e' = ef.[Rec ef, e /]); last first.
   - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
-  - intros ?. do 3 eexists. eapply BetaS. by rewrite v2v.
+  - intros ?. do 3 eexists. eapply BetaS; eassumption.
   - reflexivity.
   - apply later_mono, forall_intro=>e2. apply impl_intro_l.
     apply const_elim_l=>->. done.
 Qed.
 
-Lemma wp_lam E e v Q :
-  ▷wp (Σ:=Σ) E (e.[v2e v/]) Q ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
+Lemma wp_lam E ef e v Q :
+  e2v e = Some v →
+  ▷wp (Σ:=Σ) E ef.[e/] Q ⊑ wp (Σ:=Σ) E (App (Lam ef) e) Q.
 Proof.
-  rewrite -wp_rec.
+  intros Hv. rewrite -wp_rec; last eassumption.
   (* RJ: This pulls in functional extensionality. If that bothers us, we have
      to talk to the Autosubst guys. *)
   by asimpl.
@@ -303,7 +303,7 @@ Qed.
 
 Lemma wp_case_inl e0 v0 e1 e2 E Q :
   e2v e0 = Some v0 →
-  ▷wp (Σ:=Σ) E (e1.[e0/]) Q ⊑ wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q.
+  ▷wp (Σ:=Σ) E e1.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjL e0) e1 e2) Q.
 Proof.
   intros Hv0. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e1.[e0/]); last first.
@@ -316,7 +316,7 @@ Qed.
 
 Lemma wp_case_inr e0 v0 e1 e2 E Q :
   e2v e0 = Some v0 →
-  ▷wp (Σ:=Σ) E (e2.[e0/]) Q ⊑ wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q.
+  ▷wp (Σ:=Σ) E e2.[e0/] Q ⊑ wp (Σ:=Σ) E (Case (InjR e0) e1 e2) Q.
 Proof.
   intros Hv0. etransitivity; last eapply wp_lift_pure_step with
     (φ := λ e', e' = e2.[e0/]); last first.
@@ -326,3 +326,12 @@ Proof.
   - apply later_mono, forall_intro=>e2'. apply impl_intro_l.
     by apply const_elim_l=>->.
 Qed.
+
+(** Some stateless axioms that incorporate bind *)
+
+Lemma wp_let e1 e2 E Q :
+  wp (Σ:=Σ) E e1 (λ v, ▷wp (Σ:=Σ) E (e2.[v2e v/]) Q) ⊑ wp (Σ:=Σ) E (Let e1 e2) Q.
+Proof.
+  rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). apply wp_mono=>v.
+  rewrite -wp_lam //. by rewrite v2v.
+Qed.

barrier/tests.v

@@ -32,16 +32,16 @@ End ParamTests.
 Module LiftingTests.
   (* TODO RJ: Some syntactic sugar for language expressions would be nice. *)
   Definition e3 := Load (Var 0).
-  Definition e2 := Seq (Store (Var 0) (Plus (Load (Var 0)) (LitNat 1))) e3.
+  Definition e2 := Seq (Store (Var 0) (Plus (Load $ Var 0) (LitNat 1))) e3.
   Definition e := Let (Alloc (LitNat 1)) e2.
   Goal ∀ σ E, (ownP (Σ:=Σ) σ) ⊑ (wp (Σ:=Σ) E e (λ v, ■(v = LitNatV 2))).
   Proof.
     move=> σ E. rewrite /e.
-    rewrite -(wp_bind _ _ (LetCtx EmptyCtx e2)). rewrite -wp_alloc_pst; last done.
+    rewrite -wp_let. rewrite -wp_alloc_pst; last done.
     apply sep_intro_True_r; first done.
     rewrite -later_intro. apply forall_intro=>l.
     apply wand_intro_l. rewrite right_id. apply const_elim_l; move=>_.
-    rewrite -wp_lam -later_intro. asimpl.
+    rewrite -later_intro. asimpl.
     rewrite -(wp_bind _ _ (SeqCtx (StoreRCtx (LocV _)
                                    (PlusLCtx EmptyCtx _)) (Load (Loc _)))).
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
@@ -54,10 +54,48 @@ Module LiftingTests.
     { apply: lookup_insert. }
     { reflexivity. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
-    rewrite -wp_lam -later_intro. asimpl.
+    rewrite -wp_lam // -later_intro. asimpl.
     rewrite -wp_load_pst; first (apply sep_intro_True_r; first done); last first.
     { apply: lookup_insert. }
     rewrite -later_intro. apply wand_intro_l. rewrite right_id.
     by apply const_intro.
   Qed.
+
+  Import Nat.
+
+  Definition Lt e1 e2 := Le (Plus e1 $ LitNat 1) e2.
+  Definition FindPred' n1 Sn1 n2 f := If (Lt Sn1 n2)
+                                      (App f Sn1)
+                                      n1.
+  Definition FindPred n2 := Rec (Let (Plus (Var 1) (LitNat 1))
+                                     (FindPred' (Var 2) (Var 0) n2.[ren(+3)] (Var 1))).
+  Lemma FindPred_spec n1 n2 E Q :
+    (■(n1 < n2) ∧ Q (LitNatV $ pred n2)) ⊑
+       wp (Σ:=Σ) E (App (FindPred (LitNat n2)) (LitNat n1)) Q.
+  Proof.
+    revert n1. apply löb_all_1=>n1.
+    rewrite -wp_rec //. asimpl.
+    (* Get rid of the ▷ in the premise. *)
+    etransitivity; first (etransitivity; last eapply equiv_spec, later_and).
+    { apply and_mono; first done. by rewrite -later_intro. }
+    apply later_mono.
+    (* Go on. *)
+    rewrite -(wp_let _ (FindPred' (LitNat n1) (Var 0) (LitNat n2) (FindPred $ LitNat n2))).
+    rewrite -wp_plus. asimpl.
+    rewrite -(wp_bind _ _ (CaseCtx EmptyCtx _ _)).
+    rewrite -(wp_bind _ _ (LeLCtx EmptyCtx _)).
+    rewrite -wp_plus -!later_intro. simpl.
+    assert (Decision (S n1 + 1 ≤ n2)) as Hn12 by apply _.
+    destruct Hn12 as [Hle|Hgt].
+    - rewrite -wp_le_true /= //. rewrite -wp_case_inl //.
+      rewrite -!later_intro. asimpl.
+      rewrite (forall_elim _ (S n1)).
+      eapply impl_elim; first by eapply and_elim_l. apply and_intro.
+      + apply const_intro; omega.
+      + by rewrite !and_elim_r.
+    - rewrite -wp_le_false; last by omega.
+      rewrite -wp_case_inr // -!later_intro -wp_value' //.
+      rewrite and_elim_r. apply const_elim_l=>Hle.
+      assert (Heq: n1 = pred n2) by omega. by subst n1=>{Hle Hgt}.
+  Qed.
 End LiftingTests.