Commit ef2adeb3 authored by Ralf Jung's avatar Ralf Jung
Browse files

Merge branch 'ralf/intuitionistically' into 'gen_proofmode'

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

See merge request FP/iris-coq!130
parents 93ef2352 ff398120
Pipeline #7539 passed with stage
in 22 minutes and 40 seconds
......@@ -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
......
......@@ -879,7 +879,7 @@ Qed.
Lemma impl_wand_persistently_2 P Q : (<pers> P - Q) (<pers> P Q).
Proof. apply impl_intro_l. by rewrite persistently_and_sep_l_1 wand_elim_r. Qed.
Section persistently_affinely_bi.
Section persistently_affine_bi.
Context `{BiAffine PROP}.
Lemma persistently_emp : <pers> emp emp.
......@@ -926,72 +926,122 @@ Section persistently_affinely_bi.
- apply exist_elim=> R. apply impl_intro_l.
by rewrite assoc persistently_and_sep_r persistently_elim wand_elim_r.
Qed.
End persistently_affinely_bi.
End persistently_affine_bi.
(* The combined affinely persistently modality *)
Lemma affinely_persistently_elim P : P P.
(* The intuitionistic modality *)
Global Instance intuitionistically_ne : NonExpansive (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
Global Instance intuitionistically_proper : Proper (() ==> ()) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
Global Instance intuitionistically_mono' : Proper (() ==> ()) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
Global Instance intuitionistically_flip_mono' :
Proper (flip () ==> flip ()) (@bi_intuitionistically PROP).
Proof. solve_proper. Qed.
Lemma intuitionistically_elim P : P P.
Proof. apply persistently_and_emp_elim. Qed.
Lemma affinely_persistently_intro' P Q : ( P Q) P Q.
Proof. intros <-. by rewrite persistently_affinely persistently_idemp. Qed.
Lemma intuitionistically_elim_emp P : P emp.
Proof. rewrite /bi_intuitionistically affinely_elim_emp //. Qed.
Lemma intuitionistically_intro' P Q : ( P Q) P Q.
Proof.
intros <-.
by rewrite /bi_intuitionistically persistently_affinely persistently_idemp.
Qed.
Lemma affinely_persistently_emp : emp emp.
Lemma intuitionistically_emp : emp emp.
Proof.
by rewrite -persistently_True_emp persistently_pure affinely_True_emp
affinely_emp.
by rewrite /bi_intuitionistically -persistently_True_emp persistently_pure
affinely_True_emp affinely_emp.
Qed.
Lemma affinely_persistently_and P Q : (P Q) P Q.
Proof. by rewrite persistently_and affinely_and. Qed.
Lemma affinely_persistently_or P Q : (P Q) P Q.
Proof. by rewrite persistently_or affinely_or. Qed.
Lemma affinely_persistently_exist {A} (Φ : A PROP) : ( x, Φ x) x, Φ x.
Proof. by rewrite persistently_exist affinely_exist. Qed.
Lemma affinely_persistently_sep_2 P Q : P Q (P Q).
Proof. by rewrite affinely_sep_2 persistently_sep_2. Qed.
Lemma affinely_persistently_sep `{BiPositive PROP} P Q : (P Q) P Q.
Proof. by rewrite -affinely_sep -persistently_sep. Qed.
Lemma intuitionistically_True_emp : True emp.
Proof.
rewrite -intuitionistically_emp /bi_intuitionistically
persistently_True_emp //.
Qed.
Lemma intuitionistically_and P Q : (P Q) P Q.
Proof. by rewrite /bi_intuitionistically persistently_and affinely_and. Qed.
Lemma intuitionistically_forall {A} (Φ : A PROP) : ( x, Φ x) x, Φ x.
Proof. by rewrite /bi_intuitionistically persistently_forall affinely_forall. Qed.
Lemma intuitionistically_or P Q : (P Q) P Q.
Proof. by rewrite /bi_intuitionistically persistently_or affinely_or. Qed.
Lemma intuitionistically_exist {A} (Φ : A PROP) : ( x, Φ x) x, Φ x.
Proof. by rewrite /bi_intuitionistically persistently_exist affinely_exist. Qed.
Lemma intuitionistically_sep_2 P Q : P Q (P Q).
Proof. by rewrite /bi_intuitionistically affinely_sep_2 persistently_sep_2. Qed.
Lemma intuitionistically_sep `{BiPositive PROP} P Q : (P Q) P Q.
Proof. by rewrite /bi_intuitionistically -affinely_sep -persistently_sep. Qed.
Lemma intuitionistically_idemp P : P P.
Proof. by rewrite /bi_intuitionistically persistently_affinely persistently_idemp. Qed.
Lemma affinely_persistently_idemp P : P P.
Proof. by rewrite persistently_affinely persistently_idemp. Qed.
Lemma intuitionistically_persistently_1 P : P <pers> P.
Proof. rewrite /bi_intuitionistically affinely_elim //. Qed.
Lemma intuitionistically_persistently_persistently P : <pers> P P.
Proof. rewrite /bi_intuitionistically persistently_idemp //. Qed.
Lemma persistently_and_affinely_sep_l P Q : <pers> P Q P Q.
Lemma intuitionistic_intuitionistically P :
Affine P Persistent P P P.
Proof.
apply (anti_symm _).
intros. apply (anti_symm _); first exact: intuitionistically_elim.
rewrite -{1}(affine_affinely P) {1}(persistent P) //.
Qed.
Lemma intuitionistically_affinely P : P <affine> P.
Proof.
rewrite /bi_intuitionistically /bi_affinely. apply and_intro.
- rewrite and_elim_l //.
- apply persistently_and_emp_elim.
Qed.
Lemma intuitionistically_affinely_affinely P : <affine> P P.
Proof. rewrite /bi_intuitionistically persistently_affinely //. Qed.
Lemma persistently_and_intuitionistically_sep_l P Q : <pers> P Q P Q.
Proof.
rewrite /bi_intuitionistically. apply (anti_symm _).
- by rewrite /bi_affinely -(comm bi_and (<pers> P)%I)
-persistently_and_sep_assoc left_id.
- apply and_intro.
+ by rewrite affinely_elim persistently_absorbing.
+ by rewrite affinely_elim_emp left_id.
Qed.
Lemma persistently_and_affinely_sep_r P Q : P <pers> Q P Q.
Proof. by rewrite !(comm _ P) persistently_and_affinely_sep_l. Qed.
Lemma and_sep_affinely_persistently P Q : P Q P Q.
Lemma persistently_and_intuitionistically_sep_r P Q : P <pers> Q P Q.
Proof. by rewrite !(comm _ P) persistently_and_intuitionistically_sep_l. Qed.
Lemma and_sep_intuitionistically P Q : P Q P Q.
Proof.
by rewrite -persistently_and_affinely_sep_l -affinely_and affinely_and_r.
by rewrite -persistently_and_intuitionistically_sep_l -affinely_and affinely_and_r.
Qed.
Lemma affinely_persistently_sep_dup P : P P P.
Lemma intuitionistically_sep_dup P : P P P.
Proof.
by rewrite -persistently_and_affinely_sep_l affinely_and_r idemp.
by rewrite -persistently_and_intuitionistically_sep_l affinely_and_r idemp.
Qed.
Lemma impl_wand_affinely_persistently P Q : (<pers> P Q) ( P - Q).
Lemma impl_wand_intuitionistically P Q : (<pers> P Q) ( P - Q).
Proof.
apply (anti_symm ()).
- apply wand_intro_l. by rewrite -persistently_and_affinely_sep_l impl_elim_r.
- apply impl_intro_l. by rewrite persistently_and_affinely_sep_l wand_elim_r.
- apply wand_intro_l. by rewrite -persistently_and_intuitionistically_sep_l impl_elim_r.
- apply impl_intro_l. by rewrite persistently_and_intuitionistically_sep_l wand_elim_r.
Qed.
Lemma affinely_persistently_alt_fixpoint P :
Lemma intuitionistically_alt_fixpoint P :
P emp (P P).
Proof.
apply (anti_symm ()).
- apply and_intro; first exact: affinely_elim_emp.
rewrite {1}affinely_persistently_sep_dup. apply sep_mono; last done.
apply affinely_persistently_elim.
- apply and_mono; first done. rewrite {2}persistently_alt_fixpoint.
rewrite {1}intuitionistically_sep_dup. apply sep_mono; last done.
apply intuitionistically_elim.
- apply and_mono; first done. rewrite /bi_intuitionistically {2}persistently_alt_fixpoint.
apply sep_mono; first done. apply and_elim_r.
Qed.
Section bi_affine_intuitionistically.
Context `{BiAffine PROP}.
Lemma intuitionistically_persistently P : P <pers> P.
Proof. rewrite /bi_intuitionistically affine_affinely //. Qed.
End bi_affine_intuitionistically.
(* Conditional affinely modality *)
Global Instance affinely_if_ne p : NonExpansive (@bi_affinely_if PROP p).
Proof. solve_proper. Qed.
......@@ -1067,37 +1117,49 @@ Proof. destruct p; simpl; auto using persistently_sep. Qed.
Lemma persistently_if_idemp p P : <pers>?p <pers>?p P <pers>?p P.
Proof. destruct p; simpl; auto using persistently_idemp. Qed.
(* Conditional affinely persistently *)
Lemma affinely_persistently_if_mono p P Q : (P Q) ?p P ?p Q.
(* Conditional intuitionistically *)
Global Instance intuitionistically_if_ne p : NonExpansive (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
Global Instance intuitionistically_if_proper p :
Proper (() ==> ()) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
Global Instance intuitionistically_if_mono' p :
Proper (() ==> ()) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
Global Instance intuitionistically_if_flip_mono' p :
Proper (flip () ==> flip ()) (@bi_intuitionistically_if PROP p).
Proof. solve_proper. Qed.
Lemma intuitionistically_if_mono p P Q : (P Q) ?p P ?p Q.
Proof. by intros ->. Qed.
Lemma affinely_persistently_if_flag_mono (p q : bool) P :
Lemma intuitionistically_if_flag_mono (p q : bool) P :
(q p) ?p P ?q P.
Proof. destruct p, q; naive_solver auto using affinely_persistently_elim. Qed.
Lemma affinely_persistently_if_elim p P : ?p P P.
Proof. destruct p; simpl; auto using affinely_persistently_elim. Qed.
Lemma affinely_persistently_affinely_persistently_if p P : P ?p P.
Proof. destruct p; simpl; auto using affinely_persistently_elim. Qed.
Lemma affinely_persistently_if_intro' p P Q : (?p P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using affinely_persistently_intro'. Qed.
Lemma affinely_persistently_if_emp p : ?p emp emp.
Proof. destruct p; simpl; auto using affinely_persistently_emp. Qed.
Lemma affinely_persistently_if_and p P Q : ?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using affinely_persistently_and. Qed.
Lemma affinely_persistently_if_or p P Q : ?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using affinely_persistently_or. Qed.
Lemma affinely_persistently_if_exist {A} p (Ψ : A PROP) :
Proof. destruct p, q; naive_solver auto using intuitionistically_elim. Qed.
Lemma intuitionistically_if_elim p P : ?p P P.
Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
Lemma intuitionistically_intuitionistically_if p P : P ?p P.
Proof. destruct p; simpl; auto using intuitionistically_elim. Qed.
Lemma intuitionistically_if_intro' p P Q : (?p P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using intuitionistically_intro'. Qed.
Lemma intuitionistically_if_emp p : ?p emp emp.
Proof. destruct p; simpl; auto using intuitionistically_emp. Qed.
Lemma intuitionistically_if_and p P Q : ?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using intuitionistically_and. Qed.
Lemma intuitionistically_if_or p P Q : ?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using intuitionistically_or. Qed.
Lemma intuitionistically_if_exist {A} p (Ψ : A PROP) :
(?p a, Ψ a) a, ?p Ψ a.
Proof. destruct p; simpl; auto using affinely_persistently_exist. Qed.
Lemma affinely_persistently_if_sep_2 p P Q : ?p P ?p Q ?p (P Q).
Proof. destruct p; simpl; auto using affinely_persistently_sep_2. Qed.
Lemma affinely_persistently_if_sep `{BiPositive PROP} p P Q :
Proof. destruct p; simpl; auto using intuitionistically_exist. Qed.
Lemma intuitionistically_if_sep_2 p P Q : ?p P ?p Q ?p (P Q).
Proof. destruct p; simpl; auto using intuitionistically_sep_2. Qed.
Lemma intuitionistically_if_sep `{BiPositive PROP} p P Q :
?p (P Q) ?p P ?p Q.
Proof. destruct p; simpl; auto using affinely_persistently_sep. Qed.
Proof. destruct p; simpl; auto using intuitionistically_sep. Qed.
Lemma affinely_persistently_if_idemp p P : ?p ?p P ?p P.
Proof. destruct p; simpl; auto using affinely_persistently_idemp. Qed.
Lemma intuitionistically_if_idemp p P : ?p ?p P ?p P.
Proof. destruct p; simpl; auto using intuitionistically_idemp. Qed.
(* Properties of persistent propositions *)
Global Instance Persistent_proper : Proper (() ==> iff) (@Persistent PROP).
......@@ -1114,18 +1176,18 @@ Lemma persistently_intro P Q `{!Persistent P} : (P ⊢ Q) → P ⊢ <pers> Q.
Proof. intros HP. by rewrite (persistent P) HP. Qed.
Lemma persistent_and_affinely_sep_l_1 P Q `{!Persistent P} : P Q <affine> P Q.
Proof.
rewrite {1}(persistent_persistently_2 P) persistently_and_affinely_sep_l.
by rewrite -affinely_idemp affinely_persistently_elim.
rewrite {1}(persistent_persistently_2 P) persistently_and_intuitionistically_sep_l.
rewrite intuitionistically_affinely //.
Qed.
Lemma persistent_and_affinely_sep_r_1 P Q `{!Persistent Q} : P Q P <affine> Q.
Proof. by rewrite !(comm _ P) persistent_and_affinely_sep_l_1. Qed.
Lemma persistent_and_affinely_sep_l P Q `{!Persistent P, !Absorbing P} :
P Q <affine> P Q.
Proof. by rewrite -(persistent_persistently P) persistently_and_affinely_sep_l. Qed.
Proof. by rewrite -(persistent_persistently P) persistently_and_intuitionistically_sep_l. Qed.
Lemma persistent_and_affinely_sep_r P Q `{!Persistent Q, !Absorbing Q} :
P Q P <affine> Q.
Proof. by rewrite -(persistent_persistently Q) persistently_and_affinely_sep_r. Qed.
Proof. by rewrite -(persistent_persistently Q) persistently_and_intuitionistically_sep_r. Qed.
Lemma persistent_and_sep_1 P Q `{HPQ : !TCOr (Persistent P) (Persistent Q)} :
P Q P Q.
......@@ -1143,24 +1205,24 @@ Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
Lemma persistent_entails_r P Q `{!Persistent Q} : (P Q) P P Q.
Proof. intros. rewrite -persistent_and_sep_1; auto. Qed.
Lemma absorbingly_affinely_persistently P : <absorb> P <pers> P.
Lemma absorbingly_intuitionistically P : <absorb> P <pers> P.
Proof.
apply (anti_symm _).
- by rewrite affinely_elim absorbingly_persistently.
- rewrite -{1}(idemp bi_and (<pers> _)%I) persistently_and_affinely_sep_r.
- by rewrite intuitionistically_persistently_1 absorbingly_persistently.
- rewrite -{1}(idemp bi_and (<pers> _)%I) persistently_and_intuitionistically_sep_r.
by rewrite {1} (True_intro (<pers> _)%I).
Qed.
Lemma persistent_absorbingly_affinely_2 P `{!Persistent P} :
P <absorb> <affine> P.
Proof.
rewrite {1}(persistent P) -absorbingly_affinely_persistently.
by rewrite -{1}affinely_idemp affinely_persistently_elim.
rewrite {1}(persistent P) -absorbingly_intuitionistically.
by rewrite intuitionistically_affinely.
Qed.
Lemma persistent_absorbingly_affinely P `{!Persistent P, !Absorbing P} :
<absorb> <affine> P P.
Proof.
by rewrite -(persistent_persistently P) absorbingly_affinely_persistently.
by rewrite -(persistent_persistently P) absorbingly_intuitionistically.
Qed.
Lemma persistent_and_sep_assoc P `{!Persistent P, !Absorbing P} Q R :
......@@ -1205,6 +1267,8 @@ Global Instance sep_affine P Q : Affine P → Affine Q → Affine (P ∗ Q).
Proof. rewrite /Affine=>-> ->. by rewrite left_id. Qed.
Global Instance affinely_affine P : Affine (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance intuitionistically_affine P : Affine ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
(* Absorbing instances *)
Global Instance pure_absorbing φ : Absorbing (⌜φ⌝%I : PROP).
......@@ -1282,6 +1346,8 @@ Global Instance persistently_persistent P : Persistent (<pers> P).
Proof. by rewrite /Persistent persistently_idemp. Qed.
Global Instance affinely_persistent P : Persistent P Persistent (<affine> P).
Proof. rewrite /bi_affinely. apply _. Qed.
Global Instance intuitionistically_persistent P : Persistent ( P).
Proof. rewrite /bi_intuitionistically. apply _. Qed.
Global Instance absorbingly_persistent P : Persistent P Persistent (<absorb> P).
Proof. rewrite /bi_absorbingly. apply _. Qed.
Global Instance from_option_persistent {A} P (Ψ : A PROP) (mx : option A) :
......@@ -1565,10 +1631,10 @@ Lemma later_persistently P : ▷ <pers> P ⊣⊢ <pers> ▷ P.
Proof. apply (anti_symm _); auto using later_persistently_1, later_persistently_2. Qed.
Lemma later_affinely_2 P : <affine> P <affine> P.
Proof. rewrite /bi_affinely later_and. auto using later_intro. Qed.
Lemma later_affinely_persistently_2 P : P P.
Proof. by rewrite -later_persistently later_affinely_2. Qed.
Lemma later_affinely_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using later_affinely_persistently_2. Qed.
Lemma later_intuitionistically_2 P : P P.
Proof. by rewrite /bi_intuitionistically -later_persistently later_affinely_2. Qed.
Lemma later_intuitionistically_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using later_intuitionistically_2. Qed.
Lemma later_absorbingly P : <absorb> P <absorb> P.
Proof. by rewrite /bi_absorbingly later_sep later_True. Qed.
......@@ -1632,10 +1698,10 @@ Lemma laterN_persistently n P : ▷^n <pers> P ⊣⊢ <pers> ▷^n P.
Proof. induction n as [|n IH]; simpl; auto. by rewrite IH later_persistently. Qed.
Lemma laterN_affinely_2 n P : <affine> ^n P ^n <affine> P.
Proof. rewrite /bi_affinely laterN_and. auto using laterN_intro. Qed.
Lemma laterN_affinely_persistently_2 n P : ^n P ^n P.
Proof. by rewrite -laterN_persistently laterN_affinely_2. Qed.
Lemma laterN_affinely_persistently_if_2 n p P : ?p ^n P ^n ?p P.
Proof. destruct p; simpl; auto using laterN_affinely_persistently_2. Qed.
Lemma laterN_intuitionistically_2 n P : ^n P ^n P.
Proof. by rewrite /bi_intuitionistically -laterN_persistently laterN_affinely_2. Qed.
Lemma laterN_intuitionistically_if_2 n p P : ?p ^n P ^n ?p P.
Proof. destruct p; simpl; auto using laterN_intuitionistically_2. Qed.
Lemma laterN_absorbingly n P : ^n <absorb> P <absorb> ^n P.
Proof. by rewrite /bi_absorbingly laterN_sep laterN_True. Qed.
......@@ -1707,10 +1773,10 @@ Proof.
Qed.
Lemma except_0_affinely_2 P : <affine> P <affine> P.
Proof. rewrite /bi_affinely except_0_and. auto using except_0_intro. Qed.
Lemma except_0_affinely_persistently_2 P : P P.
Proof. by rewrite -except_0_persistently except_0_affinely_2. Qed.
Lemma except_0_affinely_persistently_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using except_0_affinely_persistently_2. Qed.
Lemma except_0_intuitionistically_2 P : P P.
Proof. by rewrite /bi_intuitionistically -except_0_persistently except_0_affinely_2. Qed.
Lemma except_0_intuitionistically_if_2 p P : ?p P ?p P.
Proof. destruct p; simpl; auto using except_0_intuitionistically_2. Qed.
Lemma except_0_absorbingly P : <absorb> P <absorb> P.
Proof. by rewrite /bi_absorbingly except_0_sep except_0_True. Qed.
......
......@@ -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).