agree.v 7.51 KB
Newer Older
1
From algebra Require Export cmra.
2
From algebra Require Import functor upred.
Robbert Krebbers's avatar
Robbert Krebbers committed
3
4
Local Hint Extern 10 (_  _) => omega.

5
Record agree (A : Type) : Type := Agree {
Robbert Krebbers's avatar
Robbert Krebbers committed
6
7
  agree_car :> nat  A;
  agree_is_valid : nat  Prop;
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
}.
10
Arguments Agree {_} _ _ _.
11
12
Arguments agree_car {_} _ _.
Arguments agree_is_valid {_} _ _.
Robbert Krebbers's avatar
Robbert Krebbers committed
13
14

Section agree.
15
Context {A : cofeT}.
Robbert Krebbers's avatar
Robbert Krebbers committed
16

17
Instance agree_validN : ValidN (agree A) := λ n x,
18
  agree_is_valid x n   n', n'  n  x n' {n'} x n.
Robbert Krebbers's avatar
Robbert Krebbers committed
19
20
21
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.
22
Instance agree_equiv : Equiv (agree A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
23
  ( n, agree_is_valid x n  agree_is_valid y n) 
24
  ( n, agree_is_valid x n  x n {n} y n).
25
Instance agree_dist : Dist (agree A) := λ n x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
26
  ( n', n'  n  agree_is_valid x n'  agree_is_valid y n') 
27
  ( n', n'  n  agree_is_valid x n'  x n' {n'} y n').
28
Program Instance agree_compl : Compl (agree A) := λ c,
29
  {| agree_car n := c (S n) n; agree_is_valid n := agree_is_valid (c (S n)) n |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
30
Next Obligation.
31
  intros c n ?. apply (chain_cauchy c n (S (S n))), agree_valid_S; auto.
Robbert Krebbers's avatar
Robbert Krebbers committed
32
Qed.
33
Definition agree_cofe_mixin : CofeMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
34
35
36
37
38
39
40
41
42
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
43
      - transitivity (agree_is_valid y n'). by apply Hxy. by apply Hyz.
Robbert Krebbers's avatar
Robbert Krebbers committed
44
45
      - transitivity (y n'). by apply Hxy. by apply Hyz, Hxy.
  * intros n x y Hxy; split; intros; apply Hxy; auto.
46
47
  * intros c n; apply and_wlog_r; intros;
      symmetry; apply (chain_cauchy c); naive_solver.
Robbert Krebbers's avatar
Robbert Krebbers committed
48
Qed.
49
Canonical Structure agreeC := CofeT agree_cofe_mixin.
Robbert Krebbers's avatar
Robbert Krebbers committed
50

51
Lemma agree_car_ne (x y : agree A) n : {n} x  x {n} y  x n {n} y n.
52
Proof. by intros [??] Hxy; apply Hxy. Qed.
53
Lemma agree_cauchy (x : agree A) n i : {n} x  i  n  x i {i} x n.
54
55
Proof. by intros [? Hx]; apply Hx. Qed.

56
Program Instance agree_op : Op (agree A) := λ x y,
Robbert Krebbers's avatar
Robbert Krebbers committed
57
  {| agree_car := x;
58
     agree_is_valid n := agree_is_valid x n  agree_is_valid y n  x {n} y |}.
Robbert Krebbers's avatar
Robbert Krebbers committed
59
Next Obligation. naive_solver eauto using agree_valid_S, dist_S. Qed.
60
61
Instance agree_unit : Unit (agree A) := id.
Instance agree_minus : Minus (agree A) := λ x y, x.
62
Instance: Comm () (@op (agree A) _).
63
Proof. intros x y; split; [naive_solver|by intros n (?&?&Hxy); apply Hxy]. Qed.
64
Definition agree_idemp (x : agree A) : x  x  x.
65
Proof. split; naive_solver. Qed.
66
67
68
69
70
71
Instance:  n : nat, Proper (dist n ==> impl) (@validN (agree A) _ n).
Proof.
  intros n x y Hxy [? Hx]; split; [by apply Hxy|intros n' ?].
  rewrite -(proj2 Hxy n') 1?(Hx n'); eauto using agree_valid_le.
  by apply dist_le with n; try apply Hxy.
Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
72
73
74
75
76
77
78
79
80
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.
81
Instance: Proper (dist n ==> dist n ==> dist n) (@op (agree A) _).
82
Proof. by intros n x1 x2 Hx y1 y2 Hy; rewrite Hy !(comm _ _ y2) Hx. Qed.
83
Instance: Proper (() ==> () ==> ()) op := ne_proper_2 _.
84
Instance: Assoc () (@op (agree A) _).
85
86
87
Proof.
  intros x y z; split; simpl; intuition;
    repeat match goal with H : agree_is_valid _ _ |- _ => clear H end;
88
    by cofe_subst; rewrite !agree_idemp.
89
Qed.
90
Lemma agree_includedN (x y : agree A) n : x {n} y  y {n} x  y.
Robbert Krebbers's avatar
Robbert Krebbers committed
91
92
Proof.
  split; [|by intros ?; exists y].
93
  by intros [z Hz]; rewrite Hz assoc agree_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
94
Qed.
95
Definition agree_cmra_mixin : CMRAMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
96
97
98
Proof.
  split; try (apply _ || done).
  * by intros n x1 x2 Hx y1 y2 Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
99
  * intros n x [? Hx]; split; [by apply agree_valid_S|intros n' ?].
Robbert Krebbers's avatar
Robbert Krebbers committed
100
101
    rewrite (Hx n'); last auto.
    symmetry; apply dist_le with n; try apply Hx; auto.
102
  * intros x; apply agree_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
103
  * by intros x y n [(?&?&?) ?].
Robbert Krebbers's avatar
Robbert Krebbers committed
104
  * by intros x y n; rewrite agree_includedN.
Robbert Krebbers's avatar
Robbert Krebbers committed
105
Qed.
106
Lemma agree_op_inv (x1 x2 : agree A) n : {n} (x1  x2)  x1 {n} x2.
107
Proof. intros Hxy; apply Hxy. Qed.
108
Lemma agree_valid_includedN (x y : agree A) n : {n} y  x {n} y  x {n} y.
109
110
Proof.
  move=> Hval [z Hy]; move: Hval; rewrite Hy.
111
  by move=> /agree_op_inv->; rewrite agree_idemp.
112
Qed.
113
Definition agree_cmra_extend_mixin : CMRAExtendMixin (agree A).
Robbert Krebbers's avatar
Robbert Krebbers committed
114
Proof.
115
  intros n x y1 y2 Hval Hx; exists (x,x); simpl; split.
116
117
  * by rewrite agree_idemp.
  * by move: Hval; rewrite Hx; move=> /agree_op_inv->; rewrite agree_idemp.
Robbert Krebbers's avatar
Robbert Krebbers committed
118
Qed.
119
120
121
Canonical Structure agreeRA : cmraT :=
  CMRAT agree_cofe_mixin agree_cmra_mixin agree_cmra_extend_mixin.

Robbert Krebbers's avatar
Robbert Krebbers committed
122
123
124
125
126
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.
127
Global Instance to_agree_proper : Proper (() ==> ()) to_agree := ne_proper _.
128
Global Instance to_agree_inj n : Inj (dist n) (dist n) (to_agree).
129
Proof. by intros x y [_ Hxy]; apply Hxy. Qed.
130
Lemma to_agree_car n (x : agree A) : {n} x  to_agree (x n) {n} x.
Robbert Krebbers's avatar
Robbert Krebbers committed
131
Proof. intros [??]; split; naive_solver eauto using agree_valid_le. Qed.
132
133
134
135

(** Internalized properties *)
Lemma agree_valid_uPred {M} x y :  (x  y)  (x  y : uPred M).
Proof. by intros r n _ ?; apply: agree_op_inv. Qed.
Robbert Krebbers's avatar
Robbert Krebbers committed
136
137
End agree.

138
139
140
Arguments agreeC : clear implicits.
Arguments agreeRA : clear implicits.

141
Program Definition agree_map {A B} (f : A  B) (x : agree A) : agree B :=
142
  {| agree_car n := f (x n); agree_is_valid := agree_is_valid x |}.
143
Solve Obligations with auto using agree_valid_S.
144
145
Lemma agree_map_id {A} (x : agree A) : agree_map id x = x.
Proof. by destruct x. Qed.
146
147
Lemma agree_map_compose {A B C} (f : A  B) (g : B  C) (x : agree A) :
  agree_map (g  f) x = agree_map g (agree_map f x).
148
Proof. done. Qed.
149

Robbert Krebbers's avatar
Robbert Krebbers committed
150
Section agree_map.
151
  Context {A B : cofeT} (f : A  B) `{Hf:  n, Proper (dist n ==> dist n) f}.
152
  Global Instance agree_map_ne n : Proper (dist n ==> dist n) (agree_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
153
  Proof. by intros x1 x2 Hx; split; simpl; intros; [apply Hx|apply Hf, Hx]. Qed.
154
155
156
157
158
159
  Global Instance agree_map_proper :
    Proper (() ==> ()) (agree_map f) := ne_proper _.
  Lemma agree_map_ext (g : A  B) x :
    ( x, f x  g x)  agree_map f x  agree_map g x.
  Proof. by intros Hfg; split; simpl; intros; rewrite ?Hfg. Qed.
  Global Instance agree_map_monotone : CMRAMonotone (agree_map f).
Robbert Krebbers's avatar
Robbert Krebbers committed
160
  Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
161
    split; [|by intros n x [? Hx]; split; simpl; [|by intros n' ?; rewrite Hx]].
Robbert Krebbers's avatar
Robbert Krebbers committed
162
    intros x y n; rewrite !agree_includedN; intros Hy; rewrite Hy.
Robbert Krebbers's avatar
Robbert Krebbers committed
163
    split; last done; split; simpl; last tauto.
Robbert Krebbers's avatar
Robbert Krebbers committed
164
165
    by intros (?&?&Hxy); repeat split; intros;
       try apply Hxy; try apply Hf; eauto using @agree_valid_le.
Robbert Krebbers's avatar
Robbert Krebbers committed
166
167
  Qed.
End agree_map.
Robbert Krebbers's avatar
Robbert Krebbers committed
168

169
170
171
Definition agreeC_map {A B} (f : A -n> B) : agreeC A -n> agreeC B :=
  CofeMor (agree_map f : agreeC A  agreeC B).
Instance agreeC_map_ne A B n : Proper (dist n ==> dist n) (@agreeC_map A B).
Robbert Krebbers's avatar
Robbert Krebbers committed
172
Proof.
Robbert Krebbers's avatar
Robbert Krebbers committed
173
  intros f g Hfg x; split; simpl; intros; first done.
Robbert Krebbers's avatar
Robbert Krebbers committed
174
175
  by apply dist_le with n; try apply Hfg.
Qed.
Ralf Jung's avatar
Ralf Jung committed
176
177
178
179

Program Definition agreeF : iFunctor :=
  {| ifunctor_car := agreeRA; ifunctor_map := @agreeC_map |}.
Solve Obligations with done.