deprecated.v 2.48 KB
Newer Older
Ralf Jung's avatar
Ralf Jung committed
1
From iris.algebra Require Import ofe cmra.
2
Set Default Proof Using "Type".
Ralf Jung's avatar
Ralf Jung committed
3
4
5
6

(* Old notation for backwards compatibility. *)

(* Deprecated 2016-11-22. Use ofeT instead. *)
7
Notation cofeT := ofeT (only parsing).
Ralf Jung's avatar
Ralf Jung committed
8
9

(* Deprecated 2016-12-09. Use agree instead. *)
10
Module dec_agree.
Ralf Jung's avatar
Ralf Jung committed
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
Local Arguments validN _ _ _ !_ /.
Local Arguments valid _ _  !_ /.
Local Arguments op _ _ _ !_ /.
Local Arguments pcore _ _ !_ /.

(* This is isomorphic to option, but has a very different RA structure. *)
Inductive dec_agree (A : Type) : Type := 
  | DecAgree : A  dec_agree A
  | DecAgreeBot : dec_agree A.
Arguments DecAgree {_} _.
Arguments DecAgreeBot {_}.
Instance maybe_DecAgree {A} : Maybe (@DecAgree A) := λ x,
  match x with DecAgree a => Some a | _ => None end.

Section dec_agree.
Context `{EqDecision A}.
Implicit Types a b : A.
Implicit Types x y : dec_agree A.

Instance dec_agree_valid : Valid (dec_agree A) := λ x,
  if x is DecAgree _ then True else False.
Canonical Structure dec_agreeC : ofeT := leibnizC (dec_agree A).

Instance dec_agree_op : Op (dec_agree A) := λ x y,
  match x, y with
  | DecAgree a, DecAgree b => if decide (a = b) then DecAgree a else DecAgreeBot
  | _, _ => DecAgreeBot
  end.
Instance dec_agree_pcore : PCore (dec_agree A) := Some.

Definition dec_agree_ra_mixin : RAMixin (dec_agree A).
Proof.
  apply ra_total_mixin; apply _ || eauto.
  - intros [?|] [?|] [?|]; by repeat (simplify_eq/= || case_match).
  - intros [?|] [?|]; by repeat (simplify_eq/= || case_match).
  - intros [?|]; by repeat (simplify_eq/= || case_match).
  - by intros [?|] [?|] ?.
Qed.

Canonical Structure dec_agreeR : cmraT :=
  discreteR (dec_agree A) dec_agree_ra_mixin.

Global Instance dec_agree_total : CMRATotal dec_agreeR.
Proof. intros x. by exists x. Qed.

(* Some properties of this CMRA *)
Global Instance dec_agree_persistent (x : dec_agreeR) : Persistent x.
Proof. by constructor. Qed.

Lemma dec_agree_ne a b : a  b  DecAgree a  DecAgree b = DecAgreeBot.
Proof. intros. by rewrite /= decide_False. Qed.

Lemma dec_agree_idemp (x : dec_agree A) : x  x = x.
Proof. destruct x; by rewrite /= ?decide_True. Qed.

Lemma dec_agree_op_inv (x1 x2 : dec_agree A) :  (x1  x2)  x1 = x2.
Proof. destruct x1, x2; by repeat (simplify_eq/= || case_match). Qed.

Lemma DecAgree_included a b : DecAgree a  DecAgree b  a = b.
Proof.
  split. intros [[c|] [=]%leibniz_equiv]. by simplify_option_eq. by intros ->.
Qed.
End dec_agree.

Arguments dec_agreeC : clear implicits.
Arguments dec_agreeR _ {_}.
77
End dec_agree.