From 0a44697a640105e7e86785e1f1b4fbcb21e2745b Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 16 Feb 2016 00:33:14 +0100
Subject: [PATCH] wp_tactics: use wp_value afterwards instead of before.

---
 heap_lang/tests.v      |  2 +-
 heap_lang/wp_tactics.v | 33 +++++++++++++++++++++------------
 2 files changed, 22 insertions(+), 13 deletions(-)

diff --git a/heap_lang/tests.v b/heap_lang/tests.v
index bc0495c23..4bb9ca606 100644
--- a/heap_lang/tests.v
+++ b/heap_lang/tests.v
@@ -69,7 +69,7 @@ Section LiftingTests.
     - wp_if. rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
       by rewrite left_id impl_elim_l.
     - assert (n1 = n2 - 1) as -> by omega.
-      wp_if. wp_value. auto with I.
+      wp_if. auto with I.
   Qed.
 
   Lemma Pred_spec n E Q : ▷ Q (LitV (n - 1)) ⊑ wp E (Pred 'n)%L Q.
diff --git a/heap_lang/wp_tactics.v b/heap_lang/wp_tactics.v
index 5d0b89a6d..7d72cbe62 100644
--- a/heap_lang/wp_tactics.v
+++ b/heap_lang/wp_tactics.v
@@ -11,49 +11,58 @@ Ltac wp_bind K :=
   | [] => idtac
   | _ => etransitivity; [|apply (wp_bind K)]; simpl
   end.
+Ltac wp_finish :=
+  let rec go :=
+  match goal with
+  | |- ∀ _, _ => let H := fresh in intro H; go; revert H
+  | |- _ ⊑ ▷ _ => etransitivity; [|apply later_mono; go; reflexivity]
+  | |- _ ⊑ wp _ _ _ => etransitivity; [|eapply wp_value; reflexivity]; simpl
+  | _ => idtac
+  end in simpl; go.
 
 Tactic Notation "wp_value" :=
   match goal with
-  | |- _ ⊑ wp ?E ?e ?Q => etransitivity; [|by eapply wp_value]; simpl
+  | |- _ ⊑ wp ?E ?e ?Q => etransitivity; [|eapply wp_value; reflexivity]; simpl
   end.
 Tactic Notation "wp_rec" "!" :=
-  repeat wp_value;
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
-    | App (Rec _ _ _) _ => wp_bind K; etransitivity; [|by eapply wp_rec]; simpl
+    | App (Rec _ _ _) _ =>
+       wp_bind K; etransitivity; [|eapply wp_rec; reflexivity]; wp_finish
     end)
   end.
 Tactic Notation "wp_rec" := wp_rec!; wp_strip_later.
 Tactic Notation "wp_bin_op" "!" :=
-  repeat wp_value;
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
-    | BinOp LtOp _ _ => wp_bind K; apply wp_lt; [|]
-    | BinOp LeOp _ _ => wp_bind K; apply wp_le; [|]
-    | BinOp EqOp _ _ => wp_bind K; apply wp_eq; [|]
-    | BinOp _ _ _ => wp_bind K; etransitivity; [|by eapply wp_bin_op]; simpl
+    | BinOp LtOp _ _ => wp_bind K; apply wp_lt; wp_finish
+    | BinOp LeOp _ _ => wp_bind K; apply wp_le; wp_finish
+    | BinOp EqOp _ _ => wp_bind K; apply wp_eq; wp_finish
+    | BinOp _ _ _ =>
+       wp_bind K; etransitivity; [|eapply wp_bin_op; reflexivity]; wp_finish
     end)
   end.
 
 Tactic Notation "wp_bin_op" := wp_bin_op!; wp_strip_later.
 Tactic Notation "wp_un_op" "!" :=
-  repeat wp_value;
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
-    | UnOp _ _ => wp_bind K; etransitivity; [|by eapply wp_un_op]; simpl
+    | UnOp _ _ =>
+       wp_bind K; etransitivity; [|eapply wp_un_op; reflexivity]; wp_finish
     end)
   end.
 Tactic Notation "wp_un_op" := wp_un_op!; wp_strip_later.
 Tactic Notation "wp_if" "!" :=
-  repeat wp_value;
+  try wp_value;
   match goal with
   | |- _ ⊑ wp ?E ?e ?Q => reshape_expr e ltac:(fun K e' =>
     match eval cbv in e' with
     | If _ _ _ =>
-       wp_bind K; etransitivity; [|by apply wp_if_true || by apply wp_if_false]
+       wp_bind K;
+       etransitivity; [|apply wp_if_true || apply wp_if_false]; wp_finish
     end)
   end.
 Tactic Notation "wp_if" := wp_if!; wp_strip_later.
-- 
GitLab