Commit ee12aa64 authored by Ralf Jung's avatar Ralf Jung

rename affinely_persistently -> intuitionistically; and make it a TC-opaque definition

parent b1ddcc68
......@@ -73,7 +73,7 @@ Qed.
Global Instance into_and_ownM p (a b1 b2 : M) :
IsOp a b1 b2 IntoAnd p (uPred_ownM a) (uPred_ownM b1) (uPred_ownM b2).
Proof.
intros. apply affinely_persistently_if_mono. by rewrite (is_op a) ownM_op sep_and.
intros. apply intuitionistically_if_mono. by rewrite (is_op a) ownM_op sep_and.
Qed.
Global Instance into_sep_ownM (a b1 b2 : M) :
......
......@@ -20,7 +20,8 @@ Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ <pers> (✓ a :
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
Lemma affinely_persistently_ownM (a : M) : CoreId a uPred_ownM a uPred_ownM a.
Proof.
rewrite affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|].
rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
[by rewrite persistently_elim|].
by rewrite {1}persistently_ownM_core core_id_core.
Qed.
Lemma ownM_invalid (a : M) : ¬ {0} a uPred_ownM a False.
......@@ -33,7 +34,8 @@ Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a.
Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed.
Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) : a a.
Proof.
rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
first by rewrite persistently_elim.
apply:persistently_cmra_valid_1.
Qed.
Lemma bupd_ownM_update x y : x ~~> y uPred_ownM x |==> uPred_ownM y.
......
......@@ -68,4 +68,4 @@ Proof.
iIntros "[Hvs HQ]". iDestruct "Hvs" as (R) "[HR Hvs]".
iExists (R Q)%I. iFrame "HR HQ". by iApply vs_frame_r.
Qed.
End fupd.
\ No newline at end of file
End fupd.
......@@ -150,10 +150,10 @@ Section sep_list.
Proof.
apply wand_intro_l. revert Φ Ψ. induction l as [|x l IH]=> Φ Ψ /=.
{ by rewrite sep_elim_r. }
rewrite affinely_persistently_sep_dup -assoc [( _ _)%I]comm -!assoc assoc.
rewrite intuitionistically_sep_dup -assoc [( _ _)%I]comm -!assoc assoc.
apply sep_mono.
- rewrite (forall_elim 0) (forall_elim x) pure_True // True_impl.
by rewrite affinely_persistently_elim wand_elim_l.
by rewrite intuitionistically_elim wand_elim_l.
- rewrite comm -(IH (Φ S) (Ψ S)) /=.
apply sep_mono_l, affinely_mono, persistently_mono.
apply forall_intro=> k. by rewrite (forall_elim (S k)).
......@@ -423,10 +423,10 @@ Section gmap.
Proof.
apply wand_intro_l. induction m as [|i x m ? IH] using map_ind.
{ by rewrite sep_elim_r. }
rewrite !big_sepM_insert // affinely_persistently_sep_dup.
rewrite !big_sepM_insert // intuitionistically_sep_dup.
rewrite -assoc [( _ _)%I]comm -!assoc assoc. apply sep_mono.
- rewrite (forall_elim i) (forall_elim x) pure_True ?lookup_insert //.
by rewrite True_impl affinely_persistently_elim wand_elim_l.
by rewrite True_impl intuitionistically_elim wand_elim_l.
- rewrite comm -IH /=.
apply sep_mono_l, affinely_mono, persistently_mono, forall_mono=> k.
apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
......@@ -584,10 +584,10 @@ Section gset.
Proof.
apply wand_intro_l. induction X as [|x X ? IH] using collection_ind_L.
{ by rewrite sep_elim_r. }
rewrite !big_sepS_insert // affinely_persistently_sep_dup.
rewrite !big_sepS_insert // intuitionistically_sep_dup.
rewrite -assoc [( _ _)%I]comm -!assoc assoc. apply sep_mono.
- rewrite (forall_elim x) pure_True; last set_solver.
by rewrite True_impl affinely_persistently_elim wand_elim_l.
by rewrite True_impl intuitionistically_elim wand_elim_l.
- rewrite comm -IH /=. apply sep_mono_l, affinely_mono, persistently_mono.
apply forall_mono=> y. apply impl_intro_l, pure_elim_l=> ?.
by rewrite pure_True ?True_impl; last set_solver.
......
......@@ -26,9 +26,6 @@ Typeclasses Opaque bi_affinely.
Notation "'<affine>' P" := (bi_affinely P)
(at level 20, right associativity) : bi_scope.
Notation "□ P" := (<affine> <pers> P)%I
(at level 20, right associativity) : bi_scope.
Class Affine {PROP : bi} (Q : PROP) := affine : Q emp.
Arguments Affine {_} _%I : simpl never.
Arguments affine {_} _%I {_}.
......@@ -72,9 +69,22 @@ Notation "'<affine>?' p P" := (bi_affinely_if p P)
(at level 20, p at level 9, P at level 20,
right associativity, format "'<affine>?' p P") : bi_scope.
Notation "□? p P" := (<affine>?p <pers>?p P)%I
Definition bi_intuitionistically {PROP : bi} (P : PROP) : PROP :=
(<affine> <pers> P)%I.
Arguments bi_intuitionistically {_} _%I : simpl never.
Instance: Params (@bi_intuitionistically) 1.
Typeclasses Opaque bi_intuitionistically.
Notation "□ P" := (bi_intuitionistically P)%I
(at level 20, right associativity) : bi_scope.
Definition bi_intuitionistically_if {PROP : bi} (p : bool) (P : PROP) : PROP :=
(if p then P else P)%I.
Arguments bi_intuitionistically_if {_} !_ _%I /.
Instance: Params (@bi_intuitionistically_if) 2.
Typeclasses Opaque bi_intuitionistically_if.
Notation "'□?' p P" := (bi_intuitionistically_if p P)
(at level 20, p at level 9, P at level 20,
right associativity, format "□? p P") : bi_scope.
right associativity, format "'□?' p P") : bi_scope.
Fixpoint bi_hexist {PROP : bi} {As} : himpl As PROP PROP :=
match As return himpl As PROP PROP with
......
This diff is collapsed.
......@@ -145,10 +145,14 @@ Section embed.
Proof. by rewrite embed_and embed_emp. Qed.
Lemma embed_absorbingly P : <absorb> P <absorb> P.
Proof. by rewrite embed_sep embed_pure. Qed.
Lemma embed_intuitionistically P : ⎡□ P P.
Proof. rewrite embed_and embed_emp embed_persistently //. Qed.
Lemma embed_persistently_if P b : <pers>?b P <pers>?b P.
Proof. destruct b; simpl; auto using embed_persistently. Qed.
Lemma embed_affinely_if P b : <affine>?b P <affine>?b P.
Proof. destruct b; simpl; auto using embed_affinely. Qed.
Lemma embed_intuitionistically_if P b : ⎡□?b P ?b P.
Proof. destruct b; simpl; auto using embed_intuitionistically. Qed.
Lemma embed_hforall {As} (Φ : himpl As PROP1):
bi_hforall Φ⎤ bi_hforall (hcompose embed Φ).
Proof. induction As=>//. rewrite /= embed_forall. by do 2 f_equiv. Qed.
......
......@@ -85,7 +85,8 @@ Section greatest.
F (bi_greatest_fixpoint F) x bi_greatest_fixpoint F x.
Proof.
iIntros "HF". iExists (CofeMor (F (bi_greatest_fixpoint F))).
iIntros "{$HF} !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
(* FIXME: The framing here adds an <affine> modality that we have to introduce. *)
iIntros "{$HF} !# !#" (y) "Hy". iApply (bi_mono_pred with "[#] Hy").
iIntros "!#" (z) "?". by iApply greatest_fixpoint_unfold_1.
Qed.
......
......@@ -173,6 +173,6 @@ Section fractional.
- rewrite fractional /Frame /MakeSep=><-<-. by rewrite assoc.
- rewrite fractional /Frame /MakeSep=><-<-=>_.
by rewrite (comm _ Q (Φ q0)) !assoc (comm _ (Φ _)).
- move=>-[-> _]->. by rewrite bi.affinely_persistently_if_elim -fractional Qp_div_2.
- move=>-[-> _]->. by rewrite bi.intuitionistically_if_elim -fractional Qp_div_2.
Qed.
End fractional.
......@@ -637,12 +637,16 @@ Proof. intros i j. unseal. by rewrite objective_at. Qed.
Global Instance affinely_objective P `{!Objective P} : Objective (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance intuitionistically_objective P `{!Objective P} : Objective ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
Global Instance absorbingly_objective P `{!Objective P} : Objective (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance persistently_if_objective P p `{!Objective P} : Objective (<pers>?p P).
Proof. rewrite /bi_persistently_if. destruct p; apply _. Qed.
Global Instance affinely_if_objective P p `{!Objective P} : Objective (<affine>?p P).
Proof. rewrite /bi_affinely_if. destruct p; apply _. Qed.
Global Instance intuitionistically_if_objective P p `{!Objective P} : Objective (<affine>?p P).
Proof. rewrite /bi_intuitionistically_if. destruct p; apply _. Qed.
(** monPred_in *)
Lemma monPred_in_intro P : P i, monPred_in i P i.
......
......@@ -119,7 +119,7 @@ Global Instance plainly_flip_mono' :
Proof. intros P Q; apply plainly_mono. Qed.
Lemma affinely_plainly_elim P : <affine> P P.
Proof. by rewrite plainly_elim_persistently affinely_persistently_elim. Qed.
Proof. by rewrite plainly_elim_persistently /bi_affinely persistently_and_emp_elim. Qed.
Lemma persistently_plainly P : <pers> P P.
Proof.
......@@ -216,6 +216,14 @@ Qed.
Lemma plainly_affinely P : <affine> P P.
Proof. by rewrite /bi_affinely plainly_and -plainly_True_emp plainly_pure left_id. Qed.
Lemma intuitionistically_plainly_elim P : P - P.
Proof. rewrite intuitionistically_affinely plainly_elim_persistently //. Qed.
Lemma intuitionistically_plainly P : P - P.
Proof.
rewrite /bi_intuitionistically plainly_affinely affinely_elim.
rewrite persistently_plainly plainly_persistently. done.
Qed.
Lemma and_sep_plainly P Q : P Q P Q.
Proof.
apply (anti_symm _); auto using plainly_and_sep_l_1.
......@@ -252,7 +260,7 @@ Lemma impl_wand_plainly_2 P Q : (■ P -∗ Q) ⊢ (■ P → Q).
Proof. apply impl_intro_l. by rewrite plainly_and_sep_l_1 wand_elim_r. Qed.
Lemma impl_wand_affinely_plainly P Q : ( P Q) (<affine> P - Q).
Proof. by rewrite -(persistently_plainly P) impl_wand_affinely_persistently. Qed.
Proof. by rewrite -(persistently_plainly P) impl_wand_intuitionistically. Qed.
Lemma persistently_wand_affinely_plainly P Q :
(<affine> P - <pers> Q) <pers> (<affine> P - Q).
......@@ -441,6 +449,8 @@ Proof.
Qed.
Global Instance affinely_plain P : Plain P Plain (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance intuitionistically_plain P : Plain P Plain ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
Global Instance absorbingly_plain P : Plain P Plain (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance from_option_plain {A} P (Ψ : A PROP) (mx : option A) :
......
......@@ -76,7 +76,7 @@ Section increment_client.
(λ _ _, True))%I as "#Aupd".
{ iAlways. iExists True%I, True%I. repeat (iSplit; first done). clear x.
iIntros (E) "!# % _".
iIntros "!#" (E) "% _".
assert (E = ) as -> by set_solver.
iInv nroot as (x) ">H↦" "Hclose".
iMod fupd_intro_mask' as "Hclose2"; last iModIntro; first set_solver.
......
This diff is collapsed.
This diff is collapsed.
......@@ -6,8 +6,8 @@ Import bi.
(** The `iModIntro` tactic is not tied the Iris modalities, but can be
instantiated with a variety of modalities.
In order to plug in a modality, one has to decide for both the persistent and
spatial what action should be performed upon introducing the modality:
In order to plug in a modality, one has to decide for both the intuitionistic and
spatial context 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
......@@ -35,7 +35,7 @@ Arguments MIEnvId {_}.
Notation MIEnvFilter C := (MIEnvTransform (TCDiag C)).
Definition modality_intro_spec_persistent {PROP1 PROP2}
Definition modality_intro_spec_intuitionistic {PROP1 PROP2}
(s : modality_intro_spec PROP1 PROP2) : (PROP1 PROP2) Prop :=
match s with
| MIEnvIsEmpty => λ M, True
......@@ -63,7 +63,7 @@ Definition modality_intro_spec_spatial {PROP1 PROP2}
should satisfy to justify the given actions for both contexts: *)
Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 PROP2)
(pspec sspec : modality_intro_spec PROP1 PROP2) := {
modality_mixin_persistent : modality_intro_spec_persistent pspec M;
modality_mixin_intuitionistic : modality_intro_spec_intuitionistic pspec M;
modality_mixin_spatial : modality_intro_spec_spatial sspec M;
modality_mixin_emp : emp M emp;
modality_mixin_mono P Q : (P Q) M P M Q;
......@@ -72,23 +72,23 @@ Record modality_mixin {PROP1 PROP2 : bi} (M : PROP1 → PROP2)
Record modality (PROP1 PROP2 : bi) := Modality {
modality_car :> PROP1 PROP2;
modality_persistent_spec : modality_intro_spec PROP1 PROP2;
modality_intuitionistic_spec : modality_intro_spec PROP1 PROP2;
modality_spatial_spec : modality_intro_spec PROP1 PROP2;
modality_mixin_of :
modality_mixin modality_car modality_persistent_spec modality_spatial_spec
modality_mixin modality_car modality_intuitionistic_spec modality_spatial_spec
}.
Arguments Modality {_ _} _ {_ _} _.
Arguments modality_persistent_spec {_ _} _.
Arguments modality_intuitionistic_spec {_ _} _.
Arguments modality_spatial_spec {_ _} _.
Section modality.
Context {PROP1 PROP2} (M : modality PROP1 PROP2).
Lemma modality_persistent_transform C P Q :
modality_persistent_spec M = MIEnvTransform C C P Q P M ( Q).
Lemma modality_intuitionistic_transform C P Q :
modality_intuitionistic_spec M = MIEnvTransform C C P Q P M ( Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_and_transform C P Q :
modality_persistent_spec M = MIEnvTransform C M P M Q M (P Q).
modality_intuitionistic_spec M = MIEnvTransform C M P M Q M (P Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_transform C P Q :
modality_spatial_spec M = MIEnvTransform C C P Q P M Q.
......@@ -114,14 +114,14 @@ End modality.
Section modality1.
Context {PROP} (M : modality PROP PROP).
Lemma modality_persistent_forall C P :
modality_persistent_spec M = MIEnvForall C C P P M ( P).
Lemma modality_intuitionistic_forall C P :
modality_intuitionistic_spec M = MIEnvForall C C P P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_and_forall C P Q :
modality_persistent_spec M = MIEnvForall C M P M Q M (P Q).
modality_intuitionistic_spec M = MIEnvForall C M P M Q M (P Q).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_persistent_id P :
modality_persistent_spec M = MIEnvId P M ( P).
Lemma modality_intuitionistic_id P :
modality_intuitionistic_spec M = MIEnvId P M ( P).
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_spatial_forall C P :
modality_spatial_spec M = MIEnvForall C C P P M P.
......@@ -130,14 +130,14 @@ Section modality1.
modality_spatial_spec M = MIEnvId P M P.
Proof. destruct M as [??? []]; naive_solver. Qed.
Lemma modality_persistent_forall_big_and C Ps :
modality_persistent_spec M = MIEnvForall C
Lemma modality_intuitionistic_forall_big_and C Ps :
modality_intuitionistic_spec M = MIEnvForall C
Forall C Ps [] Ps M ( [] Ps).
Proof.
induction 2 as [|P Ps ? _ IH]; simpl.
- by rewrite persistently_pure affinely_True_emp affinely_emp -modality_emp.
- rewrite affinely_persistently_and -modality_and_forall // -IH.
by rewrite {1}(modality_persistent_forall _ P).
- by rewrite intuitionistically_True_emp -modality_emp.
- rewrite intuitionistically_and -modality_and_forall // -IH.
by rewrite {1}(modality_intuitionistic_forall _ P).
Qed.
Lemma modality_spatial_forall_big_sep C Ps :
modality_spatial_spec M = MIEnvForall C
......
......@@ -24,15 +24,15 @@ Section bi_modalities.
Definition modality_affinely :=
Modality _ modality_affinely_mixin.
Lemma modality_affinely_persistently_mixin :
Lemma modality_intuitionistically_mixin :
modality_mixin (λ P : PROP, P)%I MIEnvId MIEnvIsEmpty.
Proof.
split; simpl; eauto using equiv_entails_sym, affinely_persistently_emp,
affinely_mono, persistently_mono, affinely_persistently_idemp,
affinely_persistently_sep_2 with typeclass_instances.
split; simpl; eauto using equiv_entails_sym, intuitionistically_emp,
affinely_mono, persistently_mono, intuitionistically_idemp,
intuitionistically_sep_2 with typeclass_instances.
Qed.
Definition modality_affinely_persistently :=
Modality _ modality_affinely_persistently_mixin.
Definition modality_intuitionistically :=
Modality _ modality_intuitionistically_mixin.
Lemma modality_embed_mixin `{BiEmbed PROP PROP'} :
modality_mixin (@embed PROP PROP' _)
......@@ -66,7 +66,7 @@ Section sbi_modalities.
Proof.
split; simpl; split_and?; eauto using equiv_entails_sym, laterN_intro,
laterN_mono, laterN_and, laterN_sep with typeclass_instances.
rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_affinely_persistently_2.
rewrite /MaybeIntoLaterN=> P Q ->. by rewrite laterN_intuitionistically_2.
Qed.
Definition modality_laterN n :=
Modality _ (modality_laterN_mixin n).
......
......@@ -62,8 +62,8 @@ Proof.
rewrite /FromModal /MakeMonPredAt /==> <- <-. by rewrite monPred_at_persistently.
Qed.
Global Instance from_modal_affinely_persistently_monPred_at `(sel : A) P Q 𝓠 i :
FromModal modality_affinely_persistently sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_affinely_persistently sel (P i) 𝓠 | 0.
FromModal modality_intuitionistically sel P Q MakeMonPredAt i Q 𝓠
FromModal modality_intuitionistically sel (P i) 𝓠 | 0.
Proof.
rewrite /FromModal /MakeMonPredAt /==> <- <-.
by rewrite monPred_at_affinely monPred_at_persistently.
......@@ -126,13 +126,13 @@ Global Instance from_assumption_make_monPred_at_l p i j P 𝓟 :
MakeMonPredAt i P 𝓟 IsBiIndexRel j i KnownLFromAssumption p (P j) 𝓟.
Proof.
rewrite /MakeMonPredAt /KnownLFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
apply bi.affinely_persistently_if_elim.
apply bi.intuitionistically_if_elim.
Qed.
Global Instance from_assumption_make_monPred_at_r p i j P 𝓟 :
MakeMonPredAt i P 𝓟 IsBiIndexRel i j KnownRFromAssumption p 𝓟 (P j).
Proof.
rewrite /MakeMonPredAt /KnownRFromAssumption /FromAssumption /IsBiIndexRel=><- ->.
apply bi.affinely_persistently_if_elim.
apply bi.intuitionistically_if_elim.
Qed.
Global Instance from_assumption_make_monPred_objectively P Q :
......
......@@ -1981,6 +1981,7 @@ Hint Extern 1 (envs_entails _ (▷ _)) => iNext.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ (<pers> _)) => iAlways.
Hint Extern 1 (envs_entails _ (<affine> _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _)) => iAlways.
Hint Extern 1 (envs_entails _ ( _, _)) => iExists _.
Hint Extern 1 (envs_entails _ ( _)) => iModIntro.
Hint Extern 1 (envs_entails _ (_ _)) => iLeft.
......
From iris.proofmode Require Import tactics monpred.
From iris.base_logic Require Import base_logic lib.invariants.
Section tests.
Context {I : biIndex} {PROP : sbi}.
......
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