derived.v 4.62 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1 2
From iris.base_logic Require Export upred.
From iris.bi Require Export interface derived.
3
Set Default Proof Using "Type".
Robbert Krebbers's avatar
Robbert Krebbers committed
4 5
Import upred.uPred.
Import interface.bi derived.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

Robbert Krebbers's avatar
Robbert Krebbers committed
18 19 20
(* Limits *)
Lemma limit_preserving_entails {A : ofeT} `{Cofe A} (Φ Ψ : A  uPred M) :
  NonExpansive Φ  NonExpansive Ψ  LimitPreserving (λ x, Φ x  Ψ x).
21
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
25
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
26 27
Lemma limit_preserving_equiv {A : ofeT} `{Cofe A} (Φ Ψ : A  uPred M) :
  NonExpansive Φ  NonExpansive Ψ  LimitPreserving (λ x, Φ x  Ψ x).
28
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
32 33
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
34 35 36
(* Affine *)
Global Instance uPred_affine : AffineBI (uPredI M) | 0.
Proof. intros P. rewrite /Affine. by apply bi.pure_intro. Qed.
37 38

(* Own and valid derived *)
39
Lemma persistently_ownM (a : M) : CoreId a   uPred_ownM a  uPred_ownM a.
40
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
41 42
  intros; apply (anti_symm _); first by apply: persistently_elim_absorbing.
    by rewrite {1}persistently_ownM_core core_id_core.
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's avatar
Robbert Krebbers committed
47
Proof. intros a b [b' ->]. by rewrite ownM_op sep_elim_l. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Lemma ownM_unit' : uPred_ownM ε  True.
Robbert Krebbers's avatar
Robbert Krebbers committed
49
Proof. apply (anti_symm _); first by apply pure_intro. apply ownM_empty. Qed.
50
Lemma persistently_cmra_valid {A : cmraT} (a : A) :   a   a.
51
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
52
  intros; apply (anti_symm _); first by apply: persistently_elim_absorbing.
53
  apply:persistently_cmra_valid_1.
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.
61
Lemma bupd_frame_l R Q : (R  |==> Q) == R  Q.
62
Proof. rewrite !(comm _ R); apply bupd_frame_r. Qed.
63
Lemma bupd_wand_l P Q : (P - Q)  (|==> P) == Q.
64
Proof. by rewrite bupd_frame_l wand_elim_l. Qed.
65
Lemma bupd_wand_r P Q : (|==> P)  (P - Q) == Q.
66
Proof. by rewrite bupd_frame_r wand_elim_r. Qed.
67
Lemma bupd_sep P Q : (|==> P)  (|==> Q) == P  Q.
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.
74
Lemma except_0_bupd P :  (|==> P)  (|==>  P).
75
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
76
  rewrite /bi_except_0. apply or_elim; auto using bupd_mono, or_intro_r.
77 78 79
  by rewrite -bupd_intro -or_intro_l.
Qed.

Robbert Krebbers's avatar
Robbert Krebbers committed
80
(* Timeless instances *)
81
Global Instance valid_timeless {A : cmraT} `{CmraDiscrete A} (a : A) :
82
  Timeless ( a : uPred M)%I.
Robbert Krebbers's avatar
Robbert Krebbers committed
83
Proof. rewrite /Timeless !discrete_valid. apply (timeless _). Qed.
84
Global Instance ownM_timeless (a : M) : Discrete a  Timeless (uPred_ownM a).
85
Proof.
86
  intros ?. rewrite /Timeless later_ownM. apply exist_elim=> b.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
  rewrite (timeless (ab)) (except_0_intro (uPred_ownM b)) -except_0_and.
88
  apply except_0_mono. rewrite internal_eq_sym.
Robbert Krebbers's avatar
Robbert Krebbers committed
89 90
  apply (internal_eq_rewrite' b a (uPred_ownM) _);
    auto using and_elim_l, and_elim_r.
91 92
Qed.

93
(* Derived lemmas for persistence *)
94 95
Global Instance limit_preserving_Persistent {A:ofeT} `{Cofe A} (Φ : A  uPred M) :
  NonExpansive Φ  LimitPreserving (λ x, Persistent (Φ x)).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
Proof. intros. apply limit_preserving_equiv; solve_proper. Qed.
97

98 99
(* Persistence *)
Global Instance cmra_valid_persistent {A : cmraT} (a : A) :
100
  Persistent ( a : uPred M)%I.
101
Proof. by intros; rewrite /Persistent persistently_cmra_valid. Qed.
102
Global Instance ownM_persistent : CoreId a  Persistent (@uPred_ownM M a).
103
Proof. intros. by rewrite /Persistent persistently_ownM. Qed.
104 105 106

(* For big ops *)
Global Instance uPred_ownM_sep_homomorphism :
107
  MonoidHomomorphism op uPred_sep () (@uPred_ownM M).
Robbert Krebbers's avatar
Robbert Krebbers committed
108
Proof. split; [split; try apply _|]. apply ownM_op. apply ownM_unit'. Qed.
109
End derived.
Robbert Krebbers's avatar
Robbert Krebbers committed
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.
114
End uPred.