Commit 59bbb184 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Experiment: Merge bi & sbi structures for some performance tests.

parent 6dba682d
......@@ -91,7 +91,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
heapG0 : heapG Σ
n : Z
H : 0 < n
Φ : val → iPropI Σ
Φ : val → iPropSI Σ
l : loc
============================
"HΦ" : ∀ l0 : loc, l0 ↦∗ replicate (Z.to_nat n) #0 -∗ Φ #l0
......@@ -138,7 +138,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
Σ : gFunctors
heapG0 : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ
Φ : language.val heap_lang → iPropSI Σ
============================
--------------------------------------∗
WP let: "val1" := fun1 #() in
......@@ -151,7 +151,7 @@ Tactic failure: wp_pure: cannot find ?y in (Var "x") or
Σ : gFunctors
heapG0 : heapG Σ
fun1, fun2, fun3 : expr
Φ : language.val heap_lang → iPropI Σ
Φ : language.val heap_lang → iPropSI Σ
E : coPset
============================
--------------------------------------∗
......
......@@ -4,7 +4,7 @@
heapG0 : heapG Σ
hd, acc : val
xs, ys : list val
Φ : val → iPropI Σ
Φ : val → iPropSI Σ
============================
"Hxs" : is_list hd xs
"Hys" : is_list acc ys
......@@ -18,7 +18,7 @@
heapG0 : heapG Σ
acc : val
ys : list val
Φ : val → iPropI Σ
Φ : val → iPropSI Σ
============================
"Hys" : is_list acc ys
"HΦ" : ∀ w : val, is_list w ys -∗ Φ w
......
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -12,7 +12,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -25,7 +25,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -38,7 +38,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -50,7 +50,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -61,7 +61,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -74,7 +74,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -87,7 +87,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -100,7 +100,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P : PROP
Φ, Ψ : A → PROP
......@@ -114,7 +114,7 @@
1 subgoal
PROP : bi
PROP : sbi
A : Type
P, Q : PROP
============================
......@@ -126,7 +126,7 @@
1 subgoal
I : biIndex
PROP : bi
PROP : sbi
Φ, Ψ : monPred I PROP
============================
"H1" : Φ
......@@ -137,7 +137,7 @@
1 subgoal
I : biIndex
PROP : bi
PROP : sbi
Φ, Ψ : monPred I PROP
============================
--------------------------------------∗
......@@ -146,7 +146,7 @@
1 subgoal
I : biIndex
PROP : bi
PROP : sbi
Φ : monPred I PROP
P, Q : PROP
============================
......@@ -160,7 +160,7 @@
1 subgoal
I : biIndex
PROP : bi
PROP : sbi
Φ : monPred I PROP
P, Q : PROP
============================
......
......@@ -336,8 +336,7 @@ Tactic failure: iFrame: cannot frame Q.
BiFUpd0 : BiFUpd PROP
X : Type
E1, E2 : coPset.coPset
α : X → PROP
β : X → PROP
α, β : X → PROP
γ : X → option PROP
============================
"Hacc" : ∃ x : X, α x ∗ (β x ={E2,E1}=∗ default emp (γ x))
......@@ -622,10 +621,6 @@ k is used in hypothesis Hk.
: string
The command has indeed failed with message:
Tactic failure: iRevert: k is used in hypothesis "Hk".
"iLöb_no_sbi"
: string
The command has indeed failed with message:
Tactic failure: iLöb: not a step-indexed BI entailment.
"test_pure_name"
: string
1 subgoal
......
......@@ -1126,10 +1126,6 @@ End error_tests.
Section error_tests_bi.
Context {PROP : bi}.
Implicit Types P Q R : PROP.
Check "iLöb_no_sbi".
Lemma iLöb_no_sbi P : P.
Proof. Fail iLöb as "IH". Abort.
End error_tests_bi.
Section pure_name_tests.
......
......@@ -2,7 +2,7 @@
I : biIndex
PROP : sbi
P, Q : monpred.monPred I PROP
P, Q : monPred
i : I
============================
"HW" : (P -∗ Q) i
......@@ -13,7 +13,7 @@
I : biIndex
PROP : sbi
P, Q : monpred.monPred I PROP
P, Q : monPred
i, j : I
============================
"HW" : (P -∗ Q) j
......@@ -25,7 +25,7 @@
I : biIndex
PROP : sbi
P, Q : monpred.monPred I PROP
P, Q : monPred
Objective0 : Objective Q
𝓟, 𝓠 : PROP
============================
......@@ -40,7 +40,7 @@
I : biIndex
PROP : sbi
FU0 : BiFUpd PROP * ()
P, Q : monpred.monPred I PROP
P, Q : monPred
i : I
============================
--------------------------------------∗
......@@ -51,7 +51,7 @@
I : biIndex
PROP : sbi
FU0 : BiFUpd PROP * ()
P : monpred.monPred I PROP
P : monPred
i : I
============================
--------------------------------------∗
......
......@@ -93,10 +93,9 @@ Proof.
Qed.
Canonical Structure uPredI (M : ucmraT) : bi :=
{| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M |}.
Canonical Structure uPredSI (M : ucmraT) : sbi :=
{| sbi_ofe_mixin := ofe_mixin_of (uPred M);
sbi_bi_mixin := uPred_bi_mixin M; sbi_sbi_mixin := uPred_sbi_mixin M |}.
{| bi_ofe_mixin := ofe_mixin_of (uPred M); bi_bi_mixin := uPred_bi_mixin M;
sbi_sbi_mixin := uPred_sbi_mixin M |}.
Notation uPredSI := uPredI.
Lemma uPred_plainly_mixin M : BiPlainlyMixin (uPredSI M) uPred_plainly.
Proof.
......@@ -220,12 +219,10 @@ End restate.
This is used by [base_logic.double_negation].
TODO: Can we get rid of this? *)
Ltac unseal := (* Coq unfold is used to circumvent bug #5699 in rewrite /foo *)
unfold bi_emp; simpl; unfold sbi_emp; simpl;
unfold bi_emp; simpl; simpl;
unfold uPred_emp, bupd, bi_bupd_bupd, bi_pure,
bi_and, bi_or, bi_impl, bi_forall, bi_exist,
bi_sep, bi_wand, bi_persistently, sbi_internal_eq, 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; simpl;
unfold plainly, bi_plainly_plainly; simpl;
uPred_primitive.unseal.
......
......@@ -163,9 +163,15 @@ Structure bi := Bi {
bi_sep : bi_car bi_car bi_car;
bi_wand : bi_car bi_car bi_car;
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);
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
bi_forall bi_exist bi_sep
bi_persistently sbi_internal_eq sbi_later;
}.
Coercion bi_ofeO (PROP : bi) : ofeT := OfeT PROP (bi_ofe_mixin PROP).
......@@ -198,31 +204,10 @@ Arguments bi_sep {PROP} _%I _%I : simpl never, rename.
Arguments bi_wand {PROP} _%I _%I : simpl never, rename.
Arguments bi_persistently {PROP} _%I : simpl never, rename.
Structure sbi := Sbi {
sbi_car :> Type;
sbi_dist : Dist sbi_car;
sbi_equiv : Equiv sbi_car;
sbi_entails : sbi_car sbi_car Prop;
sbi_emp : sbi_car;
sbi_pure : Prop sbi_car;
sbi_and : sbi_car sbi_car sbi_car;
sbi_or : sbi_car sbi_car sbi_car;
sbi_impl : sbi_car sbi_car sbi_car;
sbi_forall : A, (A sbi_car) sbi_car;
sbi_exist : A, (A sbi_car) sbi_car;
sbi_sep : sbi_car sbi_car sbi_car;
sbi_wand : sbi_car sbi_car sbi_car;
sbi_persistently : sbi_car sbi_car;
sbi_internal_eq : A : ofeT, A A sbi_car;
sbi_later : sbi_car sbi_car;
sbi_ofe_mixin : OfeMixin sbi_car;
sbi_cofe : Cofe (OfeT sbi_car sbi_ofe_mixin);
sbi_bi_mixin : BiMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl
sbi_forall sbi_exist sbi_sep sbi_wand sbi_persistently;
sbi_sbi_mixin : SbiMixin sbi_entails sbi_pure sbi_or sbi_impl
sbi_forall sbi_exist sbi_sep
sbi_persistently sbi_internal_eq sbi_later;
}.
Notation sbi := bi.
Global Instance sbi_cofe' (PROP : sbi) : Cofe PROP.
Proof. apply sbi_cofe. Qed.
Instance: Params (@sbi_later) 1 := {}.
Instance: Params (@sbi_internal_eq) 1 := {}.
......@@ -230,28 +215,6 @@ Instance: Params (@sbi_internal_eq) 1 := {}.
Arguments sbi_later {PROP} _%I : simpl never, rename.
Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
Coercion sbi_ofeO (PROP : sbi) : ofeT := OfeT PROP (sbi_ofe_mixin PROP).
Canonical Structure sbi_ofeO.
Coercion sbi_bi (PROP : sbi) : bi :=
{| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}.
Canonical Structure sbi_bi.
Global Instance sbi_cofe' (PROP : sbi) : Cofe PROP.
Proof. apply sbi_cofe. Qed.
Arguments sbi_car : simpl never.
Arguments sbi_dist : simpl never.
Arguments sbi_equiv : simpl never.
Arguments sbi_entails {PROP} _%I _%I : simpl never, rename.
Arguments sbi_emp {PROP} : simpl never, rename.
Arguments sbi_pure {PROP} _%stdpp : simpl never, rename.
Arguments sbi_and {PROP} _%I _%I : simpl never, rename.
Arguments sbi_or {PROP} _%I _%I : simpl never, rename.
Arguments sbi_impl {PROP} _%I _%I : simpl never, rename.
Arguments sbi_forall {PROP _} _%I : simpl never, rename.
Arguments sbi_exist {PROP _} _%I : simpl never, rename.
Arguments sbi_sep {PROP} _%I _%I : simpl never, rename.
Arguments sbi_wand {PROP} _%I _%I : simpl never, rename.
Arguments sbi_persistently {PROP} _%I : simpl never, rename.
Arguments sbi_internal_eq {PROP _} _ _ : simpl never, rename.
Arguments sbi_later {PROP} _%I : simpl never, rename.
......
......@@ -248,10 +248,7 @@ Ltac unseal :=
unfold bi_affinely, bi_absorbingly, sbi_except_0, bi_pure, bi_emp,
monPred_upclosed, 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;
bi_persistently, bi_affinely, sbi_later, sbi_internal_eq;
simpl;
rewrite !unseal_eqs /=.
End MonPred.
......@@ -310,13 +307,6 @@ Proof.
- intros P Q. split=> i. by apply bi.persistently_and_sep_elim.
Qed.
Canonical Structure monPredI : bi :=
{| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin |}.
End canonical_bi.
Section canonical_sbi.
Context (I : biIndex) (PROP : sbi).
Lemma monPred_sbi_mixin :
SbiMixin (PROP:=monPred I PROP) monPred_entails monPred_pure
monPred_or monPred_impl monPred_forall monPred_exist
......@@ -347,10 +337,12 @@ Proof.
intros j. rewrite bi.pure_impl_forall. apply bi.forall_intro=> Hij. by rewrite Hij.
Qed.
Canonical Structure monPredSI : sbi :=
{| sbi_ofe_mixin := monPred_ofe_mixin; sbi_bi_mixin := monPred_bi_mixin I PROP;
Canonical Structure monPredI : bi :=
{| bi_ofe_mixin := monPred_ofe_mixin; bi_bi_mixin := monPred_bi_mixin;
sbi_sbi_mixin := monPred_sbi_mixin |}.
End canonical_sbi.
End canonical_bi.
Notation monPredSI := monPredI.
Class Objective {I : biIndex} {PROP : bi} (P : monPred I PROP) :=
objective_at i j : P i - P j.
......
......@@ -120,10 +120,9 @@ Proof.
Qed.
Canonical Structure siPropI : bi :=
{| bi_ofe_mixin := ofe_mixin_of siProp; bi_bi_mixin := siProp_bi_mixin |}.
Canonical Structure siPropSI : sbi :=
{| sbi_ofe_mixin := ofe_mixin_of siProp;
sbi_bi_mixin := siProp_bi_mixin; sbi_sbi_mixin := siProp_sbi_mixin |}.
{| bi_ofe_mixin := ofe_mixin_of siProp; bi_bi_mixin := siProp_bi_mixin;
sbi_sbi_mixin := siProp_sbi_mixin |}.
Notation siPropSI := siPropI.
Lemma siProp_plainly_mixin : BiPlainlyMixin siPropSI siProp_plainly.
Proof.
......
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