naught and future
The snippet can be accessed without any authentication.
Authored by
Amin Timany
Edited
naught_and_future.v 23.52 KiB
From iris.base_logic Require Import upred derived lib.fancy_updates
primitive lib.wsat soundness.
Import uPred_primitive.
Import uPred.
Require Import iris.proofmode.tactics.
(* Some interesting lemmas! *)
Lemma core_unit {M : ucmraT} : core (∅ : M) ≡ ∅.
Proof. by rewrite /core /core' ucmra_pcore_unit. Qed.
Lemma except_0_sep' (M : ucmraT) (P Q : uPred M) : (◇ (P ★ Q))%I ⊢ (◇ P ★ ◇ Q)%I.
Proof. by rewrite except_0_sep. Qed.
Lemma except_0_exist (M : ucmraT) A `{Inhabited A} (P : A → uPred M) :
(◇ ∃ x, P x) ⊢ ∃ x, ◇ P x.
Proof.
rewrite /uPred_except_0; unseal; constructor => n x Hnx Hde.
destruct n.
- exists inhabitant; by left.
- destruct Hde as [Hde|Hde]; first done. destruct Hde as [z Hde].
by exists z; right.
Qed.
Lemma except_0_forall (M : ucmraT) A (P : A → uPred M) :
(∀ x, ◇ P x) ⊢ (◇ ∀ x, P x).
Proof.
rewrite /uPred_except_0; unseal; constructor => n x Hnx Hde.
destruct n; first by left.
right=>z. specialize (Hde z); destruct Hde as [Hde|Hde]; done.
Qed.
(* Naught modality *)
Program Definition uPred_naught_def {M} (P : uPred M) : uPred M :=
{| uPred_holds n x := P n ∅ |}.
Next Obligation.
intros M; naive_solver eauto using uPred_mono, @cmra_core_monoN.
Qed.
Next Obligation. naive_solver eauto using uPred_closed, @ucmra_unit_validN. Qed.
Definition uPred_naught_aux : { x | x = @uPred_naught_def }. by eexists. Qed.
Definition uPred_naught {M} := proj1_sig uPred_naught_aux M.
Definition uPred_naught_eq :
@uPred_naught = @uPred_naught_def := proj2_sig uPred_naught_aux.
(* Notation for naught: ⨳ (\smashtimes) *)
Notation "⨳ P" := (uPred_naught P)
(at level 20, right associativity) : uPred_scope.
(* A plain fact is one that holds independent of resources. *)
Class PlainP {M} (P : uPred M) := plainP : P ⊢ ⨳ P.
Arguments plainP {_} _ {_}.
Section naught_properties.
Context {M : ucmraT}.
Implicit Types φ : Prop.
Implicit Types P Q : uPred M.
Implicit Types A : Type.
Notation "P ⊢ Q" := (@uPred_entails M P%I Q%I). (* Force implicit argument M *)
Notation "P ⊣⊢ Q" := (equiv (A:=uPred M) P%I Q%I). (* Force implicit argument M *)
(* naught primitive properties *)
Global Instance naught_ne n : Proper (dist n ==> dist n) (@uPred_naught M).
Proof.
intros P1 P2 HP.
rewrite uPred_naught_eq; split=> n' x; split; apply HP;
eauto using @ucmra_unit_validN.
Qed.
Global Instance naught_proper :
Proper ((⊣⊢) ==> (⊣⊢)) (@uPred_naught M) := ne_proper _.
Lemma true_entails_naught P : (True ⊢ P) → (True ⊢ ⨳ P).
Proof.
unseal; rewrite uPred_naught_eq; intros HP. split=>n x Hx HT.
apply HP; last done; apply ucmra_unit_validN.
Qed.
Lemma naught_irrel P n x y : (⨳ P)%I n x → (⨳ P)%I n y.
Proof. by rewrite uPred_naught_eq. Qed.
Lemma naught_keeps_premises P Q : (P ⊢ ⨳ Q) → P ⊢ P ★ ⨳ Q.
Proof.
intros HPQ. split=> n x Hx HPx. unseal.
exists x, (∅ : M); repeat split; trivial; first by rewrite right_id.
apply HPQ in HPx; last trivial. eauto using naught_irrel.
Qed.
Lemma naught_mono P Q : (P ⊢ Q) → ⨳ P ⊢ ⨳ Q.
Proof.
intros HP; rewrite uPred_naught_eq; split=> n x ? /=.
apply HP, ucmra_unit_validN.
Qed.
Lemma naught_elim P : ⨳ P ⊢ P.
Proof.
rewrite uPred_naught_eq; split=> n x ? ? /=.
by eapply uPred_mono; last eapply cmra_included_includedN, @ucmra_unit_least.
Qed.
Lemma naught_idemp P : ⨳ P ⊢ ⨳ ⨳ P.
Proof. by rewrite uPred_naught_eq. Qed.
Lemma naught_pure_2 φ : ■ φ ⊢ ⨳ ■ φ.
Proof. by unseal; rewrite uPred_naught_eq. Qed.
Lemma naught_implies_always P : ⨳ P ⊢ □ P.
Proof.
unseal; rewrite uPred_naught_eq. split=> n x Hx.
cbv [uPred_naught_def uPred_always_def uPred_holds]=> HP.
eapply uPred_mono; eauto; apply ucmra_unit_leastN.
Qed.
Lemma naught_always_1 P : □ ⨳ P ⊢ ⨳ □ P.
Proof.
unseal; rewrite uPred_naught_eq; split=> n x ? /=.
cbv [uPred_naught_def uPred_always_def uPred_holds].
by rewrite core_unit.
Qed.
Lemma naught_always_2 P : ⨳ □ P ⊢ □ ⨳ P.
Proof.
unseal; rewrite uPred_naught_eq; split=> n x ? /=.
cbv [uPred_naught_def uPred_always_def uPred_holds].
by rewrite core_unit.
Qed.
Lemma naught_forall_2 {A} (Ψ : A → uPred M) : (∀ a, ⨳ Ψ a) ⊢ (⨳ ∀ a, Ψ a).
Proof. by unseal; rewrite uPred_naught_eq. Qed.
Lemma naught_exist_1 {A} (Ψ : A → uPred M) : (⨳ ∃ a, Ψ a) ⊢ (∃ a, ⨳ Ψ a).
Proof. by unseal; rewrite uPred_naught_eq. Qed.
Lemma naught_and_sep_1 P Q : ⨳ (P ∧ Q) ⊢ ⨳ (P ★ Q).
Proof.
unseal; rewrite uPred_naught_eq; split=> n x ? [??].
exists (∅ : M), (∅ : M); rewrite left_id; auto.
Qed.
Lemma naught_and_sep_l_1 P Q : ⨳ P ∧ Q ⊢ ⨳ P ★ Q.
Proof.
unseal; rewrite uPred_naught_eq; split=> n x ? [??]; exists ∅, x; simpl in *.
by rewrite left_id.
Qed.
Lemma naught_later P : ⨳ ▷ P ⊣⊢ ▷ ⨳ P.
Proof. by unseal; rewrite uPred_naught_eq. Qed.
Lemma naught_ownM : ⨳ uPred_ownM ∅ ⊣⊢ uPred_ownM ∅. (* perhaps quite useless!? *)
Proof.
intros; apply (anti_symm _); first by apply:naught_elim.
unseal; rewrite uPred_naught_eq; split=> n x ? ?.
by cbv [uPred_naught_def uPred_ownM_def uPred_holds].
Qed.
Lemma naught_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ ⨳ ✓ a.
Proof. by unseal; rewrite uPred_naught_eq. Qed.
Hint Resolve pure_intro.
Hint Resolve or_elim or_intro_l' or_intro_r'.
Hint Resolve and_intro and_elim_l' and_elim_r'.
Hint Immediate True_intro False_elim.
(* Naught derived *)
Hint Resolve naught_mono naught_elim.
Global Instance naught_mono' : Proper ((⊢) ==> (⊢)) (@uPred_naught M).
Proof. intros P Q; apply naught_mono. Qed.
Global Instance naught_flip_mono' :
Proper (flip (⊢) ==> flip (⊢)) (@uPred_naught M).
Proof. intros P Q; apply naught_mono. Qed.
Lemma naught_intro' P Q : (⨳ P ⊢ Q) → ⨳ P ⊢ ⨳ Q.
Proof. intros <-. apply naught_idemp. Qed.
Lemma naught_pure φ : ⨳ ■ φ ⊣⊢ ■ φ.
Proof. apply (anti_symm _); auto using naught_pure_2. Qed.
Lemma naught_forall {A} (Ψ : A → uPred M) : (⨳ ∀ a, Ψ a) ⊣⊢ (∀ a, ⨳ Ψ a).
Proof.
apply (anti_symm _); auto using naught_forall_2.
apply forall_intro=> x. by rewrite (forall_elim x).
Qed.
Lemma naught_exist {A} (Ψ : A → uPred M) : (⨳ ∃ a, Ψ a) ⊣⊢ (∃ a, ⨳ Ψ a).
Proof.
apply (anti_symm _); auto using naught_exist_1.
apply exist_elim=> x. by rewrite (exist_intro x).
Qed.
Lemma naught_and P Q : ⨳ (P ∧ Q) ⊣⊢ ⨳ P ∧ ⨳ Q.
Proof. rewrite !and_alt naught_forall. by apply forall_proper=> -[]. Qed.
Lemma naught_or P Q : ⨳ (P ∨ Q) ⊣⊢ ⨳ P ∨ ⨳ Q.
Proof. rewrite !or_alt naught_exist. by apply exist_proper=> -[]. Qed.
Lemma naught_impl P Q : ⨳ (P → Q) ⊢ ⨳ P → ⨳ Q.
Proof.
apply impl_intro_l; rewrite -naught_and.
apply naught_mono, impl_elim with P; auto.
Qed.
Lemma naught_internal_eq {A:cofeT} (a b : A) : ⨳ (a ≡ b) ⊣⊢ a ≡ b.
Proof.
apply (anti_symm (⊢)); auto using naught_elim.
apply (internal_eq_rewrite a b (λ b, ⨳ (a ≡ b))%I); auto.
{ intros n; solve_proper. }
rewrite -(internal_eq_refl a) naught_pure; auto.
Qed.
Lemma naught_always P : ⨳ □ P ⊣⊢ □ ⨳ P.
Proof.
apply (anti_symm _); auto using naught_always_1, naught_always_2.
Qed.
Lemma naught_and_sep P Q : ⨳ (P ∧ Q) ⊣⊢ ⨳ (P ★ Q).
Proof.
apply (anti_symm (⊢)); last rewrite sep_and; auto using naught_and_sep_1.
Qed.
Lemma naught_and_sep_l' P Q : ⨳ P ∧ Q ⊣⊢ ⨳ P ★ Q.
Proof.
apply (anti_symm (⊢)); last rewrite sep_and; auto using naught_and_sep_l_1.
Qed.
Lemma naught_and_sep_r' P Q : P ∧ ⨳ Q ⊣⊢ P ★ ⨳ Q.
Proof. by rewrite !(comm _ P) naught_and_sep_l'. Qed.
Lemma naught_sep P Q : ⨳ (P ★ Q) ⊣⊢ ⨳ P ★ ⨳ Q.
Proof. by rewrite -naught_and_sep -naught_and_sep_l' naught_and. Qed.
Lemma naught_sep_dup' P : ⨳ P ⊣⊢ ⨳ P ★ ⨳ P.
Proof. by rewrite -naught_sep -naught_and_sep (idemp _). Qed.
Lemma naught_wand P Q : ⨳ (P -★ Q) ⊢ ⨳ P -★ ⨳ Q.
Proof. by apply wand_intro_r; rewrite -naught_sep wand_elim_l. Qed.
Lemma naught_wand_impl P Q : ⨳ (P -★ Q) ⊣⊢ ⨳ (P → Q).
Proof.
apply (anti_symm (⊢)); [|by rewrite -impl_wand].
apply naught_intro', impl_intro_r.
by rewrite naught_and_sep_l' naught_elim wand_elim_l.
Qed.
Lemma naught_entails_l' P Q : (P ⊢ ⨳ Q) → P ⊢ ⨳ Q ★ P.
Proof. intros; rewrite -naught_and_sep_l'; auto. Qed.
Lemma naught_entails_r' P Q : (P ⊢ ⨳ Q) → P ⊢ P ★ ⨳ Q.
Proof. intros; rewrite -naught_and_sep_r'; auto. Qed.
Lemma except_0_naught P : ◇ ⨳ P ⊣⊢ ⨳ ◇ P.
Proof. by rewrite /uPred_except_0 naught_or naught_later naught_pure. Qed.
Lemma naught_cmra_valid {A : cmraT} (a : A) : ⨳ ✓ a ⊣⊢ ✓ a.
Proof.
intros; apply (anti_symm _); first by apply:naught_elim.
apply:naught_cmra_valid_1.
Qed.
(* Plainness *)
Global Instance pure_plain φ : PlainP (■ φ : uPred M)%I.
Proof. by rewrite /PlainP naught_pure. Qed.
Global Instance naught_plain P : PlainP (⨳ P).
Proof. by intros; apply naught_intro'. Qed.
Global Instance and_plain P Q :
PlainP P → PlainP Q → PlainP (P ∧ Q).
Proof. by intros; rewrite /PlainP naught_and; apply and_mono. Qed.
Global Instance or_plain P Q :
PlainP P → PlainP Q → PlainP (P ∨ Q).
Proof. by intros; rewrite /PlainP naught_or; apply or_mono. Qed.
Global Instance sep_plain P Q :
PlainP P → PlainP Q → PlainP (P ★ Q).
Proof. by intros; rewrite /PlainP naught_sep; apply sep_mono. Qed.
Global Instance forall_plain {A} (Ψ : A → uPred M) :
(∀ x, PlainP (Ψ x)) → PlainP (∀ x, Ψ x).
Proof. by intros; rewrite /PlainP naught_forall; apply forall_mono. Qed.
Global Instance exist_plain {A} (Ψ : A → uPred M) :
(∀ x, PlainP (Ψ x)) → PlainP (∃ x, Ψ x).
Proof. by intros; rewrite /PlainP naught_exist; apply exist_mono. Qed.
Global Instance internal_eq_plain {A : cofeT} (a b : A) :
PlainP (a ≡ b : uPred M)%I.
Proof. by intros; rewrite /PlainP naught_internal_eq. Qed.
Global Instance cmra_valid_plain {A : cmraT} (a : A) :
PlainP (✓ a : uPred M)%I.
Proof. by intros; rewrite /PlainP naught_cmra_valid. Qed.
Global Instance later_plain P : PlainP P → PlainP (▷ P).
Proof. by intros; rewrite /PlainP naught_later; apply later_mono. Qed.
Global Instance ownM_plain : PlainP (@uPred_ownM M ∅). (* perhaps quite useless!? *)
Proof. intros. by rewrite /PlainP naught_ownM. Qed.
Global Instance from_option_plain {A} P (Ψ : A → uPred M) (mx : option A) :
(∀ x, PlainP (Ψ x)) → PlainP P → PlainP (from_option Ψ P mx).
Proof. destruct mx; apply _. Qed.
Global Instance except_0_plain P : PlainP P → PlainP (◇ P).
Proof. intros; by rewrite /PlainP -except_0_naught except_0_mono. Qed.
(* Plainness implies persistence *)
Global Instance plain_persistent P : PlainP P → PersistentP P.
Proof.
rewrite /PlainP /PersistentP => HP.
by etrans; last apply naught_implies_always.
Qed.
(* Derived lemmas for plainness *)
Lemma naught_naught P `{!PlainP P} : ⨳ P ⊣⊢ P.
Proof. apply (anti_symm (⊢)); auto. Qed.
Lemma naught_intro P Q `{!PlainP P} : (P ⊢ Q) → P ⊢ ⨳ Q.
Proof. rewrite -(naught_naught P); apply naught_intro'. Qed.
Lemma naught_and_sep_l P Q `{!PlainP P} : P ∧ Q ⊣⊢ P ★ Q.
Proof. by rewrite -(naught_naught P) naught_and_sep_l'. Qed.
Lemma naught_and_sep_r P Q `{!PlainP Q} : P ∧ Q ⊣⊢ P ★ Q.
Proof. by rewrite -(naught_naught Q) naught_and_sep_r'. Qed.
Lemma naught_sep_dup P `{!PlainP P} : P ⊣⊢ P ★ P.
Proof. by rewrite -(naught_naught P) -naught_sep_dup'. Qed.
Lemma naught_entails_l P Q `{!PlainP Q} : (P ⊢ Q) → P ⊢ Q ★ P.
Proof. by rewrite -(naught_naught Q); apply naught_entails_l'. Qed.
Lemma naught_entails_r P Q `{!PlainP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
Proof. by rewrite -(naught_naught Q); apply naught_entails_r'. Qed.
(* important for proving properties in the model. *)
Lemma naught_irrel' P `{HPl: !PlainP P} n x y : ✓{n} x → ✓{n} y → P n x → P n y.
Proof.
intros Hx Hy Hnx; apply HPl in Hnx; last done.
apply naught_elim; first done. eapply naught_irrel; eauto.
Qed.
Lemma naught_keeps_premises' P Q `{HPl: !PlainP Q} : (P ⊢ Q) → P ⊢ P ★ Q.
Proof.
iIntros (HPQ) "HP".
assert (HPQ': P ⊢ ⨳ Q) by (by iIntros "HP"; iApply HPl; iApply HPQ).
iPoseProof (naught_keeps_premises _ _ HPQ' with "HP") as "HPQ".
iDestruct "HPQ" as "[HP HQ]"; iSplitL "HP"; first trivial.
by iApply naught_elim.
Qed.
Global Instance iter_Plain_Plain P `{Hpl: !PlainP P} n f :
(∀ Q, PlainP Q -> PlainP (f Q)) →
PlainP (Nat.iter n f P).
Proof.
revert P Hpl. induction n => P Hpl; first done.
rewrite Nat_iter_S_r; auto.
Qed.
End naught_properties.
Lemma bupd_extract_plain {M : ucmraT} (P Q : uPred M) `{!PlainP P} :
(Q ⊢ P) → (|==> Q) ⊢ P.
Proof.
intros HQP; unseal; split=> n x Hnx Hbp.
destruct (Hbp n ∅ (le_n _)) as [z [Hz1 Hz2]]; first by rewrite right_id.
revert Hz1; rewrite right_id=> Hz1.
apply HQP in Hz2; trivial. eauto using naught_irrel', ucmra_unit_validN.
Qed.
(* future modality *)
Program Definition future_def `{invG Σ}
(E : coPset) n (P : iProp Σ) : iProp Σ :=
(Nat.iter n (λ Q, (|={E}=> ▷ Q)) (|={E}=> P))%I.
Definition future_aux : { x | x = @future_def }. by eexists. Qed.
Definition future := proj1_sig future_aux.
Definition future_eq : @future = @future_def := proj2_sig future_aux.
Arguments future {_ _} _ _ _%I.
Instance: Params (@fupd) 4.
Notation "|≫{ E }=[ n ]=> Q" := (future E n Q)
(at level 99, E at level 50, Q at level 200,
format "|≫{ E }=[ n ]=> Q") : uPred_scope.
Notation "P ≫{ E }=[ n ]=★ Q" := (P -★ |≫{E}=[n]=> Q)%I
(at level 99, E at level 50, Q at level 200,
format "P ≫{ E }=[ n ]=★ Q") : uPred_scope.
Notation "P ≫{ E }=[ n ]=★ Q" := (P ⊢ |≫{E}=[n]=> Q)
(at level 99, E at level 50, Q at level 200, only parsing) : C_scope.
Lemma future_unfold `{invG Σ} (E : coPset) n (P : iProp Σ) :
(|≫{E}=[n]=> P) ⊣⊢
(match n with
| O => |={E}=> P
| S n => (Nat.iter (S n) (λ Q, (|={E}=> ▷ Q)) (|={E}=> P))
end).
Proof.
rewrite future_eq. destruct n; trivial.
Qed.
Lemma future_unfold_O `{invG Σ} (E : coPset) (P : iProp Σ) :
(|≫{E}=[0]=> P) ⊣⊢ |={E}=> P.
Proof. by rewrite future_unfold. Qed.
Lemma future_unfold_S `{invG Σ} (E : coPset) n (P : iProp Σ) :
(|≫{E}=[S n]=> P) ⊣⊢ (Nat.iter (S n) (λ Q, (|={E}=> ▷ Q)) (|={E}=> P)).
Proof. by rewrite future_unfold. Qed.
Section fupd_and_plain.
Context `{invG Σ}.
Lemma fupd_extract_plain {E1 E2} P Q `{!PlainP P} :
(Q ⊢ P) → (|={E1, E2}=> Q) ⊢ |={E1}=> ((|={E1, E2}=> Q) ★ P).
Proof.
intros HQP. rewrite fupd_eq /fupd_def; unseal.
split => n x Hx Hfp k x' Hkn Hxx' Hwo.
destruct (Hfp k x' Hkn Hxx' Hwo k ∅ (le_n _)) as [z [Hz1 Hz2]];
first by rewrite right_id.
assert (Hz1' : ✓{k} (z)) by (by revert Hz1; rewrite right_id).
assert (HP : (◇ P)%I k ∅).
{ rewrite -uPred_sep_eq in Hz2. apply except_0_sep' in Hz2; last done.
rewrite uPred_sep_eq in Hz2. destruct Hz2 as (z1 & z2 & Hz & _ & Hz2).
rewrite -uPred_sep_eq in Hz2.
assert (Hz2vl : ✓{k} z2) by (revert Hz1'; rewrite Hz;
eauto using cmra_validN_op_l, cmra_validN_op_r).
apply except_0_sep' in Hz2; last done.
rewrite uPred_sep_eq in Hz2. destruct Hz2 as (w1 & w2 & Hw & _ & Hz2).
assert (Hw2vl : ✓{k} w2) by (revert Hz2vl; rewrite Hw;
eauto using cmra_validN_op_l, cmra_validN_op_r).
eapply (naught_irrel' _ _ w2); auto using ucmra_unit_validN.
by eapply (except_0_mono _ _ HQP). }
intros m yf Hmk Hxx'yf. exists (x ⋅ x'); split; auto.
destruct Hwo as (u1 & u2 & Hu & Hu1 & Hu2).
rewrite -uPred_sep_eq; apply except_0_sep; first eauto using cmra_validN_le.
rewrite uPred_sep_eq.
exists u1, (x ⋅ u2); split;
first by rewrite (comm _ u1) -assoc (dist_le _ _ _ _ Hu) // (comm _ u1).
split.
{ assert (✓{m} u1) by
(revert Hxx'; rewrite Hu=> Hxx';
eapply cmra_validN_op_l, cmra_validN_op_r, cmra_validN_le; eauto).
apply except_0_intro; last eapply uPred_closed; eauto. }
assert (✓{m} (x ⋅ u2)) by
(revert Hxx'; rewrite Hu=> Hxx';
eapply cmra_validN_op_l; rewrite -assoc (comm _ u2);
eapply cmra_validN_le; eauto).
rewrite -uPred_sep_eq; apply except_0_sep; first done. rewrite uPred_sep_eq.
exists u2, x; split; first by rewrite (comm _ u2).
split.
{ assert (✓{m} u2) by eauto using cmra_validN_op_r.
apply except_0_intro; last eapply uPred_closed; eauto. }
rewrite -uPred_sep_eq. apply except_0_sep; first eauto using cmra_validN_op_l.
rewrite uPred_sep_eq.
exists x, (∅ : iResUR Σ); split; first by rewrite right_id.
split.
{ apply except_0_intro; first eauto using cmra_validN_op_l.
eapply uPred_closed; eauto; last eauto using cmra_validN_op_l. omega. }
eapply uPred_closed; eauto using ucmra_unit_validN.
Qed.
Lemma later_fupd_plain {E} P `{Hpl: !PlainP P} :
(▷ |={E}=> P) ⊢ |={E}=> ▷ ◇ P.
Proof.
rewrite fupd_eq /fupd_def later_wand; unseal.
split=> n x Hx Hfp k x' Hkn Hxx' Hwo.
pose proof (Hwo) as Hwo'; apply later_intro in Hwo';
last eauto using cmra_validN_op_r; rewrite uPred_later_eq in Hwo'.
specialize (Hfp k x' Hkn Hxx' Hwo').
assert (HP : (▷ ◇ P)%I k x).
{ eapply (naught_irrel' _ _ (x ⋅ x')); eauto using cmra_validN_op_l.
eapply later_mono; last (rewrite uPred_later_eq; apply Hfp); trivial.
rewrite -uPred_bupd_eq; apply bupd_extract_plain; first typeclasses eauto.
apply except_0_mono; rewrite -uPred_sep_eq; by iIntros "(_&_&?)".
}
rewrite -uPred_bupd_eq; apply bupd_intro; trivial.
rewrite -uPred_sep_eq -uPred_later_eq. rewrite -uPred_sep_eq in Hwo.
apply except_0_intro; trivial.
apply sep_assoc'; trivial.
rewrite {1}uPred_sep_eq; eexists x', x.
repeat split; trivial; by rewrite (comm _ x).
Qed.
Lemma step_Sn_fupd_mono {E} P Q n :
(P ⊢ Q) →
Nat.iter n (λ Q : iProp Σ, |={E}=> ▷ Q) P ⊢
Nat.iter n (λ Q : iProp Σ, |={E}=> ▷ Q) Q.
Proof.
revert P Q; induction n=> P Q HPQ; first done.
rewrite !Nat_iter_S_r; apply IHn. iIntros "HP".
iMod "HP"; iModIntro; iNext; by iApply HPQ.
Qed.
Lemma future_plain_base {E} P `{Hpl: !PlainP P} n :
(Nat.iter (S n) (λ Q, (|={E}=> ▷ Q)) (|={E}=> P)) ⊢
|={E}=> Nat.iter (S n) (λ Q, ▷ ◇ Q) P.
Proof.
revert P Hpl. induction n=> P Hpl.
- simpl. iIntros "HP"; iMod "HP"; by iApply later_fupd_plain.
- rewrite !(Nat_iter_S_r (S n)). iIntros "Hfpn".
iApply IHn. iApply step_Sn_fupd_mono; last trivial.
iIntros "HP"; iMod "HP"; by iApply later_fupd_plain.
Qed.
Lemma later_n_mono {M} P Q n :
(P ⊢ Q) → Nat.iter n (λ Q : uPred M, ▷ Q) P ⊢ Nat.iter n (λ Q, ▷ Q) Q.
Proof.
revert P Q; induction n=> P Q HPQ; first trivial.
rewrite !Nat_iter_S_r. by apply IHn, later_mono.
Qed.
Lemma later_except_0_n {M} P n :
Nat.iter (S n) (λ Q : uPred M, ▷ ◇ Q) P ⊢ Nat.iter (S n) (λ Q, ▷ Q) (◇ P)%I.
Proof.
revert P; induction n=> P; first trivial.
rewrite !(Nat_iter_S_r (S n)). iIntros "Hfpn".
iPoseProof (IHn with "Hfpn") as "Hfpn".
iApply later_n_mono; last trivial.
apply except_0_later.
Qed.
Lemma fupd_plain_forall_comm {E1 E2} (A :Type) (P : A → iProp Σ)
`{Hpl: ∀ x, PlainP (P x)} :
(∀ x : A, (|={E1,E2}=> P x))%I ⊢ |={E1}=> (∀ x : A, P x).
Proof.
rewrite fupd_eq /fupd_def; unseal.
split=> n x Hx Hfp k x' Hkn Hxx' Hwo k' yf Hkk' Hxx'yf.
exists (x ⋅ x'); split; first trivial.
assert (Hk'xx' : ✓{k'} (x ⋅ x')) by eauto using cmra_validN_le.
rewrite -uPred_sep_eq. rewrite -uPred_sep_eq in Hwo.
eapply except_0_mono; first apply sep_assoc';
last apply except_0_frame_l; trivial.
rewrite {1}uPred_sep_eq; eexists x', x; repeat split; first by rewrite comm.
eapply uPred_closed; eauto using cmra_validN_op_r.
rewrite uPred_sep_eq in Hwo.
rewrite -uPred_forall_eq; apply except_0_forall; eauto using cmra_validN_op_l.
rewrite uPred_forall_eq => u.
destruct (Hfp u k x' Hkn Hxx' Hwo k ∅ (le_n _)) as [z [Hz1 Hz2]];
first by rewrite right_id.
assert (✓{k} z) by (by revert Hz1; rewrite right_id).
eapply (naught_irrel' _ _ z); eauto using cmra_validN_op_l, cmra_validN_le.
eapply except_0_mono; last (eapply uPred_closed; first eapply Hz2);
eauto using cmra_validN_le.
rewrite -uPred_sep_eq; iIntros "(_ & _ & ?)"; iFrame.
Qed.
Lemma future_S {E} P n : (|≫{E}=[S n]=> P) ⊣⊢ |={E}=> ▷ (|≫{E}=[n]=> P).
Proof. by rewrite !future_eq. Qed.
Lemma future_mono {E} Q P n :
(Q ⊢ P) → (|≫{E}=[n]=> Q) ⊢ (|≫{E}=[n]=> P).
Proof.
revert Q P; induction n => Q P HQP.
- by rewrite !future_unfold_O; apply fupd_mono.
- rewrite !future_S; auto using fupd_mono, later_mono.
Qed.
Lemma future_plain {E} P `{Hpl: !PlainP P} n :
(|≫{E}=[n]=> P) ⊢ |={E}=> Nat.iter n (λ Q, ▷ Q) (◇ P).
Proof.
rewrite future_unfold; destruct n; iIntros "HP".
- by iMod "HP"; iModIntro; iApply except_0_intro.
- iPoseProof (future_plain_base with "HP") as "HP".
iMod "HP"; iModIntro; by iApply later_except_0_n.
Qed.
Lemma future_plain'_base {E} Q P `{Hpl: !PlainP P} n :
(Q ⊢ P) → (|≫{E}=[n]=> Q) ⊢ |={E}=> Nat.iter n (λ Q, ▷ Q) (◇ P).
Proof.
iIntros (HQP) "HQ". iApply future_plain. iApply future_mono; eauto.
Qed.
Lemma future_plain' {E} Q P `{Hpl: !PlainP P} n :
(Q ⊢ P) →
(|≫{E}=[n]=> Q) ⊢ |={E}=> (|≫{E}=[n]=> Q) ★ (Nat.iter n (λ Q, ▷ Q) (◇ P)).
Proof.
intros HQP.
split => k x Hx HQ.
pose proof (HQ) as HP; apply (future_plain'_base _ _ _ HQP) in HP; auto.
revert HP; rewrite fupd_eq /fupd_def; unseal => HP.
intros k' x' Hkk' Hxx' Hwo k'' yf Hk'k'' Hxx'yf.
destruct (HP k' x' Hkk' Hxx' Hwo k'' yf Hk'k'' Hxx'yf) as [u [Hvu Hu]].
rewrite -uPred_sep_eq in Hu.
assert (Hvu' : ✓{k''} u) by eauto using cmra_validN_op_l.
do 2 (apply except_0_sep' in Hu; trivial; apply sep_elim_r in Hu; trivial).
exists (x ⋅ x'); split; trivial.
assert (Hk'xx' : ✓{k''} (x ⋅ x')) by eauto using cmra_validN_le.
rewrite -uPred_sep_eq. rewrite -uPred_sep_eq in Hwo.
eapply except_0_mono; first apply sep_assoc';
last apply except_0_frame_l; trivial.
rewrite {1}uPred_sep_eq; eexists x', x; repeat split; first by rewrite comm.
eapply uPred_closed; eauto using cmra_validN_op_r.
rewrite uPred_sep_eq in Hwo.
apply except_0_frame_l; eauto using cmra_validN_op_l.
rewrite uPred_sep_eq. exists x, (∅ : iResUR Σ); split; first by rewrite right_id.
split; first (eapply uPred_closed; first apply HQ);
try omega; eauto using cmra_validN_op_l.
rewrite -uPred_later_eq; rewrite -uPred_later_eq in Hu.
(eapply (naught_irrel' _ _ _ ∅) in Hu); eauto using ucmra_unit_validN.
Qed.
Lemma later_n_except_0_future {E} P n :
Nat.iter n (λ Q, ▷ Q) (◇ P) ⊢ (|≫{E}=[n]=> P).
Proof.
rewrite future_eq; induction n; simpl.
- by iIntros "HP"; iMod "HP"; iModIntro.
- by iIntros "HP"; iModIntro; iNext; iApply IHn.
Qed.
Lemma future_sep {E} P Q n :
(|≫{E}=[n]=> P) ★ (|≫{E}=[n]=> Q) ⊢ (|≫{E}=[n]=> P ★ Q).
Proof.
rewrite future_eq; induction n; simpl.
- iIntros "[HP HQ]"; iMod "HP"; iMod "HQ"; iModIntro; iFrame.
- iIntros "[HP HQ]";iMod "HP"; iMod "HQ"; iModIntro; iNext; iApply IHn; iFrame.
Qed.
Lemma future_cancel_2 {E} P Q Q' m n :
((|≫{E}=[m - n]=> P) ★ Q ⊢ Q') →
(|≫{E}=[m]=> P) ★ (|≫{E}=[n]=> Q) ⊢ (|≫{E}=[n]=> Q').
Proof.
revert m; induction n => m; simpl.
- replace (m - 0) with m by omega. intros HA.
iIntros "[HP HQ]". rewrite !future_unfold_O.
iMod "HQ"; iModIntro; iApply HA; iFrame.
- destruct m.
+ replace (0 - S n) with (0 - n) by omega. intros HB; specialize (IHn _ HB).
iIntros "[HP HQ]"; rewrite !future_S. iMod "HQ"; iModIntro; iNext.
iApply IHn; iFrame.
+ replace (S m - S n) with (m - n) by omega.
intros HB; specialize (IHn _ HB).
iIntros "[HP HQ]"; rewrite !future_S. iMod "HP"; iMod "HQ"; iModIntro; iNext.
iApply IHn; iFrame.
Qed.
End fupd_and_plain.-
[Cẩm Nang A-Z] Phân Loại Thận Đa Nang Theo Bosniak Mới Nhất
Giai đoạn III tương ứng với các u nang nghi ngờ ác tính. Chúng tôi đã quan sát thấy trong loạt 30% các khối u ác tính trong các u nang giai đoạn III này. Trong tài liệu, tỷ lệ này tăng trung bình lên tới 50% [16, 18, 22] với cực trị lên tới 75% đối với Israel [20]. Tuy nhiên, có những biến thể liên cá nhân trong giải thích X quang là một nguồn của sự phân kỳ stadization, đặc biệt là giữa giai đoạn IIF và III [23]. Những lỗi dàn dựng này có thể giải thích tần suất ung thư trong giai đoạn IIF.
Một u nang giai đoạn IV nên được coi là một khối u ác tính cho đến khi được chứng minh khác đi. Do đó, điều trị của anh là phẫu thuật. Tần suất ung thư được tìm thấy trong u nang giai đoạn IV trong nghiên cứu của chúng tôi là 86%. Những kết quả này phù hợp với những tài liệu [16, 18, 23]. Chỉ có một dương tính giả được tìm thấy trong nghiên cứu của chúng tôi. Đó là một u nang xuất huyết mà sự quản lý của họ có thể được sửa đổi bằng cách thực hiện MRI, nhạy hơn trong chẩn đoán u nang xuất huyết [12].
Việc chọc thủng sinh thiết bao gồm lấy một mảnh của nang thận (vách, vách ngăn, thảm thực vật ...) để phân tích mô học. Tỷ lệ mắc bệnh của thủng là thấp, tuy nhiên, nguy cơ lý thuyết về phổ biến khối u, dưới 0,01% [10]. Âm tính giả về cơ bản được thể hiện bằng những khó khăn trong việc xác định mục tiêu khối u nhỏ như thành mô với vách ngăn cực mỏng. Tuy nhiên, nó có một sự phát triển rộng rãi trong việc phân loại các khối u thận nhỏ phát hiện ngẫu nhiên nhưng có bản chất rắn [4, 5]. Đối với u nang, nó gây tranh cãi cao vì năng suất rất thấp. Harisinghani [24] là một trong số ít trong tài liệu đạt được kết quả tốt cho phép nó chỉ hoạt động trong các u nang ung thư giai đoạn III. Trong nghiên cứu của chúng tôi, 9 chọc thủng sinh thiết đã được thực hiện. Một vết đâm duy nhất cho thấy các tế bào tân sinh trong khi thăm dò phẫu thuật và phân tích mô học tìm thấy sự hiện diện của các tế bào khối u trong tất cả các trường hợp. Trong nghiên cứu của chúng tôi, độ nhạy của chọc thủng sinh thiết là 11%.
Theo kinh nghiệm của chúng tôi, chúng tôi đồng ý với các khuyến nghị của Hiệp hội Tiết niệu Pháp, lưu ý rằng ít quan tâm đến kỹ thuật này trong chẩn đoán u nang không điển hình [4, 5]
Phác Đồ Điều Trị Bệnh Thận Đa Nang Mới Nhất
➽ Cách chữa nang nước ở thận Hiệu Quả Nhất. Xem chi tiết tại: https://trello.com/b/QGoyjp73/y-duoc-xanh-yduocxanhcom
➽ Thuốc điều trị nang thận Mới Nhất. Xem chi tiết tại: https://www.woddal.com/yduocxanh
➽ Nang thận uống thuốc gì cho mau khỏi. Chia sẻ đặc biệt: https://www.trover.com/l/6h2cZ-benh-u-nang-than-don-nang-da-nang
Tác giả: Nhóm Dược Sĩ Lâm sàng Y Dược Xanh
Please register or sign in to comment