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

Bump Iris (sbi changes).

parent a180a025
Pipeline #29361 failed with stage
in 18 minutes and 8 seconds
......@@ -9,5 +9,5 @@ build: [make "-j%{jobs}%"]
install: [make "install"]
remove: [ "sh" "-c" "rm -rf '%{lib}%/coq/user-contrib/iron" ]
depends: [
"coq-iris" { (= "dev.2020-05-18.2.fdda97e8") | (= "dev") }
"coq-iris" { (= "dev.2020-05-24.1.76bec8b7") | (= "dev") }
]
......@@ -26,11 +26,11 @@ Arguments fracPred_at {_} _ _.
Section ofe.
Context {PROP : bi}.
Inductive fracPred_equiv' (P Q : fracPred PROP) :=
{ monPred_in_equiv π : P π Q π }.
{ fracPred_in_equiv π : P π Q π }.
Instance fracPred_equiv : Equiv (fracPred PROP) := fracPred_equiv'.
Inductive fracPred_dist' (n : nat) (P Q : fracPred PROP) :=
{ monPred_in_dist π : P π {n} Q π }.
{ fracPred_in_dist π : P π {n} Q π }.
Instance fracPred_dist : Dist (fracPred PROP) := fracPred_dist'.
Lemma fracPred_ofe_mixin : OfeMixin (fracPred PROP).
......@@ -53,7 +53,7 @@ Section ofe.
Proof. by intros ?? [?] ?? ->. Qed.
End ofe.
(** BI and SBI structures. *)
(** BI canonical structure *)
Section bi.
Context {PROP : bi}.
Notation fracPred := (fracPred PROP).
......@@ -122,38 +122,23 @@ Section bi.
Definition fracPred_persistently := fracPred_persistently_aux.(unseal).
Definition fracPred_persistently_eq : @fracPred_persistently = _ :=
fracPred_persistently_aux.(seal_eq).
End bi.
Section sbi.
Context {PROP : sbi}.
Notation fracPred := (fracPred PROP).
Definition fracPred_internal_eq_def (A : ofeT) (a b : A) : fracPred :=
FracPred (λ _, a b)%I.
Definition fracPred_internal_eq_aux : seal (@fracPred_internal_eq_def). by eexists. Qed.
Definition fracPred_internal_eq := fracPred_internal_eq_aux.(unseal).
Definition fracPred_internal_eq_eq : @fracPred_internal_eq = _ :=
fracPred_internal_eq_aux.(seal_eq).
Definition fracPred_later_def (P : fracPred) : fracPred := FracPred (λ π, P π)%I.
Definition fracPred_later_aux : seal fracPred_later_def. by eexists. Qed.
Definition fracPred_later := fracPred_later_aux.(unseal).
Definition fracPred_later_eq : fracPred_later = _ := fracPred_later_aux.(seal_eq).
End sbi.
End bi.
Module Import fracPred.
Definition unseal_eqs :=
(@fracPred_and_eq, @fracPred_or_eq, @fracPred_impl_eq,
@fracPred_forall_eq, @fracPred_exist_eq, @fracPred_sep_eq, @fracPred_wand_eq,
@fracPred_persistently_eq, @fracPred_later_eq, @fracPred_internal_eq_eq,
@fracPred_persistently_eq, @fracPred_later_eq,
@fracPred_embed_eq, @fracPred_emp_eq, @fracPred_pure_eq).
Ltac unseal :=
unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, sbi_internal_eq, bi_sep, bi_wand,
bi_persistently, bi_affinely, sbi_later;
simpl;
unfold sbi_emp, sbi_pure, sbi_and, sbi_or, sbi_impl, sbi_forall, sbi_exist,
sbi_internal_eq, sbi_sep, sbi_wand, sbi_persistently;
unfold bi_affinely, bi_absorbingly, bi_except_0, bi_pure, bi_emp, bi_and, bi_or,
bi_impl, bi_forall, bi_exist, bi_sep, bi_wand,
bi_persistently, bi_affinely, bi_later;
simpl;
rewrite !unseal_eqs /=.
End fracPred.
......@@ -220,33 +205,20 @@ Proof.
rewrite left_id_L bi.pure_True // left_id. by apply bi.persistently_and_sep_elim.
Qed.
Canonical Structure fracPredI (PROP : bi) : bi :=
{| bi_ofe_mixin := fracPred_ofe_mixin; bi_bi_mixin := fracPred_bi_mixin PROP |}.
Lemma fracPred_sbi_mixin (PROP : sbi) :
SbiMixin (PROP:=fracPred PROP) fracPred_entails fracPred_pure
fracPred_or fracPred_impl fracPred_forall fracPred_exist
fracPred_sep fracPred_persistently fracPred_internal_eq fracPred_later.
Lemma fracPred_bi_later_mixin (PROP : bi) : BiLaterMixin (PROP:=fracPred PROP)
fracPred_entails fracPred_pure fracPred_or fracPred_impl
fracPred_forall fracPred_exist fracPred_sep
fracPred_persistently fracPred_later.
Proof.
split; unseal.
- intros n P Q HPQ. split=> π /=.
apply bi.later_contractive. destruct n as [|n]=> //. by apply HPQ.
- by split=> ? /=; repeat f_equiv.
- intros A P a. split=> π. by apply bi.internal_eq_refl.
- intros A a b Ψ ?. split=> π /=.
erewrite (bi.internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
- intros A1 A2 f g. split=> π. by apply bi.fun_ext.
- intros A P x y. split=> π. by apply bi.sig_eq.
- intros A a b ?. split=> π. by apply bi.discrete_eq_1.
- intros A x y. split=> π. by apply bi.later_eq_1.
- intros A x y. split=> π. by apply bi.later_eq_2.
- intros P Q [?]. split=> π. by apply bi.later_mono.
- intros P. split=> π /=. by apply bi.later_intro.
- intros A Ψ. split=> π. by apply bi.later_forall_2.
- intros A Ψ. split=> π. by apply bi.later_exist_false.
- intros A Ψ. split=> π. simpl. by apply bi.later_exist_false.
- intros P Q. split=> π /=. repeat setoid_rewrite bi.later_exist.
apply bi.exist_elim=> π1. apply bi.exist_elim=> π2.
rewrite bi.later_and (timeless _ %I) /sbi_except_0 bi.and_or_r.
rewrite bi.later_and (timeless _ %I) /bi_except_0 bi.and_or_r.
apply bi.or_elim.
{ rewrite bi.and_elim_l -(bi.exist_intro π) -(bi.exist_intro ε).
rewrite right_id_L -bi.later_sep.
......@@ -260,9 +232,9 @@ Proof.
- intros P. split=> π /=. apply bi.later_false_em.
Qed.
Canonical Structure fracPredSI (PROP: sbi) : sbi :=
{| sbi_ofe_mixin := fracPred_ofe_mixin; sbi_bi_mixin := fracPred_bi_mixin PROP;
sbi_sbi_mixin := fracPred_sbi_mixin PROP |}.
Canonical Structure fracPredI (PROP : bi) : bi :=
{| bi_ofe_mixin := fracPred_ofe_mixin; bi_bi_mixin := fracPred_bi_mixin PROP;
bi_bi_later_mixin := fracPred_bi_later_mixin PROP |}.
Class FObjective {PROP : bi} (P : fracPred PROP) :=
fobjective_at π π' : P π - P π'.
......@@ -286,6 +258,11 @@ Section bi_facts.
Proper (flip () ==> (=) ==> flip ()) fracPred_at.
Proof. solve_proper. Qed.
Global Instance fracPred_later_contractive :
Contractive (bi_later (PROP:=PROP)) Contractive (bi_later (PROP:=fracPredI)).
Proof. unseal=> ? n P Q HPQ. split=> i /=. f_contractive. apply HPQ. Qed.
Global Instance fracPred_bi_löb : BiLöb PROP BiLöb fracPredI.
Proof. split=> i. unseal. by apply löb. Qed.
Global Instance fracPred_positive : BiPositive PROP BiPositive fracPredI.
Proof.
split => π. unseal. rewrite bi.affinely_and_l -bi.affinely_and_r.
......@@ -318,6 +295,10 @@ Section bi_facts.
split; try apply _; unfold bi_emp_valid; unseal; try done.
- move => P [/(_ inhabitant) /= <-].
by apply (bi.affinely_intro _ _), bi.pure_intro.
- intros PROP' ? P Q.
set (f P := fracPred_at P inhabitant).
assert (NonExpansive f) by solve_proper.
apply (f_equivI f).
- split=> π /=. by apply bi.affinely_elim_emp.
- split=> π /=. apply (anti_symm _).
+ by rewrite -(bi.exist_intro π) -(bi.exist_intro ε) right_id_L bi.pure_True // left_id.
......@@ -455,7 +436,7 @@ Section bi_facts.
Proof. by rewrite fracPred_bupd_eq. Qed.
Global Instance fracPred_bi_embed_bupd `{BiBUpd PROP} : BiEmbedBUpd PROP fracPredI.
Proof. split. split=>π /=. by rewrite fracPred_at_bupd !fracPred_at_embed. Qed.
Proof. split=>π /=. by rewrite fracPred_at_bupd !fracPred_at_embed. Qed.
Global Instance bupd_objective `{BiBUpd PROP} P :
FObjective P FObjective (|==> P).
......@@ -468,46 +449,16 @@ Section bi_facts.
rewrite !bi.affine_affinely. apply bi.pure_elim_l=> ->.
by rewrite bi.pure_True // left_id.
Qed.
End bi_facts.
Hint Immediate persistent_objective : typeclass_instances.
Section sbi_facts.
Context {PROP : sbi}.
Local Notation fracPred := (fracPred PROP).
Local Notation fracPredSI := (fracPredSI PROP).
Implicit Types P Q : fracPred.
(** Later *)
Global Instance fracPred_bi_embed_later : BiEmbedLater PROP fracPredI.
Proof. split; by unseal. Qed.
Global Instance fracPred_sbi_embed : SbiEmbed PROP fracPredSI.
Proof.
split; unseal=> //. intros ? P Q.
apply (@bi.f_equiv _ _ _ (λ P, fracPred_at P inhabitant)); solve_proper.
Qed.
Lemma fracPred_internal_eq_unfold : @sbi_internal_eq fracPredSI = λ A x y, x y %I.
Proof. by unseal. Qed.
(** Unfolding lemmas *)
Lemma fracPred_at_internal_eq {A : ofeT} π (a b : A) :
@fracPred_at PROP (a b) π a b.
Proof. rewrite fracPred_internal_eq_unfold. by apply fracPred_at_embed. Qed.
Lemma fracPred_at_later π P : ( P) π P π.
Proof. by unseal. Qed.
Lemma fracPred_at_except_0 π P : ( P) π P π.
Proof. by unseal. Qed.
Lemma fracPred_equivI {PROP' : sbi} P Q :
sbi_internal_eq (PROP:=PROP') P Q π, P π Q π.
Proof.
apply bi.equiv_spec. split.
- apply bi.forall_intro=>?. apply (bi.f_equiv (flip fracPred_at _)).
- rewrite {2}(_ : P = FracPred P); last by destruct P.
rewrite {2}(_ : Q = FracPred Q); last by destruct Q.
by rewrite -(@bi.f_equiv _ _ _ (@FracPred PROP : (_ -d> _) fracPred)
ltac:(by constructor)) -bi.fun_ext.
Qed.
Lemma fracPred_at_timeless_alt P : Timeless P π, Timeless (P π).
Proof.
rewrite /Timeless; split.
......@@ -515,22 +466,70 @@ Section sbi_facts.
- intros HP; split=> π. by rewrite fracPred_at_later fracPred_at_except_0.
Qed.
Global Instance fracPred_emp_timeless :
Timeless (@bi_emp PROP) Timeless (@bi_emp (fracPredI PROP)).
Timeless (@bi_emp PROP) Timeless (@bi_emp fracPredI).
Proof. intros. apply fracPred_at_timeless_alt. unseal. apply _. Qed.
Global Instance fracPred_at_timeless P π : Timeless P Timeless (P π).
Proof. rewrite fracPred_at_timeless_alt. auto. Qed.
(** Objective *)
Global Instance internal_eq_objective {A : ofeT} (x y : A) :
@FObjective PROP (x y).
Proof. intros ??. by unseal. Qed.
Global Instance later_objective P : FObjective P FObjective ( P).
Proof. intros ? π π'. unseal. by f_equiv. Qed.
Global Instance laterN_objective P n : FObjective P FObjective (^n P).
Proof. induction n; apply _. Qed.
Global Instance except0_objective P : FObjective P FObjective ( P).
Proof. rewrite /sbi_except_0. apply _. Qed.
Proof. rewrite /bi_except_0. apply _. Qed.
(** Internal equality *)
Definition fracPred_internal_eq_def `{!BiInternalEq PROP} (A : ofeT) (a b : A) : fracPred :=
FracPred (λ _, a b)%I.
Definition fracPred_internal_eq_aux `{!BiInternalEq PROP} : seal (@fracPred_internal_eq_def _).
Proof. by eexists. Qed.
Definition fracPred_internal_eq `{!BiInternalEq PROP} := fracPred_internal_eq_aux.(unseal).
Definition fracPred_internal_eq_eq `{!BiInternalEq PROP} :
@internal_eq _ (@fracPred_internal_eq _) = _ := fracPred_internal_eq_aux.(seal_eq).
Lemma fracPred_internal_eq_mixin `{!BiInternalEq PROP} :
BiInternalEqMixin fracPredI (@fracPred_internal_eq _).
Proof.
split; rewrite fracPred_internal_eq_eq.
- by split=> ? /=; repeat f_equiv.
- intros A P a. split=> π. by apply internal_eq_refl.
- intros A a b Ψ ?. split=> π /=. unseal.
erewrite (internal_eq_rewrite _ _ (flip Ψ _)) => //=. solve_proper.
- intros A1 A2 f g. split=> π. unseal. by apply fun_extI.
- intros A P x y. split=> π. by apply sig_equivI_1.
- intros A a b ?. split=> π. unseal. by apply discrete_eq_1.
- intros A x y. split=> π. unseal. by apply later_equivI_1.
- intros A x y. split=> π. unseal. by apply later_equivI_2.
Qed.
Global Instance fracPred_bi_internal_eq `{BiInternalEq PROP} : BiInternalEq fracPredI :=
{| bi_internal_eq_mixin := fracPred_internal_eq_mixin |}.
Global Instance fracPred_bi_embed_internal_eq `{BiInternalEq PROP} :
BiEmbedInternalEq PROP fracPredI.
Proof. split=> i. rewrite fracPred_internal_eq_eq. by unseal. Qed.
Lemma fracPred_internal_eq_unfold `{!BiInternalEq PROP} :
@internal_eq fracPredI _ = λ A x y, x y %I.
Proof. rewrite fracPred_internal_eq_eq. by unseal. Qed.
Lemma fracPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} π (a b : A) :
@fracPred_at (a b) π a b.
Proof. rewrite fracPred_internal_eq_unfold. by apply fracPred_at_embed. Qed.
Lemma fracPred_equivI `{!BiInternalEq PROP'} P Q :
P Q @{PROP'} π, P π Q π.
Proof.
apply bi.equiv_spec. split.
- apply bi.forall_intro=>?. apply (f_equivI (flip fracPred_at _)).
- rewrite {2}(_ : P = FracPred P); last by destruct P.
rewrite {2}(_ : Q = FracPred Q); last by destruct Q.
by rewrite -(@f_equivI PROP' _ _ _ (@FracPred PROP : (_ -d> _) fracPred)
ltac:(by constructor)) -fun_extI.
Qed.
Global Instance internal_eq_objective `{!BiInternalEq PROP} {A : ofeT} (x y : A) :
@FObjective PROP (x y).
Proof. intros ??. by rewrite !fracPred_at_internal_eq. Qed.
(** Plainly *)
Definition fracPred_plainly_def `{BiPlainly PROP} P : fracPred :=
......@@ -540,7 +539,7 @@ Section sbi_facts.
Definition fracPred_plainly_eq `{BiPlainly PROP} :
@plainly _ fracPred_plainly = _ := fracPred_plainly_aux.(seal_eq).
Lemma fracPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin fracPredSI fracPred_plainly.
Lemma fracPred_plainly_mixin `{BiPlainly PROP} : BiPlainlyMixin fracPredI fracPred_plainly.
Proof.
split; rewrite fracPred_plainly_eq; try unseal.
- by (split=> ? /=; repeat f_equiv).
......@@ -554,27 +553,37 @@ Section sbi_facts.
by rewrite bi.affinely_emp -plainly_emp_intro.
- intros P Q. split=> π /=. apply bi.exist_elim=> π1; apply bi.exist_elim=> π2.
apply bi.pure_elim_l=> _. by rewrite bi.sep_elim_l.
- intros P Q. split=> π /=. rewrite fracPred_equivI. apply bi.forall_intro=> π'.
by rewrite prop_ext !(bi.forall_elim π') left_id_L.
- intros P. split=> π /=. by rewrite -later_plainly_1.
- intros P. split=> π /=. by rewrite -later_plainly_2.
Qed.
Global Instance fracPred_bi_plainly `{BiPlainly PROP} : BiPlainly fracPredSI :=
Global Instance fracPred_bi_plainly `{BiPlainly PROP} : BiPlainly fracPredI :=
{| bi_plainly_mixin := fracPred_plainly_mixin |}.
Lemma fracPred_at_plainly `{BiPlainly PROP} π P : ( P) π (P ε).
Proof. by rewrite fracPred_plainly_eq. Qed.
Global Instance fracPred_bi_plainly_exist `{BiPlainly PROP} :
BiPlainlyExist PROP BiPlainlyExist fracPredSI.
BiPlainlyExist PROP BiPlainlyExist fracPredI.
Proof.
split=> π /=. rewrite fracPred_plainly_eq /= !fracPred_at_exist.
by rewrite -plainly_exist_1.
Qed.
Global Instance fracPred_bi_prop_ext
`{!BiPlainly PROP, !BiInternalEq PROP, !BiPropExt PROP} : BiPropExt fracPredI.
Proof.
intros P Q. split=> π /=. rewrite fracPred_equivI fracPred_at_forall.
apply bi.forall_intro=> π'. rewrite fracPred_at_internal_eq fracPred_at_plainly.
rewrite /bi_wand_iff fracPred_at_and !fracPred_at_wand.
by rewrite prop_ext !(bi.forall_elim π') left_id_L.
Qed.
Global Instance fracPred_bi_embed_plainly `{BiPlainly PROP} :
BiEmbedPlainly PROP fracPredSI.
Proof. constructor=> P. by rewrite fracPred_plainly_eq; unseal. Qed.
BiEmbedPlainly PROP fracPredI.
Proof. intros P. by rewrite fracPred_plainly_eq; unseal. Qed.
Global Instance plainly_objective `{BiPlainly PROP} P : FObjective ( P).
Proof. intros π π'. by rewrite fracPred_plainly_eq. Qed.
Lemma fracPred_at_plainly `{BiPlainly PROP} π P : ( P) π (P ε).
Proof. by rewrite fracPred_plainly_eq. Qed.
End sbi_facts.
End bi_facts.
Hint Immediate persistent_objective : typeclass_instances.
......@@ -44,7 +44,6 @@ Class ironInvG (Σ : gFunctors) := IronInvG {
Notation ironProp Σ := (fracPred (iProp Σ)).
Notation ironPropO Σ := (fracPredO (iPropO Σ)).
Notation ironPropI Σ := (fracPredI (uPredI (iResUR Σ))).
Notation ironPropSI Σ := (fracPredSI (uPredSI (iResUR Σ))).
Instance perm_as_fractional `{ironInvG Σ} π : AsFractional (perm π) perm π.
Proof. split. done. apply _. Qed.
......@@ -75,7 +74,7 @@ Context `{ironInvG Σ, invG Σ}.
Implicit Types P : ironProp Σ.
(** Fancy updates *)
Lemma iron_fupd_mixin : BiFUpdMixin (ironPropSI Σ) iron_fupd.
Lemma iron_fupd_mixin : BiFUpdMixin (ironPropI Σ) iron_fupd.
Proof.
split; rewrite iron_fupd_eq.
- split=>/= π. solve_proper.
......@@ -106,7 +105,7 @@ Proof.
apply bi.pure_elim_l=> ->. rewrite bi.pure_True // left_id.
by rewrite -assoc -fracPred_at_sep_2.
Qed.
Global Instance iron_bi_fupd : BiFUpd (ironPropSI Σ) :=
Global Instance iron_bi_fupd : BiFUpd (ironPropI Σ) :=
{| bi_fupd_mixin := iron_fupd_mixin |}.
Lemma fracPred_at_fupd π2 E1 E2 P :
......@@ -120,7 +119,7 @@ Proof.
by rewrite fupd_frame_l.
Qed.
Global Instance iron_bi_bupd_fupd : BiBUpdFUpd (ironPropSI Σ).
Global Instance iron_bi_bupd_fupd : BiBUpdFUpd (ironPropI Σ).
Proof.
intros E P. split=>/= π2. rewrite fracPred_at_bupd -fracPred_at_fupd_2 /=.
by rewrite bupd_fupd.
......
......@@ -375,7 +375,6 @@ Global Instance elim_modal_embed_affine_bupd_hyp `{BiAffine PROP, BiBUpd PROP}
ElimModal φ p p' (|==> <affine> PP)%I P' Q Q'
ElimModal φ p p' (<affine> |==> PP) P' Q Q'.
Proof. by rewrite /ElimModal embed_bupd -fracPred_affinely_bupd. Qed.
End bi.
(* LEFT OVER from monpred, SEE ABOVE:
(* When P and/or Q are evars when doing typeclass search on [IntoWand
......@@ -401,13 +400,6 @@ Hint Extern 2 (IntoWand _ _ (fracPred_at _ _) (fracPred_at ?P _) ?Q) =>
: typeclass_instances.
*)
Section sbi.
Context {PROP : sbi}.
Local Notation fracPred := (fracPred PROP).
Implicit Types P Q R : fracPred.
Implicit Types PP QQ RR : PROP.
Implicit Types φ : Prop.
(* LEFT OVER from monpred, SEE ABOVE:
Global Instance from_forall_fracPred_at_plainly `{BiPlainly PROP} i P Φ :
(∀ π, MakeFracPredAt π P (Φ π)) →
......@@ -429,8 +421,8 @@ Global Instance is_except_0_fracPred_at π P :
Proof. rewrite /IsExcept0=>- [/(_ π)]. by rewrite fracPred_at_except_0. Qed.
*)
Global Instance make_fracPred_at_internal_eq {A : ofeT} (x y : A) π :
@MakeFracPredAt PROP π (x y) (x y).
Global Instance make_fracPred_at_internal_eq `{!BiInternalEq PROP} {A : ofeT} (x y : A) π :
MakeFracPredAt π (x y) (x y).
Proof. by rewrite /MakeFracPredAt fracPred_at_internal_eq. Qed.
Global Instance make_fracPred_at_except_0 π P QQ :
MakeFracPredAt π P QQ MakeFracPredAt π ( P) ( QQ).
......@@ -496,4 +488,4 @@ Proof.
iIntros (?) "(?&?&HQ')". iApply H; [done|]. iFrame. iIntros "?". by iApply "HQ'".
Qed.
*)
End sbi.
End bi.
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