Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-coq

algebra/upred_tactics.v

 From algebra Require Export upred.
 From algebra Require Export upred_big_op.
+Import uPred.
 
 Module upred_reflection. Section upred_reflection.
   Context {M : cmraT}.
@@ -89,7 +90,7 @@ Module upred_reflection. Section upred_reflection.
   Proof.
     intros ??. rewrite !eval_flatten.
     rewrite (flatten_cancel e1 e1' ns) // (flatten_cancel e2 e2' ns) //; csimpl.
-    rewrite !fmap_app !big_sep_app. apply uPred.sep_mono_r.
+    rewrite !fmap_app !big_sep_app. apply sep_mono_r.
   Qed.
 
   Class Quote (Σ1 Σ2 : list (uPred M)) (P : uPred M) (e : expr) := {}.
@@ -144,3 +145,98 @@ Tactic Notation "ecancel" open_constr(Ps) :=
     | |- @uPred_entails ?M _ _ =>
        close Ps (@nil (uPred M)) ltac:(fun Qs => cancel Qs)
     end. 
+
+(* Some more generic uPred tactics.
+   TODO: Naming. *)
+
+Ltac revert_intros tac :=
+  lazymatch goal with
+  | |- ∀ _, _ => let H := fresh in intro H; revert_intros tac; revert H
+  | |- _ => tac
+  end.
+
+(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
+    is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
+    Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
+Ltac u_strip_later :=
+  let rec strip :=
+      lazymatch goal with
+      | |- (_ ★ _) ⊑ ▷ _  =>
+        etrans; last (eapply equiv_entails_sym, later_sep);
+        apply sep_mono; strip
+      | |- (_ ∧ _) ⊑ ▷ _  =>
+        etrans; last (eapply equiv_entails_sym, later_and);
+        apply sep_mono; strip
+      | |- (_ ∨ _) ⊑ ▷ _  =>
+        etrans; last (eapply equiv_entails_sym, later_or);
+        apply sep_mono; strip
+      | |- ▷ _ ⊑ ▷ _ => apply later_mono; reflexivity
+      | |- _ ⊑ ▷ _ => apply later_intro; reflexivity
+      end
+  in let rec shape_Q :=
+    lazymatch goal with
+    | |- _ ⊑ (_ ★ _) =>
+      (* Force the later on the LHS to be top-level, matching laters
+         below ★ on the RHS *)
+      etrans; first (apply equiv_entails, later_sep; reflexivity);
+      (* Match the arm recursively *)
+      apply sep_mono; shape_Q
+    | |- _ ⊑ (_ ∧ _) =>
+      etrans; first (apply equiv_entails, later_and; reflexivity);
+      apply sep_mono; shape_Q
+    | |- _ ⊑ (_ ∨ _) =>
+      etrans; first (apply equiv_entails, later_or; reflexivity);
+      apply sep_mono; shape_Q
+    | |- _ ⊑ ▷ _ => apply later_mono; reflexivity
+    (* We fail if we don't find laters in all branches. *)
+    end
+  in revert_intros ltac:(etrans; [|shape_Q];
+                         etrans; last eapply later_mono; first solve [ strip ]).
+
+(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
+    into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
+    the moves all the assumptions back. *)
+Ltac u_revert_all :=
+  lazymatch goal with
+  | |- ∀ _, _ => let H := fresh in intro H; u_revert_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 (apply equiv_entails_sym, left_id, _; reflexivity);
+           apply impl_elim_l'
+  end.
+
+(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
+   It applies löb where all the Coq assumptions have been turned into logical
+   assumptions, then moves all the Coq assumptions back out to the context,
+   applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
+   Coq assumption so that we end up with the same shape as where we started,
+   but with an additional assumption ★-ed to the context *)
+Ltac u_löb tac :=
+  u_revert_all;
+  (* Add a box *)
+  etrans; last (eapply always_elim; reflexivity);
+  (* We now have a goal for the form True ⊑ P, with the "original" conclusion
+     being locked. *)
+  apply löb_strong; etransitivity;
+    first (apply equiv_entails, left_id, _; reflexivity);
+  apply: always_intro;
+  (* 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
+      (* This is the "bottom" of the goal, where we see the impl introduced
+         by u_revert_all as well as the ▷ from löb_strong and the □ we added. *)
+      | |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l;
+               trans (L ★ ▷ □ R)%I;
+                 first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
+               tac
+      end
+  in go.

heap_lang/wp_tactics.v

+From algebra Require Export upred_tactics.
 From heap_lang Require Export tactics substitution.
 Import uPred.
 
-(* TODO: The next few tactics are not wp-specific at all. They should move elsewhere. *)
-
-Ltac revert_intros tac :=
-  lazymatch goal with
-  | |- ∀ _, _ => let H := fresh in intro H; revert_intros tac; revert H
-  | |- _ => tac
-  end.
-
-(** Assumes a goal of the shape P ⊑ ▷ Q. Alterantively, if Q
-    is built of ★, ∧, ∨ with ▷ in all branches; that will work, too.
-    Will turn this goal into P ⊑ Q and strip ▷ in P below ★, ∧, ∨. *)
-Ltac u_strip_later :=
-  let rec strip :=
-      lazymatch goal with
-      | |- (_ ★ _) ⊑ ▷ _  =>
-        etrans; last (eapply equiv_entails_sym, later_sep);
-        apply sep_mono; strip
-      | |- (_ ∧ _) ⊑ ▷ _  =>
-        etrans; last (eapply equiv_entails_sym, later_and);
-        apply sep_mono; strip
-      | |- (_ ∨ _) ⊑ ▷ _  =>
-        etrans; last (eapply equiv_entails_sym, later_or);
-        apply sep_mono; strip
-      | |- ▷ _ ⊑ ▷ _ => apply later_mono; reflexivity
-      | |- _ ⊑ ▷ _ => apply later_intro; reflexivity
-      end
-  in let rec shape_Q :=
-    lazymatch goal with
-    | |- _ ⊑ (_ ★ _) =>
-      (* Force the later on the LHS to be top-level, matching laters
-         below ★ on the RHS *)
-      etrans; first (apply equiv_entails, later_sep; reflexivity);
-      (* Match the arm recursively *)
-      apply sep_mono; shape_Q
-    | |- _ ⊑ (_ ∧ _) =>
-      etrans; first (apply equiv_entails, later_and; reflexivity);
-      apply sep_mono; shape_Q
-    | |- _ ⊑ (_ ∨ _) =>
-      etrans; first (apply equiv_entails, later_or; reflexivity);
-      apply sep_mono; shape_Q
-    | |- _ ⊑ ▷ _ => apply later_mono; reflexivity
-    (* We fail if we don't find laters in all branches. *)
-    end
-  in revert_intros ltac:(etrans; [|shape_Q];
-                         etrans; last eapply later_mono; first solve [ strip ]).
-
-(** Transforms a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2
-    into True ⊑ ∀..., ■?0... → ?1 → ?2, applies tac, and
-    the moves all the assumptions back. *)
-Ltac u_revert_all :=
-  lazymatch goal with
-  | |- ∀ _, _ => let H := fresh in intro H; u_revert_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 (apply equiv_entails_sym, left_id, _; reflexivity);
-           apply impl_elim_l'
-  end.
-
-(** This starts on a goal of the form ∀ ..., ?0... → ?1 ⊑ ?2.
-   It applies löb where all the Coq assumptions have been turned into logical
-   assumptions, then moves all the Coq assumptions back out to the context,
-   applies [tac] on the goal (now of the form _ ⊑ _), and then reverts the
-   Coq assumption so that we end up with the same shape as where we started,
-   but with an additional assumption ★-ed to the context *)
-Ltac u_löb tac :=
-  u_revert_all;
-  (* Add a box *)
-  etrans; last (eapply always_elim; reflexivity);
-  (* We now have a goal for the form True ⊑ P, with the "original" conclusion
-     being locked. *)
-  apply löb_strong; etransitivity;
-    first (apply equiv_entails, left_id, _; reflexivity);
-  apply: always_intro;
-  (* 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
-      (* This is the "bottom" of the goal, where we see the impl introduced
-         by u_revert_all as well as the ▷ from löb_strong and the □ we added. *)
-      | |- ▷ □ ?R ⊑ (?L → _) => apply impl_intro_l;
-               trans (L ★ ▷ □ R)%I;
-                 first (eapply equiv_entails, always_and_sep_r, _; reflexivity);
-               tac
-      end
-  in go.
-
 (** wp-specific helper tactics *)
 (* First try to productively strip off laters; if that fails, at least
    cosmetically get rid of laters in the conclusion. *)