heap_lang: Separate derived notions and notations into different files

_CoqProject

@@ -69,5 +69,6 @@ program_logic/ghost_ownership.v
 heap_lang/heap_lang.v
 heap_lang/heap_lang_tactics.v
 heap_lang/lifting.v
-heap_lang/sugar.v
+heap_lang/derived.v
+heap_lang/notation.v
 heap_lang/tests.v

heap_lang/sugar.v → heap_lang/derived.v

-Require Export heap_lang.heap_lang heap_lang.lifting.
-Import uPred heap_lang.
+Require Export heap_lang.lifting.
+Import uPred.
 
-(** Define some syntactic sugar. *)
+(** Define some derived forms, and derived lemmas about them. *)
 Notation Lam x e := (Rec "" x e).
 Notation Let x e1 e2 := (App (Lam x e2) e1).
 Notation Seq e1 e2 := (Let "" e1 e2).
@@ -9,53 +9,7 @@ Notation LamV x e := (RecV "" x e).
 Notation LetCtx x e2 := (AppRCtx (LamV x e2)).
 Notation SeqCtx e2 := (LetCtx "" e2).
 
-Module notations.
-  Delimit Scope lang_scope with L.
-  Bind Scope lang_scope with expr val.
-  Arguments wp {_ _} _ _%L _.
-
-  Coercion LitNat : nat >-> base_lit.
-  Coercion LitBool : bool >-> base_lit.
-  (** 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.
-  Coercion of_val : val >-> expr.
-
-  (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
-  first. *)
-  (* What about Arguments for hoare triples?. *)
-  Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
-  Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
-  Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
-  Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
-    (at level 50, left associativity) : lang_scope.
-  Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
-    (at level 50, left associativity) : lang_scope.
-  Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
-  Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
-  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 "'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. 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, 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.
-Export notations.
-
-Section sugar.
+Section derived.
 Context {Σ : iFunctor}.
 Implicit Types P : iProp heap_lang Σ.
 Implicit Types Q : val → iProp heap_lang Σ.
@@ -79,30 +33,30 @@ Proof.
 Qed.
 
 Lemma wp_le E (n1 n2 : nat) P Q :
-  (n1 ≤ n2 → P ⊑ ▷ Q (LitV true)) →
-  (n2 < n1 → P ⊑ ▷ Q (LitV false)) →
-  P ⊑ wp E ('n1 ≤ 'n2) Q.
+  (n1 ≤ n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
+  (n2 < n1 → P ⊑ ▷ Q (LitV $ LitBool false)) →
+  P ⊑ wp E (BinOp LeOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 ≤ n2)); by eauto with omega.
 Qed.
 
 Lemma wp_lt E (n1 n2 : nat) P Q :
-  (n1 < n2 → P ⊑ ▷ Q (LitV true)) →
-  (n2 ≤ n1 → P ⊑ ▷ Q (LitV false)) →
-  P ⊑ wp E ('n1 < 'n2) Q.
+  (n1 < n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
+  (n2 ≤ n1 → P ⊑ ▷ Q (LitV $ LitBool false)) →
+  P ⊑ wp E (BinOp LtOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 < n2)); by eauto with omega.
 Qed.
 
 Lemma wp_eq E (n1 n2 : nat) P Q :
-  (n1 = n2 → P ⊑ ▷ Q (LitV true)) →
-  (n1 ≠ n2 → P ⊑ ▷ Q (LitV false)) →
-  P ⊑ wp E ('n1 = 'n2) Q.
+  (n1 = n2 → P ⊑ ▷ Q (LitV $ LitBool true)) →
+  (n1 ≠ n2 → P ⊑ ▷ Q (LitV $ LitBool false)) →
+  P ⊑ wp E (BinOp EqOp (Lit $ LitNat n1) (Lit $ LitNat n2)) Q.
 Proof.
   intros. rewrite -wp_bin_op //; [].
   destruct (bool_decide_reflect (n1 = n2)); by eauto with omega.
 Qed.
 
-End sugar.
+End derived.

heap_lang/lifting.v

 Require Import prelude.gmap program_logic.lifting program_logic.ownership.
 Require Export program_logic.weakestpre heap_lang.heap_lang_tactics.
-Import uPred heap_lang.
+Export heap_lang. (* Prefer heap_lang names over language names. *)
+Import uPred.
 Local Hint Extern 0 (language.reducible _ _) => do_step ltac:(eauto 2).
 
 (** The substitution operation [gsubst e x ev] behaves just as [subst] but

heap_lang/notation.v

+Require Export heap_lang.derived.
+
+Delimit Scope lang_scope with L.
+Bind Scope lang_scope with expr val.
+Arguments wp {_ _} _ _%L _.
+
+Coercion LitNat : nat >-> base_lit.
+Coercion LitBool : bool >-> base_lit.
+(** 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.
+Coercion of_val : val >-> expr.
+
+(** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
+    first. *)
+(* What about Arguments for hoare triples?. *)
+Notation "' l" := (LitV l) (at level 8, format "' l") : lang_scope.
+Notation "! e" := (Load e%L) (at level 10, format "! e") : lang_scope.
+Notation "'ref' e" := (Alloc e%L) (at level 30) : lang_scope.
+Notation "e1 + e2" := (BinOp PlusOp e1%L e2%L)
+  (at level 50, left associativity) : lang_scope.
+Notation "e1 - e2" := (BinOp MinusOp e1%L e2%L)
+  (at level 50, left associativity) : lang_scope.
+Notation "e1 ≤ e2" := (BinOp LeOp e1%L e2%L) (at level 70) : lang_scope.
+Notation "e1 < e2" := (BinOp LtOp e1%L e2%L) (at level 70) : lang_scope.
+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 "'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. 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, e2 at level 200) : lang_scope.
+Notation "e1 ; e2" := (Lam "" e2%L e1%L)
+  (at level 100, e2 at level 200) : lang_scope.

heap_lang/tests.v

 (** This file is essentially a bunch of testcases. *)
 Require Import program_logic.ownership.
-Require Import heap_lang.lifting heap_lang.sugar.
-Import heap_lang uPred.
+Require Import heap_lang.notation.
+Import uPred.
 
 Module LangTests.
   Definition add := ('21 + '21)%L.