derived.v 3.32 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
From iris.base_logic Require Export upred.
2
From iris.bi Require Export derived_laws.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4
Import upred.uPred.
5
Import interface.bi derived_laws.bi.
6

7
Module uPred.
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's avatar
Robbert Krebbers committed
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).
17 18

(* Own and valid derived *)
19 20 21
Lemma persistently_cmra_valid_1 {A : cmraT} (a : A) :
   a  bi_persistently ( a : uPred M).
Proof. by rewrite {1}plainly_cmra_valid_1 plainly_elim_persistently. Qed.
22
Lemma affinely_persistently_ownM (a : M) : CoreId a   uPred_ownM a  uPred_ownM a.
23
Proof.
24
  rewrite affine_affinely=>?; apply (anti_symm _); [by rewrite persistently_elim|].
25
  by rewrite {1}persistently_ownM_core core_id_core.
26 27 28 29
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
30
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
Lemma ownM_unit' : uPred_ownM ε  True.
32
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_unit. Qed.
33 34 35 36 37
Lemma affinely_plainly_cmra_valid {A : cmraT} (a : A) :   a   a.
Proof.
  rewrite affine_affinely.
  apply (anti_symm _), plainly_cmra_valid_1. apply plainly_elim, _.
Qed.
38
Lemma affinely_persistently_cmra_valid {A : cmraT} (a : A) :   a   a.
39
Proof.
40
  rewrite affine_affinely. intros; apply (anti_symm _); first by rewrite persistently_elim.
41
  apply:persistently_cmra_valid_1.
42 43 44 45 46 47 48
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's avatar
Robbert Krebbers committed
49
(* Timeless instances *)
50
Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
51
  Timeless ( a : uPred M)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
53
Global Instance ownM_timeless (a : M) : Discrete a  Timeless (uPred_ownM a).
54
Proof.
55
  intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
  rewrite (timeless (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
57
  apply except_0_mono. rewrite internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
58 59
  apply (internal_eq_rewrite' b a (uPred_ownM) _);
    auto using and_elim_l, and_elim_r.
60 61
Qed.

62 63 64 65
(* Plainness *)
Global Instance cmra_valid_plain {A : cmraT} (a : A) :
  Plain ( a : uPred M)%I.
Proof. rewrite /Persistent. apply plainly_cmra_valid_1. Qed.
66

67 68
(* Persistence *)
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
69
  Persistent ( a : uPred M)%I.
70 71 72 73 74
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.
75 76 77

(* For big ops *)
Global Instance uPred_ownM_sep_homomorphism :
78
  MonoidHomomorphism op uPred_sep () (@uPred_ownM M).
Robbert Krebbers's avatar
Robbert Krebbers committed
79
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
80
End derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
81 82

(* Also add this to the global hint database, otherwise [eauto] won't work for
83
many lemmas that have [BiAffine] as a premise. *)
Robbert Krebbers's avatar
Robbert Krebbers committed
84
Hint Immediate uPred_affine.
85
End uPred.