derived.v 4.37 KB
 1 ``````From iris.base_logic Require Export bi. `````` Ralf Jung committed Mar 21, 2018 2 ``````From iris.bi Require Export bi. `````` Ralf Jung committed Jan 05, 2017 3 ``````Set Default Proof Using "Type". `````` Ralf Jung committed Jun 05, 2018 4 ``````Import bi base_logic.bi.uPred. `````` Robbert Krebbers committed Oct 25, 2016 5 `````` `````` Ralf Jung committed Jun 05, 2018 6 7 ``````(** Derived laws for Iris-specific primitive connectives (own, valid). This file does NOT unseal! *) `````` 8 `````` `````` Ralf Jung committed Jun 05, 2018 9 ``````Module uPred. `````` Robbert Krebbers committed Oct 25, 2016 10 11 12 13 14 15 ``````Section derived. Context {M : ucmraT}. Implicit Types φ : Prop. Implicit Types P Q : uPred M. Implicit Types A : Type. `````` Robbert Krebbers committed Oct 30, 2017 16 17 18 ``````(* 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 19 `````` `````` 20 21 22 23 24 25 26 27 28 29 30 31 32 33 ``````(** Propers *) Global Instance uPred_valid_proper : Proper ((⊣⊢) ==> iff) (@uPred_valid M). Proof. solve_proper. Qed. Global Instance uPred_valid_mono : Proper ((⊢) ==> impl) (@uPred_valid M). Proof. solve_proper. Qed. Global Instance uPred_valid_flip_mono : Proper (flip (⊢) ==> flip impl) (@uPred_valid M). Proof. solve_proper. Qed. Global Instance ownM_proper: Proper ((≡) ==> (⊣⊢)) (@uPred_ownM M) := ne_proper _. Global Instance cmra_valid_proper {A : cmraT} : Proper ((≡) ==> (⊣⊢)) (@uPred_cmra_valid M A) := ne_proper _. (** Own and valid derived *) `````` Robbert Krebbers committed Mar 04, 2018 34 ``````Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) : ✓ a ⊢ (✓ a : uPred M). `````` Jacques-Henri Jourdan committed Nov 03, 2017 35 ``````Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed. `````` 36 ``````Lemma intuitionistically_ownM (a : M) : CoreId a → □ uPred_ownM a ⊣⊢ uPred_ownM a. `````` Robbert Krebbers committed Oct 25, 2016 37 ``````Proof. `````` 38 39 `````` rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|]. `````` Robbert Krebbers committed Oct 30, 2017 40 `````` by rewrite {1}persistently_ownM_core core_id_core. `````` Robbert Krebbers committed Oct 25, 2016 41 42 43 44 ``````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 45 ``````Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed. `````` Robbert Krebbers committed Sep 17, 2017 46 ``````Lemma ownM_unit' : uPred_ownM ε ⊣⊢ True. `````` Robbert Krebbers committed Dec 02, 2017 47 ``````Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed. `````` Robbert Krebbers committed Mar 03, 2018 48 49 ``````Lemma plainly_cmra_valid {A : cmraT} (a : A) : ■ ✓ a ⊣⊢ ✓ a. Proof. apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _. Qed. `````` 50 ``````Lemma intuitionistically_cmra_valid {A : cmraT} (a : A) : □ ✓ a ⊣⊢ ✓ a. `````` Robbert Krebbers committed Oct 25, 2016 51 ``````Proof. `````` 52 53 `````` rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim. `````` Robbert Krebbers committed Oct 25, 2017 54 `````` apply:persistently_cmra_valid_1. `````` Robbert Krebbers committed Oct 25, 2016 55 56 57 58 59 60 61 ``````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. `````` Ralf Jung committed Jun 05, 2018 62 ``````(** Timeless instances *) `````` Ralf Jung committed Mar 05, 2019 63 ``````Global Instance valid_timeless {A : cmraT} `{!CmraDiscrete A} (a : A) : `````` Robbert Krebbers committed Oct 25, 2017 64 `````` Timeless (✓ a : uPred M)%I. `````` Robbert Krebbers committed Oct 30, 2017 65 ``````Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed. `````` Robbert Krebbers committed Oct 25, 2017 66 ``````Global Instance ownM_timeless (a : M) : Discrete a → Timeless (uPred_ownM a). `````` Robbert Krebbers committed Oct 25, 2016 67 ``````Proof. `````` Robbert Krebbers committed Oct 25, 2017 68 `````` intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b. `````` Robbert Krebbers committed Oct 30, 2017 69 `````` rewrite (timeless (a≡b)) (except_0_intro (uPred_ownM b)) -except_0_and. `````` Robbert Krebbers committed Oct 25, 2016 70 `````` apply except_0_mono. rewrite internal_eq_sym. `````` Robbert Krebbers committed Oct 30, 2017 71 72 `````` apply (internal_eq_rewrite' b a (uPred_ownM) _); auto using and_elim_l, and_elim_r. `````` Robbert Krebbers committed Oct 25, 2016 73 74 ``````Qed. `````` Ralf Jung committed Jun 05, 2018 75 ``````(** Plainness *) `````` Jacques-Henri Jourdan committed Nov 03, 2017 76 77 78 ``````Global Instance cmra_valid_plain {A : cmraT} (a : A) : Plain (✓ a : uPred M)%I. Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed. `````` Amin Timany committed Oct 26, 2017 79 `````` `````` Ralf Jung committed Jun 05, 2018 80 ``````(** Persistence *) `````` Robbert Krebbers committed Oct 25, 2016 81 ``````Global Instance cmra_valid_persistent {A : cmraT} (a : A) : `````` Robbert Krebbers committed Oct 25, 2017 82 `````` Persistent (✓ a : uPred M)%I. `````` Jacques-Henri Jourdan committed Nov 02, 2017 83 84 85 86 87 ``````Proof. rewrite /Persistent. apply persistently_cmra_valid_1. Qed. Global Instance ownM_persistent a : CoreId a → Persistent (@uPred_ownM M a). Proof. intros. rewrite /Persistent -{2}(core_id_core a). apply persistently_ownM_core. Qed. `````` Robbert Krebbers committed Mar 24, 2017 88 `````` `````` Ralf Jung committed Jun 05, 2018 89 ``````(** For big ops *) `````` Robbert Krebbers committed Mar 24, 2017 90 ``````Global Instance uPred_ownM_sep_homomorphism : `````` Robbert Krebbers committed Aug 17, 2017 91 `````` MonoidHomomorphism op uPred_sep (≡) (@uPred_ownM M). `````` Robbert Krebbers committed Sep 17, 2017 92 ``````Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed. `````` Ralf Jung committed Jun 05, 2018 93 94 `````` (** Consistency/soundness statement *) `````` Ralf Jung committed Mar 29, 2019 95 96 97 98 99 100 ``````Lemma soundness_bupd_plain P `{!Plain P} : bi_emp_valid (|==> P) → bi_emp_valid P. Proof. eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'. apply: plain. Qed. `````` Robbert Krebbers committed Mar 29, 2019 101 102 103 104 105 106 ``````Corollary soundness φ n : (▷^n ⌜ φ ⌝ : uPred M)%I → φ. Proof. induction n as [|n IH]=> /=. - apply soundness_pure. - intros H. by apply IH, soundness_later. Qed. `````` Ralf Jung committed Jul 04, 2018 107 `````` `````` Ralf Jung committed Jun 05, 2018 108 109 110 111 112 ``````Corollary consistency_modal n : ¬ (▷^n False : uPred M)%I. Proof. exact (soundness False n). Qed. Corollary consistency : ¬(False : uPred M)%I. Proof. exact (consistency_modal 0). Qed. `````` Robbert Krebbers committed Oct 25, 2016 113 ``````End derived. `````` Robbert Krebbers committed Oct 30, 2017 114 `````` `````` Robbert Krebbers committed Dec 13, 2016 115 ``End uPred.``