Commit 6dc83bcb authored by Robbert Krebbers's avatar Robbert Krebbers

Generic `iAlways` tactic.

This commit implements a generic `iAlways` tactic that is not tied to
`persistently`, `affinely` and `plainly` but can be instantiated with a
variety of always-style modalities.

In order to plug in an always-style modality, one has to decide for both
the persistent and spatial what action should be performed upon introducing
the modality:

- Introduction is only allowed when the context is empty.
- Introduction is only allowed when all hypotheses satisfy some predicate
  `C : PROP → Prop` (where `C` should be a type class).
- Introduction will only keep the hypotheses that satisfy some predicate
  `C : PROP → Prop` (where `C` should be a type class).
- Introduction will clear the context.
- Introduction will keep the context as-if.

Formally, these actions correspond to the following inductive type:

```coq
Inductive always_intro_spec (PROP : bi) :=
  | AIEnvIsEmpty
  | AIEnvForall (C : PROP → Prop)
  | AIEnvFilter (C : PROP → Prop)
  | AIEnvClear
  | AIEnvId.
```

An always-style modality is then a record `always_modality` packing together the
modality with the laws it should satisfy to justify the given actions for both
contexts.
parent 493d7eb9
...@@ -3,6 +3,56 @@ From iris.bi Require Import bi tactics. ...@@ -3,6 +3,56 @@ From iris.bi Require Import bi tactics.
Set Default Proof Using "Type". Set Default Proof Using "Type".
Import bi. Import bi.
Section always_modalities.
Context {PROP : bi}.
Lemma always_modality_persistently_mixin :
always_modality_mixin (@bi_persistently PROP) AIEnvId AIEnvClear.
Proof.
split; eauto using equiv_entails_sym, persistently_intro, persistently_mono,
persistently_and, persistently_sep_2 with typeclass_instances.
Qed.
Definition always_modality_persistently :=
AlwaysModality _ always_modality_persistently_mixin.
Lemma always_modality_affinely_mixin :
always_modality_mixin (@bi_affinely PROP) AIEnvId (AIEnvForall Affine).
Proof.
split; eauto using equiv_entails_sym, affinely_intro, affinely_mono,
affinely_and, affinely_sep_2 with typeclass_instances.
Qed.
Definition always_modality_affinely :=
AlwaysModality _ always_modality_affinely_mixin.
Lemma always_modality_affinely_persistently_mixin :
always_modality_mixin (λ P : PROP, P)%I AIEnvId AIEnvIsEmpty.
Proof.
split; eauto using equiv_entails_sym, affinely_persistently_emp,
affinely_mono, persistently_mono, affinely_persistently_idemp,
affinely_persistently_and, affinely_persistently_sep_2 with typeclass_instances.
Qed.
Definition always_modality_affinely_persistently :=
AlwaysModality _ always_modality_affinely_persistently_mixin.
Lemma always_modality_plainly_mixin :
always_modality_mixin (@bi_plainly PROP) (AIEnvForall Plain) AIEnvClear.
Proof.
split; eauto using equiv_entails_sym, plainly_intro, plainly_mono,
plainly_and, plainly_sep_2 with typeclass_instances.
Qed.
Definition always_modality_plainly :=
AlwaysModality _ always_modality_plainly_mixin.
Lemma always_modality_affinely_plainly_mixin :
always_modality_mixin (λ P : PROP, P)%I (AIEnvForall Plain) AIEnvIsEmpty.
Proof.
split; eauto using equiv_entails_sym, affinely_plainly_emp, affinely_intro,
plainly_intro, affinely_mono, plainly_mono, affinely_plainly_idemp,
affinely_plainly_and, affinely_plainly_sep_2 with typeclass_instances.
Qed.
Definition always_modality_affinely_plainly :=
AlwaysModality _ always_modality_affinely_plainly_mixin.
End always_modalities.
Section bi_instances. Section bi_instances.
Context {PROP : bi}. Context {PROP : bi}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
...@@ -190,31 +240,53 @@ Global Instance into_persistent_persistent P : ...@@ -190,31 +240,53 @@ Global Instance into_persistent_persistent P :
Proof. intros. by rewrite /IntoPersistent. Qed. Proof. intros. by rewrite /IntoPersistent. Qed.
(* FromAlways *) (* FromAlways *)
Global Instance from_always_here P : FromAlways false false false P P | 1. Global Instance from_always_affinely P :
FromAlways always_modality_affinely (bi_affinely P) P | 2.
Proof. by rewrite /FromAlways. Qed. Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_plainly a pe pl P Q :
FromAlways a pe pl P Q FromAlways false true true (bi_plainly P) Q | 0. Global Instance from_always_persistently P :
Proof. FromAlways always_modality_persistently (bi_persistently P) P | 2.
rewrite /FromAlways /= => <-. Proof. by rewrite /FromAlways. Qed.
destruct a, pe, pl; rewrite /= ?persistently_affinely ?plainly_affinely Global Instance from_always_affinely_persistently P :
!persistently_plainly ?plainly_idemp ?plainly_persistently //. FromAlways always_modality_affinely_persistently ( P) P | 1.
Qed. Proof. by rewrite /FromAlways. Qed.
Global Instance from_always_persistently a pe pl P Q : Global Instance from_always_affinely_persistently_affine_bi P :
FromAlways a pe pl P Q FromAlways false true pl (bi_persistently P) Q | 0. BiAffine PROP FromAlways always_modality_persistently ( P) P | 0.
Proof. Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
rewrite /FromAlways /= => <-.
destruct a, pe; rewrite /= ?persistently_affinely ?persistently_idemp //. Global Instance from_always_plainly P :
Qed. FromAlways always_modality_plainly (bi_plainly P) P | 2.
Global Instance from_always_affinely a pe pl P Q : Proof. by rewrite /FromAlways. Qed.
FromAlways a pe pl P Q FromAlways true pe pl (bi_affinely P) Q | 0. Global Instance from_always_affinely_plainly P :
Proof. FromAlways always_modality_affinely_plainly ( P) P | 1.
rewrite /FromAlways /= => <-. destruct a; by rewrite /= ?affinely_idemp. Proof. by rewrite /FromAlways. Qed.
Qed. Global Instance from_always_affinely_plainly_affine_bi P :
Global Instance from_always_embed `{BiEmbedding PROP PROP'} a pe pl P Q : BiAffine PROP FromAlways always_modality_plainly ( P) P | 0.
FromAlways a pe pl P Q FromAlways a pe pl P Q | 0. Proof. intros. by rewrite /FromAlways /= affine_affinely. Qed.
Proof.
rewrite /FromAlways=><-. Global Instance from_always_affinely_embed `{BiEmbedding PROP PROP'} P Q :
by rewrite bi_embed_affinely_if bi_embed_persistently_if bi_embed_plainly_if. FromAlways always_modality_affinely P Q
FromAlways always_modality_affinely P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely. Qed.
Global Instance from_always_persistently_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_persistently P Q
FromAlways always_modality_persistently P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_persistently. Qed.
Global Instance from_always_affinely_persistently_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_affinely_persistently P Q
FromAlways always_modality_affinely_persistently P Q.
Proof.
rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_persistently.
Qed.
Global Instance from_always_plainly_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_plainly P Q
FromAlways always_modality_plainly P Q.
Proof. rewrite /FromAlways /= =><-. by rewrite bi_embed_plainly. Qed.
Global Instance from_always_affinely_plainly_embed `{BiEmbedding PROP PROP'} P Q :
FromAlways always_modality_affinely_plainly P Q
FromAlways always_modality_affinely_plainly P Q.
Proof.
rewrite /FromAlways /= =><-. by rewrite bi_embed_affinely bi_embed_plainly.
Qed. Qed.
(* IntoWand *) (* IntoWand *)
......
...@@ -68,11 +68,120 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never. ...@@ -68,11 +68,120 @@ Arguments IntoPersistent {_} _ _%I _%I : simpl never.
Arguments into_persistent {_} _ _%I _%I {_}. Arguments into_persistent {_} _ _%I _%I {_}.
Hint Mode IntoPersistent + + ! - : typeclass_instances. Hint Mode IntoPersistent + + ! - : typeclass_instances.
Class FromAlways {PROP : bi} (a pe pl : bool) (P Q : PROP) := Inductive always_intro_spec (PROP : bi) :=
from_always : bi_affinely_if a (bi_persistently_if pe (bi_plainly_if pl Q)) P. | AIEnvIsEmpty
Arguments FromAlways {_} _ _ _ _%I _%I : simpl never. | AIEnvForall (C : PROP Prop)
Arguments from_always {_} _ _ _ _%I _%I {_}. | AIEnvFilter (C : PROP Prop)
Hint Mode FromAlways + - - - ! - : typeclass_instances. | AIEnvClear
| AIEnvId.
Arguments AIEnvIsEmpty {_}.
Arguments AIEnvForall {_} _.
Arguments AIEnvFilter {_} _.
Arguments AIEnvClear {_}.
Arguments AIEnvId {_}.
Record always_modality_mixin {PROP : bi} (M : PROP PROP)
(pspec sspec : always_intro_spec PROP) := {
always_modality_mixin_persistent :
match pspec with
| AIEnvIsEmpty => True
| AIEnvForall C | AIEnvFilter C => P, C P P M ( P)
| AIEnvClear => True
| AIEnvId => P, P M ( P)
end;
always_modality_mixin_spatial :
match sspec with
| AIEnvIsEmpty => True
| AIEnvForall C => P, C P P M P
| AIEnvFilter C => ( P, C P P M P) ( P, Absorbing (M P))
| AIEnvClear => P, Absorbing (M P)
| AIEnvId => False
end;
always_modality_mixin_emp : emp M emp;
always_modality_mixin_mono P Q : (P Q) M P M Q;
always_modality_mixin_and P Q : M P M Q M (P Q);
always_modality_mixin_sep P Q : M P M Q M (P Q)
}.
Record always_modality (PROP : bi) := AlwaysModality {
always_modality_car :> PROP PROP;
always_modality_persistent_spec : always_intro_spec PROP;
always_modality_spatial_spec : always_intro_spec PROP;
always_modality_mixin_of : always_modality_mixin
always_modality_car
always_modality_persistent_spec always_modality_spatial_spec
}.
Arguments AlwaysModality {_} _ {_ _} _.
Arguments always_modality_persistent_spec {_} _.
Arguments always_modality_spatial_spec {_} _.
Section always_modality.
Context {PROP} (M : always_modality PROP).
Lemma always_modality_persistent_forall C P :
always_modality_persistent_spec M = AIEnvForall C C P P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_persistent_filter C P :
always_modality_persistent_spec M = AIEnvFilter C C P P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_persistent_id P :
always_modality_persistent_spec M = AIEnvId P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_forall C P :
always_modality_spatial_spec M = AIEnvForall C C P P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_filter C P :
always_modality_spatial_spec M = AIEnvFilter C C P P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_filter_absorbing C P :
always_modality_spatial_spec M = AIEnvFilter C Absorbing (M P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_clear P :
always_modality_spatial_spec M = AIEnvClear Absorbing (M P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_spatial_id :
always_modality_spatial_spec M AIEnvId.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma always_modality_emp : emp M emp.
Proof. eapply always_modality_mixin_emp, always_modality_mixin_of. Qed.
Lemma always_modality_mono P Q : (P Q) M P M Q.
Proof. eapply always_modality_mixin_mono, always_modality_mixin_of. Qed.
Lemma always_modality_and P Q : M P M Q M (P Q).
Proof. eapply always_modality_mixin_and, always_modality_mixin_of. Qed.
Lemma always_modality_sep P Q : M P M Q M (P Q).
Proof. eapply always_modality_mixin_sep, always_modality_mixin_of. Qed.
Global Instance always_modality_mono' : Proper (() ==> ()) M.
Proof. intros P Q. apply always_modality_mono. Qed.
Global Instance always_modality_flip_mono' : Proper (flip () ==> flip ()) M.
Proof. intros P Q. apply always_modality_mono. Qed.
Global Instance always_modality_proper : Proper (() ==> ()) M.
Proof. intros P Q. rewrite !equiv_spec=> -[??]; eauto using always_modality_mono. Qed.
Lemma always_modality_persistent_forall_big_and C Ps :
always_modality_persistent_spec M = AIEnvForall C
Forall C Ps [] Ps M ( [] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite persistently_pure affinely_True_emp affinely_emp -always_modality_emp.
- rewrite affinely_persistently_and -always_modality_and -IH.
by rewrite {1}(always_modality_persistent_forall _ P).
Qed.
Lemma always_modality_spatial_forall_big_sep C Ps :
always_modality_spatial_spec M = AIEnvForall C
Forall C Ps [] Ps M ([] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite -always_modality_emp.
- by rewrite -always_modality_sep -IH {1}(always_modality_spatial_forall _ P).
Qed.
End always_modality.
Class FromAlways {PROP : bi} (M : always_modality PROP) (P Q : PROP) :=
from_always : M Q P.
Arguments FromAlways {_} _ _%I _%I : simpl never.
Arguments from_always {_} _ _%I _%I {_}.
Hint Mode FromAlways + - ! - : typeclass_instances.
Class FromAffinely {PROP : bi} (P Q : PROP) := Class FromAffinely {PROP : bi} (P Q : PROP) :=
from_affinely : bi_affinely Q P. from_affinely : bi_affinely Q P.
......
...@@ -543,72 +543,124 @@ Qed. ...@@ -543,72 +543,124 @@ Qed.
Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ Q) (φ envs_entails Δ Q). Lemma tac_pure_revert Δ φ Q : envs_entails Δ (⌜φ⌝ Q) (φ envs_entails Δ Q).
Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed. Proof. rewrite /envs_entails. intros HΔ ?. by rewrite HΔ pure_True // left_id. Qed.
(** * Persistence and plainness modalities *) (** * Always modalities *)
Class IntoPlainEnv (Γ1 Γ2 : env PROP) := { Class FilterPersistentEnv
into_plain_env_subenv : env_subenv Γ2 Γ1; (M : always_modality PROP) (C : PROP Prop) (Γ1 Γ2 : env PROP) := {
into_plain_env_plain : Plain ([] Γ2); filter_persistent_env :
( P, C P P M ( P))
([] Γ1) M ( ([] Γ2));
filter_persistent_env_wf : env_wf Γ1 env_wf Γ2;
filter_persistent_env_dom i : Γ1 !! i = None Γ2 !! i = None;
}. }.
Global Instance filter_persistent_env_nil M C : FilterPersistentEnv M C Enil Enil.
Global Instance into_plain_env_nil : IntoPlainEnv Enil Enil. Proof.
Proof. constructor. constructor. simpl; apply _. Qed. split=> // HC /=. rewrite !persistently_pure !affinely_True_emp.
Global Instance into_plain_env_snoc_plain Γ1 Γ2 i P : by rewrite affinely_emp -always_modality_emp.
Plain P IntoPlainEnv Γ1 Γ2 Qed.
IntoPlainEnv (Esnoc Γ1 i P) (Esnoc Γ2 i P) | 1. Global Instance filter_persistent_env_snoc M (C : PROP Prop) Γ Γ' i P :
Proof. intros ? [??]; constructor. by constructor. simpl; apply _. Qed. C P
Global Instance into_plain_env_snoc_skip Γ1 Γ2 i P : FilterPersistentEnv M C Γ Γ'
IntoPlainEnv Γ1 Γ2 IntoPlainEnv (Esnoc Γ1 i P) Γ2 | 2. FilterPersistentEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
Proof. intros [??]; constructor. by constructor. done. Qed. Proof.
intros ? [HΓ Hwf Hdom]; split; simpl.
Lemma into_plain_env_sound Γ1 Γ2 : - intros HC. rewrite affinely_persistently_and HC // HΓ //.
IntoPlainEnv Γ1 Γ2 of_envs (Envs Γ1 Enil) bi_plainly $ of_envs $ Envs Γ2 Enil. by rewrite always_modality_and -affinely_persistently_and.
Proof. - inversion 1; constructor; auto.
intros [Hsub ?]. rewrite !of_envs_eq plainly_and plainly_pure /=. f_equiv. - intros j. destruct (ident_beq _ _); naive_solver.
{ f_equiv=>-[/= ???]. split; auto. by eapply env_subenv_wf. } Qed.
rewrite !(right_id emp%I). trans ( [] Γ2)%I. Global Instance filter_persistent_env_snoc_not M (C : PROP Prop) Γ Γ' i P :
- do 2 f_equiv. clear -Hsub. FilterPersistentEnv M C Γ Γ'
induction Hsub as [|????? IH|????? IH]=>//=; rewrite IH //. apply and_elim_r. FilterPersistentEnv M C (Esnoc Γ i P) Γ' | 100.
- by rewrite {1}(plain ([] Γ2)) affinely_elim plainly_affinely Proof.
plainly_persistently persistently_plainly. intros [HΓ Hwf Hdom]; split; simpl.
Qed. - intros HC. by rewrite and_elim_r HΓ.
- inversion 1; auto.
Class IntoAlwaysEnvs (pe : bool) (pl : bool) (Δ1 Δ2 : envs PROP) := { - intros j. destruct (ident_beq _ _); naive_solver.
into_persistent_envs_persistent : Qed.
if pl then IntoPlainEnv (env_persistent Δ1) (env_persistent Δ2)
else env_persistent Δ1 = env_persistent Δ2; Class FilterSpatialEnv
into_persistent_envs_spatial : (M : always_modality PROP) (C : PROP Prop) (Γ1 Γ2 : env PROP) := {
if pe || pl then env_spatial Δ2 = Enil else env_spatial Δ1 = env_spatial Δ2 filter_spatial_env :
( P, C P P M P) ( P, Absorbing (M P))
([] Γ1) M ([] Γ2);
filter_spatial_env_wf : env_wf Γ1 env_wf Γ2;
filter_spatial_env_dom i : Γ1 !! i = None Γ2 !! i = None;
}. }.
Global Instance filter_spatial_env_nil M C : FilterSpatialEnv M C Enil Enil.
Global Instance into_always_false_false Δ : IntoAlwaysEnvs false false Δ Δ. Proof. split=> // HC /=. by rewrite -always_modality_emp. Qed.
Proof. by split. Qed. Global Instance filter_spatial_env_snoc M (C : PROP Prop) Γ Γ' i P :
Global Instance into_always_envs_true_false Γp Γs : C P
IntoAlwaysEnvs true false (Envs Γp Γs) (Envs Γp Enil). FilterSpatialEnv M C Γ Γ'
Proof. by split. Qed. FilterSpatialEnv M C (Esnoc Γ i P) (Esnoc Γ' i P).
Global Instance into_always_envs_x_true Γp1 Γp2 Γs1 pe : Proof.
IntoPlainEnv Γp1 Γp2 intros ? [HΓ Hwf Hdom]; split; simpl.
IntoAlwaysEnvs pe true (Envs Γp1 Γs1) (Envs Γp2 Enil). - intros HC ?. by rewrite {1}(HC P) // HΓ // always_modality_sep.
Proof. destruct pe; by split. Qed. - inversion 1; constructor; auto.
- intros j. destruct (ident_beq _ _); naive_solver.
Lemma tac_always_intro Δ Δ' a pe pl Q Q' : Qed.
FromAlways a pe pl Q' Q
(if a then AffineEnv (env_spatial Δ') else TCTrue) Global Instance filter_spatial_env_snoc_not M (C : PROP Prop) Γ Γ' i P :
IntoAlwaysEnvs pe pl Δ' Δ FilterSpatialEnv M C Γ Γ'
envs_entails Δ Q envs_entails Δ' Q'. FilterSpatialEnv M C (Esnoc Γ i P) Γ' | 100.
Proof. Proof.
rewrite /envs_entails => ? Haffine [Hep Hes] HQ. intros [HΓ Hwf Hdom]; split; simpl.
rewrite -(from_always a pe pl Q') -HQ. - intros HC ?. by rewrite HΓ // sep_elim_r.
trans (bi_affinely_if a (of_envs Δ')); - inversion 1; auto.
[destruct a=>//; by apply: affinely_intro|f_equiv]. - intros j. destruct (ident_beq _ _); naive_solver.
destruct pl; [|destruct pe]. Qed.
- rewrite (envs_clear_spatial_sound Δ') into_plain_env_sound sep_elim_l.
destruct Δ as [Δ ?]. rewrite orb_true_r /= in Hes. rewrite Hes /=. Ltac tac_always_cases :=
destruct pe=>/= //. by rewrite persistently_plainly. simplify_eq/=;
- rewrite (envs_clear_spatial_sound Δ') /= /envs_clear_spatial Hep. repeat match goal with
destruct Δ as [Δ ?]. simpl in Hes. subst. simpl. | H : TCAnd _ _ |- _ => destruct H
rewrite -(sep_elim_l (bi_persistently _)). f_equiv. | H : TCEq ?x _ |- _ => inversion H; subst x; clear H
rewrite {1}(env_spatial_is_nil_affinely_persistently (Envs Δ Enil)) //. | H : TCForall _ _ |- _ => apply TCForall_Forall in H
by rewrite affinely_elim. | H : FilterPersistentEnv _ _ _ _ |- _ => destruct H
- destruct Δ, Δ'; simpl in *. by subst. | H : FilterSpatialEnv _ _ _ _ |- _ => destruct H
end; simpl; auto using Enil_wf.
Lemma tac_always_intro Γp Γs Γp' Γs' M Q Q' :
FromAlways M Q' Q
match always_modality_persistent_spec M with
| AIEnvForall C => TCAnd (TCForall C (env_to_list Γp)) (TCEq Γp Γp')
| AIEnvFilter C => FilterPersistentEnv M C Γp Γp'
| AIEnvIsEmpty => TCAnd (TCEq Γp Enil) (TCEq Γp' Enil)
| AIEnvClear => TCEq Γp' Enil
| AIEnvId => TCEq Γp Γp'
end
match always_modality_spatial_spec M with
| AIEnvForall C => TCAnd (TCForall C (env_to_list Γs)) (TCEq Γs Γs')
| AIEnvFilter C => FilterSpatialEnv M C Γs Γs'
| AIEnvIsEmpty => TCAnd (TCEq Γs Enil) (TCEq Γs' Enil)
| AIEnvClear => TCEq Γs' Enil
| AIEnvId => TCEq Γs Γs'
end
envs_entails (Envs Γp' Γs') Q envs_entails (Envs Γp Γs) Q'.
Proof.
rewrite /envs_entails /FromAlways /of_envs /= => <- HΓp HΓs <-.
apply pure_elim_l=> -[???]. assert (envs_wf (Envs Γp' Γs')).
{ split; simpl in *.
- destruct (always_modality_persistent_spec M); tac_always_cases.
- destruct (always_modality_spatial_spec M); tac_always_cases.
- destruct (always_modality_persistent_spec M),
(always_modality_spatial_spec M); tac_always_cases; naive_solver. }
rewrite pure_True // left_id. rewrite -always_modality_sep. apply sep_mono.
- destruct (always_modality_persistent_spec M) eqn:?; tac_always_cases.
+ by rewrite {1}affinely_elim_emp (always_modality_emp M)
persistently_True_emp affinely_persistently_emp.
+ eauto using always_modality_persistent_forall_big_and.
+ eauto using always_modality_persistent_filter.
+ by rewrite {1}affinely_elim_emp (always_modality_emp M)
persistently_True_emp affinely_persistently_emp.
+ eauto using always_modality_persistent_id.
- destruct (always_modality_spatial_spec M) eqn:?; tac_always_cases.
+ by rewrite -always_modality_emp.
+ eauto using always_modality_spatial_forall_big_sep.
+ eauto using always_modality_spatial_filter,
always_modality_spatial_filter_absorbing.
+ rewrite -(always_modality_spatial_clear M) // -always_modality_emp.
by rewrite -absorbingly_True_emp absorbingly_pure -True_intro.
+ by destruct (always_modality_spatial_id M).
Qed. Qed.
Lemma tac_persistent Δ Δ' i p P P' Q : Lemma tac_persistent Δ Δ' i p P P' Q :
......
From iris.bi Require Export monpred. From iris.bi Require Export monpred.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics class_instances.
Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I) Class MakeMonPredAt {I : biIndex} {PROP : bi} (i : I)
(P : monPred I PROP) (𝓟 : PROP) := (P : monPred I PROP) (𝓟 : PROP) :=
...@@ -137,12 +137,24 @@ Proof. ...@@ -137,12 +137,24 @@ Proof.
by rewrite -monPred_at_persistently -monPred_at_persistently_if. by rewrite -monPred_at_persistently -monPred_at_persistently_if.
Qed. Qed.
Global Instance from_always_monPred_at a pe P Q 𝓠 i : Global Instance from_always_affinely_monPred_at P Q 𝓠 i :
FromAlways a pe false P Q MakeMonPredAt i Q 𝓠 FromAlways always_modality_affinely P Q MakeMonPredAt i Q 𝓠
FromAlways a pe false (P i) 𝓠 | 0. FromAlways always_modality_affinely (P i) 𝓠 | 0.
Proof. Proof.
rewrite /FromAlways /MakeMonPredAt /bi_persistently_if /bi_affinely_if=><- /=. rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_affinely.
destruct a, pe=><- /=; by rewrite ?monPred_at_affinely ?monPred_at_persistently. Qed.
Global Instance from_always_persistently_monPred_at P Q 𝓠 i :
FromAlways always_modality_persistently P Q MakeMonPredAt i Q 𝓠
FromAlways always_modality_persistently (P i) 𝓠 | 0.
Proof.
rewrite /FromAlways /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Qed.
Global Instance from_always_affinely_persistently_monPred_at P Q 𝓠 i :
FromAlways always_modality_affinely_persistently P Q MakeMonPredAt i Q 𝓠
FromAlways always_modality_affinely_persistently (P i) 𝓠 | 0.
Proof.
rewrite /FromAlways /MakeMonPredAt /==> <- <-.
by rewrite monPred_at_affinely monPred_at_persistently.
Qed. Qed.
Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i : Lemma into_wand_monPred_at_unknown_unknown p q R P 𝓟 Q 𝓠 i :
......
...@@ -903,10 +903,18 @@ Local Tactic Notation "iExistDestruct" constr(H) ...@@ -903,10 +903,18 @@ Local Tactic Notation "iExistDestruct" constr(H)
Tactic Notation "iAlways":= Tactic Notation "iAlways":=
iStartProof; iStartProof;
eapply tac_always_intro; eapply tac_always_intro;
[apply _ (* || fail "iAlways: the goal is not a persistently modality" *) [apply _ ||
|env_cbv; apply _ || fail "iAlways: the goal is not an always-style modality"
fail "iAlways: spatial context contains non-affine hypotheses" |hnf; env_cbv; apply _ ||
|apply _ lazymatch goal with
| |- TCAnd (TCForall ?C _) _ => fail "iAlways: persistent context does not satisfy" C
| |- TCAnd (TCEq _ Enil) _ => fail "iAlways: persistent context is non-empty"
end
|hnf; env_cbv; apply _ ||
lazymatch goal with
| |- TCAnd (TCForall ?C _) _ => fail "iAlways: spatial context does not satisfy" C
| |- TCAnd (TCEq _ Enil) _ => fail "iAlways: spatial context is non-empty"
end
|env_cbv]. |env_cbv].
(** * Later *) (** * Later *)
......
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