Commit 9d533fdd authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Failed experiment: put `ofe` directly in `bi`.

parent 59bbb184
......@@ -93,7 +93,7 @@ Proof.
Qed.
Canonical Structure uPredI (M : ucmraT) : bi :=
{| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M;
{| bi_bi_mixin := uPred_bi_mixin M;
sbi_sbi_mixin := uPred_sbi_mixin M |}.
Notation uPredSI := uPredI.
......
......@@ -3,7 +3,7 @@ From iris.algebra Require Export ofe.
Set Primitive Projections.
Section bi_mixin.
Context {PROP : Type} `{Dist PROP, Equiv PROP}.
Context {PROP : ofeT}.
Context (bi_entails : PROP PROP Prop).
Context (bi_emp : PROP).
Context (bi_pure : Prop PROP).
......@@ -149,9 +149,7 @@ Section bi_mixin.
End bi_mixin.
Structure bi := Bi {
bi_car :> Type;
bi_dist : Dist bi_car;
bi_equiv : Equiv bi_car;
bi_car :> ofeT;
bi_entails : bi_car bi_car Prop;
bi_emp : bi_car;
bi_pure : Prop bi_car;
......@@ -165,8 +163,7 @@ Structure bi := Bi {
bi_persistently : bi_car bi_car;
sbi_internal_eq : A : ofeT, A A bi_car;
sbi_later : bi_car bi_car;
bi_ofe_mixin : OfeMixin bi_car;
sbi_cofe : Cofe (OfeT bi_car bi_ofe_mixin);
sbi_cofe : Cofe bi_car;
bi_bi_mixin : BiMixin bi_entails bi_emp bi_pure bi_and bi_or bi_impl bi_forall
bi_exist bi_sep bi_wand bi_persistently;
sbi_sbi_mixin : SbiMixin bi_entails bi_pure bi_or bi_impl
......@@ -174,8 +171,7 @@ Structure bi := Bi {
bi_persistently sbi_internal_eq sbi_later;
}.
Coercion bi_ofeO (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
Canonical Structure bi_ofeO.
Notation bi_ofeO := bi_car.
Instance: Params (@bi_entails) 1 := {}.
Instance: Params (@bi_emp) 1 := {}.
......@@ -190,8 +186,6 @@ Instance: Params (@bi_wand) 1 := {}.
Instance: Params (@bi_persistently) 1 := {}.
Arguments bi_car : simpl never.
Arguments bi_dist : simpl never.
Arguments bi_equiv : simpl never.
Arguments bi_entails {PROP} _%I _%I : simpl never, rename.
Arguments bi_emp {PROP} : simpl never, rename.
Arguments bi_pure {PROP} _%stdpp : simpl never, rename.
......
......@@ -257,7 +257,7 @@ Import MonPred.
Section canonical_bi.
Context (I : biIndex) (PROP : bi).
Lemma monPred_bi_mixin : BiMixin (PROP:=monPred I PROP)
Lemma monPred_bi_mixin : BiMixin (PROP:=monPredO I PROP)
monPred_entails monPred_emp monPred_pure monPred_and monPred_or
monPred_impl monPred_forall monPred_exist monPred_sep monPred_wand
monPred_persistently.
......@@ -308,7 +308,7 @@ Proof.
Qed.
Lemma monPred_sbi_mixin :
SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
SbiMixin (PROP:=monPredO I PROP) monPred_entails monPred_pure
monPred_or monPred_impl monPred_forall monPred_exist
monPred_sep monPred_persistently monPred_internal_eq monPred_later.
Proof.
......@@ -338,7 +338,7 @@ Proof.
Qed.
Canonical Structure monPredI : bi :=
{| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
{| bi_bi_mixin := monPred_bi_mixin;
sbi_sbi_mixin := monPred_sbi_mixin |}.
End canonical_bi.
......
......@@ -120,7 +120,7 @@ Proof.
Qed.
Canonical Structure siPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of siProp; bi_bi_mixin := siProp_bi_mixin;
{| bi_bi_mixin := siProp_bi_mixin;
sbi_sbi_mixin := siProp_sbi_mixin |}.
Notation siPropSI := siPropI.
......
Supports Markdown
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