fix Lam and Seq sugar; prove base rules for Rec and Lam

barrier/heap_lang.v

-Require Import Autosubst.Autosubst.
+Require Export Autosubst.Autosubst.
 Require Import prelude.option prelude.gmap iris.language.
 
 (** Some tactics useful when dealing with equality of sigma-like types:
@@ -26,7 +26,7 @@ Definition loc := positive. (* Really, any countable type. *)
 Inductive expr :=
 (* Base lambda calculus *)
 | Var (x : var)
-| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. *)
+| Rec (e : {bind 2 of expr}) (* These are recursive lambdas. The *inner* binder is the recursive call! *)
 | App (e1 e2 : expr)
 (* Embedding of Coq values and operations *)
 | Lit {T : Type} (t: T)  (* arbitrary Coq values become literals *)
@@ -55,9 +55,9 @@ 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.[up ids]).
+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.[up ids]).
+Definition Seq (e1 e2: expr) := Let' e1 (e2.[ren(+1)]).
 
 Inductive value :=
 | RecV (e : {bind 2 of expr})
@@ -252,7 +252,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.[e2.:(Rec e1).:ids]) σ None
+    prim_step (App (Rec e1) e2) σ (e1.[(Rec e1),e2/]) σ None
 | Op1S T1 To (f : T1 -> To) t σ:
     prim_step (Op1 f (Lit t)) σ (Lit (f t)) σ None
 | Op2S T1 T2 To (f : T1 -> T2 -> To) t1 t2 σ:

barrier/lifting.v

@@ -6,7 +6,7 @@ Import uPred.
 
 (** Bind. *)
 Lemma wp_bind E e K Q :
-  wp E e (λ v, wp (Σ:=Σ) E (fill K (of_val v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q.
+  wp (Σ:=Σ) E e (λ v, wp (Σ:=Σ) E (fill K (v2e v)) Q) ⊑ wp (Σ:=Σ) E (fill K e) Q.
 Proof.
   by apply (wp_bind (Σ:=Σ) (K := fill K)), fill_is_ctx.
 Qed.
@@ -47,7 +47,7 @@ Lemma wp_alloc E σ v:
   ownP (Σ:=Σ) σ ⊑ wp (Σ:=Σ) E (Alloc (v2e v))
        (λ v', ∃ l, ■(v' = LocV l ∧ σ !! l = None) ∧ ownP (Σ:=Σ) (<[l:=v]>σ)).
 Proof.
-  (* RJ FIXME: rewrite would be nicer... *)
+  (* RJ FIXME (also for most other lemmas in this file): rewrite would be nicer... *)
   etransitivity; last eapply wp_lift_step with (σ1 := σ)
     (φ := λ e' σ', ∃ l, e' = Loc l ∧ σ' = <[l:=v]>σ ∧ σ !! l = None);
     last first.
@@ -160,3 +160,28 @@ Proof.
     eapply const_intro_l; first eexact Hφ. rewrite impl_elim_r.
     rewrite right_id. done.
 Qed.
+
+Lemma wp_rec' E e v P Q :
+  P ⊑ wp (Σ:=Σ) E (e.[Rec e, v2e v /]) Q →
+  ▷P ⊑ wp (Σ:=Σ) E (App (Rec e) (v2e v)) Q.
+Proof.
+  intros HP.
+  etransitivity; last eapply wp_lift_pure_step with
+    (φ := λ e', e' = e.[Rec e, v2e v /]); last first.
+  - intros ? ? ? ? Hstep. inversion_clear Hstep. done.
+  - intros ?. do 3 eexists. eapply BetaS. by rewrite v2v.
+  - reflexivity.
+  - apply later_mono, forall_intro=>e2. apply impl_intro_l.
+    apply const_elim_l=>->. done.
+Qed.
+
+Lemma wp_lam E e v P Q :
+  P ⊑ wp (Σ:=Σ) E (e.[v2e v/]) Q →
+  ▷P ⊑ wp (Σ:=Σ) E (App (Lam e) (v2e v)) Q.
+Proof.
+  intros HP. rewrite -wp_rec'; first (intros; apply later_mono; eassumption).
+  (* RJ: This pulls in functional extensionality. If that bothers us, we have
+     to talk to the Autosubst guys. *)
+  by asimpl.
+Qed.
+

barrier/tests.v

 (** This file is essentially a bunch of testcases. *)
 Require Import modures.base.
-Require Import barrier.lifting.
+Require Import barrier.parameter.
 
 Module LangTests.
   Definition add := Op2 plus (Lit 21) (Lit 21).
@@ -10,11 +10,11 @@ Module LangTests.
     apply Op2S.
   Qed.
 
-  Definition rec := Rec (App (Var 1) (Var 0)). (* fix f x => f x *)
+  Definition rec := Rec (App (Var 0) (Var 1)). (* fix f x => f x *)
   Definition rec_app := App rec (Lit 0).
   Goal ∀ σ, prim_step rec_app σ rec_app σ None.
   Proof.
-    move=>?. eapply BetaS. (* Honestly, I have no idea why this works. *)
+    move=>?. eapply BetaS.
     reflexivity.
   Qed.