Commit 1aae01e6 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename type classes in proof mode.

We are now using the prefixes Into, From, and Is (the first two are
inspired by the names of some traits in the Rust stdlib), and hopefully
doing that consistenly.
parent b5a23477
......@@ -12,14 +12,14 @@ Implicit Types P Q : iPropG heap_lang Σ.
Implicit Types Φ : val iPropG heap_lang Σ.
Implicit Types Δ : envs (iResUR heap_lang (globalF Σ)).
Global Instance sep_destruct_mapsto l q v :
SepDestruct false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /SepDestruct heap_mapsto_op_split. Qed.
Global Instance into_sep_mapsto l q v :
IntoSep false (l {q} v) (l {q/2} v) (l {q/2} v).
Proof. by rewrite /IntoSep heap_mapsto_op_split. Qed.
Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
to_val e = Some v
(Δ heap_ctx N) nclose N E
StripLaterEnvs Δ Δ'
IntoLaterEnvs Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
(Δ'' Φ (LitV (LitLoc l))))
......@@ -27,60 +27,60 @@ Lemma tac_wp_alloc Δ Δ' N E j e v Φ :
Proof.
intros ???? HΔ. rewrite -wp_alloc // -always_and_sep_l.
apply and_intro; first done.
rewrite strip_later_env_sound; apply later_mono, forall_intro=> l.
rewrite into_later_env_sound; apply later_mono, forall_intro=> l.
destruct (HΔ l) as (Δ''&?&HΔ'). rewrite envs_app_sound //; simpl.
by rewrite right_id HΔ'.
Qed.
Lemma tac_wp_load Δ Δ' N E i l q v Φ :
(Δ heap_ctx N) nclose N E
StripLaterEnvs Δ Δ'
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
(Δ' Φ v)
Δ WP Load (Lit (LitLoc l)) @ E {{ Φ }}.
Proof.
intros. rewrite -wp_load // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_store Δ Δ' Δ'' N E i l v e v' Φ :
to_val e = Some v'
(Δ heap_ctx N) nclose N E
StripLaterEnvs Δ Δ'
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
(Δ'' Φ (LitV LitUnit)) Δ WP Store (Lit (LitLoc l)) e @ E {{ Φ }}.
Proof.
intros. rewrite -wp_store // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas_fail Δ Δ' N E i l q v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx N) nclose N E
StripLaterEnvs Δ Δ'
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1
(Δ' Φ (LitV (LitBool false)))
Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros. rewrite -wp_cas_fail // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_lookup_split //; simpl.
rewrite into_later_env_sound -later_sep envs_lookup_split //; simpl.
by apply later_mono, sep_mono_r, wand_mono.
Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' N E i l v e1 v1 e2 v2 Φ :
to_val e1 = Some v1 to_val e2 = Some v2
(Δ heap_ctx N) nclose N E
StripLaterEnvs Δ Δ'
IntoLaterEnvs Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
(Δ'' Φ (LitV (LitBool true))) Δ WP CAS (Lit (LitLoc l)) e1 e2 @ E {{ Φ }}.
Proof.
intros; subst.
rewrite -wp_cas_suc // -always_and_sep_l. apply and_intro; first done.
rewrite strip_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite into_later_env_sound -later_sep envs_simple_replace_sound //; simpl.
rewrite right_id. by apply later_mono, sep_mono_r, wand_mono.
Qed.
End heap.
......
......@@ -292,19 +292,19 @@ Proof.
Qed.
(** * Basic rules *)
Class ToAssumption (p : bool) (P Q : uPred M) := to_assumption : ?p P Q.
Arguments to_assumption _ _ _ {_}.
Global Instance to_assumption_exact p P : ToAssumption p P P.
Proof. destruct p; by rewrite /ToAssumption /= ?always_elim. Qed.
Global Instance to_assumption_always_l p P Q :
ToAssumption p P Q ToAssumption p ( P) Q.
Proof. rewrite /ToAssumption=><-. by rewrite always_elim. Qed.
Global Instance to_assumption_always_r P Q :
ToAssumption true P Q ToAssumption true P ( Q).
Proof. rewrite /ToAssumption=><-. by rewrite always_always. Qed.
Class FromAssumption (p : bool) (P Q : uPred M) := from_assumption : ?p P Q.
Arguments from_assumption _ _ _ {_}.
Global Instance from_assumption_exact p P : FromAssumption p P P.
Proof. destruct p; by rewrite /FromAssumption /= ?always_elim. Qed.
Global Instance from_assumption_always_l p P Q :
FromAssumption p P Q FromAssumption p ( P) Q.
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.
Lemma tac_assumption Δ i p P Q :
envs_lookup i Δ = Some (p,P) ToAssumption p P Q Δ Q.
envs_lookup i Δ = Some (p,P) FromAssumption p P Q Δ Q.
Proof. intros. by rewrite envs_lookup_sound // sep_elim_l. Qed.
Lemma tac_rename Δ Δ' i j p P Q :
......@@ -327,96 +327,96 @@ Lemma tac_ex_falso Δ Q : (Δ ⊢ False) → Δ ⊢ Q.
Proof. by rewrite -(False_elim Q). Qed.
(** * Pure *)
Class ToPure (P : uPred M) (φ : Prop) := to_pure : P ⊣⊢ φ.
Arguments to_pure : clear implicits.
Global Instance to_pure_pure φ : ToPure ( φ) φ.
Class IsPure (P : uPred M) (φ : Prop) := is_pure : P ⊣⊢ φ.
Arguments is_pure : clear implicits.
Global Instance is_pure_pure φ : IsPure ( φ) φ.
Proof. done. Qed.
Global Instance to_pure_eq {A : cofeT} (a b : A) :
Timeless a ToPure (a b) (a b).
Global Instance is_pure_eq {A : cofeT} (a b : A) :
Timeless a IsPure (a b) (a b).
Proof. intros; red. by rewrite timeless_eq. Qed.
Global Instance to_pure_valid `{CMRADiscrete A} (a : A) : ToPure ( a) ( a).
Global Instance is_pure_valid `{CMRADiscrete A} (a : A) : IsPure ( a) ( a).
Proof. intros; red. by rewrite discrete_valid. Qed.
Lemma tac_pure_intro Δ Q (φ : Prop) : ToPure Q φ φ Δ Q.
Lemma tac_pure_intro Δ Q (φ : Prop) : IsPure Q φ φ Δ Q.
Proof. intros ->. apply pure_intro. Qed.
Lemma tac_pure Δ Δ' i p P φ Q :
envs_lookup_delete i Δ = Some (p, P, Δ') ToPure P φ
envs_lookup_delete i Δ = Some (p, P, Δ') IsPure P φ
(φ Δ' Q) Δ Q.
Proof.
intros ?? HQ. rewrite envs_lookup_delete_sound' //; simpl.
rewrite (to_pure P); by apply pure_elim_sep_l.
rewrite (is_pure P); by apply pure_elim_sep_l.
Qed.
Lemma tac_pure_revert Δ φ Q : (Δ φ Q) (φ Δ Q).
Proof. intros HΔ ?. by rewrite HΔ pure_equiv // left_id. Qed.
(** * Later *)
Class StripLaterR (P Q : uPred M) := strip_later_r : P Q.
Arguments strip_later_r _ _ {_}.
Class StripLaterL (P Q : uPred M) := strip_later_l : Q P.
Arguments strip_later_l _ _ {_}.
Class StripLaterEnv (Γ1 Γ2 : env (uPred M)) :=
strip_later_env : env_Forall2 StripLaterR Γ1 Γ2.
Class StripLaterEnvs (Δ1 Δ2 : envs M) := {
strip_later_persistent: StripLaterEnv (env_persistent Δ1) (env_persistent Δ2);
strip_later_spatial: StripLaterEnv (env_spatial Δ1) (env_spatial Δ2)
Class IntoLater (P Q : uPred M) := into_later : P Q.
Arguments into_later _ _ {_}.
Class FromLater (P Q : uPred M) := from_later : Q P.
Arguments from_later _ _ {_}.
Class IntoLaterEnv (Γ1 Γ2 : env (uPred M)) :=
into_later_env : env_Forall2 IntoLater Γ1 Γ2.
Class IntoLaterEnvs (Δ1 Δ2 : envs M) := {
into_later_persistent: IntoLaterEnv (env_persistent Δ1) (env_persistent Δ2);
into_later_spatial: IntoLaterEnv (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance strip_later_r_fallthrough P : StripLaterR P P | 1000.
Global Instance into_later_fallthrough P : IntoLater P P | 1000.
Proof. apply later_intro. Qed.
Global Instance strip_later_r_later P : StripLaterR ( P) P.
Global Instance into_later_later P : IntoLater ( P) P.
Proof. done. Qed.
Global Instance strip_later_r_and P1 P2 Q1 Q2 :
StripLaterR P1 Q1 StripLaterR P2 Q2 StripLaterR (P1 P2) (Q1 Q2).
Global Instance into_later_and P1 P2 Q1 Q2 :
IntoLater P1 Q1 IntoLater P2 Q2 IntoLater (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
Global Instance strip_later_r_or P1 P2 Q1 Q2 :
StripLaterR P1 Q1 StripLaterR P2 Q2 StripLaterR (P1 P2) (Q1 Q2).
Global Instance into_later_or P1 P2 Q1 Q2 :
IntoLater P1 Q1 IntoLater P2 Q2 IntoLater (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
Global Instance strip_later_r_sep P1 P2 Q1 Q2 :
StripLaterR P1 Q1 StripLaterR P2 Q2 StripLaterR (P1 P2) (Q1 Q2).
Global Instance into_later_sep P1 P2 Q1 Q2 :
IntoLater P1 Q1 IntoLater P2 Q2 IntoLater (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
Global Instance strip_later_r_big_sepM `{Countable K} {A}
Global Instance into_later_big_sepM `{Countable K} {A}
(Φ Ψ : K A uPred M) (m : gmap K A) :
( x k, StripLaterR (Φ k x) (Ψ k x))
StripLaterR ([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
( x k, IntoLater (Φ k x) (Ψ k x))
IntoLater ([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
Proof.
rewrite /StripLaterR=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
rewrite /IntoLater=> ?. rewrite big_sepM_later; by apply big_sepM_mono.
Qed.
Global Instance strip_later_r_big_sepS `{Countable A}
Global Instance into_later_big_sepS `{Countable A}
(Φ Ψ : A uPred M) (X : gset A) :
( x, StripLaterR (Φ x) (Ψ x))
StripLaterR ([ set] x X, Φ x) ([ set] x X, Ψ x).
( x, IntoLater (Φ x) (Ψ x))
IntoLater ([ set] x X, Φ x) ([ set] x X, Ψ x).
Proof.
rewrite /StripLaterR=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
rewrite /IntoLater=> ?. rewrite big_sepS_later; by apply big_sepS_mono.
Qed.
Global Instance strip_later_l_later P : StripLaterL ( P) P.
Global Instance from_later_later P : FromLater ( P) P.
Proof. done. Qed.
Global Instance strip_later_l_and P1 P2 Q1 Q2 :
StripLaterL P1 Q1 StripLaterL P2 Q2 StripLaterL (P1 P2) (Q1 Q2).
Global Instance from_later_and P1 P2 Q1 Q2 :
FromLater P1 Q1 FromLater P2 Q2 FromLater (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite later_and; apply and_mono. Qed.
Global Instance strip_later_l_or P1 P2 Q1 Q2 :
StripLaterL P1 Q1 StripLaterL P2 Q2 StripLaterL (P1 P2) (Q1 Q2).
Global Instance from_later_or P1 P2 Q1 Q2 :
FromLater P1 Q1 FromLater P2 Q2 FromLater (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite later_or; apply or_mono. Qed.
Global Instance strip_later_l_sep P1 P2 Q1 Q2 :
StripLaterL P1 Q1 StripLaterL P2 Q2 StripLaterL (P1 P2) (Q1 Q2).
Global Instance from_later_sep P1 P2 Q1 Q2 :
FromLater P1 Q1 FromLater P2 Q2 FromLater (P1 P2) (Q1 Q2).
Proof. intros ??; red. by rewrite later_sep; apply sep_mono. Qed.
Global Instance strip_later_env_nil : StripLaterEnv Enil Enil.
Global Instance into_later_env_nil : IntoLaterEnv Enil Enil.
Proof. constructor. Qed.
Global Instance strip_later_env_snoc Γ1 Γ2 i P Q :
StripLaterEnv Γ1 Γ2 StripLaterR P Q
StripLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Global Instance into_later_env_snoc Γ1 Γ2 i P Q :
IntoLaterEnv Γ1 Γ2 IntoLater P Q
IntoLaterEnv (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.
Global Instance strip_later_envs Γp1 Γp2 Γs1 Γs2 :
StripLaterEnv Γp1 Γp2 StripLaterEnv Γs1 Γs2
StripLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Global Instance into_later_envs Γp1 Γp2 Γs1 Γs2 :
IntoLaterEnv Γp1 Γp2 IntoLaterEnv Γs1 Γs2
IntoLaterEnvs (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Proof. by split. Qed.
Lemma strip_later_env_sound Δ1 Δ2 : StripLaterEnvs Δ1 Δ2 Δ1 Δ2.
Lemma into_later_env_sound Δ1 Δ2 : IntoLaterEnvs Δ1 Δ2 Δ1 Δ2.
Proof.
intros [Hp Hs]; rewrite /of_envs /= !later_sep -always_later.
repeat apply sep_mono; try apply always_mono.
......@@ -427,8 +427,8 @@ Proof.
Qed.
Lemma tac_next Δ Δ' Q Q' :
StripLaterEnvs Δ Δ' StripLaterL Q Q' (Δ' Q') Δ Q.
Proof. intros ?? HQ. by rewrite -(strip_later_l Q) strip_later_env_sound HQ. Qed.
IntoLaterEnvs Δ Δ' FromLater Q Q' (Δ' Q') Δ Q.
Proof. intros ?? HQ. by rewrite -(from_later Q) into_later_env_sound HQ. Qed.
Lemma tac_löb Δ Δ' i Q :
envs_persistent Δ = true
......@@ -445,24 +445,24 @@ Qed.
Lemma tac_always_intro Δ Q : envs_persistent Δ = true (Δ Q) Δ Q.
Proof. intros. by apply: always_intro. Qed.
Class ToPersistentP (P Q : uPred M) := to_persistentP : P Q.
Arguments to_persistentP : clear implicits.
Global Instance to_persistentP_always_trans P Q :
ToPersistentP P Q ToPersistentP ( P) Q | 0.
Proof. rewrite /ToPersistentP=> ->. by rewrite always_always. Qed.
Global Instance to_persistentP_always P : ToPersistentP ( P) P | 1.
Class IntoPersistentP (P Q : uPred M) := into_persistentP : P Q.
Arguments into_persistentP : clear implicits.
Global Instance into_persistentP_always_trans P Q :
IntoPersistentP P Q IntoPersistentP ( P) Q | 0.
Proof. rewrite /IntoPersistentP=> ->. by rewrite always_always. Qed.
Global Instance into_persistentP_always P : IntoPersistentP ( P) P | 1.
Proof. done. Qed.
Global Instance to_persistentP_persistent P :
PersistentP P ToPersistentP P P | 100.
Global Instance into_persistentP_persistent P :
PersistentP P IntoPersistentP P P | 100.
Proof. done. Qed.
Lemma tac_persistent Δ Δ' i p P P' Q :
envs_lookup i Δ = Some (p, P) ToPersistentP P P'
envs_lookup i Δ = Some (p, P) IntoPersistentP P P'
envs_replace i p true (Esnoc Enil i P') Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros ??? <-. rewrite envs_replace_sound //; simpl.
by rewrite right_id (to_persistentP P) always_if_always wand_elim_r.
by rewrite right_id (into_persistentP P) always_if_always wand_elim_r.
Qed.
(** * Implication and wand *)
......@@ -475,16 +475,16 @@ Proof.
by rewrite right_id always_wand_impl always_elim HQ.
Qed.
Lemma tac_impl_intro_persistent Δ Δ' i P P' Q :
ToPersistentP P P'
IntoPersistentP P P'
envs_app true (Esnoc Enil i P') Δ = Some Δ'
(Δ' Q) Δ P Q.
Proof.
intros ?? HQ. rewrite envs_app_sound //; simpl. apply impl_intro_l.
by rewrite right_id {1}(to_persistentP P) always_and_sep_l wand_elim_r.
by rewrite right_id {1}(into_persistentP P) always_and_sep_l wand_elim_r.
Qed.
Lemma tac_impl_intro_pure Δ P φ Q : ToPure P φ (φ Δ Q) Δ P Q.
Lemma tac_impl_intro_pure Δ P φ Q : IsPure P φ (φ Δ Q) Δ P Q.
Proof.
intros. by apply impl_intro_l; rewrite (to_pure P); apply pure_elim_l.
intros. by apply impl_intro_l; rewrite (is_pure P); apply pure_elim_l.
Qed.
Lemma tac_wand_intro Δ Δ' i P Q :
......@@ -493,37 +493,37 @@ Proof.
intros ? HQ. rewrite envs_app_sound //; simpl. by rewrite right_id HQ.
Qed.
Lemma tac_wand_intro_persistent Δ Δ' i P P' Q :
ToPersistentP P P'
IntoPersistentP P P'
envs_app true (Esnoc Enil i P') Δ = Some Δ'
(Δ' Q) Δ P - Q.
Proof.
intros. rewrite envs_app_sound //; simpl.
rewrite right_id. by apply wand_mono.
Qed.
Lemma tac_wand_intro_pure Δ P φ Q : ToPure P φ (φ Δ Q) Δ P - Q.
Lemma tac_wand_intro_pure Δ P φ Q : IsPure P φ (φ Δ Q) Δ P - Q.
Proof.
intros. by apply wand_intro_l; rewrite (to_pure P); apply pure_elim_sep_l.
intros. by apply wand_intro_l; rewrite (is_pure P); apply pure_elim_sep_l.
Qed.
Class ToWand (R P Q : uPred M) := to_wand : R P - Q.
Arguments to_wand : clear implicits.
Global Instance to_wand_wand P Q : ToWand (P - Q) P Q.
Class IntoWand (R P Q : uPred M) := into_wand : R P - Q.
Arguments into_wand : clear implicits.
Global Instance into_wand_wand P Q : IntoWand (P - Q) P Q.
Proof. done. Qed.
Global Instance to_wand_impl P Q : ToWand (P Q) P Q.
Global Instance into_wand_impl P Q : IntoWand (P Q) P Q.
Proof. apply impl_wand. Qed.
Global Instance to_wand_iff_l P Q : ToWand (P Q) P Q.
Global Instance into_wand_iff_l P Q : IntoWand (P Q) P Q.
Proof. by apply and_elim_l', impl_wand. Qed.
Global Instance to_wand_iff_r P Q : ToWand (P Q) Q P.
Global Instance into_wand_iff_r P Q : IntoWand (P Q) Q P.
Proof. apply and_elim_r', impl_wand. Qed.
Global Instance to_wand_always R P Q : ToWand R P Q ToWand ( R) P Q.
+Proof. rewrite /ToWand=> ->. apply always_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.
(* This is pretty much [tac_specialize_assert] with [js:=[j]] and [tac_exact],
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)
ToWand R P1 P2
IntoWand 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) Δ'
......@@ -533,22 +533,22 @@ 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 (to_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
rewrite assoc (into_wand R) (always_elim_if q) -always_if_sep wand_elim_r.
by rewrite right_id wand_elim_r.
- rewrite envs_lookup_sound //; simpl.
rewrite envs_lookup_sound // (envs_replace_sound' _ Δ'') //; simpl.
by rewrite right_id assoc (to_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.
Class ToAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
to_assert : R (P - Q) Q.
Global Arguments to_assert _ _ _ {_}.
Lemma to_assert_fallthrough P Q : ToAssert P Q P.
Proof. by rewrite /ToAssert wand_elim_r. Qed.
Class IntoAssert (P : uPred M) (Q : uPred M) (R : uPred M) :=
into_assert : R (P - Q) Q.
Global Arguments into_assert _ _ _ {_}.
Lemma into_assert_fallthrough P Q : IntoAssert P Q P.
Proof. by rewrite /IntoAssert 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, Δ')
ToWand R P1 P2 ToAssert P1 Q P1'
IntoWand R P1 P2 IntoAssert P1 Q P1'
('(Δ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] *)
......@@ -559,24 +559,24 @@ Proof.
destruct (envs_app _ _ _) eqn:?; simplify_eq/=.
rewrite envs_lookup_sound // envs_split_sound //.
rewrite (envs_app_sound Δ2) //; simpl.
rewrite right_id (to_wand R) HP1 assoc -(comm _ P1') -assoc.
rewrite -(to_assert P1 Q); apply sep_mono_r, wand_intro_l.
rewrite right_id (into_wand R) HP1 assoc -(comm _ P1') -assoc.
rewrite -(into_assert P1 Q); apply sep_mono_r, wand_intro_l.
by rewrite always_if_elim assoc !wand_elim_r.
Qed.
Lemma tac_specialize_pure Δ Δ' j q R P1 P2 φ Q :
envs_lookup j Δ = Some (q, R)
ToWand R P1 P2 ToPure P1 φ
IntoWand R P1 P2 IsPure P1 φ
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ'
φ (Δ' Q) Δ Q.
Proof.
intros. rewrite envs_simple_replace_sound //; simpl.
by rewrite right_id (to_wand R) (to_pure P1) pure_equiv // wand_True wand_elim_r.
by rewrite right_id (into_wand R) (is_pure P1) pure_equiv // wand_True wand_elim_r.
Qed.
Lemma tac_specialize_persistent Δ Δ' Δ'' j q P1 P2 R Q :
envs_lookup_delete j Δ = Some (q, R, Δ')
ToWand R P1 P2
IntoWand R P1 P2
envs_simple_replace j q (Esnoc Enil j P2) Δ = Some Δ''
(Δ' P1) (PersistentP P1 PersistentP P2)
(Δ'' Q) Δ Q.
......@@ -586,11 +586,11 @@ 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 (to_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.
- rewrite -(idemp uPred_and Δ) {1}envs_lookup_sound //; simpl; rewrite HP1.
rewrite envs_simple_replace_sound //; simpl.
rewrite (sep_elim_r _ (_ - _)) right_id (to_wand R) always_if_elim.
rewrite (sep_elim_r _ (_ - _)) right_id (into_wand R) always_if_elim.
by rewrite wand_elim_l always_and_sep_l -{1}(always_if_always q P2) wand_elim_r.
Qed.
......@@ -610,7 +610,7 @@ Proof.
Qed.
Lemma tac_assert Δ Δ1 Δ2 Δ2' lr js j P Q R :
ToAssert P Q R
IntoAssert P Q R
envs_split lr js Δ = Some (Δ1,Δ2)
envs_app false (Esnoc Enil j P) Δ2 = Some Δ2'
(Δ1 R) (Δ2' Q) Δ Q.
......@@ -630,22 +630,24 @@ Proof.
Qed.
(** Whenever posing [lem : True ⊢ Q] as [H] we want it to appear as [H : Q] and
not as [H : True -★ Q]. The class [ToPosedProof] is used to strip off the
not as [H : True -★ Q]. The class [IntoPosedProof] is used to strip off the
[True]. Note that [to_posed_proof_True] is declared using a [Hint Extern] to
make sure it is not used while posing [lem : ?P ⊢ Q] with [?P] an evar. *)
Class ToPosedProof (P1 P2 R : uPred M) := to_pose_proof : (P1 P2) True R.
Arguments to_pose_proof : clear implicits.
Instance to_posed_proof_True P : ToPosedProof True P P.
Proof. by rewrite /ToPosedProof. Qed.
Global Instance to_posed_proof_wand P Q : ToPosedProof P Q (P - Q).
Proof. rewrite /ToPosedProof. apply entails_wand. Qed.
Class IntoPosedProof (P1 P2 R : uPred M) :=
into_pose_proof : (P1 P2) True R.
Arguments into_pose_proof : clear implicits.
Instance to_posed_proof_True P : IntoPosedProof True P P.
Proof. by rewrite /IntoPosedProof. Qed.
Global Instance to_posed_proof_wand P Q : IntoPosedProof P Q (P - Q).
Proof. rewrite /IntoPosedProof. apply entails_wand. Qed.
Lemma tac_pose_proof Δ Δ' j P1 P2 R Q :
(P1 P2) ToPosedProof P1 P2 R envs_app true (Esnoc Enil j R) Δ = Some Δ'
(P1 P2) IntoPosedProof P1 P2 R
envs_app true (Esnoc Enil j R) Δ = Some Δ'
(Δ' Q) Δ Q.
Proof.
intros HP ?? <-. rewrite envs_app_sound //; simpl.
by rewrite right_id -(to_pose_proof P1 P2 R) // always_pure wand_True.
by rewrite right_id -(into_pose_proof P1 P2 R) // always_pure wand_True.
Qed.
Lemma tac_pose_proof_hyp Δ Δ' Δ'' i p j P Q :
......@@ -661,11 +663,11 @@ Proof.
Qed.
Lemma tac_apply Δ Δ' i p R P1 P2 :
envs_lookup_delete i Δ = Some (p, R, Δ') ToWand R P1 P2
envs_lookup_delete i Δ = Some (p, R, Δ') IntoWand R P1 P2
(Δ' P1) Δ P2.
Proof.
intros ?? HP1. rewrite envs_lookup_delete_sound' //.
by rewrite (to_wand R) HP1 wand_elim_l.
by rewrite (into_wand R) HP1 wand_elim_l.
Qed.
(** * Rewriting *)
......@@ -703,71 +705,71 @@ Proof.
Qed.
(** * Conjunction splitting *)
Class AndSplit (P Q1 Q2 : uPred M) := and_split : Q1 Q2 P.
Arguments and_split : clear implicits.
Class FromAnd (P Q1 Q2 : uPred M) := from_and : Q1 Q2 P.
Arguments from_and : clear implicits.
Global Instance and_split_and P1 P2 : AndSplit (P1 P2) P1 P2.
Global Instance from_and_and P1 P2 : FromAnd (P1 P2) P1 P2.
Proof. done. Qed.
Global Instance and_split_sep_persistent_l P1 P2 :
PersistentP P1 AndSplit (P1 P2) P1 P2.
Proof. intros. by rewrite /AndSplit always_and_sep_l. Qed.
Global Instance and_split_sep_persistent_r P1 P2 :
PersistentP P2 AndSplit (P1 P2) P1 P2.
Proof. intros. by rewrite /AndSplit always_and_sep_r. Qed.
Global Instance and_split_always P Q1 Q2 :
AndSplit P Q1 Q2 AndSplit ( P) ( Q1) ( Q2).
Proof. rewrite /AndSplit=> <-. by rewrite always_and. Qed.
Global Instance and_split_later P Q1 Q2 :
AndSplit P Q1 Q2 AndSplit ( P) ( Q1) ( Q2).
Proof. rewrite /AndSplit=> <-. by rewrite later_and. Qed.
Lemma tac_and_split Δ P Q1 Q2 : AndSplit P Q1 Q2 (Δ Q1) (Δ Q2) Δ P.
Proof. intros. rewrite -(and_split P). by apply and_intro. Qed.
Global Instance from_and_sep_persistent_l P1 P2 :
PersistentP P1 FromAnd (P1 P2) P1 P2.
Proof. intros. by rewrite /FromAnd always_and_sep_l. Qed.
Global Instance from_and_sep_persistent_r P1 P2 :
PersistentP P2 FromAnd (P1 P2) P1 P2.
Proof. intros. by rewrite /FromAnd always_and_sep_r. Qed.
Global Instance from_and_always P Q1 Q2 :
FromAnd P Q1 Q2 FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite always_and. Qed.
Global Instance from_and_later P Q1 Q2 :
FromAnd P Q1 Q2 FromAnd ( P) ( Q1) ( Q2).
Proof. rewrite /FromAnd=> <-. by rewrite later_and. Qed.
Lemma tac_and_split Δ P Q1 Q2 : FromAnd P Q1 Q2 (Δ Q1) (Δ Q2) Δ P.
Proof. intros. rewrite -(from_and P). by apply and_intro. Qed.
(** * Separating conjunction splitting *)
Class SepSplit (P Q1 Q2 : uPred M) := sep_split : Q1 Q2 P.
Arguments sep_split : clear implicits.
Class FromSep (P Q1 Q2 : uPred M) := from_sep : Q1 Q2 P.
Arguments from_sep : clear implicits.
Global Instance sep_split_sep P1 P2 : SepSplit (P1 P2) P1 P2 | 100.
Global Instance from_sep_sep P1 P2 : FromSep (P1 P2) P1 P2 | 100.
Proof. done. Qed.
Global Instance sep_split_always P Q1 Q2 :
SepSplit P Q1 Q2 SepSplit ( P) ( Q1) ( Q2).
Proof. rewrite /SepSplit=> <-. by rewrite always_sep. Qed.
Global Instance sep_split_later P Q1 Q2 :
SepSplit P Q1 Q2 SepSplit ( P) ( Q1) ( Q2).
Proof. rewrite /SepSplit=> <-. by rewrite later_sep. Qed.
Global Instance sep_split_ownM (a b : M) :
SepSplit (uPred_ownM (a b)) (uPred_ownM a) (uPred_ownM b) | 99.
Proof. by rewrite /SepSplit ownM_op. Qed.
Global Instance sep_split_big_sepM
Global Instance from_sep_always P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite always_sep. Qed.
Global Instance from_sep_later P Q1 Q2 :
FromSep P Q1 Q2 FromSep ( P) ( Q1) ( Q2).
Proof. rewrite /FromSep=> <-. by rewrite later_sep. Qed.