Fix issue #68.

TODO: document the setup of the IntoWand and WandWeaken type classes
and the tricks using Hint Mode.

theories/base_logic/lib/fancy_updates.v

@@ -154,10 +154,10 @@ Section proofmode_classes.
     FromAssumption p P (|==> Q) → FromAssumption p P (|={E}=> Q)%I.
   Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
 
-  Global Instance into_wand_fupd E1 E2 R P Q :
-    IntoWand R P Q → IntoWand' R (|={E1,E2}=> P) (|={E1,E2}=> Q) | 100.
+  Global Instance wand_weaken_fupd E1 E2 P Q P' Q' :
+    WandWeaken P Q P' Q' → WandWeaken' P Q (|={E1,E2}=> P') (|={E1,E2}=> Q').
   Proof.
-    rewrite /IntoWand' /IntoWand=>->. apply wand_intro_l. by rewrite fupd_wand_r.
+    rewrite /WandWeaken' /WandWeaken=>->. apply wand_intro_l. by rewrite fupd_wand_r.
   Qed.
 
   Global Instance from_sep_fupd E P Q1 Q2 :

theories/proofmode/class_instances.v

@@ -18,6 +18,12 @@ Proof. rewrite /FromAssumption=><-. by rewrite always_elim. Qed.
 Global Instance from_assumption_always_r P Q :
   FromAssumption true P Q → FromAssumption true P (□ Q).
 Proof. rewrite /FromAssumption=><-. by rewrite always_always. Qed.
+Global Instance from_assumption_later p P Q :
+  FromAssumption p P Q → FromAssumption p P (▷ Q)%I.
+Proof. rewrite /FromAssumption=>->. apply later_intro. Qed.
+Global Instance from_assumption_laterN n p P Q :
+  FromAssumption p P Q → FromAssumption p P (▷^n Q)%I.
+Proof. rewrite /FromAssumption=>->. apply laterN_intro. Qed.
 Global Instance from_assumption_bupd p P Q :
   FromAssumption p P Q → FromAssumption p P (|==> Q)%I.
 Proof. rewrite /FromAssumption=>->. apply bupd_intro. Qed.
@@ -209,16 +215,38 @@ Global Instance from_later_sep n P1 P2 Q1 Q2 :
 Proof. intros ??; red. by rewrite laterN_sep; apply sep_mono. Qed.
 
 (* IntoWand *)
-Global Instance into_wand_wand P Q Q' :
-  FromAssumption false Q Q' → IntoWand (P -∗ Q) P Q'.
-Proof. by rewrite /FromAssumption /IntoWand /= => ->. Qed.
-Global Instance into_wand_impl P Q Q' :
-  FromAssumption false Q Q' → IntoWand (P → Q) P Q'.
-Proof. rewrite /FromAssumption /IntoWand /= => ->. by rewrite impl_wand. Qed.
-Global Instance into_wand_iff_l P Q : IntoWand (P ↔ Q) P Q.
-Proof. by apply and_elim_l', impl_wand. Qed.
-Global Instance into_wand_iff_r P Q : IntoWand (P ↔ Q) Q P.
-Proof. apply and_elim_r', impl_wand. Qed.
+Global Instance wand_weaken_exact P Q : WandWeaken P Q P Q.
+Proof. done. Qed.
+Global Instance wand_weaken_later P Q P' Q' :
+  WandWeaken P Q P' Q' → WandWeaken' P Q (▷ P') (▷ Q').
+Proof.
+  rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -later_wand -later_intro.
+Qed.
+Global Instance wand_weaken_laterN n P Q P' Q' :
+  WandWeaken P Q P' Q' → WandWeaken' P Q (▷^n P') (▷^n Q').
+Proof.
+  rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -laterN_wand -laterN_intro.
+Qed.
+Global Instance bupd_weaken_laterN P Q P' Q' :
+  WandWeaken P Q P' Q' → WandWeaken' P Q (|==> P') (|==> Q').
+Proof.
+  rewrite /WandWeaken' /WandWeaken=> ->.
+  apply wand_intro_l. by rewrite bupd_wand_r.
+Qed.
+
+Global Instance into_wand_wand P P' Q Q' :
+  WandWeaken P Q P' Q' → IntoWand (P -∗ Q) P' Q'.
+Proof. done. Qed.
+Global Instance into_wand_impl P P' Q Q' :
+  WandWeaken P Q P' Q' → IntoWand (P → Q) P' Q'.
+Proof. rewrite /WandWeaken /IntoWand /= => <-. apply impl_wand. Qed.
+
+Global Instance into_wand_iff_l P P' Q Q' :
+  WandWeaken P Q P' Q' → IntoWand (P ↔ Q) P' Q'.
+Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_l', impl_wand. Qed.
+Global Instance into_wand_iff_r P P' Q Q' :
+  WandWeaken Q P Q' P' → IntoWand (P ↔ Q) Q' P'.
+Proof. rewrite /WandWeaken /IntoWand=> <-. apply and_elim_r', impl_wand. Qed.
 
 Global Instance into_wand_forall {A} (Φ : A → uPred M) P Q x :
   IntoWand (Φ x) P Q → IntoWand (∀ x, Φ x) P Q.
@@ -226,20 +254,16 @@ Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
 Global Instance into_wand_always R P Q : IntoWand R P Q → IntoWand (□ R) P Q.
 Proof. rewrite /IntoWand=> ->. apply always_elim. Qed.
 
-Global Instance into_wand_later (R1 R2 P Q : uPred M) :
-  IntoLaterN 1 R1 R2 → IntoWand R2 P Q → IntoWand' R1 (▷ P) (▷ Q) | 99.
-Proof.
-  rewrite /IntoLaterN /IntoWand' /IntoWand=> -> ->. by rewrite -later_wand.
-Qed.
-Global Instance into_wand_laterN n (R1 R2 P Q : uPred M) :
-  IntoLaterN n R1 R2 → IntoWand R2 P Q → IntoWand' R1 (▷^n P) (▷^n Q) | 100.
-Proof.
-  rewrite /IntoLaterN /IntoWand' /IntoWand=> -> ->. by rewrite -laterN_wand.
-Qed.
+Global Instance into_wand_later R P Q :
+  IntoWand R P Q → IntoWand (▷ R) (▷ P) (▷ Q).
+Proof. rewrite /IntoWand=> ->. by rewrite -later_wand. Qed.
+Global Instance into_wand_laterN n R P Q :
+  IntoWand R P Q → IntoWand (▷^n R) (▷^n P) (▷^n Q).
+Proof. rewrite /IntoWand=> ->. by rewrite -laterN_wand. Qed.
 Global Instance into_wand_bupd R P Q :
-  IntoWand R P Q → IntoWand' R (|==> P) (|==> Q) | 98.
+  IntoWand R P Q → IntoWand (|==> R) (|==> P) (|==> Q).
 Proof.
-  rewrite /IntoWand' /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_wand_r.
+  rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
 Qed.
 
 (* FromAnd *)

theories/proofmode/classes.v

@@ -27,15 +27,18 @@ Class FromLaterN {M} (n : nat) (P Q : uPred M) := from_laterN : ▷^n Q ⊢ P.
 Arguments from_laterN {_} _ _ _ {_}.
 Hint Mode FromLaterN + - ! - : typeclass_instances.
 
+Class WandWeaken {M} (P Q P' Q' : uPred M) := wand_weaken : (P -∗ Q) ⊢ (P' -∗ Q').
+Hint Mode WandWeaken + - - - - : typeclass_instances.
+
+Class WandWeaken' {M} (P Q P' Q' : uPred M) :=
+  wand_weaken' :> WandWeaken P Q P' Q'.
+Hint Mode WandWeaken' + - - ! - : typeclass_instances.
+Hint Mode WandWeaken' + - - - ! : typeclass_instances.
+
 Class IntoWand {M} (R P Q : uPred M) := into_wand : R ⊢ P -∗ Q.
 Arguments into_wand {_} _ _ _ {_}.
 Hint Mode IntoWand + ! - - : typeclass_instances.
 
-Class IntoWand' {M} (R P Q : uPred M) := into_wand' :> IntoWand R P Q.
-Arguments into_wand' {_} _ _ _ {_}.
-Hint Mode IntoWand' + ! ! - : typeclass_instances.
-Hint Mode IntoWand' + ! - ! : typeclass_instances.
-
 Class FromAnd {M} (P Q1 Q2 : uPred M) := from_and : Q1 ∧ Q2 ⊢ P.
 Arguments from_and {_} _ _ _ {_}.
 Hint Mode FromAnd + ! - - : typeclass_instances.