Commit 0e49878b authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Prove Timeless instances in the logic instead of the model.

Thanks to Ranald Clouston for suggesting the axiom:

  ▷ P ⊢ ▷ False ∨ (▷ False → P)

This axiom is used to prove timeless of implication, wand and forall.

Timelessness of the pure and ownM connectives is still proven in the model, but
we first state the property in a way that it does not involved derived notions
(like the except_last modality).
parent 4e59a653
...@@ -1014,6 +1014,8 @@ Proof. ...@@ -1014,6 +1014,8 @@ Proof.
unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|]. unseal; split=> n x ? HP; induction n as [|n IH]; [by apply HP|].
apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S. apply HP, IH, uPred_closed with (S n); eauto using cmra_validN_S.
Qed. Qed.
Lemma later_pure φ : φ False φ.
Proof. unseal; split=> -[|n] x ?? /=; auto. Qed.
Lemma later_and P Q : (P Q) ⊣⊢ P Q. Lemma later_and P Q : (P Q) ⊣⊢ P Q.
Proof. unseal; split=> -[|n] x; by split. Qed. Proof. unseal; split=> -[|n] x; by split. Qed.
Lemma later_or P Q : (P Q) ⊣⊢ P Q. Lemma later_or P Q : (P Q) ⊣⊢ P Q.
...@@ -1034,6 +1036,12 @@ Proof. ...@@ -1034,6 +1036,12 @@ Proof.
- destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)]. - destruct n as [|n]; simpl; [done|intros (x1&x2&Hx&?&?)].
exists x1, x2; eauto using dist_S. exists x1, x2; eauto using dist_S.
Qed. Qed.
Lemma later_false_excluded_middle P : P False ( False P).
Proof.
unseal; split=> -[|n] x ? /= HP; [by left|right].
intros [|n'] x' ????; [|done].
eauto using uPred_closed, uPred_mono, cmra_included_includedN.
Qed.
(* Later derived *) (* Later derived *)
Lemma later_proper P Q : (P ⊣⊢ Q) P ⊣⊢ Q. Lemma later_proper P Q : (P ⊣⊢ Q) P ⊣⊢ Q.
...@@ -1130,6 +1138,12 @@ Proof. ...@@ -1130,6 +1138,12 @@ Proof.
Qed. Qed.
Lemma ownM_empty : True uPred_ownM . Lemma ownM_empty : True uPred_ownM .
Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed. Proof. unseal; split=> n x ??; by exists x; rewrite left_id. Qed.
Lemma later_ownM a : Timeless a uPred_ownM a False uPred_ownM a.
Proof.
unseal=> Ha; split=> -[|n] x ?? /=; [by left|right].
apply cmra_included_includedN, cmra_timeless_included_l,
cmra_includedN_le with n; eauto using cmra_validN_le.
Qed.
(* Valid *) (* Valid *)
Lemma ownM_valid (a : M) : uPred_ownM a a. Lemma ownM_valid (a : M) : uPred_ownM a a.
...@@ -1238,47 +1252,44 @@ Lemma option_validI {A : cmraT} (mx : option A) : ...@@ -1238,47 +1252,44 @@ Lemma option_validI {A : cmraT} (mx : option A) :
mx ⊣⊢ match mx with Some x => x | None => True end. mx ⊣⊢ match mx with Some x => x | None => True end.
Proof. uPred.unseal. by destruct mx. Qed. Proof. uPred.unseal. by destruct mx. Qed.
(* Equivalent definition of timeless in the model *)
Lemma timelessP_spec P : TimelessP P n x, {n} x P 0 x P n x.
Proof.
split.
- intros HP n x ??; induction n as [|n]; auto.
move: HP; rewrite /TimelessP /uPred_except_last /=.
unseal=> /uPred_in_entails /(_ (S n) x) /=.
by destruct 1; auto using cmra_validN_S.
- move=> HP; rewrite /TimelessP /uPred_except_last /=.
unseal; split=> -[|n] x /=; auto.
right. apply HP, uPred_closed with n; eauto using cmra_validN_le.
Qed.
(* Timeless instances *) (* Timeless instances *)
Global Instance pure_timeless φ : TimelessP ( φ : uPred M)%I. Global Instance pure_timeless φ : TimelessP ( φ : uPred M)%I.
Proof. by apply timelessP_spec; unseal => -[|n] x. Qed. Proof. by rewrite /TimelessP later_pure. Qed.
Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) : Global Instance valid_timeless {A : cmraT} `{CMRADiscrete A} (a : A) :
TimelessP ( a : uPred M)%I. TimelessP ( a : uPred M)%I.
Proof. Proof. rewrite /TimelessP !discrete_valid. apply (timelessP _). Qed.
apply timelessP_spec; unseal=> n x /=. by rewrite -!cmra_discrete_valid_iff.
Qed.
Global Instance and_timeless P Q: TimelessP P TimelessP Q TimelessP (P Q). Global Instance and_timeless P Q: TimelessP P TimelessP Q TimelessP (P Q).
Proof. intros; rewrite /TimelessP except_last_and later_and; auto. Qed. Proof. intros; rewrite /TimelessP except_last_and later_and; auto. Qed.
Global Instance or_timeless P Q : TimelessP P TimelessP Q TimelessP (P Q). Global Instance or_timeless P Q : TimelessP P TimelessP Q TimelessP (P Q).
Proof. intros; rewrite /TimelessP except_last_or later_or; auto. Qed. Proof. intros; rewrite /TimelessP except_last_or later_or; auto. Qed.
Global Instance impl_timeless P Q : TimelessP Q TimelessP (P Q). Global Instance impl_timeless P Q : TimelessP Q TimelessP (P Q).
Proof. Proof.
rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ????; auto. rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
apply HP, HPQ, uPred_closed with (S n'); eauto using cmra_validN_le. apply or_mono, impl_intro_l; first done.
rewrite -{2}(löb Q); apply impl_intro_l.
rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
by rewrite assoc (comm _ _ P) -assoc !impl_elim_r.
Qed. Qed.
Global Instance sep_timeless P Q: TimelessP P TimelessP Q TimelessP (P Q). Global Instance sep_timeless P Q: TimelessP P TimelessP Q TimelessP (P Q).
Proof. intros; rewrite /TimelessP except_last_sep later_sep; auto. Qed. Proof. intros; rewrite /TimelessP except_last_sep later_sep; auto. Qed.
Global Instance wand_timeless P Q : TimelessP Q TimelessP (P - Q). Global Instance wand_timeless P Q : TimelessP Q TimelessP (P - Q).
Proof. Proof.
rewrite !timelessP_spec; unseal=> HP [|n] x ? HPQ [|n'] x' ???; auto. rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
apply HP, HPQ, uPred_closed with (S n'); apply or_mono, wand_intro_l; first done.
eauto 3 using cmra_validN_le, cmra_validN_op_r. rewrite -{2}(löb Q); apply impl_intro_l.
rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
rewrite -(always_pure) -always_later always_and_sep_l'.
by rewrite assoc (comm _ _ P) -assoc -always_and_sep_l' impl_elim_r wand_elim_r.
Qed. Qed.
Global Instance forall_timeless {A} (Ψ : A uPred M) : Global Instance forall_timeless {A} (Ψ : A uPred M) :
( x, TimelessP (Ψ x)) TimelessP ( x, Ψ x). ( x, TimelessP (Ψ x)) TimelessP ( x, Ψ x).
Proof. by setoid_rewrite timelessP_spec; unseal=> HΨ n x ?? a; apply HΨ. Qed. Proof.
rewrite /TimelessP=> HQ. rewrite later_false_excluded_middle.
apply or_mono; first done. apply forall_intro=> x.
rewrite -(löb (Ψ x)); apply impl_intro_l.
rewrite HQ /uPred_except_last !and_or_r. apply or_elim; last auto.
by rewrite impl_elim_r (forall_elim x).
Qed.
Global Instance exist_timeless {A} (Ψ : A uPred M) : Global Instance exist_timeless {A} (Ψ : A uPred M) :
( x, TimelessP (Ψ x)) TimelessP ( x, Ψ x). ( x, TimelessP (Ψ x)) TimelessP ( x, Ψ x).
Proof. Proof.
...@@ -1292,14 +1303,9 @@ Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P). ...@@ -1292,14 +1303,9 @@ Global Instance always_if_timeless p P : TimelessP P → TimelessP (□?p P).
Proof. destruct p; apply _. Qed. Proof. destruct p; apply _. Qed.
Global Instance eq_timeless {A : cofeT} (a b : A) : Global Instance eq_timeless {A : cofeT} (a b : A) :
Timeless a TimelessP (a b : uPred M)%I. Timeless a TimelessP (a b : uPred M)%I.
Proof. Proof. intros. rewrite /TimelessP !timeless_eq. apply (timelessP _). Qed.
intro; apply timelessP_spec; unseal=> n x ??; by apply equiv_dist, timeless.
Qed.
Global Instance ownM_timeless (a : M) : Timeless a TimelessP (uPred_ownM a). Global Instance ownM_timeless (a : M) : Timeless a TimelessP (uPred_ownM a).
Proof. Proof. apply later_ownM. Qed.
intro; apply timelessP_spec; unseal=> n x ??; apply cmra_included_includedN,
cmra_timeless_included_l; eauto using cmra_validN_le.
Qed.
(* Persistence *) (* Persistence *)
Global Instance pure_persistent φ : PersistentP ( φ : uPred M)%I. Global Instance pure_persistent φ : PersistentP ( φ : uPred M)%I.
......
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