functions.v 7.31 KB
Newer Older
1
From stdpp Require Import finite.
2 3 4 5
From iris.algebra Require Export cmra.
From iris.algebra Require Import updates.
Set Default Proof Using "Type".

6 7
Definition discrete_fun_insert `{EqDecision A} {B : A  ofeT}
    (x : A) (y : B x) (f : discrete_fun B) : discrete_fun B := λ x',
8
  match decide (x = x') with left H => eq_rect _ B y _ H | right _ => f x' end.
9
Instance: Params (@discrete_fun_insert) 5 := {}.
10

11 12 13
Definition discrete_fun_singleton `{EqDecision A} {B : A  ucmraT}
  (x : A) (y : B x) : discrete_fun B := discrete_fun_insert x y ε.
Instance: Params (@discrete_fun_singleton) 5 := {}.
14 15 16 17

Section ofe.
  Context `{Heqdec : EqDecision A} {B : A  ofeT}.
  Implicit Types x : A.
18
  Implicit Types f g : discrete_fun B.
19

20 21
  Global Instance discrete_funO_ofe_discrete :
    ( i, OfeDiscrete (B i))  OfeDiscrete (discrete_funO B).
22 23
  Proof. intros HB f f' Heq i. apply HB, Heq. Qed.

24 25 26
  (** Properties of discrete_fun_insert. *)
  Global Instance discrete_fun_insert_ne x :
    NonExpansive2 (discrete_fun_insert (B:=B) x).
27
  Proof.
28
    intros n y1 y2 ? f1 f2 ? x'; rewrite /discrete_fun_insert.
29 30
    by destruct (decide _) as [[]|].
  Qed.
31 32
  Global Instance discrete_fun_insert_proper x :
    Proper (() ==> () ==> ()) (discrete_fun_insert (B:=B) x) := ne_proper_2 _.
33

34
  Lemma discrete_fun_lookup_insert f x y : (discrete_fun_insert x y f) x = y.
35
  Proof.
36
    rewrite /discrete_fun_insert; destruct (decide _) as [Hx|]; last done.
37 38
    by rewrite (proof_irrel Hx eq_refl).
  Qed.
39 40 41
  Lemma discrete_fun_lookup_insert_ne f x x' y :
    x  x'  (discrete_fun_insert x y f) x' = f x'.
  Proof. by rewrite /discrete_fun_insert; destruct (decide _). Qed.
42

43 44
  Global Instance discrete_fun_insert_discrete f x y :
    Discrete f  Discrete y  Discrete (discrete_fun_insert x y f).
45 46
  Proof.
    intros ?? g Heq x'; destruct (decide (x = x')) as [->|].
47 48 49 50
    - rewrite discrete_fun_lookup_insert.
      apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert.
    - rewrite discrete_fun_lookup_insert_ne //.
      apply: discrete. by rewrite -(Heq x') discrete_fun_lookup_insert_ne.
51 52 53 54
  Qed.
End ofe.

Section cmra.
55
  Context `{EqDecision A} {B : A  ucmraT}.
56
  Implicit Types x : A.
57
  Implicit Types f g : discrete_fun B.
58

59 60
  Global Instance discrete_funR_cmra_discrete:
    ( i, CmraDiscrete (B i))  CmraDiscrete (discrete_funR B).
61 62
  Proof. intros HB. split; [apply _|]. intros x Hv i. apply HB, Hv. Qed.

63 64 65 66 67
  Global Instance discrete_fun_singleton_ne x :
    NonExpansive (discrete_fun_singleton x : B x  _).
  Proof. intros n y1 y2 ?; apply discrete_fun_insert_ne. done. by apply equiv_dist. Qed.
  Global Instance discrete_fun_singleton_proper x :
    Proper (() ==> ()) (discrete_fun_singleton x) := ne_proper _.
68

69 70 71 72 73
  Lemma discrete_fun_lookup_singleton x (y : B x) : (discrete_fun_singleton x y) x = y.
  Proof. by rewrite /discrete_fun_singleton discrete_fun_lookup_insert. Qed.
  Lemma discrete_fun_lookup_singleton_ne x x' (y : B x) :
    x  x'  (discrete_fun_singleton x y) x' = ε.
  Proof. intros; by rewrite /discrete_fun_singleton discrete_fun_lookup_insert_ne. Qed.
74

75 76
  Global Instance discrete_fun_singleton_discrete x (y : B x) :
    ( i, Discrete (ε : B i))   Discrete y  Discrete (discrete_fun_singleton x y).
77 78
  Proof. apply _. Qed.

79
  Lemma discrete_fun_singleton_validN n x (y : B x) : {n} discrete_fun_singleton x y  {n} y.
80
  Proof.
81
    split; [by move=>/(_ x); rewrite discrete_fun_lookup_singleton|].
82
    move=>Hx x'; destruct (decide (x = x')) as [->|];
83
      rewrite ?discrete_fun_lookup_singleton ?discrete_fun_lookup_singleton_ne //.
84 85 86
    by apply ucmra_unit_validN.
  Qed.

87 88
  Lemma discrete_fun_core_singleton x (y : B x) :
    core (discrete_fun_singleton x y)  discrete_fun_singleton x (core y).
89 90
  Proof.
    move=>x'; destruct (decide (x = x')) as [->|];
91 92
      by rewrite discrete_fun_lookup_core ?discrete_fun_lookup_singleton
      ?discrete_fun_lookup_singleton_ne // (core_id_core ).
93 94
  Qed.

95 96 97
  Global Instance discrete_fun_singleton_core_id x (y : B x) :
    CoreId y  CoreId (discrete_fun_singleton x y).
  Proof. by rewrite !core_id_total discrete_fun_core_singleton=> ->. Qed.
98

99 100
  Lemma discrete_fun_op_singleton (x : A) (y1 y2 : B x) :
    discrete_fun_singleton x y1  discrete_fun_singleton x y2  discrete_fun_singleton x (y1  y2).
101 102
  Proof.
    intros x'; destruct (decide (x' = x)) as [->|].
103 104
    - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton.
    - by rewrite discrete_fun_lookup_op !discrete_fun_lookup_singleton_ne // left_id.
105 106
  Qed.

107 108 109
  Lemma discrete_fun_insert_updateP x (P : B x  Prop) (Q : discrete_fun B  Prop) g y1 :
    y1 ~~>: P  ( y2, P y2  Q (discrete_fun_insert x y2 g)) 
    discrete_fun_insert x y1 g ~~>: Q.
110 111 112
  Proof.
    intros Hy1 HP; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hy1 n (Some (gf x))) as (y2&?&?).
113 114
    { move: (Hg x). by rewrite discrete_fun_lookup_op discrete_fun_lookup_insert. }
    exists (discrete_fun_insert x y2 g); split; [auto|].
115
    intros x'; destruct (decide (x' = x)) as [->|];
116 117
      rewrite discrete_fun_lookup_op ?discrete_fun_lookup_insert //; [].
    move: (Hg x'). by rewrite discrete_fun_lookup_op !discrete_fun_lookup_insert_ne.
118 119
  Qed.

120
  Lemma discrete_fun_insert_updateP' x (P : B x  Prop) g y1 :
121
    y1 ~~>: P 
122 123 124 125
    discrete_fun_insert x y1 g ~~>: λ g',  y2, g' = discrete_fun_insert x y2 g  P y2.
  Proof. eauto using discrete_fun_insert_updateP. Qed.
  Lemma discrete_fun_insert_update g x y1 y2 :
    y1 ~~> y2  discrete_fun_insert x y1 g ~~> discrete_fun_insert x y2 g.
126
  Proof.
127
    rewrite !cmra_update_updateP; eauto using discrete_fun_insert_updateP with subst.
128 129
  Qed.

130 131 132 133 134
  Lemma discrete_fun_singleton_updateP x (P : B x  Prop) (Q : discrete_fun B  Prop) y1 :
    y1 ~~>: P  ( y2, P y2  Q (discrete_fun_singleton x y2)) 
    discrete_fun_singleton x y1 ~~>: Q.
  Proof. rewrite /discrete_fun_singleton; eauto using discrete_fun_insert_updateP. Qed.
  Lemma discrete_fun_singleton_updateP' x (P : B x  Prop) y1 :
135
    y1 ~~>: P 
136 137 138 139 140 141 142 143
    discrete_fun_singleton x y1 ~~>: λ g,  y2, g = discrete_fun_singleton x y2  P y2.
  Proof. eauto using discrete_fun_singleton_updateP. Qed.
  Lemma discrete_fun_singleton_update x (y1 y2 : B x) :
    y1 ~~> y2  discrete_fun_singleton x y1 ~~> discrete_fun_singleton x y2.
  Proof. eauto using discrete_fun_insert_update. Qed.

  Lemma discrete_fun_singleton_updateP_empty x (P : B x  Prop) (Q : discrete_fun B  Prop) :
    ε ~~>: P  ( y2, P y2  Q (discrete_fun_singleton x y2))  ε ~~>: Q.
144 145 146
  Proof.
    intros Hx HQ; apply cmra_total_updateP.
    intros n gf Hg. destruct (Hx n (Some (gf x))) as (y2&?&?); first apply Hg.
147
    exists (discrete_fun_singleton x y2); split; [by apply HQ|].
148
    intros x'; destruct (decide (x' = x)) as [->|].
149 150
    - by rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton.
    - rewrite discrete_fun_lookup_op discrete_fun_lookup_singleton_ne //. apply Hg.
151
  Qed.
152 153 154 155 156
  Lemma discrete_fun_singleton_updateP_empty' x (P : B x  Prop) :
    ε ~~>: P  ε ~~>: λ g,  y2, g = discrete_fun_singleton x y2  P y2.
  Proof. eauto using discrete_fun_singleton_updateP_empty. Qed.
  Lemma discrete_fun_singleton_update_empty x (y : B x) :
    ε ~~> y  ε ~~> discrete_fun_singleton x y.
157 158
  Proof.
    rewrite !cmra_update_updateP;
159
      eauto using discrete_fun_singleton_updateP_empty with subst.
160 161
  Qed.
End cmra.