fix Pred test. also make it more complicated.

heap_lang/notation.v

@@ -14,23 +14,29 @@ Coercion of_val : val >-> expr.
 
 (** Syntax inspired by Coq/Ocaml. Constructions with higher precedence come
     first. *)
+(* We have overlapping notation for values and expressions, with the expressions
+   coming first. This way, parsing as a value will be preferred. If an expression
+   was needed, the coercion of_val will be called. *)
 (* What about Arguments for hoare triples?. *)
+Notation "' l" := (Lit l) (at level 8, format "' l") : lang_scope.
 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 "- e" := (UnOp MinusUnOp e%L) (at level 35, right associativity) : 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 "- e" := (UnOp MinusUnOp e%L) (at level 35, right associativity) : lang_scope.
-Notation "~ e" := (UnOp NegOp e%L) (at level 75, right 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.
+Notation "~ e" := (UnOp NegOp e%L) (at level 75, right associativity) : 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 "'rec:' f x := e" := (RecV 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.
 
@@ -40,6 +46,8 @@ 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 "λ: x , e" := (LamV 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)

heap_lang/tests.v

@@ -54,18 +54,22 @@ Module LiftingTests.
     by apply const_intro.
   Qed.
 
-  Definition FindPred (n2 : expr) : expr :=
-    rec: "pred" "y" :=
+  Definition FindPred : val :=
+    λ: "x", (rec: "pred" "y" :=
       let: "yp" := "y" + '1 in
-      if "yp" < n2 then "pred" "yp" else "y".
-  Definition Pred : expr :=
-    λ: "x", if "x" ≤ '0 then '0 else FindPred "x" '0.
+      if "yp" < "x" then "pred" "yp" else "y").
+  Definition Pred : val :=
+    λ: "x", if "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Q :
     (■ (n1 < n2) ∧ Q (LitV (n2 - 1))) ⊑ wp E (FindPred 'n2 'n1)%L Q.
   Proof.
+    (* FIXME there are some annoying scopes shown here: %Z, %L. *)
+    rewrite /FindPred.
+    rewrite -(wp_bindi (AppLCtx _)) -wp_let //=.
     revert n1. apply löb_all_1=>n1.
     rewrite (commutative uPred_and (■ _)%I) associative; apply const_elim_r=>?.
+    rewrite -wp_value' //.
     rewrite -wp_rec' // =>-/=.
     (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
     rewrite ->(later_intro (Q _)).
@@ -75,21 +79,33 @@ Module LiftingTests.
     rewrite -(wp_bindi (IfCtx _ _)) /= -!later_intro.
     apply wp_lt=> ?.
     - rewrite -wp_if_true.
-      rewrite -!later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
-      by rewrite left_id impl_elim_l.
+      rewrite -later_intro (forall_elim (n1 + 1)) const_equiv; last omega.
+      rewrite left_id impl_elim_l. by rewrite -(wp_bindi (AppLCtx _)).
     - assert (n1 = n2 - 1) as -> by omega.
       rewrite -wp_if_false.
       by rewrite -!later_intro -wp_value' // and_elim_r.
   Qed.
 
+  (* FIXME : For now apparent reason, I cannot prove this inline. *)
+  Lemma Pred_sub_helper n : n - 1 = - (- n + 2 - 1).
+  Proof. intros. omega. Qed.
+
   Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
   Proof.
     rewrite -wp_lam //=.
     rewrite -(wp_bindi (IfCtx _ _)) /=.
     apply later_mono, wp_le=> Hn.
     - rewrite -wp_if_true.
-      rewrite -!later_intro -wp_value' //=.
-      auto with f_equal omega.
+      rewrite -(wp_bindi (UnOpCtx _)).
+      (* FIXME use list notation. *)
+      rewrite -(wp_bind ((AppLCtx _)::(AppRCtx FindPred)::nil)).
+      rewrite -(wp_bindi (BinOpLCtx _ _)).
+      rewrite -wp_un_op //=.
+      rewrite -wp_bin_op //= -!later_intro.
+      rewrite -FindPred_spec. apply and_intro; first by (apply const_intro; omega).
+      rewrite -wp_un_op //= -later_intro.
+      assert (n - 1 = - (- n + 2 - 1)) as EQ by omega.
+      by rewrite EQ.
     - rewrite -wp_if_false.
       rewrite -!later_intro -FindPred_spec.
       auto using and_intro, const_intro with omega.