Commit 4e82b191 authored by Robbert Krebbers's avatar Robbert Krebbers Committed by Jacques-Henri Jourdan

Remove axiom that emp is timeless.

As Aleš observed, in the ordered RA model it is not, unless the order on the
unit is timeless.
parent 57890ebd
......@@ -461,7 +461,7 @@ Proof.
Qed.
Lemma uPred_sbi_mixin (M : ucmraT) : SBIMixin
uPred_entails uPred_emp uPred_pure uPred_or uPred_impl
uPred_entails uPred_pure uPred_or uPred_impl
(@uPred_forall M) (@uPred_exist M) (@uPred_internal_eq M)
uPred_sep uPred_persistently uPred_later.
Proof.
......@@ -483,8 +483,6 @@ Proof.
intros A Φ. unseal; by split=> -[|n] x.
- (* (▷ ∃ a, Φ a) ⊢ ▷ False ∨ (∃ a, ▷ Φ a) *)
intros A Φ. unseal; split=> -[|[|n]] x /=; eauto.
- (* ▷ emp ⊢ ▷ False ∨ emp *)
rewrite /uPred_emp. unseal; split; by right.
- (* ▷ (P ∗ Q) ⊢ ▷ P ∗ ▷ Q *)
intros P Q. unseal; split=> -[|n] x ? /=.
{ by exists x, (core x); rewrite cmra_core_r. }
......
......@@ -687,10 +687,10 @@ Section list.
^n ([ list] kx l, Φ k x) ([ list] kx l, ^n Φ k x).
Proof. apply (big_opL_commute _). Qed.
Global Instance big_sepL_nil_timeless Φ :
Global Instance big_sepL_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([ list] kx [], Φ k x).
Proof. simpl; apply _. Qed.
Global Instance big_sepL_timeless Φ l :
Global Instance big_sepL_timeless `{!Timeless (emp%I : PROP)} Φ l :
( k x, Timeless (Φ k x)) Timeless ([ list] kx l, Φ k x).
Proof. revert Φ. induction l as [|x l IH]=> Φ ? /=; apply _. Qed.
Global Instance big_sepL_timeless_id `{!Timeless (emp%I : PROP)} Ps :
......@@ -712,10 +712,10 @@ Section gmap.
^n ([ map] kx m, Φ k x) ([ map] kx m, ^n Φ k x).
Proof. apply (big_opM_commute _). Qed.
Global Instance big_sepM_nil_timeless Φ :
Global Instance big_sepM_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([ map] kx , Φ k x).
Proof. rewrite /big_opM map_to_list_empty. apply _. Qed.
Global Instance big_sepM_timeless Φ m :
Global Instance big_sepM_timeless `{!Timeless (emp%I : PROP)} Φ m :
( k x, Timeless (Φ k x)) Timeless ([ map] kx m, Φ k x).
Proof. intros. apply big_sepL_timeless=> _ [??]; apply _. Qed.
End gmap.
......@@ -734,9 +734,10 @@ Section gset.
^n ([ set] y X, Φ y) ([ set] y X, ^n Φ y).
Proof. apply (big_opS_commute _). Qed.
Global Instance big_sepS_nil_timeless Φ : Timeless ([ set] x , Φ x).
Global Instance big_sepS_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([ set] x , Φ x).
Proof. rewrite /big_opS elements_empty. apply _. Qed.
Global Instance big_sepS_timeless Φ X :
Global Instance big_sepS_timeless `{!Timeless (emp%I : PROP)} Φ X :
( x, Timeless (Φ x)) Timeless ([ set] x X, Φ x).
Proof. rewrite /big_opS. apply _. Qed.
End gset.
......@@ -755,9 +756,10 @@ Section gmultiset.
^n ([ mset] y X, Φ y) ([ mset] y X, ^n Φ y).
Proof. apply (big_opMS_commute _). Qed.
Global Instance big_sepMS_nil_timeless Φ : Timeless ([ mset] x , Φ x).
Global Instance big_sepMS_nil_timeless `{!Timeless (emp%I : PROP)} Φ :
Timeless ([ mset] x , Φ x).
Proof. rewrite /big_opMS gmultiset_elements_empty. apply _. Qed.
Global Instance big_sepMS_timeless Φ X :
Global Instance big_sepMS_timeless `{!Timeless (emp%I : PROP)} Φ X :
( x, Timeless (Φ x)) Timeless ([ mset] x X, Φ x).
Proof. rewrite /big_opMS. apply _. Qed.
End gmultiset.
......
......@@ -1554,13 +1554,14 @@ Proof. by rewrite {1}(except_0_intro Q) except_0_sep. Qed.
Global Instance Timeless_proper : Proper (() ==> iff) (@Timeless PROP).
Proof. solve_proper. Qed.
Global Instance emp_timeless : Timeless (emp : PROP)%I.
Proof. apply later_emp_false. Qed.
Global Instance pure_timeless φ : Timeless (⌜φ⌝ : PROP)%I.
Proof.
rewrite /Timeless /bi_except_0 pure_alt later_exist_false.
apply or_elim, exist_elim; [auto|]=> Hφ. rewrite -(exist_intro Hφ). auto.
Qed.
Global Instance emp_timeless `{AffineBI PROP} : Timeless (emp : PROP)%I.
Proof. rewrite -True_emp. apply _. Qed.
Global Instance and_timeless P Q : Timeless P Timeless Q Timeless (P Q).
Proof. intros; rewrite /Timeless except_0_and later_and; auto. Qed.
Global Instance or_timeless P Q : Timeless P Timeless Q Timeless (P Q).
......
......@@ -127,7 +127,6 @@ Section bi_mixin.
sbi_mixin_later_forall_2 {A} (Φ : A PROP) : ( a, Φ a) a, Φ a;
sbi_mixin_later_exist_false {A} (Φ : A PROP) :
( a, Φ a) False ( a, Φ a);
sbi_mixin_later_emp_false : emp False emp;
sbi_mixin_later_sep_1 P Q : (P Q) P Q;
sbi_mixin_later_sep_2 P Q : P Q (P Q);
sbi_mixin_later_persistently_1 P : P P;
......@@ -213,7 +212,7 @@ Structure sbi := SBI {
sbi_bi_mixin : BIMixin sbi_entails sbi_emp sbi_pure sbi_and sbi_or sbi_impl
sbi_forall sbi_exist sbi_internal_eq
sbi_sep sbi_wand sbi_persistently;
sbi_sbi_mixin : SBIMixin sbi_entails sbi_emp 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_persistently bi_later;
}.
......@@ -447,8 +446,6 @@ Proof. eapply sbi_mixin_later_forall_2, sbi_sbi_mixin. Qed.
Lemma later_exist_false {A} (Φ : A PROP) :
( a, Φ a) False ( a, Φ a).
Proof. eapply sbi_mixin_later_exist_false, sbi_sbi_mixin. Qed.
Lemma later_emp_false : (emp : PROP) False emp.
Proof. eapply sbi_mixin_later_emp_false, sbi_sbi_mixin. Qed.
Lemma later_sep_1 P Q : (P Q) P Q.
Proof. eapply sbi_mixin_later_sep_1, sbi_sbi_mixin. Qed.
Lemma later_sep_2 P Q : P Q (P Q).
......
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