Commit 680e10eb authored by Robbert Krebbers's avatar Robbert Krebbers

Rename `IntoLaterN` → `MaybeIntoLaterN` and `IntoLaterN'` → `IntoLaterN`.

We now use the `Maybe` prefix as also used for `Frame`: it indicates
whether progress has been made by stripping of a later or not.
parent e55b06dd
......@@ -27,7 +27,7 @@ Ltac wp_expr_simpl_subst := wp_expr_eval simpl_subst.
Lemma tac_wp_pure `{heapG Σ} Δ Δ' s E e1 e2 φ Φ :
PureExec φ e1 e2
φ
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_entails Δ' (WP e2 @ s; E {{ Φ }})
envs_entails Δ (WP e1 @ s; E {{ Φ }}).
Proof.
......@@ -141,7 +141,7 @@ Implicit Types Δ : envs (iResUR Σ).
Lemma tac_wp_alloc Δ Δ' s E j K e v Φ :
IntoVal e v
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
( l, Δ'',
envs_app false (Esnoc Enil j (l v)) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitLoc l)) @ s; E {{ Φ }}))
......@@ -168,7 +168,7 @@ Proof.
Qed.
Lemma tac_wp_load Δ Δ' s E i K l q v Φ :
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I
envs_entails Δ' (WP fill K (of_val v) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (Load (Lit (LitLoc l))) @ s; E {{ Φ }}).
......@@ -191,7 +191,7 @@ Qed.
Lemma tac_wp_store Δ Δ' Δ'' s E i K l v e v' Φ :
IntoVal e v'
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I
envs_simple_replace i false (Esnoc Enil i (l v')) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit LitUnit) @ s; E {{ Φ }})
......@@ -216,7 +216,7 @@ Qed.
Lemma tac_wp_cas_fail Δ Δ' s E i K l q v e1 v1 e2 Φ :
IntoVal e1 v1 AsVal e2
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l {q} v)%I v v1
envs_entails Δ' (WP fill K (Lit (LitBool false)) @ s; E {{ Φ }})
envs_entails Δ (WP fill K (CAS (Lit (LitLoc l)) e1 e2) @ s; E {{ Φ }}).
......@@ -238,7 +238,7 @@ Qed.
Lemma tac_wp_cas_suc Δ Δ' Δ'' s E i K l v e1 v1 e2 v2 Φ :
IntoVal e1 v1 IntoVal e2 v2
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l v)%I v = v1
envs_simple_replace i false (Esnoc Enil i (l v2)) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitBool true)) @ s; E {{ Φ }})
......@@ -263,7 +263,7 @@ Qed.
Lemma tac_wp_faa Δ Δ' Δ'' s E i K l i1 e2 i2 Φ :
IntoVal e2 (LitV (LitInt i2))
IntoLaterNEnvs 1 Δ Δ'
MaybeIntoLaterNEnvs 1 Δ Δ'
envs_lookup i Δ' = Some (false, l LitV (LitInt i1))%I
envs_simple_replace i false (Esnoc Enil i (l LitV (LitInt (i1 + i2)))) Δ' = Some Δ''
envs_entails Δ'' (WP fill K (Lit (LitInt i1)) @ s; E {{ Φ }})
......
......@@ -168,92 +168,92 @@ Proof. by rewrite /FromAlways. Qed.
(* IntoLater *)
Global Instance into_laterN_later n P Q :
IntoLaterN n P Q IntoLaterN' (S n) ( P) Q | 0.
Proof. by rewrite /IntoLaterN' /IntoLaterN =>->. Qed.
MaybeIntoLaterN n P Q IntoLaterN (S n) ( P) Q | 0.
Proof. by rewrite /IntoLaterN /MaybeIntoLaterN =>->. Qed.
Global Instance into_laterN_later_further n P Q :
IntoLaterN' n P Q IntoLaterN' n ( P) ( Q) | 1000.
Proof. rewrite /IntoLaterN' /IntoLaterN =>->. by rewrite -laterN_later. Qed.
IntoLaterN n P Q IntoLaterN n ( P) ( Q) | 1000.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN =>->. by rewrite -laterN_later. Qed.
Global Instance into_laterN_laterN n P : IntoLaterN' n (^n P) P | 0.
Global Instance into_laterN_laterN n P : IntoLaterN n (^n P) P | 0.
Proof. done. Qed.
Global Instance into_laterN_laterN_plus n m P Q :
IntoLaterN m P Q IntoLaterN' (n + m) (^n P) Q | 1.
Proof. rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite laterN_plus. Qed.
MaybeIntoLaterN m P Q IntoLaterN (n + m) (^n P) Q | 1.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=>->. by rewrite laterN_plus. Qed.
Global Instance into_laterN_laterN_further n m P Q :
IntoLaterN' m P Q IntoLaterN' m (^n P) (^n Q) | 1000.
IntoLaterN m P Q IntoLaterN m (^n P) (^n Q) | 1000.
Proof.
rewrite /IntoLaterN' /IntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
rewrite /IntoLaterN /MaybeIntoLaterN=>->. by rewrite -!laterN_plus Nat.add_comm.
Qed.
Global Instance into_laterN_and_l n P1 P2 Q1 Q2 :
IntoLaterN' n P1 Q1 IntoLaterN n P2 Q2
IntoLaterN' n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_and. Qed.
IntoLaterN n P1 Q1 MaybeIntoLaterN n P2 Q2
IntoLaterN n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_and. Qed.
Global Instance into_laterN_and_r n P P2 Q2 :
IntoLaterN' n P2 Q2 IntoLaterN' n (P P2) (P Q2) | 11.
IntoLaterN n P2 Q2 IntoLaterN n (P P2) (P Q2) | 11.
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_and -(laterN_intro _ P).
Qed.
Global Instance into_later_forall {A} n (Φ Ψ : A uPred M) :
( x, IntoLaterN' n (Φ x) (Ψ x)) IntoLaterN' n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN' /IntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
( x, IntoLaterN n (Φ x) (Ψ x)) IntoLaterN n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN laterN_forall=> ?. by apply forall_mono. Qed.
Global Instance into_later_exist {A} n (Φ Ψ : A uPred M) :
( x, IntoLaterN' n (Φ x) (Ψ x))
IntoLaterN' n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN' /IntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
( x, IntoLaterN n (Φ x) (Ψ x))
IntoLaterN n ( x, Φ x) ( x, Ψ x).
Proof. rewrite /IntoLaterN /MaybeIntoLaterN -laterN_exist_2=> ?. by apply exist_mono. Qed.
Global Instance into_laterN_or_l n P1 P2 Q1 Q2 :
IntoLaterN' n P1 Q1 IntoLaterN n P2 Q2
IntoLaterN' n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_or. Qed.
IntoLaterN n P1 Q1 MaybeIntoLaterN n P2 Q2
IntoLaterN n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_or. Qed.
Global Instance into_laterN_or_r n P P2 Q2 :
IntoLaterN' n P2 Q2
IntoLaterN' n (P P2) (P Q2) | 11.
IntoLaterN n P2 Q2
IntoLaterN n (P P2) (P Q2) | 11.
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_or -(laterN_intro _ P).
Qed.
Global Instance into_laterN_sep_l n P1 P2 Q1 Q2 :
IntoLaterN' n P1 Q1 IntoLaterN n P2 Q2
IntoLaterN' n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN' /IntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
IntoLaterN n P1 Q1 MaybeIntoLaterN n P2 Q2
IntoLaterN n (P1 P2) (Q1 Q2) | 10.
Proof. rewrite /IntoLaterN /MaybeIntoLaterN=> -> ->. by rewrite laterN_sep. Qed.
Global Instance into_laterN_sep_r n P P2 Q2 :
IntoLaterN' n P2 Q2
IntoLaterN' n (P P2) (P Q2) | 11.
IntoLaterN n P2 Q2
IntoLaterN n (P P2) (P Q2) | 11.
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
rewrite /IntoLaterN /MaybeIntoLaterN=> ->. by rewrite laterN_sep -(laterN_intro _ P).
Qed.
Global Instance into_laterN_big_sepL n {A} (Φ Ψ : nat A uPred M) (l: list A) :
( x k, IntoLaterN' n (Φ k x) (Ψ k x))
IntoLaterN' n ([ list] k x l, Φ k x) ([ list] k x l, Ψ k x).
( x k, IntoLaterN n (Φ k x) (Ψ k x))
IntoLaterN n ([ list] k x l, Φ k x) ([ list] k x l, Ψ k x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opL_commute. by apply big_sepL_mono.
Qed.
Global Instance into_laterN_big_sepM n `{Countable K} {A}
(Φ Ψ : K A uPred M) (m : gmap K A) :
( x k, IntoLaterN' n (Φ k x) (Ψ k x))
IntoLaterN' n ([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
( x k, IntoLaterN n (Φ k x) (Ψ k x))
IntoLaterN n ([ map] k x m, Φ k x) ([ map] k x m, Ψ k x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opM_commute; by apply big_sepM_mono.
Qed.
Global Instance into_laterN_big_sepS n `{Countable A}
(Φ Ψ : A uPred M) (X : gset A) :
( x, IntoLaterN' n (Φ x) (Ψ x))
IntoLaterN' n ([ set] x X, Φ x) ([ set] x X, Ψ x).
( x, IntoLaterN n (Φ x) (Ψ x))
IntoLaterN n ([ set] x X, Φ x) ([ set] x X, Ψ x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opS_commute; by apply big_sepS_mono.
Qed.
Global Instance into_laterN_big_sepMS n `{Countable A}
(Φ Ψ : A uPred M) (X : gmultiset A) :
( x, IntoLaterN' n (Φ x) (Ψ x))
IntoLaterN' n ([ mset] x X, Φ x) ([ mset] x X, Ψ x).
( x, IntoLaterN n (Φ x) (Ψ x))
IntoLaterN n ([ mset] x X, Φ x) ([ mset] x X, Ψ x).
Proof.
rewrite /IntoLaterN' /IntoLaterN=> ?.
rewrite /IntoLaterN /MaybeIntoLaterN=> ?.
rewrite big_opMS_commute; by apply big_sepMS_mono.
Qed.
......@@ -638,10 +638,10 @@ Global Instance make_later_default P : MakeLater P (▷ P) | 100.
Proof. done. Qed.
Global Instance frame_later p R R' P Q Q' :
NoBackTrack (IntoLaterN 1 R' R)
NoBackTrack (MaybeIntoLaterN 1 R' R)
Frame p R P Q MakeLater Q Q' Frame p R' ( P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
rewrite /Frame /MakeLater /MaybeIntoLaterN=>-[->] <- <-.
by rewrite persistently_if_later later_sep.
Qed.
......@@ -652,10 +652,10 @@ Global Instance make_laterN_default P : MakeLaterN n P (▷^n P) | 100.
Proof. done. Qed.
Global Instance frame_laterN p n R R' P Q Q' :
NoBackTrack (IntoLaterN n R' R)
NoBackTrack (MaybeIntoLaterN n R' R)
Frame p R P Q MakeLaterN n Q Q' Frame p R' (^n P) Q'.
Proof.
rewrite /Frame /MakeLater /IntoLaterN=>-[->] <- <-.
rewrite /Frame /MakeLater /MaybeIntoLaterN=>-[->] <- <-.
by rewrite persistently_if_laterN laterN_sep.
Qed.
......
......@@ -76,40 +76,42 @@ Class FromAlways {M} (p : bool) (P Q : uPred M) :=
Arguments from_always {_} _ _ _ {_}.
Hint Mode FromAlways + - ! - : typeclass_instances.
(* The class [IntoLaterN] has only two instances:
(* The class [MaybeIntoLaterN] has only two instances:
- The default instance [IntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN' n P Q → IntoLaterN n P Q], where [IntoLaterN']
is identical to [IntoLaterN], but computationally is supposed to make
progress, i.e. its instances should actually strip a later.
- The default instance [MaybeIntoLaterN n P P], i.e. [▷^n P -∗ P]
- The instance [IntoLaterN n P Q → MaybeIntoLaterN n P Q], where [IntoLaterN]
is identical to [MaybeIntoLaterN], but is supposed to make progress, i.e. it
should actually strip a later.
The point of using the auxilary class [IntoLaterN'] is to ensure that the
default instance is not applied deeply in the term, which may result in too many
definitions being unfolded (see issue #55).
The point of using the auxilary class [IntoLaterN] is to ensure that the
default instance is not applied deeply inside a term, which may result in too
many definitions being unfolded (see issue #55).
For binary connectives we have the following instances:
<<
IntoLaterN' n P P' IntoLaterN n Q Q'
IntoLaterN n P P' MaybeIntoLaterN n Q Q'
------------------------------------------
IntoLaterN' n (P /\ Q) (P' /\ Q')
IntoLaterN n (P /\ Q) (P' /\ Q')
IntoLaterN' n Q Q'
IntoLaterN n Q Q'
-------------------------------
IntoLaterN' n (P /\ Q) (P /\ Q')
IntoLaterN n (P /\ Q) (P /\ Q')
>>
*)
Class IntoLaterN {M} (n : nat) (P Q : uPred M) := into_laterN : P ^n Q.
Arguments into_laterN {_} _ _ _ {_}.
Hint Mode IntoLaterN + - - - : typeclass_instances.
Class MaybeIntoLaterN {M} (n : nat) (P Q : uPred M) :=
maybe_into_laterN : P ^n Q.
Arguments maybe_into_laterN {_} _ _ _ {_}.
Hint Mode MaybeIntoLaterN + - - - : typeclass_instances.
Class IntoLaterN' {M} (n : nat) (P Q : uPred M) :=
into_laterN' :> IntoLaterN n P Q.
Arguments into_laterN' {_} _ _ _ {_}.
Hint Mode IntoLaterN' + - ! - : typeclass_instances.
Class IntoLaterN {M} (n : nat) (P Q : uPred M) :=
into_laterN :> MaybeIntoLaterN n P Q.
Arguments into_laterN {_} _ _ _ {_}.
Hint Mode IntoLaterN + - ! - : typeclass_instances.
Instance into_laterN_default {M} n (P : uPred M) : IntoLaterN n P P | 1000.
Instance maybe_into_laterN_default {M} n (P : uPred M) :
MaybeIntoLaterN n P P | 1000.
Proof. apply laterN_intro. Qed.
Class FromLaterN {M} (n : nat) (P Q : uPred M) := from_laterN : ^n Q P.
......@@ -279,7 +281,7 @@ with the exception of:
- [FromAssumption] used by [iAssumption]
- [Frame] used by [iFrame]
- [IntoLaterN] and [FromLaterN] used by [iNext]
- [MaybeIntoLaterN] and [FromLaterN] used by [iNext]
- [IntoPersistent] used by [iPersistent]
*)
Instance into_pure_tc_opaque {M} (P : uPred M) φ :
......
......@@ -472,27 +472,27 @@ Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ → Q) → (φ → env
Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
(** * Later *)
Class IntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
into_laterN_env : env_Forall2 (IntoLaterN n) Γ1 Γ2.
Class IntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
into_later_persistent: IntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
into_later_spatial: IntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
Class MaybeIntoLaterNEnv (n : nat) (Γ1 Γ2 : env (uPred M)) :=
into_laterN_env : env_Forall2 (MaybeIntoLaterN n) Γ1 Γ2.
Class MaybeIntoLaterNEnvs (n : nat) (Δ1 Δ2 : envs M) := {
into_later_persistent: MaybeIntoLaterNEnv n (env_persistent Δ1) (env_persistent Δ2);
into_later_spatial: MaybeIntoLaterNEnv n (env_spatial Δ1) (env_spatial Δ2)
}.
Global Instance into_laterN_env_nil n : IntoLaterNEnv n Enil Enil.
Global Instance into_laterN_env_nil n : MaybeIntoLaterNEnv n Enil Enil.
Proof. constructor. Qed.
Global Instance into_laterN_env_snoc n Γ1 Γ2 i P Q :
IntoLaterNEnv n Γ1 Γ2 IntoLaterN n P Q
IntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
MaybeIntoLaterNEnv n Γ1 Γ2 MaybeIntoLaterN n P Q
MaybeIntoLaterNEnv n (Esnoc Γ1 i P) (Esnoc Γ2 i Q).
Proof. by constructor. Qed.
Global Instance into_laterN_envs n Γp1 Γp2 Γs1 Γs2 :
IntoLaterNEnv n Γp1 Γp2 IntoLaterNEnv n Γs1 Γs2
IntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
MaybeIntoLaterNEnv n Γp1 Γp2 MaybeIntoLaterNEnv n Γs1 Γs2
MaybeIntoLaterNEnvs n (Envs Γp1 Γs1) (Envs Γp2 Γs2).
Proof. by split. Qed.
Lemma into_laterN_env_sound n Δ1 Δ2 :
IntoLaterNEnvs n Δ1 Δ2 of_envs Δ1 ^n (of_envs Δ2).
MaybeIntoLaterNEnvs n Δ1 Δ2 of_envs Δ1 ^n (of_envs Δ2).
Proof.
intros [Hp Hs]; rewrite /of_envs /= !laterN_sep -persistently_laterN.
repeat apply sep_mono; try apply persistently_mono.
......@@ -503,7 +503,7 @@ Proof.
Qed.
Lemma tac_next Δ Δ' n Q Q' :
FromLaterN n Q Q' IntoLaterNEnvs n Δ Δ'
FromLaterN n Q Q' MaybeIntoLaterNEnvs n Δ Δ'
envs_entails Δ' Q' envs_entails Δ Q.
Proof.
rewrite /envs_entails=> ?? HQ.
......
......@@ -860,7 +860,7 @@ Tactic Notation "iNext" open_constr(n) :=
eapply (tac_next _ _ n);
[apply _ || fail "iNext:" P "does not contain" n "laters"
|lazymatch goal with
| |- IntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
| |- MaybeIntoLaterNEnvs 0 _ _ => fail "iNext:" P "does not contain laters"
| _ => apply _
end
|lazy beta (* remove beta redexes caused by removing laters under binders*)].
......
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