derived.v 4.37 KB
Newer Older
1
From iris.bi Require Export bi.
2
From iris.base_logic Require Export bi.
3
Set Default Proof Using "Type".
4
Import bi.bi base_logic.bi.uPred.
5

6 7
(** Derived laws for Iris-specific primitive connectives (own, valid).
    This file does NOT unseal! *)
8

9
Module uPred.
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's avatar
Robbert Krebbers committed
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).
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 *)
34
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :  a  <pers> ( a : uPred M).
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.
37
Proof.
38 39
  rewrite /bi_intuitionistically affine_affinely=>?; apply (anti_symm _);
    [by rewrite persistently_elim|].
40
  by rewrite {1}persistently_ownM_core core_id_core.
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's avatar
Robbert Krebbers committed
45
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
Lemma ownM_unit' : uPred_ownM ε  True.
47
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
51
Proof.
52 53
  rewrite /bi_intuitionistically affine_affinely. intros; apply (anti_symm _);
    first by rewrite persistently_elim.
54
  apply:persistently_cmra_valid_1.
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.

62
(** Timeless instances *)
63
Global Instance valid_timeless {A : cmraT} `{!CmraDiscrete A} (a : A) :
64
  Timeless ( a : uPred M)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
65
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
66
Global Instance ownM_timeless (a : M) : Discrete a  Timeless (uPred_ownM a).
67
Proof.
68
  intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
Robbert Krebbers's avatar
Robbert Krebbers committed
69
  rewrite (timeless (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
70
  apply except_0_mono. rewrite internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
71 72
  apply (internal_eq_rewrite' b a (uPred_ownM) _);
    auto using and_elim_l, and_elim_r.
73 74
Qed.

75
(** Plainness *)
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.
79

80
(** Persistence *)
81
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
82
  Persistent ( a : uPred M)%I.
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.
88

89
(** For big ops *)
90
Global Instance uPred_ownM_sep_homomorphism :
91
  MonoidHomomorphism op uPred_sep () (@uPred_ownM M).
Robbert Krebbers's avatar
Robbert Krebbers committed
92
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
93 94

(** Consistency/soundness statement *)
Ralf Jung's avatar
Ralf Jung committed
95
Lemma bupd_plain_soundness P `{!Plain P} : bi_emp_valid (|==> P)  bi_emp_valid P.
96 97 98 99 100
Proof.
  eapply bi_emp_valid_mono. etrans; last exact: bupd_plainly. apply bupd_mono'.
  apply: plain.
Qed.

101 102 103
Corollary soundness φ n : (^n  φ  : uPred M)%I  φ.
Proof.
  induction n as [|n IH]=> /=.
Ralf Jung's avatar
Ralf Jung committed
104 105
  - apply pure_soundness.
  - intros H. by apply IH, later_soundness.
106
Qed.
107

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.
113
End derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
114

115
End uPred.