derived.v 4.62 KB
 Robbert Krebbers committed Oct 30, 2017 1 2 ``````From iris.base_logic Require Export upred. From iris.bi Require Export interface derived. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type". `````` Robbert Krebbers committed Oct 30, 2017 4 5 ``````Import upred.uPred. Import interface.bi derived.bi. `````` Robbert Krebbers committed Oct 25, 2016 6 `````` `````` Robbert Krebbers committed Dec 13, 2016 7 ``````Module uPred. `````` Robbert Krebbers committed Oct 25, 2016 8 9 10 11 12 13 ``````Section derived. Context {M : ucmraT}. Implicit Types φ : Prop. Implicit Types P Q : uPred M. Implicit Types A : Type. `````` Robbert Krebbers committed Oct 30, 2017 14 15 16 ``````(* Force implicit argument M *) Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I). Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I). `````` Robbert Krebbers committed Oct 25, 2016 17 `````` `````` Robbert Krebbers committed Oct 30, 2017 18 19 20 ``````(* Limits *) Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A → uPred M) : NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊢ Ψ x). `````` Robbert Krebbers committed Oct 25, 2016 21 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 22 23 24 `````` intros HΦ HΨ c Hc. etrans; [apply equiv_spec, compl_chain_map|]. etrans; [|apply equiv_spec, symmetry, compl_chain_map]. by apply entails_lim. `````` Robbert Krebbers committed Oct 25, 2016 25 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 26 27 ``````Lemma limit_preserving_equiv {A : ofeT} `{Cofe A} (Φ Ψ : A → uPred M) : NonExpansive Φ → NonExpansive Ψ → LimitPreserving (λ x, Φ x ⊣⊢ Ψ x). `````` Robbert Krebbers committed Oct 25, 2016 28 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 29 30 31 `````` intros HΦ HΨ. eapply limit_preserving_ext. { intros x. symmetry; apply equiv_spec. } apply limit_preserving_and; by apply limit_preserving_entails. `````` Robbert Krebbers committed Oct 25, 2016 32 33 ``````Qed. `````` Robbert Krebbers committed Oct 30, 2017 34 35 36 ``````(* Affine *) Global Instance uPred_affine : AffineBI (uPredI M) | 0. Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed. `````` Robbert Krebbers committed Oct 25, 2016 37 38 `````` (* Own and valid derived *) `````` Robbert Krebbers committed Oct 25, 2017 39 ``````Lemma persistently_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a. `````` Robbert Krebbers committed Oct 25, 2016 40 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 41 42 `````` intros; apply (anti_symm _); first by apply: persistently_elim_absorbing. by rewrite {1}persistently_ownM_core core_id_core. `````` Robbert Krebbers committed Oct 25, 2016 43 44 45 46 ``````Qed. Lemma ownM_invalid (a : M) : ¬ ✓{0} a → uPred_ownM a ⊢ False. Proof. by intros; rewrite ownM_valid cmra_valid_elim. Qed. Global Instance ownM_mono : Proper (flip (≼) ==> (⊢)) (@uPred_ownM M). `````` Robbert Krebbers committed Oct 30, 2017 47 ``````Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed. `````` Robbert Krebbers committed Sep 17, 2017 48 ``````Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True. `````` Robbert Krebbers committed Oct 30, 2017 49 ``````Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed. `````` Robbert Krebbers committed Oct 25, 2017 50 ``````Lemma persistently_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a. `````` Robbert Krebbers committed Oct 25, 2016 51 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 52 `````` intros; apply (anti_symm _); first by apply: persistently_elim_absorbing. `````` Robbert Krebbers committed Oct 25, 2017 53 `````` apply:persistently_cmra_valid_1. `````` Robbert Krebbers committed Oct 25, 2016 54 55 56 57 58 59 60 ``````Qed. (** * Derived rules *) Global Instance bupd_mono' : Proper ((⊢) ==> (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. Global Instance bupd_flip_mono' : Proper (flip (⊢) ==> flip (⊢)) (@uPred_bupd M). Proof. intros P Q; apply bupd_mono. Qed. `````` Robbert Krebbers committed Nov 03, 2016 61 ``````Lemma bupd_frame_l R Q : (R ∗ |==> Q) ==∗ R ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 62 ``````Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 63 ``````Lemma bupd_wand_l P Q : (P -∗ Q) ∗ (|==> P) ==∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 64 ``````Proof. by rewrite bupd_frame_l wand_elim_l. Qed. `````` Robbert Krebbers committed Nov 03, 2016 65 ``````Lemma bupd_wand_r P Q : (|==> P) ∗ (P -∗ Q) ==∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 66 ``````Proof. by rewrite bupd_frame_r wand_elim_r. Qed. `````` Robbert Krebbers committed Nov 03, 2016 67 ``````Lemma bupd_sep P Q : (|==> P) ∗ (|==> Q) ==∗ P ∗ Q. `````` Robbert Krebbers committed Oct 25, 2016 68 69 70 71 72 73 ``````Proof. by rewrite bupd_frame_r bupd_frame_l bupd_trans. Qed. Lemma bupd_ownM_update x y : x ~~> y → uPred_ownM x ⊢ |==> uPred_ownM y. Proof. intros; rewrite (bupd_ownM_updateP _ (y =)); last by apply cmra_update_updateP. by apply bupd_mono, exist_elim=> y'; apply pure_elim_l=> ->. Qed. `````` Robbert Krebbers committed Oct 25, 2016 74 ``````Lemma except_0_bupd P : ◇ (|==> P) ⊢ (|==> ◇ P). `````` Robbert Krebbers committed Oct 25, 2016 75 ``````Proof. `````` Robbert Krebbers committed Oct 30, 2017 76 `````` rewrite /bi_except_0. apply or_elim; auto using bupd_mono, or_intro_r. `````` Robbert Krebbers committed Oct 25, 2016 77 78 79 `````` by rewrite -bupd_intro -or_intro_l. Qed. `````` Robbert Krebbers committed Oct 30, 2017 80 ``````(* Timeless instances *) `````` Robbert Krebbers committed Oct 25, 2017 81 ``````Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) : `````` Robbert Krebbers committed Oct 25, 2017 82 `````` Timeless (✓ a : uPred M)%I. `````` Robbert Krebbers committed Oct 30, 2017 83 ``````Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed. `````` Robbert Krebbers committed Oct 25, 2017 84 ``````Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a). `````` Robbert Krebbers committed Oct 25, 2016 85 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2017 86 `````` intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b. `````` Robbert Krebbers committed Oct 30, 2017 87 `````` rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and. `````` Robbert Krebbers committed Oct 25, 2016 88 `````` apply except_0_mono. rewrite internal_eq_sym. `````` Robbert Krebbers committed Oct 30, 2017 89 90 `````` apply (internal_eq_rewrite' b a (uPred_ownM) _); auto using and_elim_l, and_elim_r. `````` Robbert Krebbers committed Oct 25, 2016 91 92 ``````Qed. `````` Robbert Krebbers committed Jan 22, 2017 93 ``````(* Derived lemmas for persistence *) `````` Robbert Krebbers committed Oct 25, 2017 94 95 ``````Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A → uPred M) : NonExpansive Φ → LimitPreserving (λ x, Persistent (Φ x)). `````` Robbert Krebbers committed Oct 30, 2017 96 ``````Proof. intros. apply limit_preserving_equiv; solve_proper. Qed. `````` Robbert Krebbers committed Jan 22, 2017 97 `````` `````` Robbert Krebbers committed Oct 25, 2016 98 99 ``````(* Persistence *) Global Instance cmra_valid_persistent {A : cmraT} (a : A) : `````` Robbert Krebbers committed Oct 25, 2017 100 `````` Persistent (✓ a : uPred M)%I. `````` Robbert Krebbers committed Oct 25, 2017 101 ``````Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed. `````` Robbert Krebbers committed Oct 25, 2017 102 ``````Global Instance ownM_persistent : CoreId a → Persistent (@uPred_ownM M a). `````` Robbert Krebbers committed Oct 25, 2017 103 ``````Proof. intros. by rewrite /Persistent persistently_ownM. Qed. `````` Robbert Krebbers committed Mar 24, 2017 104 105 106 `````` (* For big ops *) Global Instance uPred_ownM_sep_homomorphism : `````` Robbert Krebbers committed Aug 17, 2017 107 `````` MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M). `````` Robbert Krebbers committed Sep 17, 2017 108 ``````Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed. `````` Robbert Krebbers committed Oct 25, 2016 109 ``````End derived. `````` Robbert Krebbers committed Oct 30, 2017 110 111 112 113 `````` (* Also add this to the global hint database, otherwise [eauto] won't work for many lemmas that have [AffineBI] as a premise. *) Hint Immediate uPred_affine. `````` Robbert Krebbers committed Dec 13, 2016 114 ``End uPred.``