Remove let as a built-in and make it syntactic sugar again.

heap_lang/heap_lang.v

@@ -19,8 +19,6 @@ Inductive expr :=
   | Var (x : string)
   | Rec (f x : string) (e : expr)
   | App (e1 e2 : expr)
-  (* Let *)
-  | Let (x : string) (e1 e2 : expr)
   (* Base types and their operations *)
   | Lit (l : base_lit)
   | UnOp (op : un_op) (e : expr)
@@ -78,7 +76,6 @@ Definition state := gmap loc val.
 Inductive ectx_item :=
   | AppLCtx (e2 : expr)
   | AppRCtx (v1 : val)
-  | LetCtx (x : string) (e2 : expr)
   | UnOpCtx (op : un_op)
   | BinOpLCtx (op : bin_op) (e2 : expr)
   | BinOpRCtx (op : bin_op) (v1 : val)
@@ -104,7 +101,6 @@ Definition fill_item (Ki : ectx_item) (e : expr) : expr :=
   match Ki with
   | AppLCtx e2 => App e e2
   | AppRCtx v1 => App (of_val v1) e
-  | LetCtx x e2 => Let x e e2
   | UnOpCtx op => UnOp op e
   | BinOpLCtx op e2 => BinOp op e e2
   | BinOpRCtx op v1 => BinOp op (of_val v1) e
@@ -133,8 +129,6 @@ Fixpoint subst (e : expr) (x : string) (v : val) : expr :=
   | Var y => if decide (x = y ∧ x ≠ "") then of_val v else Var y
   | Rec f y e => Rec f y (if decide (x ≠ f ∧ x ≠ y) then subst e x v else e)
   | App e1 e2 => App (subst e1 x v) (subst e2 x v)
-  | Let y e1 e2 =>
-     Let y (subst e1 x v) (if decide (x ≠ y) then subst e2 x v else e2)
   | Lit l => Lit l
   | UnOp op e => UnOp op (subst e x v)
   | BinOp op e1 e2 => BinOp op (subst e1 x v) (subst e2 x v)
@@ -178,9 +172,6 @@ Inductive head_step : expr -> state -> expr -> state -> option expr -> Prop :=
      to_val e2 = Some v2 →
      head_step (App (Rec f x e1) e2) σ
        (subst (subst e1 f (RecV f x e1)) x v2) σ None
-  | DeltaS x e1 e2 v1 σ :
-     to_val e1 = Some v1 →
-     head_step (Let x e1 e2) σ (subst e2 x v1) σ None
   | UnOpS op l l' σ :
      un_op_eval op l = Some l' → 
      head_step (UnOp op (Lit l)) σ (Lit l') σ None

heap_lang/lifting.v

@@ -90,14 +90,6 @@ Proof.
     last by intros; inv_step; eauto.
 Qed.
 
-Lemma wp_let E x e1 e2 v Q :
-  to_val e1 = Some v →
-  ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q.
-Proof.
-  intros. rewrite -(wp_lift_pure_det_step (Let _ _ _)
-    (subst e2 x v) None) ?right_id //=; intros; inv_step; eauto.
-Qed.
-
 Lemma wp_un_op E op l l' Q :
   un_op_eval op l = Some l' →
   ▷ Q (LitV l') ⊑ wp E (UnOp op (Lit l)) Q.

heap_lang/sugar.v

@@ -3,8 +3,10 @@ Import uPred heap_lang.
 
 (** Define some syntactic sugar. LitTrue and LitFalse are defined in heap_lang.v. *)
 Notation Lam x e := (Rec "" x e).
+Notation Let x e1 e2 := (App (Lam x e2) e1).
 Notation Seq e1 e2 := (Let "" e1 e2).
 Notation LamV x e := (RecV "" x e).
+Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
 Notation SeqCtx e2 := (LetCtx "" e2).
 
 Module notations.
@@ -14,7 +16,7 @@ Module notations.
 
   Coercion LitNat : nat >-> base_lit.
   Coercion LitBool : bool >-> base_lit.
-  (* No coercion from base_lit to expr. This makes is slightly easier to tell
+  (** No coercion from base_lit to expr. This makes is slightly easier to tell
      apart language and Coq expressions. *)
   Coercion Var : string >-> expr.
   Coercion App : expr >-> Funclass.
@@ -33,18 +35,21 @@ Module notations.
   Notation "e1 = e2" := (BinOp EqOp e1%L e2%L) (at level 70) : lang_scope.
   (* The unicode ← is already part of the notation "_ ← _; _" for bind. *)
   Notation "e1 <- e2" := (Store e1%L e2%L) (at level 80) : lang_scope.
-  Notation "'let:' x := e1 'in' e2" := (Let x e1%L e2%L)
-    (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
-  Notation "e1 ; e2" := (Seq e1%L e2%L)
-    (at level 100, e2 at level 200) : lang_scope.
   Notation "'rec:' f x := e" := (Rec f x e%L)
     (at level 102, f at level 1, x at level 1, e at level 200) : lang_scope.
   Notation "'if' e1 'then' e2 'else' e3" := (If e1%L e2%L e3%L)
     (at level 200, e1, e2, e3 at level 200) : lang_scope.
 
-  (* derived notions, in order of declaration *)
+  (** Derived notions, in order of declaration. The notations for let and seq
+  are stated explicitly instead of relying on the Notations Let and Seq as
+  defined above. This is needed because App is now a coercion, and these
+  notations are otherwise not pretty printed back accordingly. *)
   Notation "λ: x , e" := (Lam x e%L)
     (at level 102, x at level 1, e at level 200) : lang_scope.
+  Notation "'let:' x := e1 'in' e2" := (Lam x e2%L e1%L)
+    (at level 102, x at level 1, e1 at level 1, e2 at level 200) : lang_scope.
+  Notation "e1 ; e2" := (Lam "" e2%L e1%L)
+    (at level 100, e2 at level 200) : lang_scope.
 End notations.
 
 Section suger.
@@ -57,6 +62,10 @@ Lemma wp_lam E x ef e v Q :
   to_val e = Some v → ▷ wp E (subst ef x v) Q ⊑ wp E (App (Lam x ef) e) Q.
 Proof. intros. by rewrite -wp_rec ?subst_empty; eauto. Qed.
 
+Lemma wp_let E x e1 e2 v Q :
+  to_val e1 = Some v → ▷ wp E (subst e2 x v) Q ⊑ wp E (Let x e1 e2) Q.
+Proof. apply wp_lam. Qed.
+
 Lemma wp_seq E e1 e2 Q : wp E e1 (λ _, ▷ wp E e2 Q) ⊑ wp E (Seq e1 e2) Q.
 Proof.
   rewrite -(wp_bind [LetCtx "" e2]). apply wp_mono=>v.