Commit 67e76d84 authored by Jacques-Henri Jourdan's avatar Jacques-Henri Jourdan

Merge branch 'gen_proofmode' of gitlab.mpi-sws.org:FP/iris-coq into gen_proofmode

parents 02a11183 e5177df5
......@@ -358,7 +358,7 @@ Import uPred_unseal.
Local Arguments uPred_holds {_} !_ _ _ /.
Lemma uPred_bi_mixin (M : ucmraT) : BIMixin (ofe_mixin_of (uPred M))
Lemma uPred_bi_mixin (M : ucmraT) : BiMixin (ofe_mixin_of (uPred M))
uPred_entails uPred_emp uPred_pure uPred_and uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
uPred_sep uPred_wand uPred_plainly uPred_persistently.
......@@ -518,7 +518,7 @@ Proof.
exists (core x), x; rewrite ?cmra_core_l; auto.
Qed.
Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin
Lemma uPred_sbi_mixin (M : ucmraT) : SbiMixin
uPred_entails uPred_pure uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
uPred_sep uPred_plainly uPred_persistently uPred_later.
......
......@@ -5,7 +5,7 @@ Import bi.
(** Least and greatest fixpoint of a monotone function, defined entirely inside
the logic. *)
Class BIMonoPred {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) := {
Class BiMonoPred {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) := {
bi_mono_pred Φ Ψ : ((bi_persistently ( x, Φ x - Ψ x)) x, F Φ x - F Ψ x)%I;
bi_mono_pred_ne Φ : NonExpansive Φ NonExpansive (F Φ)
}.
......@@ -21,7 +21,7 @@ Definition bi_greatest_fixpoint {PROP : bi} {A : ofeT}
( Φ : A -n> PROP, bi_persistently ( x, Φ x - F Φ x) Φ x)%I.
Section least.
Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BIMonoPred F}.
Context {PROP : bi} {A : ofeT} (F : (A PROP) (A PROP)) `{!BiMonoPred F}.
Global Instance least_fixpoint_ne : NonExpansive (bi_least_fixpoint F).
Proof. solve_proper. Qed.
......
......@@ -42,7 +42,7 @@ Section bi_mixin.
Local Infix "-∗" := bi_wand.
Local Notation "▷ P" := (sbi_later P).
Record BIMixin := {
Record BiMixin := {
bi_mixin_entails_po : PreOrder bi_entails;
bi_mixin_equiv_spec P Q : equiv P Q (P Q) (Q P);
......@@ -141,7 +141,7 @@ Section bi_mixin.
bi_persistently P Q (emp P) Q;
}.
Record SBIMixin := {
Record SbiMixin := {
sbi_mixin_later_contractive : Contractive sbi_later;
sbi_mixin_later_eq_1 {A : ofeT} (x y : A) : Next x Next y (x y);
......@@ -166,7 +166,7 @@ Section bi_mixin.
}.
End bi_mixin.
Structure bi := BI {
Structure bi := Bi {
bi_car :> Type;
bi_dist : Dist bi_car;
bi_equiv : Equiv bi_car;
......@@ -184,7 +184,7 @@ Structure bi := BI {
bi_plainly : bi_car bi_car;
bi_persistently : bi_car bi_car;
bi_ofe_mixin : OfeMixin bi_car;
bi_bi_mixin : BIMixin bi_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or
bi_bi_mixin : BiMixin bi_ofe_mixin bi_entails bi_emp bi_pure bi_and bi_or
bi_impl bi_forall bi_exist bi_internal_eq
bi_sep bi_wand bi_plainly bi_persistently;
}.
......@@ -224,7 +224,7 @@ Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments bi_plainly {PROP} _%I : simpl never, rename.
Arguments bi_persistently {PROP} _%I : simpl never, rename.
Structure sbi := SBI {
Structure sbi := Sbi {
sbi_car :> Type;
sbi_dist : Dist sbi_car;
sbi_equiv : Equiv sbi_car;
......@@ -243,10 +243,10 @@ Structure sbi := SBI {
sbi_persistently : sbi_car sbi_car;
sbi_later : sbi_car sbi_car;
sbi_ofe_mixin : OfeMixin sbi_car;
sbi_bi_mixin : BIMixin sbi_ofe_mixin sbi_entails sbi_emp sbi_pure sbi_and
sbi_bi_mixin : BiMixin sbi_ofe_mixin sbi_entails sbi_emp sbi_pure sbi_and
sbi_or sbi_impl sbi_forall sbi_exist sbi_internal_eq
sbi_sep sbi_wand sbi_plainly sbi_persistently;
sbi_sbi_mixin : SBIMixin sbi_entails sbi_pure sbi_or sbi_impl
sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
sbi_forall sbi_exist sbi_internal_eq
sbi_sep sbi_plainly sbi_persistently sbi_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