make wp_rec also apply löb

algebra/upred.v

@@ -217,6 +217,10 @@ Notation "✓ x" := (uPred_valid x) (at level 20) : uPred_scope.
 Definition uPred_iff {M} (P Q : uPred M) : uPred M := ((P → Q) ∧ (Q → P))%I.
 Infix "↔" := uPred_iff : uPred_scope.
 
+Lemma uPred_lock_conclusion {M} (P Q : uPred M) :
+  P ⊑ locked Q → P ⊑ Q.
+Proof. by rewrite -lock. Qed.
+
 Class TimelessP {M} (P : uPred M) := timelessP : ▷ P ⊑ (P ∨ ▷ False).
 Arguments timelessP {_} _ {_} _ _ _ _.
 Class AlwaysStable {M} (P : uPred M) := always_stable : P ⊑ □ P.
@@ -393,6 +397,8 @@ Lemma or_intro_r' P Q R : P ⊑ R → P ⊑ (Q ∨ R).
 Proof. intros ->; apply or_intro_r. Qed.
 Lemma exist_intro' {A} P (Ψ : A → uPred M) a : P ⊑ Ψ a → P ⊑ (∃ a, Ψ a).
 Proof. intros ->; apply exist_intro. Qed.
+Lemma forall_elim' {A} P (Ψ : A → uPred M) : P ⊑ (∀ a, Ψ a) → (∀ a, P ⊑ Ψ a).
+Proof. move=>EQ ?. rewrite EQ. by apply forall_elim. Qed.
 
 Hint Resolve or_elim or_intro_l' or_intro_r'.
 Hint Resolve and_intro and_elim_l' and_elim_r'.
@@ -413,24 +419,6 @@ Proof. intros HPQ; apply impl_elim with P; rewrite -?HPQ; auto. Qed.
 Lemma entails_impl P Q : (P ⊑ Q) → True ⊑ (P → Q).
 Proof. auto using impl_intro_l. Qed.
 
-Lemma const_intro_l φ Q R : φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
-Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R.
-Proof. intros ? <-; auto using const_intro. Qed.
-Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
-Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.
-Proof. intros; apply const_elim with φ; eauto. Qed.
-Lemma const_equiv (φ : Prop) : φ → (■ φ : uPred M)%I ≡ True%I.
-Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
-Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
-Proof. intros ->; apply eq_refl. Qed.
-Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
-Proof.
-  apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl.
-  intros n; solve_proper.
-Qed.
-
 Lemma const_mono φ1 φ2 : (φ1 → φ2) → ■ φ1 ⊑ ■ φ2.
 Proof. intros; apply const_elim with φ1; eauto using const_intro. Qed.
 Lemma and_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ∧ P') ⊑ (Q ∧ Q').
@@ -544,6 +532,29 @@ Proof.
   rewrite -(comm _ P) and_exist_l. apply exist_proper=>a. by rewrite comm.
 Qed.
 
+Lemma const_intro_l φ Q R : φ → (■φ ∧ Q) ⊑ R → Q ⊑ R.
+Proof. intros ? <-; auto using const_intro. Qed.
+Lemma const_intro_r φ Q R : φ → (Q ∧ ■φ) ⊑ R → Q ⊑ R.
+Proof. intros ? <-; auto using const_intro. Qed.
+Lemma const_intro_impl φ Q R : φ → Q ⊑ (■ φ → R) → Q ⊑ R.
+Proof.
+  intros ? ->; apply (const_intro_l φ); first done. by rewrite impl_elim_r.
+Qed.
+Lemma const_elim_l φ Q R : (φ → Q ⊑ R) → (■ φ ∧ Q) ⊑ R.
+Proof. intros; apply const_elim with φ; eauto. Qed.
+Lemma const_elim_r φ Q R : (φ → Q ⊑ R) → (Q ∧ ■ φ) ⊑ R.
+Proof. intros; apply const_elim with φ; eauto. Qed.
+Lemma const_equiv (φ : Prop) : φ → (■ φ : uPred M)%I ≡ True%I.
+Proof. intros; apply (anti_symm _); auto using const_intro. Qed.
+Lemma equiv_eq {A : cofeT} P (a b : A) : a ≡ b → P ⊑ (a ≡ b).
+Proof. intros ->; apply eq_refl. Qed.
+Lemma eq_sym {A : cofeT} (a b : A) : (a ≡ b) ⊑ (b ≡ a).
+Proof.
+  apply (eq_rewrite a b (λ b, b ≡ a)%I); auto using eq_refl.
+  intros n; solve_proper.
+Qed.
+
+
 (* BI connectives *)
 Lemma sep_mono P P' Q Q' : P ⊑ Q → P' ⊑ Q' → (P ★ P') ⊑ (Q ★ Q').
 Proof.

barrier/barrier.v

@@ -236,14 +236,7 @@ Section proof.
   Lemma wait_spec l P (Φ : val → iProp) :
     heapN ⊥ N → (recv l P ★ (P -★ Φ '())) ⊑ || wait (LocV l) {{ Φ }}.
   Proof.
-    rename P into R.
-    intros Hdisj.
-    (* TODO we probably want a tactic or lemma that does the next 2 lines for us.
-       It should be general enough to also cover FindPred_spec. Probably this
-       should be the default behavior of wp_rec - since this is what we need every time
-       we prove a recursive function correct. *)
-    rewrite /wait. rewrite [(_ ★ _)%I](pvs_intro ⊤).
-    apply löb_strong_sep. rewrite pvs_frame_r. apply wp_strip_pvs. wp_rec.
+    rename P into R. intros Hdisj. wp_rec.
     rewrite {1}/recv /barrier_ctx. rewrite !sep_exist_r.
     apply exist_elim=>γ. rewrite !sep_exist_r. apply exist_elim=>P.
     rewrite !sep_exist_r. apply exist_elim=>Q. rewrite !sep_exist_r.
@@ -258,8 +251,7 @@ Section proof.
     eapply wp_load; eauto with I ndisj.
     rewrite -!assoc. apply sep_mono_r. etrans; last eapply later_mono.
     { (* Is this really the best way to strip the later? *)
-      erewrite later_sep. apply sep_mono_r. rewrite !assoc. erewrite later_sep.
-      apply sep_mono_l, later_intro. }
+      erewrite later_sep. apply sep_mono_r, later_intro. }
     apply wand_intro_l. destruct p.
     { (* a Low state. The comparison fails, and we recurse. *)
       rewrite -(exist_intro (State Low I)) -(exist_intro {[ Change i ]}).
@@ -267,7 +259,7 @@ Section proof.
       rewrite left_id -[(▷ barrier_inv _ _ _)%I]later_intro {3}/barrier_inv.
       rewrite -!assoc. apply sep_mono_r, sep_mono_r, wand_intro_l.
       wp_op; first done. intros _. wp_if. rewrite !assoc.
-      eapply wand_apply_r'; first done.
+      rewrite -{2}pvs_wp. apply pvs_wand_r.
       rewrite -(exist_intro γ) -(exist_intro P) -(exist_intro Q) -(exist_intro i).
       rewrite !assoc. do 3 (rewrite -pvs_frame_r; apply sep_mono_l).
       rewrite [(_ ★ heap_ctx _)%I]comm -!assoc -pvs_frame_l. apply sep_mono_r.

heap_lang/tests.v

@@ -49,17 +49,13 @@ Section LiftingTests.
       if: "x" ≤ '0 then -FindPred (-"x" + '2) '0 else FindPred "x" '0.
 
   Lemma FindPred_spec n1 n2 E Φ :
-    (■ (n1 < n2) ∧ Φ '(n2 - 1)) ⊑ || FindPred 'n2 'n1 @ E {{ Φ }}.
+    n1 < n2 → 
+    Φ '(n2 - 1) ⊑ || FindPred 'n2 'n1 @ E {{ Φ }}.
   Proof.
-    revert n1; apply löb_all_1=>n1.
-    rewrite (comm uPred_and (■ _)%I) assoc; apply const_elim_r=>?.
-    (* first need to do the rec to get a later *)
-    wp_rec>. 
-    (* FIXME: ssr rewrite fails with "Error: _pattern_value_ is used in conclusion." *)
-    rewrite ->(later_intro (Φ _)); rewrite -!later_and; apply later_mono.
+    revert n1. wp_rec=>n1 Hn.
     wp_let. wp_op. wp_let. wp_op=> ?; wp_if.
     - rewrite (forall_elim (n1 + 1)) const_equiv; last omega.
-      by rewrite left_id impl_elim_l.
+      by rewrite left_id wand_elim_r.
     - assert (n1 = n2 - 1) as -> by omega; auto with I.
   Qed.
 

heap_lang/wp_tactics.v

@@ -15,6 +15,27 @@ Ltac wp_strip_later :=
     end
   in revert_intros ltac:(etrans; [|go]).
 
+(* ssreflect-locks the part after the ⊑ *)
+(* FIXME: I tried doing a lazymatch to only apply the tactic if the goal has shape ⊑,
+   bit the match is executed *before* doing the recursion... WTF? *)
+Ltac uLock_goal := revert_intros ltac:(apply uPred_lock_conclusion).
+
+(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
+    into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
+    the moves all the assumptions back. *)
+Ltac uRevert_all :=
+  lazymatch goal with
+  | |- ∀ _, _ => let H := fresh in intro H; uRevert_all;
+                 (* TODO: Really, we should distinguish based on whether this is a
+                    dependent function type or not. Right now, we distinguish based
+                    on the sort of the argument, which is suboptimal. *)
+                 first [ apply (const_intro_impl _ _ _ H); clear H
+                       | revert H; apply forall_elim']
+  | |- ?C ⊑ _ => trans (True ★ C)%I;
+                 first (rewrite [(True ★ C)%I]left_id; reflexivity);
+                 apply wand_elim_l'
+  end.
+
 Ltac wp_bind K :=
   lazymatch eval hnf in K with
   | [] => idtac
@@ -33,15 +54,34 @@ Ltac wp_finish :=
   | _ => idtac
   end in simpl; revert_intros go.
 
-Tactic Notation "wp_rec" ">" :=
-  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; etrans; [|eapply wp_rec; reflexivity]; wp_finish
-    end)
-  end.
-Tactic Notation "wp_rec" := wp_rec>; wp_strip_later.
+Tactic Notation "wp_rec" :=
+  uLock_goal; uRevert_all;
+  (* We now have a goal for the form True ⊑ P, with the "original" conclusion
+     being locked. *)
+  apply löb_strong; etransitivity;
+    first (apply equiv_spec; symmetry; apply (left_id _ _ _)); [];
+  (* Now introduce again all the things that we reverted, and at the bottom, do the work *)
+  let rec go :=
+      lazymatch goal with
+      | |- _ ⊑ (∀ _, _) => apply forall_intro;
+               let H := fresh in intro H; go; revert H
+      | |- _ ⊑ (■ _ → _) => apply impl_intro_l, const_elim_l;
+               let H := fresh in intro H; go; revert H
+      | |- ▷ ?R ⊑ (?L -★ locked _) => apply wand_intro_l;
+               (* TODO: Do sth. more robust than rewriting. *)
+               trans (▷ (L ★ R))%I; first (rewrite later_sep -(later_intro L); reflexivity );
+               unlock;
+               (* Find the redex and apply wp_rec *)
+               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; etrans; [|eapply wp_rec; reflexivity]; wp_finish
+                        end)
+               end;
+               apply later_mono
+      end
+  in go.
 
 Tactic Notation "wp_lam" ">" :=
   match goal with