Commit 2821e99e authored by Robbert Krebbers's avatar Robbert Krebbers

Also keep track of whether a hypothesis is persistent in IntoWand.

This enables things like `iSpecialize ("H2" with "H1") in the below:

  "H1" : P
  ---------□
  "H2" : □ P -∗ Q
  ---------∗
  R
parent fbc6b6b6
......@@ -155,7 +155,8 @@ Section proofmode_classes.
Proof. rewrite /FromAssumption=>->. apply bupd_fupd. Qed.
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').
WandWeaken false P Q P' Q'
WandWeaken' false P Q (|={E1,E2}=> P') (|={E1,E2}=> Q').
Proof.
rewrite /WandWeaken' /WandWeaken=>->. apply wand_intro_l. by rewrite fupd_wand_r.
Qed.
......
......@@ -248,57 +248,66 @@ Global Instance from_later_exist {A} n (Φ Ψ : A → uPred M) :
Proof. intros ?. rewrite /FromLaterN laterN_exist=> ?. by apply exist_mono. Qed.
(* IntoWand *)
Global Instance wand_weaken_assumption P1 P2 Q :
FromAssumption false P2 P1 WandWeaken P1 Q P2 Q | 0.
Global Instance wand_weaken_assumption p P1 P2 Q :
FromAssumption p P2 P1 WandWeaken p P1 Q P2 Q | 0.
Proof. by rewrite /WandWeaken /FromAssumption /= =>->. Qed.
Global Instance wand_weaken_later P Q P' Q' :
WandWeaken P Q P' Q' WandWeaken' P Q ( P') ( Q').
Global Instance wand_weaken_later p P Q P' Q' :
WandWeaken p P Q P' Q' WandWeaken' p P Q ( P') ( Q').
Proof.
rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -later_wand -later_intro.
rewrite /WandWeaken' /WandWeaken=> ->.
by rewrite always_if_later -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').
Global Instance wand_weaken_laterN p n P Q P' Q' :
WandWeaken p P Q P' Q' WandWeaken' p P Q (^n P') (^n Q').
Proof.
rewrite /WandWeaken' /WandWeaken=> ->. by rewrite -laterN_wand -laterN_intro.
rewrite /WandWeaken' /WandWeaken=> ->.
by rewrite always_if_laterN -laterN_wand -laterN_intro.
Qed.
Global Instance bupd_weaken_laterN P Q P' Q' :
WandWeaken P Q P' Q' WandWeaken' P Q (|==> P') (|==> Q').
Global Instance bupd_weaken_laterN p P Q P' Q' :
WandWeaken false P Q P' Q' WandWeaken' p P Q (|==> P') (|==> Q').
Proof.
rewrite /WandWeaken' /WandWeaken=> ->.
apply wand_intro_l. by rewrite bupd_wand_r.
apply wand_intro_l. by rewrite always_if_elim bupd_wand_r.
Qed.
Global Instance into_wand_wand P P' Q Q' :
WandWeaken P Q P' Q' IntoWand (P - Q) P' Q'.
Global Instance into_wand_wand p P P' Q Q' :
WandWeaken p P Q P' Q' IntoWand p (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'.
Global Instance into_wand_impl p P P' Q Q' :
WandWeaken p P Q P' Q' IntoWand p (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'.
Global Instance into_wand_iff_l p P P' Q Q' :
WandWeaken p P Q P' Q' IntoWand p (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'.
Global Instance into_wand_iff_r p P P' Q Q' :
WandWeaken p Q P Q' P' IntoWand p (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.
Global Instance into_wand_forall {A} p (Φ : A uPred M) P Q x :
IntoWand p (Φ x) P Q IntoWand p ( x, Φ x) P Q.
Proof. rewrite /IntoWand=> <-. apply forall_elim. Qed.
Global Instance into_wand_always R P Q : IntoWand R P Q IntoWand ( R) P Q.
Global Instance into_wand_always p R P Q :
IntoWand p R P Q IntoWand p ( R) P Q.
Proof. rewrite /IntoWand=> ->. apply always_elim. 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_later p R P Q :
IntoWand p R P Q IntoWand p ( R) ( P) ( Q).
Proof. rewrite /IntoWand=> ->. by rewrite always_if_later -later_wand. Qed.
Global Instance into_wand_laterN p n R P Q :
IntoWand p R P Q IntoWand p (^n R) (^n P) (^n Q).
Proof. rewrite /IntoWand=> ->. by rewrite always_if_laterN -laterN_wand. Qed.
Global Instance into_wand_bupd R P Q :
IntoWand R P Q IntoWand (|==> R) (|==> P) (|==> Q).
IntoWand false R P Q IntoWand false (|==> R) (|==> P) (|==> Q).
Proof.
rewrite /IntoWand=> ->. apply wand_intro_l. by rewrite bupd_sep wand_elim_r.
Qed.
Global Instance into_wand_bupd_persistent R P Q :
IntoWand true R P Q IntoWand true (|==> R) P (|==> Q).
Proof.
rewrite /IntoWand=>->. apply wand_intro_l. by rewrite bupd_frame_l wand_elim_r.
Qed.
(* FromAnd *)
Global Instance from_and_and p P1 P2 : FromAnd p (P1 P2) P1 P2 | 100.
......
......@@ -71,17 +71,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 WandWeaken {M} (p : bool) (P Q P' Q' : uPred M) :=
wand_weaken : (P - Q) (?p P' - Q').
Hint Mode WandWeaken + + - - - - : typeclass_instances.
Class WandWeaken' {M} (p : bool) (P Q P' Q' : uPred M) :=
wand_weaken' :> WandWeaken p P Q P' Q'.
Hint Mode WandWeaken' + + - - ! - : typeclass_instances.
Hint Mode WandWeaken' + + - - - ! : typeclass_instances.
Class IntoWand {M} (p : bool) (R P Q : uPred M) := into_wand : R ?p P - Q.
Arguments into_wand {_} _ _ _ _ {_}.
Hint Mode IntoWand + + ! - - : typeclass_instances.
Class FromAnd {M} (p : bool) (P Q1 Q2 : uPred M) :=
from_and : (if p then Q1 Q2 else Q1 Q2) P.
......
......@@ -542,7 +542,7 @@ but it is doing some work to keep the order of hypotheses preserved. *)
Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
envs_lookup_delete i Δ = Some (p, P1, Δ')
envs_lookup j (if p then Δ else Δ') = Some (q, R)
IntoWand R P1 P2
IntoWand p R P1 P2
match p with
| true => envs_simple_replace j q (Esnoc Enil j P2) Δ
| false => envs_replace j q false (Esnoc Enil j P2) Δ'
......@@ -552,16 +552,17 @@ Lemma tac_specialize Δ Δ' Δ'' i p j q P1 P2 R Q :
Proof.
intros [? ->]%envs_lookup_delete_Some ??? <-. destruct p.
- rewrite envs_lookup_persistent_sound // envs_simple_replace_sound //; simpl.
rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
by rewrite right_id wand_elim_r.
rewrite right_id assoc (into_wand _ R) /=. destruct q; simpl.
+ by rewrite always_wand always_always !wand_elim_r.
+ by rewrite !wand_elim_r.
- rewrite envs_lookup_sound //; simpl.
rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
by rewrite right_id assoc (into_wand R) always_if_elim wand_elim_r wand_elim_r.
by rewrite right_id assoc (into_wand _ R) always_if_elim wand_elim_r wand_elim_r.
Qed.
Lemma tac_specialize_assert Δ Δ' Δ1 Δ2' j q lr js R P1 P2 P1' Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand R P1 P2 ElimModal P1' P1 Q Q
IntoWand false R P1 P2 ElimModal P1' P1 Q Q
('(Δ1,Δ2) envs_split lr js Δ';
Δ2' envs_app false (Esnoc Enil j P2) Δ2;
Some (Δ1,Δ2')) = Some (Δ1,Δ2') (* does not preserve position of [j] *)
......@@ -572,7 +573,7 @@ Proof.
destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
rewrite right_id (into_wand _ R) HP1 assoc -(comm _ P1') -assoc.
rewrite -(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
......@@ -582,7 +583,7 @@ Proof. by unlock. Qed.
Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand R P1 P2
IntoWand false R P1 P2
ElimModal P1' P1 Q Q
(Δ' P1' locked Q')
Q' = (P2 - Q)%I
......@@ -590,25 +591,25 @@ Lemma tac_specialize_frame Δ Δ' j q R P1 P2 P1' Q Q' :
Proof.
intros [? ->]%envs_lookup_delete_Some ?? HPQ ->.
rewrite envs_lookup_sound //. rewrite HPQ -lock.
rewrite (into_wand R) assoc -(comm _ P1') -assoc always_if_elim.
rewrite (into_wand _ R) assoc -(comm _ P1') -assoc always_if_elim.
rewrite -{2}(elim_modal P1' P1 Q Q). apply sep_mono_r, wand_intro_l.
by rewrite assoc !wand_elim_r.
Qed.
Lemma tac_specialize_assert_pure Δ Δ' j q R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R)
IntoWand R P1 P2 FromPure P1 φ
IntoWand false R P1 P2 FromPure P1 φ
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'
φ (Δ' Q) Δ Q.
Proof.
intros. rewrite envs_simple_replace_sound //; simpl.
rewrite right_id (into_wand R) -(from_pure P1) pure_True //.
rewrite right_id (into_wand _ R) -(from_pure P1) pure_True //.
by rewrite wand_True wand_elim_r.
Qed.
Lemma tac_specialize_assert_persistent Δ Δ' Δ'' j q P1 P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
IntoWand R P1 P2 PersistentP P1
IntoWand false R P1 P2 PersistentP P1
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ''
(Δ' P1) (Δ'' Q) Δ Q.
Proof.
......@@ -617,7 +618,7 @@ Proof.
rewrite -(idemp uPred_and (envs_delete _ _ _)).
rewrite {1}HP1 (persistentP P1) always_and_sep_l assoc.
rewrite envs_simple_replace_sound' //; simpl.
rewrite right_id (into_wand R) (always_elim_if q) -always_if_sep wand_elim_l.
rewrite right_id (into_wand _ R) (always_elim_if q) -always_if_sep wand_elim_l.
by rewrite wand_elim_r.
Qed.
......@@ -704,11 +705,11 @@ Proof.
Qed.
Lemma tac_apply Δ Δ' i p R P1 P2 :
envs_lookup_delete i Δ = Some (p, R, Δ') IntoWand R P1 P2
envs_lookup_delete i Δ = Some (p, R, Δ') IntoWand false R P1 P2
(Δ' P1) Δ P2.
Proof.
intros ?? HP1. rewrite envs_lookup_delete_sound' //.
by rewrite (into_wand R) HP1 wand_elim_l.
by rewrite (into_wand _ R) HP1 wand_elim_l.
Qed.
(** * Rewriting *)
......
......@@ -176,4 +176,7 @@ Lemma test_split_box (P Q : uPred M) :
P - (P P).
Proof. iIntros "#?". by iSplit. Qed.
Lemma test_specialize_persistent (P Q : uPred M) :
P - ( P - Q) - Q.
Proof. iIntros "#HP HPQ". by iSpecialize ("HPQ" with "HP"). Qed.
End tests.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment