Commit e2bb6d8d authored by Ralf Jung's avatar Ralf Jung

all SBI must be a COFE

parent 19f3e261
...@@ -210,8 +210,6 @@ Section löb. ...@@ -210,8 +210,6 @@ Section löb.
Local Instance flöb_pre_contractive P : Contractive (flöb_pre P). Local Instance flöb_pre_contractive P : Contractive (flöb_pre P).
Proof. solve_contractive. Qed. Proof. solve_contractive. Qed.
Context `{Cofe PROP}.
Definition flöb (P : PROP) := fixpoint (flöb_pre P). Definition flöb (P : PROP) := fixpoint (flöb_pre P).
Lemma weak_löb P : ( P P) (True P). Lemma weak_löb P : ( P P) (True P).
...@@ -412,7 +410,7 @@ Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed. ...@@ -412,7 +410,7 @@ Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
Global Instance or_timeless P Q : Timeless P Timeless Q Timeless (P Q). Global Instance or_timeless P Q : Timeless P Timeless Q Timeless (P Q).
Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed. Proof. intros; rewrite /Timeless except_0_or later_or; auto. Qed.
Global Instance impl_timeless `{Cofe PROP} P Q : Timeless Q Timeless (P Q). Global Instance impl_timeless P Q : Timeless Q Timeless (P Q).
Proof. Proof.
rewrite /Timeless=> HQ. rewrite later_false_em. rewrite /Timeless=> HQ. rewrite later_false_em.
apply or_mono, impl_intro_l; first done. apply or_mono, impl_intro_l; first done.
...@@ -425,7 +423,7 @@ Proof. ...@@ -425,7 +423,7 @@ Proof.
intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono. intros; rewrite /Timeless except_0_sep later_sep; auto using sep_mono.
Qed. Qed.
Global Instance wand_timeless `{Cofe PROP} P Q : Timeless Q Timeless (P - Q). Global Instance wand_timeless P Q : Timeless Q Timeless (P - Q).
Proof. Proof.
rewrite /Timeless=> HQ. rewrite later_false_em. rewrite /Timeless=> HQ. rewrite later_false_em.
apply or_mono, wand_intro_l; first done. apply or_mono, wand_intro_l; first done.
......
...@@ -229,6 +229,7 @@ Structure sbi := Sbi { ...@@ -229,6 +229,7 @@ Structure sbi := Sbi {
sbi_internal_eq : A : ofeT, A A sbi_car; sbi_internal_eq : A : ofeT, A A sbi_car;
sbi_later : sbi_car sbi_car; sbi_later : sbi_car sbi_car;
sbi_ofe_mixin : OfeMixin 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_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_forall sbi_exist sbi_sep sbi_wand 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
...@@ -247,6 +248,8 @@ Canonical Structure sbi_ofeC. ...@@ -247,6 +248,8 @@ Canonical Structure sbi_ofeC.
Coercion sbi_bi (PROP : sbi) : bi := Coercion sbi_bi (PROP : sbi) : bi :=
{| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}. {| bi_ofe_mixin := sbi_ofe_mixin PROP; bi_bi_mixin := sbi_bi_mixin PROP |}.
Canonical Structure sbi_bi. Canonical Structure sbi_bi.
Global Instance sbi_cofe' (PROP : sbi) : Cofe PROP.
Proof. apply sbi_cofe. Qed.
Arguments sbi_car : simpl never. Arguments sbi_car : simpl never.
Arguments sbi_dist : simpl never. Arguments sbi_dist : simpl never.
......
...@@ -1396,7 +1396,7 @@ Proof. ...@@ -1396,7 +1396,7 @@ Proof.
- by rewrite Hs //= right_id. - by rewrite Hs //= right_id.
Qed. Qed.
Lemma tac_löb `{Cofe PROP} Δ Δ' i Q : Lemma tac_löb Δ Δ' i Q :
env_spatial_is_nil Δ = true env_spatial_is_nil Δ = true
envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ' envs_app true (Esnoc Enil i ( Q)%I) Δ = Some Δ'
envs_entails Δ' Q envs_entails Δ Q. envs_entails Δ' Q envs_entails Δ Q.
......
...@@ -1659,8 +1659,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) := ...@@ -1659,8 +1659,7 @@ Tactic Notation "iLöbCore" "as" constr (IH) :=
refine should use the other unification algorithm, which should refine should use the other unification algorithm, which should
not have this issue. *) not have this issue. *)
notypeclasses refine (tac_löb _ _ IH _ _ _ _); notypeclasses refine (tac_löb _ _ IH _ _ _ _);
[iSolveTC || fail "iLöb: PROP is not a Cofe" [reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|reflexivity || fail "iLöb: spatial context not empty, this should not happen"
|env_reflexivity || fail "iLöb:" IH "not fresh"|]. |env_reflexivity || fail "iLöb:" IH "not fresh"|].
Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) := Tactic Notation "iLöbRevert" constr(Hs) "with" tactic(tac) :=
......
From iris.proofmode Require Import tactics intro_patterns. From iris.proofmode Require Import tactics intro_patterns.
From stdpp Require Import gmap hlist. From stdpp Require Import gmap hlist.
Set Default Proof Using "Type*". Set Default Proof Using "Type".
Section tests. Section tests.
Context {PROP : sbi} `{Cofe PROP}. Context {PROP : sbi}.
Implicit Types P Q R : PROP. Implicit Types P Q R : PROP.
Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P). Lemma demo_0 P Q : (P Q) - ( x, x = 0 x = 1) (Q P).
...@@ -381,8 +381,8 @@ Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qe ...@@ -381,8 +381,8 @@ Proof. iIntros (Hφ). iAssert ⌜φ⌝%I with "[%]" as "$"; auto with iFrame. Qe
Lemma test_iEval x y : (y + x)%nat = 1 - S (x + y) = 2%nat : PROP. Lemma test_iEval x y : (y + x)%nat = 1 - S (x + y) = 2%nat : PROP.
Proof. Proof.
iIntros (Hn). iIntros (H).
iEval (rewrite (Nat.add_comm x y) // Hn). iEval (rewrite (Nat.add_comm x y) // H).
done. done.
Qed. Qed.
......
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