agree.v 6.86 KB
Newer Older
1
Require Export iris.cmra.
Robbert Krebbers's avatar
Robbert Krebbers committed
2
3
4
5
6
7
Local Hint Extern 10 (_  _) => omega.

Record agree A `{Dist A} := Agree {
  agree_car :> nat  A;
  agree_is_valid : nat  Prop;
  agree_valid_0 : agree_is_valid 0;
Robbert Krebbers's avatar
Robbert Krebbers committed
8
  agree_valid_S n : agree_is_valid (S n)  agree_is_valid n
Robbert Krebbers's avatar
Robbert Krebbers committed
9
}.
Robbert Krebbers's avatar
Robbert Krebbers committed
10
Arguments Agree {_ _} _ _ _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
11
12
13
14
15
16
Arguments agree_car {_ _} _ _.
Arguments agree_is_valid {_ _} _ _.

Section agree.
Context `{Cofe A}.

Robbert Krebbers's avatar
Robbert Krebbers committed
17
18
19
20
21
Global Instance agree_validN : ValidN (agree A) := λ n x,
  agree_is_valid x n   n', n'  n  x n' ={n'}= x n.
Lemma agree_valid_le (x : agree A) n n' :
  agree_is_valid x n  n'  n  agree_is_valid x n'.
Proof. induction 2; eauto using agree_valid_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
22
Global Instance agree_valid : Valid (agree A) := λ x,  n, {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
23
Global Instance agree_equiv : Equiv (agree A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
24
25
  ( n, agree_is_valid x n  agree_is_valid y n) 
  ( n, agree_is_valid x n  x n ={n}= y n).
Robbert Krebbers's avatar
Robbert Krebbers committed
26
Global Instance agree_dist : Dist (agree A) := λ n x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
27
28
  ( n', n'  n  agree_is_valid x n'  agree_is_valid y n') 
  ( n', n'  n  agree_is_valid x n'  x n' ={n'}= y n').
Robbert Krebbers's avatar
Robbert Krebbers committed
29
Global Program Instance agree_compl : Compl (agree A) := λ c,
Robbert Krebbers's avatar
Robbert Krebbers committed
30
  {| agree_car n := c n n; agree_is_valid n := agree_is_valid (c n) n |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
31
32
33
34
35
36
37
38
39
40
41
42
43
44
Next Obligation. intros; apply agree_valid_0. Qed.
Next Obligation.
  intros c n ?; apply (chain_cauchy c n (S n)), agree_valid_S; auto.
Qed.
Instance agree_cofe : Cofe (agree A).
Proof.
  split.
  * intros x y; split.
    + by intros Hxy n; split; intros; apply Hxy.
    + by intros Hxy; split; intros; apply Hxy with n.
  * split.
    + by split.
    + by intros x y Hxy; split; intros; symmetry; apply Hxy; auto; apply Hxy.
    + intros x y z Hxy Hyz; split; intros n'; intros.
Robbert Krebbers's avatar
Robbert Krebbers committed
45
      - transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
Robbert Krebbers's avatar
Robbert Krebbers committed
46
47
48
49
50
51
52
53
      - transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
  * intros n x y Hxy; split; intros; apply Hxy; auto.
  * intros x y; split; intros n'; rewrite Nat.le_0_r; intros ->; [|done].
    by split; intros; apply agree_valid_0.
  * by intros c n; split; intros; apply (chain_cauchy c).
Qed.

Global Program Instance agree_op : Op (agree A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
54
55
  {| agree_car := x;
     agree_is_valid n := agree_is_valid x n  agree_is_valid y n  x ={n}= y |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
56
Next Obligation. by intros; simpl; split_ands; try apply agree_valid_0. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
57
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
58
59
60
Global Instance agree_unit : Unit (agree A) := id.
Global Instance agree_minus : Minus (agree A) := λ x y, x.
Instance: Commutative () (@op (agree A) _).
61
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
62
Definition agree_idempotent (x : agree A) : x  x  x.
63
Proof. split; naive_solver. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
64
65
66
67
68
69
70
71
72
73
74
Instance:  x : agree A, Proper (dist n ==> dist n) (op x).
Proof.
  intros n x y1 y2 [Hy' Hy]; split; [|done].
  split; intros (?&?&Hxy); repeat (intro || split);
    try apply Hy'; eauto using agree_valid_le.
  * etransitivity; [apply Hxy|apply Hy]; eauto using agree_valid_le.
  * etransitivity; [apply Hxy|symmetry; apply Hy, Hy'];
      eauto using agree_valid_le.
Qed.
Instance: Proper (dist n ==> dist n ==> dist n) op.
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy,!(commutative _ _ y2), Hx. Qed.
75
Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _.
76
77
78
79
80
81
Instance: Associative () (@op (agree A) _).
Proof.
  intros x y z; split; simpl; intuition;
    repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
    by cofe_subst; rewrite !agree_idempotent.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
82
83
84
85
86
Lemma agree_includedN (x y : agree A) n : x {n} y  y ={n}= x  y.
Proof.
  split; [|by intros ?; exists y].
  by intros [z Hz]; rewrite Hz, (associative _), agree_idempotent.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
87
88
89
Global Instance agree_cmra : CMRA (agree A).
Proof.
  split; try (apply _ || done).
Robbert Krebbers's avatar
Robbert Krebbers committed
90
91
92
  * intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
    rewrite <-(proj2 Hxy n'), (Hx n') by eauto using agree_valid_le.
    by apply dist_le with n; try apply Hxy.
Robbert Krebbers's avatar
Robbert Krebbers committed
93
  * by intros n x1 x2 Hx y1 y2 Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
95
96
97
  * intros x; split; [apply agree_valid_0|].
    by intros n'; rewrite Nat.le_0_r; intros ->.
  * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
    rewrite (Hx n') by auto; symmetry; apply dist_le with n; try apply Hx; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
98
  * intros x; apply agree_idempotent.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  * by intros x y n [(?&?&?) ?].
Robbert Krebbers's avatar
Robbert Krebbers committed
100
  * by intros x y n; rewrite agree_includedN.
Robbert Krebbers's avatar
Robbert Krebbers committed
101
102
Qed.
Lemma agree_op_inv (x y1 y2 : agree A) n :
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  {n} x  x ={n}= y1  y2  y1 ={n}= y2.
Robbert Krebbers's avatar
Robbert Krebbers committed
104
Proof. by intros [??] Hxy; apply Hxy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
106
Global Instance agree_extend : CMRAExtend (agree A).
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
107
  intros n x y1 y2 ? Hx; exists (x,x); simpl; split.
Robbert Krebbers's avatar
Robbert Krebbers committed
108
109
110
  * by rewrite agree_idempotent.
  * by rewrite Hx, (agree_op_inv x y1 y2), agree_idempotent by done.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
111
112
113
114
115
Program Definition to_agree (x : A) : agree A :=
  {| agree_car n := x; agree_is_valid n := True |}.
Solve Obligations with done.
Global Instance to_agree_ne n : Proper (dist n ==> dist n) to_agree.
Proof. intros x1 x2 Hx; split; naive_solver eauto using @dist_le. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
116
Lemma agree_car_ne (x y : agree A) n : {n} x  x ={n}= y  x n ={n}= y n.
Robbert Krebbers's avatar
Robbert Krebbers committed
117
Proof. by intros [??] Hxy; apply Hxy. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Lemma agree_cauchy (x : agree A) n i : n  i  {i} x  x n ={n}= x i.
Robbert Krebbers's avatar
Robbert Krebbers committed
119
120
Proof. by intros ? [? Hx]; apply Hx. Qed.
Lemma agree_to_agree_inj (x y : agree A) a n :
Robbert Krebbers's avatar
Robbert Krebbers committed
121
  {n} x  x ={n}= to_agree a  y  x n ={n}= a.
Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
124
Proof.
  by intros; transitivity ((to_agree a  y) n); [by apply agree_car_ne|].
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
125
126
127
End agree.

Section agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
128
  Context `{Cofe A,Cofe B} (f : A  B) `{Hf:  n, Proper (dist n ==> dist n) f}.
Robbert Krebbers's avatar
Robbert Krebbers committed
129
  Program Definition agree_map (x : agree A) : agree B :=
Robbert Krebbers's avatar
Robbert Krebbers committed
130
131
    {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
  Solve Obligations with auto using agree_valid_0, agree_valid_S.
Robbert Krebbers's avatar
Robbert Krebbers committed
132
133
  Global Instance agree_map_ne n : Proper (dist n ==> dist n) agree_map.
  Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
134
  Global Instance agree_map_proper: Proper (()==>()) agree_map := ne_proper _.
Robbert Krebbers's avatar
Robbert Krebbers committed
135
  Global Instance agree_map_monotone : CMRAMonotone agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
137
    split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
Robbert Krebbers's avatar
Robbert Krebbers committed
138
139
140
141
    intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
    split; [split; simpl; try tauto|done].
    by intros (?&?&Hxy); repeat split; intros;
       try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
142
143
  Qed.
End agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
144
145
146
147
148
Lemma agree_map_id `{Cofe A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. Qed.
Lemma agree_map_compose `{Cofe A, Cofe B, Cofe C} (f : A  B) (g : B  C)
  (x : agree A) : agree_map (g  f) x = agree_map g (agree_map f x).
Proof. done. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
149

Robbert Krebbers's avatar
Robbert Krebbers committed
150
Canonical Structure agreeRA (A : cofeT) : cmraT := CMRAT (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
151
152
Definition agreeRA_map {A B} (f : A -n> B) : agreeRA A -n> agreeRA B :=
  CofeMor (agree_map f : agreeRA A  agreeRA B).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
154
155
156
157
Instance agreeRA_map_ne A B n : Proper (dist n ==> dist n) (@agreeRA_map A B).
Proof.
  intros f g Hfg x; split; simpl; intros; [done|].
  by apply dist_le with n; try apply Hfg.
Qed.