Commit 1b85d654 authored by Robbert Krebbers's avatar Robbert Krebbers

Rename rvs -> bupd (basic update), pvs -> fupd (fancy update).

And also rename the corresponding proof mode tactics.
parent aec84909
...@@ -5,8 +5,8 @@ Many of the tactics below apply to more goals than described in this document ...@@ -5,8 +5,8 @@ Many of the tactics below apply to more goals than described in this document
since the behavior of these tactics can be tuned via instances of the type since the behavior of these tactics can be tuned via instances of the type
classes in the file [proofmode/classes](proofmode/classes.v). Most notable, many classes in the file [proofmode/classes](proofmode/classes.v). Most notable, many
of the tactics can be applied when the to be introduced or to be eliminated of the tactics can be applied when the to be introduced or to be eliminated
connective appears under a later, a primitive view shift, or in the conclusion connective appears under a later, an update modality, or in the conclusion of a
of a weakest precondition connective. weakest precondition.
Applying hypotheses and lemmas Applying hypotheses and lemmas
------------------------------ ------------------------------
...@@ -124,14 +124,13 @@ Rewriting ...@@ -124,14 +124,13 @@ Rewriting
Iris Iris
---- ----
- `iVsIntro` : introduction of a raw or primitive view shift. - `iUpdIntro` : introduction of an update modality.
- `iVs pm_trm as (x1 ... xn) "ipat"` : run a raw or primitive view shift - `iUpd pm_trm as (x1 ... xn) "ipat"` : run an update modality `pm_trm` (if the
`pm_trm` (if the goal permits, i.e. it is a raw or primitive view shift, or goal permits, i.e. it can be expanded to an update modality.
a weakest precondition).
- `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`. - `iInv N as (x1 ... xn) "ipat"` : open the invariant `N`.
- `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal - `iTimeless "H"` : strip a later of a timeless hypothesis `H` (if the goal
permits, i.e. it is a later, True now, raw or primitive view shift, or a permits, i.e. it is a later, True now, update modality, or a weakest
weakest precondition). precondition).
Miscellaneous Miscellaneous
------------- -------------
...@@ -140,8 +139,8 @@ Miscellaneous ...@@ -140,8 +139,8 @@ Miscellaneous
introduces pure connectives. introduces pure connectives.
- The proof mode adds hints to the core `eauto` database so that `eauto` - The proof mode adds hints to the core `eauto` database so that `eauto`
automatically introduces: conjunctions and disjunctions, universal and automatically introduces: conjunctions and disjunctions, universal and
existential quantifiers, implications and wand, always and later modalities, existential quantifiers, implications and wand, always, later and update
primitive view shifts, and pure connectives. modalities, and pure connectives.
Selection patterns Selection patterns
================== ==================
...@@ -172,7 +171,7 @@ _introduction patterns_: ...@@ -172,7 +171,7 @@ _introduction patterns_:
- `%` : move the hypothesis to the pure Coq context (anonymously). - `%` : move the hypothesis to the pure Coq context (anonymously).
- `# ipat` : move the hypothesis to the persistent context. - `# ipat` : move the hypothesis to the persistent context.
- `> ipat` : remove a later of a timeless hypothesis (if the goal permits). - `> ipat` : remove a later of a timeless hypothesis (if the goal permits).
- `==> ipat` : run a view shift (if the goal permits). - `==> ipat` : run an update modality (if the goal permits).
Apart from this, there are the following introduction patterns that can only Apart from this, there are the following introduction patterns that can only
appear at the top level: appear at the top level:
...@@ -183,7 +182,7 @@ appear at the top level: ...@@ -183,7 +182,7 @@ appear at the top level:
- `!%` : introduce a pure goal (and leave the proof mode). - `!%` : introduce a pure goal (and leave the proof mode).
- `!#` : introduce an always modality (given that the spatial context is empty). - `!#` : introduce an always modality (given that the spatial context is empty).
- `!>` : introduce a later (which strips laters from all hypotheses). - `!>` : introduce a later (which strips laters from all hypotheses).
- `!==>` : introduce a view shift. - `!==>` : introduce an update modality
- `/=` : perform `simpl`. - `/=` : perform `simpl`.
- `*` : introduce all universal quantifiers. - `*` : introduce all universal quantifiers.
- `**` : introduce all universal quantifiers, as well as all arrows and wands. - `**` : introduce all universal quantifiers, as well as all arrows and wands.
...@@ -224,7 +223,7 @@ _specification patterns_ to express splitting of hypotheses: ...@@ -224,7 +223,7 @@ _specification patterns_ to express splitting of hypotheses:
- `[-H1 ... Hn]` : negated form of the above pattern. This pattern does not - `[-H1 ... Hn]` : negated form of the above pattern. This pattern does not
accept hypotheses prefixed with a `$`. accept hypotheses prefixed with a `$`.
- `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal - `==>[H1 ... Hn]` : same as the above pattern, but can only be used if the goal
is a primitive view shift, in which case the view shift will be kept in the is an update modality, in which case the update modality will be kept in the
goal of the premise too. goal of the premise too.
- `[#]` : This pattern can be used when eliminating `P -★ Q` with `P` - `[#]` : This pattern can be used when eliminating `P -★ Q` with `P`
persistent. Using this pattern, all hypotheses are available in the goal for persistent. Using this pattern, all hypotheses are available in the goal for
......
...@@ -69,7 +69,7 @@ program_logic/lifting.v ...@@ -69,7 +69,7 @@ program_logic/lifting.v
program_logic/invariants.v program_logic/invariants.v
program_logic/wsat.v program_logic/wsat.v
program_logic/weakestpre.v program_logic/weakestpre.v
program_logic/pviewshifts.v program_logic/fancy_updates.v
program_logic/hoare.v program_logic/hoare.v
program_logic/viewshifts.v program_logic/viewshifts.v
program_logic/language.v program_logic/language.v
......
From iris.algebra Require Import upred. From iris.algebra Require Import upred.
Import upred. Import upred.
(* In this file we show that the rvs can be thought of a kind of (* In this file we show that the bupd can be thought of a kind of
step-indexed double-negation when our meta-logic is classical *) step-indexed double-negation when our meta-logic is classical *)
(* To define this, we need a way to talk about iterated later modalities: *) (* To define this, we need a way to talk about iterated later modalities: *)
...@@ -12,10 +12,10 @@ Notation "▷^ n P" := (uPred_laterN n P) ...@@ -12,10 +12,10 @@ Notation "▷^ n P" := (uPred_laterN n P)
(at level 20, n at level 9, right associativity, (at level 20, n at level 9, right associativity,
format "▷^ n P") : uPred_scope. format "▷^ n P") : uPred_scope.
Definition uPred_nnvs {M} (P: uPred M) : uPred M := Definition uPred_nnupd {M} (P: uPred M) : uPred M :=
n, (P - ^n False) - ^n False. n, (P - ^n False) - ^n False.
Notation "|=n=> Q" := (uPred_nnvs Q) Notation "|=n=> Q" := (uPred_nnupd Q)
(at level 99, Q at level 200, format "|=n=> Q") : uPred_scope. (at level 99, Q at level 200, format "|=n=> Q") : uPred_scope.
Notation "P =n=> Q" := (P |=n=> Q) Notation "P =n=> Q" := (P |=n=> Q)
(at level 99, Q at level 200, only parsing) : C_scope. (at level 99, Q at level 200, only parsing) : C_scope.
...@@ -27,7 +27,7 @@ Notation "P =n=★ Q" := (P -★ |=n=> Q)%I ...@@ -27,7 +27,7 @@ Notation "P =n=★ Q" := (P -★ |=n=> Q)%I
(2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent (2) If our meta-logic is classical, then |=n=> and |=r=> are equivalent
*) *)
Section rvs_nnvs. Section bupd_nnupd.
Context {M : ucmraT}. Context {M : ucmraT}.
Implicit Types φ : Prop. Implicit Types φ : Prop.
Implicit Types P Q : uPred M. Implicit Types P Q : uPred M.
...@@ -58,40 +58,40 @@ Proof. ...@@ -58,40 +58,40 @@ Proof.
eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S. eapply (uPred_closed _ _ (S n)); eauto using cmra_validN_S.
Qed. Qed.
(* It is easy to show that most of the basic properties of rvs that (* It is easy to show that most of the basic properties of bupd that
are used throughout Iris hold for nnvs. are used throughout Iris hold for nnupd.
In fact, the first three properties that follow hold for any In fact, the first three properties that follow hold for any
modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation modality of the form (- -★ Q) -★ Q for arbitrary Q. The situation
here is slightly different, because nnvs is of the form here is slightly different, because nnupd is of the form
∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly. ∀ n, (- -★ (Q n)) -★ (Q n), but the proofs carry over straightforwardly.
*) *)
Lemma nnvs_intro P : P =n=> P. Lemma nnupd_intro P : P =n=> P.
Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed. Proof. apply forall_intro=>?. apply wand_intro_l, wand_elim_l. Qed.
Lemma nnvs_mono P Q : (P Q) (|=n=> P) =n=> Q. Lemma nnupd_mono P Q : (P Q) (|=n=> P) =n=> Q.
Proof. Proof.
intros HPQ. apply forall_intro=>n. intros HPQ. apply forall_intro=>n.
apply wand_intro_l. rewrite -{1}HPQ. apply wand_intro_l. rewrite -{1}HPQ.
rewrite /uPred_nnvs (forall_elim n). rewrite /uPred_nnupd (forall_elim n).
apply wand_elim_r. apply wand_elim_r.
Qed. Qed.
Lemma nnvs_frame_r P R : (|=n=> P) R =n=> P R. Lemma nnupd_frame_r P R : (|=n=> P) R =n=> P R.
Proof. Proof.
apply forall_intro=>n. apply wand_intro_r. apply forall_intro=>n. apply wand_intro_r.
rewrite (comm _ P) -wand_curry. rewrite (comm _ P) -wand_curry.
rewrite /uPred_nnvs (forall_elim n). rewrite /uPred_nnupd (forall_elim n).
by rewrite -assoc wand_elim_r wand_elim_l. by rewrite -assoc wand_elim_r wand_elim_l.
Qed. Qed.
Lemma nnvs_ownM_updateP x (Φ : M Prop) : Lemma nnupd_ownM_updateP x (Φ : M Prop) :
x ~~>: Φ uPred_ownM x =n=> y, Φ y uPred_ownM y. x ~~>: Φ uPred_ownM x =n=> y, Φ y uPred_ownM y.
Proof. Proof.
intros Hrvs. split. rewrite /uPred_nnvs. repeat uPred.unseal. intros Hbupd. split. rewrite /uPred_nnupd. repeat uPred.unseal.
intros n y ? Hown a. intros n y ? Hown a.
red; rewrite //= => n' yf ??. red; rewrite //= => n' yf ??.
inversion Hown as (x'&Hequiv). inversion Hown as (x'&Hequiv).
edestruct (Hrvs n' (Some (x' yf))) as (y'&?&?); eauto. edestruct (Hbupd n' (Some (x' yf))) as (y'&?&?); eauto.
{ by rewrite //= assoc -(dist_le _ _ _ _ Hequiv). } { by rewrite //= assoc -(dist_le _ _ _ _ Hequiv). }
case (decide (a n')). case (decide (a n')).
- intros Hle Hwand. - intros Hle Hwand.
...@@ -110,18 +110,18 @@ Qed. ...@@ -110,18 +110,18 @@ Qed.
now over n? now over n?
*) *)
Remark nnvs_trans P: (|=n=> |=n=> P) (|=n=> P). Remark nnupd_trans P: (|=n=> |=n=> P) (|=n=> P).
Proof. Proof.
rewrite /uPred_nnvs. rewrite /uPred_nnupd.
apply forall_intro=>a. apply wand_intro_l. apply forall_intro=>a. apply wand_intro_l.
rewrite (forall_elim a). rewrite (forall_elim a).
rewrite (nnvs_intro (P - _)). rewrite (nnupd_intro (P - _)).
rewrite /uPred_nnvs. rewrite /uPred_nnupd.
(* Oops -- the exponents of the later modality don't match up! *) (* Oops -- the exponents of the later modality don't match up! *)
Abort. Abort.
(* Instead, we will need to prove this in the model. We start by showing that (* Instead, we will need to prove this in the model. We start by showing that
nnvs is the limit of a the following sequence: nnupd is the limit of a the following sequence:
(- -★ False) - ★ False, (- -★ False) - ★ False,
(- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False, (- -★ ▷ False) - ★ ▷ False ∧ (- -★ False) - ★ False,
...@@ -129,33 +129,33 @@ Abort. ...@@ -129,33 +129,33 @@ Abort.
... ...
Then, it is easy enough to show that each of the uPreds in this sequence Then, it is easy enough to show that each of the uPreds in this sequence
is transitive. It turns out that this implies that nnvs is transitive. *) is transitive. It turns out that this implies that nnupd is transitive. *)
(* The definition of the sequence above: *) (* The definition of the sequence above: *)
Fixpoint uPred_nnvs_k {M} k (P: uPred M) : uPred M := Fixpoint uPred_nnupd_k {M} k (P: uPred M) : uPred M :=
((P - ^k False) - ^k False) ((P - ^k False) - ^k False)
match k with match k with
O => True O => True
| S k' => uPred_nnvs_k k' P | S k' => uPred_nnupd_k k' P
end. end.
Notation "|=n=>_ k Q" := (uPred_nnvs_k k Q) Notation "|=n=>_ k Q" := (uPred_nnupd_k k Q)
(at level 99, k at level 9, Q at level 200, format "|=n=>_ k Q") : uPred_scope. (at level 99, k at level 9, Q at level 200, format "|=n=>_ k Q") : uPred_scope.
(* One direction of the limiting process is easy -- nnvs implies nnvs_k for each k *) (* One direction of the limiting process is easy -- nnupd implies nnupd_k for each k *)
Lemma nnvs_trunc1 k P: (|=n=> P) |=n=>_k P. Lemma nnupd_trunc1 k P: (|=n=> P) |=n=>_k P.
Proof. Proof.
induction k. induction k.
- rewrite /uPred_nnvs_k /uPred_nnvs. - rewrite /uPred_nnupd_k /uPred_nnupd.
rewrite (forall_elim 0) //= right_id //. rewrite (forall_elim 0) //= right_id //.
- simpl. apply and_intro; auto. - simpl. apply and_intro; auto.
rewrite /uPred_nnvs. rewrite /uPred_nnupd.
rewrite (forall_elim (S k)) //=. rewrite (forall_elim (S k)) //=.
Qed. Qed.
Lemma nnvs_k_elim n k P: n k ((|=n=>_k P) (P - (^n False)) (^n False))%I. Lemma nnupd_k_elim n k P: n k ((|=n=>_k P) (P - (^n False)) (^n False))%I.
Proof. Proof.
induction k. induction k.
- inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l. - inversion 1; subst; rewrite //= ?right_id. apply wand_elim_l.
...@@ -164,23 +164,23 @@ Proof. ...@@ -164,23 +164,23 @@ Proof.
* rewrite and_elim_r IHk //. * rewrite and_elim_r IHk //.
Qed. Qed.
Lemma nnvs_k_unfold k P: Lemma nnupd_k_unfold k P:
(|=n=>_(S k) P) ((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P). (|=n=>_(S k) P) ((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P).
Proof. done. Qed. Proof. done. Qed.
Lemma nnvs_k_unfold' k P n x: Lemma nnupd_k_unfold' k P n x:
(|=n=>_(S k) P)%I n x (((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P))%I n x. (|=n=>_(S k) P)%I n x (((P - (^(S k) False)) - (^(S k) False)) (|=n=>_k P))%I n x.
Proof. done. Qed. Proof. done. Qed.
Lemma nnvs_k_weaken k P: (|=n=>_(S k) P) |=n=>_k P. Lemma nnupd_k_weaken k P: (|=n=>_(S k) P) |=n=>_k P.
Proof. by rewrite nnvs_k_unfold and_elim_r. Qed. Proof. by rewrite nnupd_k_unfold and_elim_r. Qed.
(* Now we are ready to show nnvs is the limit -- ie, for each k, it is within distance k (* Now we are ready to show nnupd is the limit -- ie, for each k, it is within distance k
of the kth term of the sequence *) of the kth term of the sequence *)
Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I {k} (|=n=>_k P)%I. Lemma nnupd_nnupd_k_dist k P: (|=n=> P)%I {k} (|=n=>_k P)%I.
split; intros n' x Hle Hx. split. split; intros n' x Hle Hx. split.
- by apply (nnvs_trunc1 k). - by apply (nnupd_trunc1 k).
- revert n' x Hle Hx; induction k; intros n' x Hle Hx; - revert n' x Hle Hx; induction k; intros n' x Hle Hx;
rewrite ?nnvs_k_unfold' /uPred_nnvs. rewrite ?nnupd_k_unfold' /uPred_nnupd.
* rewrite //=. unseal. * rewrite //=. unseal.
inversion Hle; subst. inversion Hle; subst.
intros (HnnP&_) n k' x' ?? HPF. intros (HnnP&_) n k' x' ?? HPF.
...@@ -199,17 +199,17 @@ Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I. ...@@ -199,17 +199,17 @@ Lemma nnvs_nnvs_k_dist k P: (|=n=> P)%I ≡{k}≡ (|=n=>_k P)%I.
*** intros. exfalso. assert (n k'). omega. *** intros. exfalso. assert (n k'). omega.
assert (n = S k n < S k) as [->|] by omega. assert (n = S k n < S k) as [->|] by omega.
**** eapply laterN_big; eauto; unseal. eapply HnnP; eauto. **** eapply laterN_big; eauto; unseal. eapply HnnP; eauto.
**** move:nnvs_k_elim. unseal. intros Hnnvsk. **** move:nnupd_k_elim. unseal. intros Hnnupdk.
eapply laterN_big; eauto. unseal. eapply laterN_big; eauto. unseal.
eapply (Hnnvsk n k); first omega; eauto. eapply (Hnnupdk n k); first omega; eauto.
exists x, x'. split_and!; eauto. eapply uPred_closed; eauto. exists x, x'. split_and!; eauto. eapply uPred_closed; eauto.
eapply cmra_validN_op_l; eauto. eapply cmra_validN_op_l; eauto.
** intros HP. eapply IHk; auto. ** intros HP. eapply IHk; auto.
move:HP. unseal. intros (?&?); naive_solver. move:HP. unseal. intros (?&?); naive_solver.
Qed. Qed.
(* nnvs_k has a number of structural properties, including transitivity *) (* nnupd_k has a number of structural properties, including transitivity *)
Lemma nnvs_k_intro k P: P (|=n=>_k P). Lemma nnupd_k_intro k P: P (|=n=>_k P).
Proof. Proof.
induction k; rewrite //= ?right_id. induction k; rewrite //= ?right_id.
- apply wand_intro_l. apply wand_elim_l. - apply wand_intro_l. apply wand_elim_l.
...@@ -217,58 +217,58 @@ Proof. ...@@ -217,58 +217,58 @@ Proof.
apply wand_intro_l. apply wand_elim_l. apply wand_intro_l. apply wand_elim_l.
Qed. Qed.
Lemma nnvs_k_mono k P Q: (P Q) (|=n=>_k P) (|=n=>_k Q). Lemma nnupd_k_mono k P Q: (P Q) (|=n=>_k P) (|=n=>_k Q).
Proof. Proof.
induction k; rewrite //= ?right_id=>HPQ. induction k; rewrite //= ?right_id=>HPQ.
- do 2 (apply wand_mono; auto). - do 2 (apply wand_mono; auto).
- apply and_mono; auto; do 2 (apply wand_mono; auto). - apply and_mono; auto; do 2 (apply wand_mono; auto).
Qed. Qed.
Instance nnvs_k_mono' k: Proper (() ==> ()) (@uPred_nnvs_k M k). Instance nnupd_k_mono' k: Proper (() ==> ()) (@uPred_nnupd_k M k).
Proof. by intros P P' HP; apply nnvs_k_mono. Qed. Proof. by intros P P' HP; apply nnupd_k_mono. Qed.
Instance nnvs_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnvs_k M k). Instance nnupd_k_ne k n : Proper (dist n ==> dist n) (@uPred_nnupd_k M k).
Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed. Proof. induction k; rewrite //= ?right_id=>P P' HP; by rewrite HP. Qed.
Lemma nnvs_k_proper k P Q: (P Q) (|=n=>_k P) (|=n=>_k Q). Lemma nnupd_k_proper k P Q: (P Q) (|=n=>_k P) (|=n=>_k Q).
Proof. intros HP; apply (anti_symm ()); eapply nnvs_k_mono; by rewrite HP. Qed. Proof. intros HP; apply (anti_symm ()); eapply nnupd_k_mono; by rewrite HP. Qed.
Instance nnvs_k_proper' k: Proper (() ==> ()) (@uPred_nnvs_k M k). Instance nnupd_k_proper' k: Proper (() ==> ()) (@uPred_nnupd_k M k).
Proof. by intros P P' HP; apply nnvs_k_proper. Qed. Proof. by intros P P' HP; apply nnupd_k_proper. Qed.
Lemma nnvs_k_trans k P: (|=n=>_k |=n=>_k P) (|=n=>_k P). Lemma nnupd_k_trans k P: (|=n=>_k |=n=>_k P) (|=n=>_k P).
Proof. Proof.
revert P. revert P.
induction k; intros P. induction k; intros P.
- rewrite //= ?right_id. apply wand_intro_l. - rewrite //= ?right_id. apply wand_intro_l.
rewrite {1}(nnvs_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r. rewrite {1}(nnupd_k_intro 0 (P - False)%I) //= ?right_id. apply wand_elim_r.
- rewrite {2}(nnvs_k_unfold k P). - rewrite {2}(nnupd_k_unfold k P).
apply and_intro. apply and_intro.
* rewrite (nnvs_k_unfold k P). rewrite and_elim_l. * rewrite (nnupd_k_unfold k P). rewrite and_elim_l.
rewrite nnvs_k_unfold. rewrite and_elim_l. rewrite nnupd_k_unfold. rewrite and_elim_l.
apply wand_intro_l. apply wand_intro_l.
rewrite {1}(nnvs_k_intro (S k) (P - ^(S k) (False)%I)). rewrite {1}(nnupd_k_intro (S k) (P - ^(S k) (False)%I)).
rewrite nnvs_k_unfold and_elim_l. apply wand_elim_r. rewrite nnupd_k_unfold and_elim_l. apply wand_elim_r.
* do 2 rewrite nnvs_k_weaken //. * do 2 rewrite nnupd_k_weaken //.
Qed. Qed.
Lemma nnvs_trans P : (|=n=> |=n=> P) =n=> P. Lemma nnupd_trans P : (|=n=> |=n=> P) =n=> P.
Proof. Proof.
split=> n x ? Hnn. split=> n x ? Hnn.
eapply nnvs_nnvs_k_dist in Hnn; eauto. eapply nnupd_nnupd_k_dist in Hnn; eauto.
eapply (nnvs_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto; eapply (nnupd_k_ne (n) n ((|=n=>_(n) P)%I)) in Hnn; eauto;
[| symmetry; eapply nnvs_nnvs_k_dist]. [| symmetry; eapply nnupd_nnupd_k_dist].
eapply nnvs_nnvs_k_dist; eauto. eapply nnupd_nnupd_k_dist; eauto.
by apply nnvs_k_trans. by apply nnupd_k_trans.
Qed. Qed.
(* Now that we have shown nnvs has all of the desired properties of (* Now that we have shown nnupd has all of the desired properties of
rvs, we go further and show it is in fact equivalent to rvs! The bupd, we go further and show it is in fact equivalent to bupd! The
direction from rvs to nnvs is similar to the proof of direction from bupd to nnupd is similar to the proof of
nnvs_ownM_updateP *) nnupd_ownM_updateP *)
Lemma rvs_nnvs P: (|=r=> P) |=n=> P. Lemma bupd_nnupd P: (|=r=> P) |=n=> P.
Proof. Proof.
split. rewrite /uPred_nnvs. repeat uPred.unseal. intros n x ? Hrvs a. split. rewrite /uPred_nnupd. repeat uPred.unseal. intros n x ? Hbupd a.
red; rewrite //= => n' yf ??. red; rewrite //= => n' yf ??.
edestruct Hrvs as (x'&?&?); eauto. edestruct Hbupd as (x'&?&?); eauto.
case (decide (a n')). case (decide (a n')).
- intros Hle Hwand. - intros Hle Hwand.
exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto. exfalso. eapply laterN_big; last (uPred.unseal; eapply (Hwand n' x')); eauto.
...@@ -282,9 +282,9 @@ Qed. ...@@ -282,9 +282,9 @@ Qed.
(* However, the other direction seems to need a classical axiom: *) (* However, the other direction seems to need a classical axiom: *)
Section classical. Section classical.
Context (not_all_not_ex: (P : M Prop), ¬ ( n : M, ¬ P n) n : M, P n). Context (not_all_not_ex: (P : M Prop), ¬ ( n : M, ¬ P n) n : M, P n).
Lemma nnvs_rvs P: (|=n=> P) (|=r=> P). Lemma nnupd_bupd P: (|=n=> P) (|=r=> P).
Proof. Proof.
rewrite /uPred_nnvs. rewrite /uPred_nnupd.
split. uPred.unseal; red; rewrite //=. split. uPred.unseal; red; rewrite //=.
intros n x ? Hforall k yf Hle ?. intros n x ? Hforall k yf Hle ?.
apply not_all_not_ex. apply not_all_not_ex.
...@@ -300,36 +300,36 @@ Proof. ...@@ -300,36 +300,36 @@ Proof.
Qed. Qed.
End classical. End classical.
(* We might wonder whether we can prove an adequacy lemma for nnvs. We could combine (* We might wonder whether we can prove an adequacy lemma for nnupd. We could combine
the adequacy lemma for rvs with the previous result to get adquacy for nnvs, but the adequacy lemma for bupd with the previous result to get adquacy for nnupd, but
this would rely on the classical axiom we needed to prove the equivalence! Can this would rely on the classical axiom we needed to prove the equivalence! Can
we establish adequacy without axioms? Unfortunately not, because adequacy for we establish adequacy without axioms? Unfortunately not, because adequacy for
nnvs would imply double negation elimination, which is classical: *) nnupd would imply double negation elimination, which is classical: *)
Lemma nnvs_dne φ: True (|=n=> ((¬¬ φ φ)): uPred M)%I. Lemma nnupd_dne φ: True (|=n=> ((¬¬ φ φ)): uPred M)%I.
Proof. Proof.
rewrite /uPred_nnvs. apply forall_intro=>n. rewrite /uPred_nnupd. apply forall_intro=>n.
apply wand_intro_l. rewrite ?right_id. apply wand_intro_l. rewrite ?right_id.
assert ( φ, ¬¬¬¬φ ¬¬φ) by naive_solver. assert ( φ, ¬¬¬¬φ ¬¬φ) by naive_solver.
assert (Hdne: ¬¬ (¬¬φ φ)) by naive_solver. assert (Hdne: ¬¬ (¬¬φ φ)) by naive_solver.
split. unseal. intros n' ?? Hvs. split. unseal. intros n' ?? Hupd.
case (decide (n' < n)). case (decide (n' < n)).
- intros. move: laterN_small. unseal. naive_solver. - intros. move: laterN_small. unseal. naive_solver.
- intros. assert (n n'). omega. - intros. assert (n n'). omega.
exfalso. specialize (Hvs n' ).