move sugar to separate file, and prove some more rules for it

_CoqProject

@@ -65,4 +65,5 @@ iris/tests.v
 barrier/heap_lang.v
 barrier/parameter.v
 barrier/lifting.v
+barrier/sugar.v
 barrier/tests.v

barrier/heap_lang.v

@@ -38,10 +38,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.[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)].
+(* This sugar is used by primitive reduction riles (<=, CAS) and hence defined here. *)
+Definition LitTrue := InjL LitUnit.
+Definition LitFalse := InjR LitUnit.
 
 Inductive value :=
 | RecV (e : {bind 2 of expr})
@@ -53,11 +52,7 @@ Inductive value :=
 | LocV (l : loc)
 .
 
-Definition LamV (e : {bind expr}) := RecV e.[ren(+1)].
-
-Definition LitTrue := InjL LitUnit.
 Definition LitTrueV := InjLV LitUnitV.
-Definition LitFalse := InjR LitUnit.
 Definition LitFalseV := InjRV LitUnitV.
 
 Fixpoint v2e (v : value) : expr :=
@@ -192,9 +187,6 @@ Fixpoint comp_ctx (Ko : ectx) (Ki : ectx) :=
   | CasRCtx v0 v1 K2 => CasRCtx v0 v1 (comp_ctx K2 Ki)
   end.
 
-Definition LetCtx (K1 : ectx) (e2 : {bind expr}) := AppRCtx (LamV e2) K1.
-Definition SeqCtx (K1 : ectx) (e2 : expr) := LetCtx K1 (e2.[ren(+1)]).
-
 Lemma fill_empty e :
   fill EmptyCtx e = e.
 Proof.

barrier/lifting.v

@@ -220,16 +220,6 @@ Proof.
     apply const_elim_l=>->. done.
 Qed.
 
-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.
-  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.
-Qed.
-
 Lemma wp_plus n1 n2 E Q :
   ▷Q (LitNatV (n1 + n2)) ⊑ wp (Σ:=Σ) E (Plus (LitNat n1) (LitNat n2)) Q.
 Proof.
@@ -329,13 +319,6 @@ Qed.
 
 (** Some derived stateless axioms *)
 
-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.
-
 Lemma wp_le n1 n2 E P Q :
   (n1 ≤ n2 → P ⊑ ▷Q LitTrueV) →
   (n1 > n2 → P ⊑ ▷Q LitFalseV) →

barrier/tests.v

 (** This file is essentially a bunch of testcases. *)
 Require Import modures.logic.
-Require Import barrier.lifting.
+Require Import barrier.lifting barrier.sugar.
 Import uPred.
 
 Module LangTests.
@@ -62,7 +62,6 @@ Module LiftingTests.
 
   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.
@@ -87,10 +86,12 @@ Module LiftingTests.
     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.
-    apply wp_le; intros Hn12.
-    - rewrite -wp_case_inl //.
+    rewrite -!later_intro. simpl.
+    apply wp_lt; intros Hn12.
+    - (* TODO RJ: It would be better if we could use wp_if_true here
+         (and below). But we cannot, because the substitutions in there
+         got already unfolded. *)
+      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.