From ec66aeeaba1d7802d09ec3c78ed996b13f9e6520 Mon Sep 17 00:00:00 2001
From: dsac <arnaud@dabyseesaram.info>
Date: Tue, 28 Jun 2022 14:25:05 +0200
Subject: [PATCH] Definition of time + generic Compute_Maximals instance
---
aneris/examples/crdt/statelib/proof/events.v | 291 ++++++++++++---
aneris/examples/crdt/statelib/proof/time.v | 29 --
aneris/examples/crdt/statelib/proof/utils.v | 41 ++
aneris/examples/crdt/statelib/time/evtime.v | 62 ++++
.../examples/crdt/statelib/time/maximality.v | 351 ++++++++++++++++++
aneris/examples/crdt/statelib/time/time.v | 56 +++
6 files changed, 742 insertions(+), 88 deletions(-)
delete mode 100644 aneris/examples/crdt/statelib/proof/time.v
create mode 100644 aneris/examples/crdt/statelib/proof/utils.v
create mode 100644 aneris/examples/crdt/statelib/time/evtime.v
create mode 100644 aneris/examples/crdt/statelib/time/maximality.v
create mode 100644 aneris/examples/crdt/statelib/time/time.v
diff --git a/aneris/examples/crdt/statelib/proof/events.v b/aneris/examples/crdt/statelib/proof/events.v
index 91462e2..2a3d47d 100644
--- a/aneris/examples/crdt/statelib/proof/events.v
+++ b/aneris/examples/crdt/statelib/proof/events.v
@@ -1,63 +1,236 @@
-From stdpp Require Import base countable.
+From stdpp Require Import base countable list sets.
From aneris.aneris_lang Require Import lang.
-From aneris.prelude Require Import time.
+From aneris.prelude Require Import time misc gset_map.
From aneris.examples.crdt.spec Require Import crdt_time crdt_events.
-From aneris.examples.crdt.statelib.proof Require Import time.
+From aneris.examples.crdt.statelib.proof Require Import utils.
+From aneris.examples.crdt.statelib.time Require Import time maximality.
+
+Lemma set_choose_or_empty
+ {A: Type} {EqDecision0 : EqDecision A} {H : Countable A}
+ (X : gset A):
+ (∃ x : A, x ∈ X) ∨ X = ∅.
+Proof.
+ generalize X. apply set_ind;
+ [ intros?;set_solver | set_solver | ].
+ intros ???[?|?]; left; exists x; set_solver.
+Qed.
(** * Instantiation of Statelib events *)
-(* Section Events. *)
-
-(* Context `{!Log_Op LogOp}. *)
-
-(* Record StLibEvent := { *)
-(* ev_op : LogOp; *)
-(* ev_orig : RepId; *)
-(* ev_seqid : SeqNum; *)
-(* (* valid events should include themselves as dependencies *) *)
-(* ev_deps : Timestamp; *)
-(* }. *)
-
-(* Global Instance oplib_event_eqdec : EqDecision StLibEvent. *)
-(* Proof. solve_decision. Defined. *)
-
-(* Global Instance oplib_event_countable : Countable StLibEvent. *)
-(* Proof. *)
-(* (* *)
-(* refine {| *)
-(* encode ev := encode (ev.(ev_op), ev.(ev_orig), ev.(ev_vc)); *)
-(* decode n := (λ tr, match tr with *)
-(* | (op, orig, vc) => Build_OpLibEvent op orig vc *)
-(* end) <$> *)
-(* @decode (LogOp * nat * vector_clock) _ _ n; *)
-(* |}. *)
-(* intros []. rewrite /= decode_encode /=. done. *)
-(* Qed. *) *)
-(* Admitted. *)
-
-(* Global Instance oplib_event_timed : Timed StLibEvent := { time := ev_deps }. *)
-
-(* Global Instance OpLibEvent_LogEvents : Log_Events LogOp := { *)
-(* Event := OpLibEvent; *)
-(* EV_Op := ev_op; *)
-(* EV_Orig := ev_orig; *)
-(* }. *)
-
-(* End Events. *)
-
-(* Arguments OpLibEvent : clear implicits. *)
-
-(* Section ComputeMaximals. *)
-
-(* Context `{!Log_Op LogOp}. *)
-
-(* (* *)
-(* Global Instance maximals_computing : Maximals_Computing (OpLibEvent LogOp). *)
-(* Proof. *)
-(* refine {| Maximals := compute_maximals ev_vc; *)
-(* Maximum := compute_maximum ev_vc; |}. *)
-(* - apply (compute_maximals_correct (@ev_vc LogOp)). *)
-(* - apply compute_maximum_correct. *)
-(* Qed. *)
-(* *) *)
-
-(* End ComputeMaximals. *)
+Section Events.
+ Context {Op: Type}.
+ Context `{!EqDecision Op, !Countable Op}.
+
+ Global Instance stlib_event_eqdec : EqDecision (Event Op).
+ Proof. solve_decision. Defined.
+
+ Global Instance stlib_event_timed : Timed (Event Op) := { time := EV_Time }.
+End Events.
+
+
+Section UsefulFunctions.
+ Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+ Definition get_seqnum (ev: Event Op) : SeqNum :=
+ size (filter (λ eid: EvId, eid.1 = ev.(EV_Orig)) ev.(EV_Time)).
+
+ Definition get_evid (ev: Event Op) : EvId :=
+ (ev.(EV_Orig), get_seqnum ev).
+
+ Definition depends_on (ev ev': Event Op) := get_evid ev' ∈ ev.(EV_Time).
+
+ Definition get_deps (e: Event Op): gset EvId := e.(EV_Time).
+ Definition get_deps_set (s: event_set Op) : gset EvId :=
+ gset_flat_map get_deps s.
+
+ Definition fresh_event (s: event_set Op) (op: Op) (orig: RepId): Event Op :=
+ {|
+ EV_Op := op ;
+ EV_Orig := orig ;
+ EV_Time :=
+ match compute_maximum ( filter (λ ev, ev.(EV_Orig) = orig) s ) with
+ | None => get_deps_set s ∪ {[(orig, 1%nat)]}
+ | Some e =>
+ let seen_events := get_deps_set s in
+ seen_events
+ ∪ {[(orig,
+ S (size (filter (λ eid, eid.1 = orig) (get_deps_set s))))]}
+ end
+ |}.
+
+ Definition hproj (i: RepId) (st: event_set Op) :=
+ filter (λ ev, ev.(EV_Orig) = i) st.
+End UsefulFunctions.
+
+
+
+Section EventSets.
+ Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+ (* A set of events is `dep_closed` if it contains every causal dependency of
+ every element of the set. *)
+ Definition dep_closed (s : gset (Event Op)) : Prop :=
+ ∀ (e: Event Op) (evid: EvId),
+ e ∈ s →
+ evid ∈ e.(EV_Time) →
+ ∃ (e': Event Op), e' ∈ s ∧ get_evid e' = evid.
+
+ Definition events_ext_evid (s: event_set Op) : Prop :=
+ ∀ ev ev', ev ∈ s → ev' ∈ s → get_evid ev = get_evid ev' → ev = ev'.
+
+ Definition events_ext_time (s: event_set Op) : Prop :=
+ ∀ ev ev', ev ∈ s → ev' ∈ s → ev =_t ev' → ev = ev'.
+
+ Definition event_set_same_orig_comparable (st: event_set Op) : Prop :=
+ ∀ e e', e ∈ st → e' ∈ st → e.(EV_Orig) = e'.(EV_Orig) → e <_t e' ∨ e =_t e' ∨ e' <_t e.
+
+ Definition event_set_orig_lt {i: nat} (st: event_set Op) : Prop :=
+ ∀ ev, ev ∈ st → ev.(EV_Orig) < i.
+
+ Definition event_set_orig_deps_seq (st: event_set Op) : Prop :=
+ ∀ (e: Event Op),
+ e ∈ st →
+ ∀ (i: RepId) (sid: nat), O < sid → evid_le (i, sid) (get_evid e) →
+ (i, sid) ∈ e.(EV_Time).
+
+ Definition event_set_orig_max {nb: nat} (st: event_set Op) : Prop :=
+ ∀ (i: RepId), i < nb
+ → hproj i st = ∅ ∨ ∃ m, m ∈ st ∧ compute_maximum (hproj i st) = Some m.
+
+ Definition event_set_evid_mon (st: event_set Op) : Prop :=
+ ∀ ev ev', ev ∈ st → ev' ∈ st → ev.(EV_Orig) = ev'.(EV_Orig) →
+ ev <_t ev' → evid_le (get_evid ev) (get_evid ev').
+
+
+
+ Definition event_set_valid (s : gset (Event Op)) : Prop :=
+ dep_closed s
+ ∧ ∀ (e e': Event Op),
+ e ∈ s → e' ∈ s →
+ ((EV_Orig e = EV_Orig e' → (e ≤_t e' ∨ e' ≤_t e))
+ ∧ (e =_t e' → e = e')).
+
+
+
+ Lemma dep_closed_union (s s' : gset (Event Op)) :
+ dep_closed s -> dep_closed s' -> dep_closed (s ∪ s').
+ Proof.
+ intros Hdc Hdc' ev eid [Hin|Hin]%elem_of_union Hdep;
+ [ destruct (Hdc ev eid Hin Hdep)
+ as (ev' & Hev'_in%(elem_of_union_l _ s s') & Heq)
+ | destruct (Hdc' ev eid Hin Hdep)
+ as (ev' & Hev'_in%(elem_of_union_r _ s s') & Heq) ];
+ by exists ev'.
+ Qed.
+End EventSets.
+
+Section Events.
+ Context {Op: Type}.
+ Context `{!EqDecision Op, !Countable Op}.
+
+ Definition cc_impl : relation (gset (Event Op)) :=
+ λ s s',
+ ∀ (e e' : Event Op),
+ e ∈ s' → e' ∈ s' →
+ e ≤_t e' ->
+ e' ∈ s →
+ e ∈ s.
+
+ Global Instance cc_impl_refl : Reflexive cc_impl.
+ Proof.
+ intros s e e' Hin Hin' Hlt Hin''.
+ done.
+ Qed.
+
+ Definition cc_subseteq : relation (gset (Event Op)) :=
+ λ s s', s ⊆ s' ∧ cc_impl s s'.
+
+ Global Instance cc_subseteq_preorder : PreOrder cc_subseteq.
+ Proof.
+ split; constructor.
+ - done.
+ - rewrite /cc_impl. eauto.
+ - destruct H as [H _].
+ destruct H0 as [H0 _].
+ set_solver.
+ - destruct H as [Hsub Hy].
+ destruct H0 as [Hsub' Hz].
+ intros e e' Hin Hin' Hle Hinx.
+ assert (e' ∈ y) as He'y by set_solver.
+ assert (e ∈ y) as Hey.
+ { apply (Hz e e'); auto. }
+ apply (Hy e e'); auto.
+ Qed.
+
+ Lemma cc_subseteq_union h h1 h2 :
+ cc_subseteq h1 h -> cc_subseteq h2 h -> cc_subseteq (h1 ∪ h2) h.
+ Proof.
+ intros [Hsub1 Hcc1] [Hsub2 Hcc2].
+ split; [set_solver |].
+ intros e e' Hin Hin' Hle [Hl | Hr]%elem_of_union.
+ - apply elem_of_union_l.
+ apply (Hcc1 e e'); auto.
+ - apply elem_of_union_r.
+ apply (Hcc2 e e'); auto.
+ Qed.
+End Events.
+
+Global Arguments cc_subseteq {_ _ _}.
+
+
+
+Section ComputeMaximumLemams.
+ Context `{Op: Type, !EqDecision Op, !Countable Op}.
+
+ Lemma event_set_maximum_exists (s: event_set Op) (orig: RepId):
+ (∃ e, e ∈ s ∧ e.(EV_Orig) = orig)
+ → event_set_same_orig_comparable s
+ → events_ext_time s
+ → ∃ m, compute_maximum (hproj orig s) = Some m.
+ Proof.
+ intros (e & He_in & He_orig) Hcomp Hext_t.
+ unfold compute_maximum.
+ destruct (set_choose_or_empty (compute_maximals (hproj orig s)))
+ as [(m & [Hm_max [Hm_orig Hm_in]%elem_of_filter]%elem_of_filter) | Hnil].
+ - assert (compute_maximals (hproj orig s) = {[ m ]}) as ->.
+ { apply set_eq. intros n. split.
+ - intros [[Hn_orig Hn_in]%elem_of_filter Hn_max]%compute_maximals_correct.
+ apply elem_of_singleton.
+ specialize Hn_max with m.
+ destruct (Hcomp n m) as [H | [H | H]]; try done.
+ + by rewrite Hn_orig Hm_orig.
+ + by destruct Hn_max; first apply elem_of_filter.
+ + by apply Hext_t.
+ + by destruct (Hm_max n); first apply elem_of_filter.
+ - intros ->%elem_of_singleton.
+ apply elem_of_filter. by split; last apply elem_of_filter. }
+ rewrite elements_singleton.
+ by exists m.
+ - rewrite set_eq -set_equiv compute_maximals_empty set_equiv -set_eq in Hnil.
+ assert (He_in': e ∈ hproj orig s); first by apply elem_of_filter.
+ set_solver.
+ Qed.
+End ComputeMaximumLemams.
+
+
+
+Section UsefulLemmas.
+ Context {Op: Type}.
+ Context `{!EqDecision Op, !Countable Op}.
+
+ Lemma maximals_union (X Y: event_set Op) (x: Event Op):
+ x ∈ compute_maximals (X ∪ Y)
+ → (x ∈ compute_maximals X ∨ x ∈ compute_maximals Y).
+ Proof.
+ intros Hx_in.
+ assert (x ∈ compute_maximals (X ∪ Y))
+ as [H|H]%elem_of_compute_maximals%elem_of_union;
+ first assumption;
+ [left|right];
+ apply compute_maximals_spec in Hx_in as [Hin Hmax];
+ apply compute_maximals_spec; (split; first assumption);
+ intros y Hy;
+ apply Hmax;
+ set_solver.
+ Qed.
+End UsefulLemmas.
+
diff --git a/aneris/examples/crdt/statelib/proof/time.v b/aneris/examples/crdt/statelib/proof/time.v
deleted file mode 100644
index f5e23e0..0000000
--- a/aneris/examples/crdt/statelib/proof/time.v
+++ /dev/null
@@ -1,29 +0,0 @@
-From stdpp Require Import gmap.
-From aneris.examples.crdt.spec Require Import crdt_time.
-
-Section Time.
-
- Definition RepId := nat.
- Definition SeqNum := nat.
- Definition EvId : Type := RepId * SeqNum.
- Definition Timestamp := gset EvId.
-
- Definition ts_le (ts1 ts2 : Timestamp) : Prop := ts1 ⊆ ts2.
-
- Definition ts_lt (ts1 ts2 : Timestamp) : Prop := ts1 ⊂ ts2.
-
- Global Instance timestamp_time : Log_Time.
- Admitted.
- (* TODO
- Global Instance timestamp_time : Log_Time :=
- {| Time := vector_clock;
- TM_le := vector_clock_le;
- TM_lt := vector_clock_lt;
- TM_lt_irreflexive := vector_clock_lt_irreflexive;
- TM_lt_TM_le := vector_clock_lt_le;
- TM_le_eq_or_lt := vector_clock_le_eq_or_lt;
- TM_le_lt_trans := vector_clock_le_lt_trans;
- TM_lt_le_trans := vector_clock_lt_le_trans; |}.
- *)
-
-End Time.
diff --git a/aneris/examples/crdt/statelib/proof/utils.v b/aneris/examples/crdt/statelib/proof/utils.v
new file mode 100644
index 0000000..931ebc0
--- /dev/null
+++ b/aneris/examples/crdt/statelib/proof/utils.v
@@ -0,0 +1,41 @@
+From stdpp Require Import gmap.
+From aneris.examples.crdt.spec Require Import crdt_time.
+
+Section Defs.
+
+ Definition RepId := nat.
+ Definition SeqNum := nat.
+ Definition EvId : Type := RepId * SeqNum.
+ Definition Timestamp : Type := gset EvId.
+
+
+ Definition evid_le (ts1 ts2 : EvId) : Prop.
+ Proof.
+ destruct ts1 as [rid sid]; destruct ts2 as [rid' sid'].
+ exact (rid = rid' ∧ (sid ≤ sid')%nat).
+ Defined.
+
+ Global Instance evid_le_refl: Reflexive evid_le.
+ Proof. by intros[]. Qed.
+
+ Global Instance evid_le_trans : Transitive evid_le.
+ Proof.
+ intros [r s][r' s'][r'' s''][-> Hle][<- Hle'].
+ split; [ reflexivity | by apply le_trans with s'].
+ Qed.
+
+ Global Instance evid_le_antisym: AntiSymm eq evid_le.
+ Proof.
+ intros[r s][r' s'] [-> Hle] [Heq Hle'].
+ apply pair_equal_spec; split; [reflexivity | by apply le_antisym].
+ Qed.
+
+ Global Instance evid_le_po: PartialOrder evid_le.
+ Proof. repeat split; exact _. Qed.
+
+
+
+ Definition evid_lt := strict evid_le.
+
+End Defs.
+
diff --git a/aneris/examples/crdt/statelib/time/evtime.v b/aneris/examples/crdt/statelib/time/evtime.v
new file mode 100644
index 0000000..ffabd3f
--- /dev/null
+++ b/aneris/examples/crdt/statelib/time/evtime.v
@@ -0,0 +1,62 @@
+From stdpp Require Import gmap.
+From aneris.aneris_lang Require Import lang resources.
+From aneris.examples.crdt.spec Require Import crdt_time.
+From aneris.examples.crdt.statelib.proof Require Import utils.
+From Coq.Logic Require Import Decidable.
+
+(** Implementation of Log_Time base don the event id (EvId != RepId * SeqNum) *)
+
+Section EVTime.
+ Lemma evid_lt_irreflexive: ∀ x: EvId, ~ evid_lt x x.
+ Proof. intros?[??]; eauto. Qed.
+
+ Lemma evid_lt_trans: ∀ x y z, evid_lt x y → evid_lt y z → evid_lt x z.
+ Proof.
+ intros [rid sid] [rid' sid'] [rid'' sid''] [[-> Hle] Hnle][[<- Hle'] Hnle'].
+ split; first by apply evid_le_trans with (rid', sid').
+ intros [_ Hle_].
+ destruct Hnle. split; [ reflexivity | by apply le_trans with sid'' ].
+ Qed.
+
+ Lemma evid_lt_TM_le: ∀ x x', evid_lt x x' → evid_le x x'.
+ Proof. by intros ??[? _]. Qed.
+
+ Lemma evid_le_eq_or_lt: ∀ x x', evid_le x x' → x = x' ∨ evid_lt x x'.
+ Proof.
+ intros[rid sid][rid' sid'][-> Hle].
+ apply le_lt_or_eq in Hle as [Hlt | ->]; [right | left]; last reflexivity.
+ split; first (split; [ reflexivity | lia]).
+ intros [_ Hle]. lia.
+ Qed.
+
+ Lemma evid_le_lt_trans:
+ ∀ t t' t'' : EvId,
+ evid_le t t' → evid_lt t' t'' → evid_lt t t''.
+ Proof. exact strict_transitive_r. Qed.
+
+ Lemma evid_lt_le_trans:
+ ∀ t t' t'' : EvId,
+ evid_lt t t' → evid_le t' t'' → evid_lt t t''.
+ Proof. exact strict_transitive_l. Qed.
+
+ Global Instance evid_lt_asym: Asymmetric evid_lt.
+ Proof.
+ intros[r s][r' s'] [[-> Hle] Hnle][[Heq Hle'] Hnle'].
+ by apply Hnle.
+ Qed.
+
+ Global Instance eviq_time : Log_Time :=
+ {| Time := EvId;
+ TM_le := evid_le;
+ TM_le_PO := evid_le_po;
+ TM_lt := evid_lt;
+ TM_lt_irreflexive := evid_lt_irreflexive;
+ TM_lt_trans := evid_lt_trans;
+ TM_le_eq_or_lt := evid_le_eq_or_lt;
+ TM_lt_TM_le := evid_lt_TM_le;
+ TM_le_lt_trans := evid_le_lt_trans;
+ TM_lt_le_trans := evid_lt_le_trans
+ |}.
+
+End EVTime.
+
diff --git a/aneris/examples/crdt/statelib/time/maximality.v b/aneris/examples/crdt/statelib/time/maximality.v
new file mode 100644
index 0000000..62e26c0
--- /dev/null
+++ b/aneris/examples/crdt/statelib/time/maximality.v
@@ -0,0 +1,351 @@
+From stdpp Require Import base gmap.
+From aneris.prelude Require Import misc.
+From aneris.examples.crdt.spec Require Import crdt_time.
+
+Lemma set_choose_or_empty
+ {A: Type} {EqDecision0 : EqDecision A} {H : Countable A}
+ (X : gset A):
+ (∃ x : A, x ∈ X) ∨ X = ∅.
+Proof.
+ generalize X. apply set_ind;
+ [ intros?;set_solver | set_solver | ].
+ intros ???[?|?]; left; exists x; set_solver.
+Qed.
+
+Section ComputeMaximals.
+ Context {T: Type}.
+ Context `{
+ !EqDecision T, !Countable T,
+ !Log_Time, !Timed T,
+ !RelDecision TM_lt}.
+
+ Definition compute_maximals (g: gset T): gset T :=
+ filter
+ (λ (x: T), set_Forall (λ (y: T), ¬ x <_t y) g) g.
+
+ Definition compute_maximum (g: (gset T)): option T:=
+ match elements (compute_maximals g) with
+ | h :: [] => Some h
+ | _ => None
+ end.
+
+
+
+ Lemma set_singleton_elements
+ (X : gset T) (x: T):
+ elements X = [x] ↔ X = {[x]}.
+ Proof.
+ split.
+ - intros Helem.
+ apply set_eq. intros y.
+ split; intros Hy.
+ + apply elem_of_elements.
+ by rewrite elements_singleton, <-Helem, elem_of_elements.
+ + apply elem_of_elements.
+ by rewrite <-elem_of_elements, elements_singleton, <-Helem in Hy.
+ - intros Helem. by rewrite Helem, elements_singleton.
+ Qed.
+
+
+
+ Lemma compute_maximals_correct
+ (X : gset T): is_maximals X (compute_maximals X).
+ Proof.
+ pattern X. apply set_ind;
+ [intros ???; set_solver |
+ (split; [ set_solver | ]; by intros [? _]) |].
+ intros y Y Hy Hmax.
+ intros z. split; intros Hz.
+ - apply elem_of_filter in Hz as [Hz_forall Hz_in].
+ split; [ exact Hz_in |].
+ intros t Hi_in. by apply Hz_forall.
+ - apply elem_of_filter. split; by destruct Hz.
+ Qed.
+
+ (** The folliwing are usefull lemmas, most required for the proof of
+ [compute_maximum_correct] (conferre below) *)
+ Lemma elem_of_compute_maximals
+ (X : gset T) (x: T):
+ x ∈ compute_maximals X → x ∈ X.
+ Proof. unfold compute_maximals. rewrite elem_of_filter. by intros [_ ?]. Qed.
+
+ Lemma compute_maximals_spec_1 (g: gset T) (ev: T):
+ ev ∈ (compute_maximals g) →
+ ev ∈ g ∧ ∀ ev', (ev' ∈ g → ¬ ev <_t ev').
+ Proof.
+ intros Hev_in%elem_of_filter.
+ by destruct Hev_in as [Hv_max Hev_in].
+ Qed.
+
+ Lemma compute_maximals_spec_2 (g: gset T) (ev: T):
+ ev ∈ g → (∀ ev', (ev' ∈ g → ¬ ev <_t ev'))
+ → ev ∈ (compute_maximals g).
+ Proof.
+ intros Hev_in Hev_max.
+ apply elem_of_filter.
+ split; [| exact Hev_in].
+ intros x Hx_in. by apply Hev_max.
+ Qed.
+
+ Lemma compute_maximals_spec (g: gset T) (ev: T):
+ ev ∈ (compute_maximals g) ↔ (ev ∈ g ∧ ∀ ev', (ev' ∈ g → ¬ ev <_t ev')).
+ Proof.
+ split.
+ - apply compute_maximals_spec_1.
+ - intros [??]; by apply compute_maximals_spec_2.
+ Qed.
+
+
+ Lemma find_one_maximal_in_compute_maximals
+ (g: gset T) (x: T):
+ x ∈ g
+ → find_one_maximal (fun a => time a) TM_lt x (elements g)
+ ∈ (compute_maximals g).
+ Proof.
+ (** TODO: remove this assertion *)
+ assert (Hrex: ∀ a b, TM_lt a b → TM_lt b a → False);
+ first apply TM_lt_exclusion.
+ (**)
+ intros Hxl.
+ apply compute_maximals_spec_2;
+ first by destruct ( find_one_maximal_eq_or_elem_of (fun a => time a) TM_lt x
+ (elements g)) as [Hyp|Hyp%elem_of_elements]; first by rewrite Hyp.
+ intros ev' Hev'l%elem_of_elements Hneg.
+ by apply (find_one_maximal_maximal (fun a => time a) TM_lt TM_le
+ TM_lt_TM_le TM_le_eq_or_lt TM_lt_irreflexive Hrex TM_le_lt_trans
+ x (elements g) ev').
+ Qed.
+
+ Lemma compute_maximals_nin' (g: gset T) (x: T):
+ g ≠∅ → x ∈ g →
+ x ∉ compute_maximals g → ∃ y, y ∈ g ∧ ¬ y <_t x.
+ Proof.
+ intros Hnempty Hx_in Hx_nin.
+ exists (find_one_maximal (λ a, time a) TM_lt x (elements g));
+ pose (find_one_maximal_in_compute_maximals g x Hx_in) as Hfm;
+ apply compute_maximals_correct in Hfm as [Hin Hmax].
+ split; first assumption.
+ by apply Hmax.
+ Qed.
+
+ Lemma compute_maximals_nin (g: gset T) (x: T):
+ x ∉ (compute_maximals ({[x]} ∪ g))
+ → compute_maximals ({[x]} ∪ g) = compute_maximals g.
+ Proof.
+ intros Hx_nin.
+ assert (HnP: ¬ set_Forall (λ y, ¬ x <_t y) ({[x]} ∪ g)).
+ { unfold compute_maximals in Hx_nin; rewrite elem_of_filter in Hx_nin.
+ intros Hyp. apply Hx_nin.
+ split; set_solver. }
+ apply set_eq. intros y. split.
+ - intros [[->%elem_of_singleton|Hy_in]%elem_of_union Hy_max]%compute_maximals_correct.
+ + exfalso. destruct HnP. intros?. by apply Hy_max.
+ + apply compute_maximals_correct. split; [ assumption |].
+ intros z Hz_in. apply Hy_max. set_solver.
+ - intros [Hy_in Hy_max]%compute_maximals_correct.
+ apply compute_maximals_correct. split; [ set_solver |].
+ intros ev [->%elem_of_singleton|Hev]%elem_of_union;
+ [| by apply Hy_max].
+ intros Himp.
+ destruct Hx_nin.
+ apply compute_maximals_spec_2;
+ first by apply elem_of_union_l, elem_of_singleton.
+ intros e [->%elem_of_singleton | He_in]%elem_of_union;
+ first by apply TM_lt_irreflexive.
+ intros Hlt. apply (Hy_max e); first assumption.
+ by apply TM_lt_trans with (time x).
+ Qed.
+
+
+
+ Lemma compute_maximals_empty (X: gset T):
+ compute_maximals X ≡ ∅ ↔ X ≡ ∅.
+ Proof.
+ generalize X; apply set_ind; [(intros?; set_solver)|set_solver|].
+ intros x Y Hw_nin HY_empty_iff. split; last set_solver.
+ intros Hyp. exfalso.
+ assert (H': x ∉ compute_maximals ({[x]} ∪ Y));
+ try by rewrite Hyp.
+ rewrite compute_maximals_nin in Hyp; try exact H'.
+ apply H', elem_of_filter.
+ split; last set_solver.
+ intros x'.
+ intros [->%elem_of_singleton | Hx'_in]%elem_of_union.
+ - by apply TM_lt_irreflexive.
+ - by replace Y with (∅: gset T) in *; last set_solver.
+ Qed.
+
+ Lemma compute_maximals_bigger (g: gset T) (ev: T):
+ ev ∈ g → ∃ maxev, maxev ∈ (compute_maximals g) ∧ ev ≤_t maxev.
+ Proof.
+ intros Hev_in.
+ destruct (set_choose_or_empty g) as [eqn|eqn];
+ last (apply compute_maximals_empty in Hev_in; set_solver).
+ exists (find_one_maximal (fun a => time a) TM_lt ev (elements g)).
+ split; first by apply find_one_maximal_in_compute_maximals.
+ apply (find_one_maximal_rel (λ a, time a) TM_lt TM_le).
+ apply TM_lt_TM_le.
+ Qed.
+
+ Lemma compute_maximum_correct:
+ ∀ X : gset T,
+ (∀ x y : T, x ∈ X → y ∈ X → x =_t y → x = y)
+ → ∀ x : T, compute_maximum X = Some x ↔ is_maximum x X.
+ Proof.
+ intros g Hmaxeq x. split; intros Hmax.
+ - unfold compute_maximum in Hmax.
+ assert (Heq: compute_maximals g = {[x]}).
+ { destruct (set_choose_or_empty (compute_maximals g)) as [eqn|eqn];
+ last by rewrite eqn in Hmax.
+ destruct (elements (compute_maximals g)) as [|h t] eqn:E1;
+ [|destruct t eqn:E2]; try done.
+ apply set_singleton_elements. by simplify_eq. } clear Hmax.
+ assert (Hin: x ∈ g).
+ { apply elem_of_compute_maximals. set_solver. }
+ split; first assumption.
+ intros t Htin Htne.
+ destruct (compute_maximals_bigger g t Htin) as (y & Hyn & Hle_ty).
+ rewrite Heq in Hyn. apply elem_of_singleton in Hyn. simplify_eq.
+ by apply TM_le_eq_or_lt in Hle_ty as [Heq_ty| Hlt_ty];
+ first by rewrite (Hmaxeq t x Htin Hin Heq_ty) in Htne.
+ - unfold compute_maximum. destruct Hmax as [Hin Hlt].
+ destruct (elements (compute_maximals g)) eqn: E.
+ { apply elements_empty_inv in E.
+ rewrite compute_maximals_empty in E. set_solver. }
+ destruct l.
+ * f_equal.
+ assert (x ∈ compute_maximals g) as Hxin%elem_of_elements.
+ { assert (t ∈ compute_maximals g)
+ as [Ht_in Ht_max]%compute_maximals_correct;
+ last assert (x = t) as ->.
+ - apply elem_of_elements. rewrite E. apply elem_of_list_here.
+ - destruct (decide(x = t)); first done.
+ apply Hmaxeq; try done.
+ destruct (Ht_max x Hin).
+ by apply Hlt.
+ - apply elem_of_elements. rewrite E. apply elem_of_list_here. }
+ rewrite E in Hxin. set_solver.
+ * exfalso. (** replace s ans s0 with x*)
+ assert (H1: t ∈ elements (compute_maximals g)).
+ { rewrite E. apply elem_of_list_here. }
+ assert (H2: t0 ∈ elements (compute_maximals g)).
+ { rewrite E. apply elem_of_list_further, elem_of_list_here. }
+ destruct (compute_maximals_spec_1 g t)
+ as [Hsing Hs]; first by apply elem_of_elements in H1.
+ destruct (compute_maximals_spec_1 g t0)
+ as [Hs0ing Hs0]; first by apply elem_of_elements in H2.
+ apply (Hs x); first assumption.
+ apply (Hlt t); first assumption.
+ intros Hsx.
+ apply (Hs0 x); first assumption.
+ apply (Hlt t0); first assumption.
+ intros Hs0x.
+ simplify_eq.
+ pose (NoDup_elements (compute_maximals g)) as Hyp.
+ replace (elements (compute_maximals g)) with (x :: x :: l) in Hyp.
+ apply NoDup_cons_1_1 in Hyp.
+ apply Hyp, elem_of_list_here.
+ Qed.
+
+
+
+ Global Instance maximals_computing : Maximals_Computing T:=
+ {|
+ Maximals := λ g, compute_maximals g;
+ Maximum := λ g, compute_maximum g;
+ Maximals_correct := compute_maximals_correct;
+ Maximum_correct := compute_maximum_correct |}.
+End ComputeMaximals.
+
+Section UsefulLemmas.
+ Context {T: Type}.
+ Context `{
+ !EqDecision T, !Countable T,
+ !Log_Time, !Timed T,
+ !RelDecision TM_lt}.
+
+ Lemma maximals_union (X Y: gset T) (x: T):
+ x ∈ compute_maximals (X ∪ Y)
+ → (x ∈ compute_maximals X ∨ x ∈ compute_maximals Y).
+ Proof.
+ intros Hx_in.
+ assert (x ∈ compute_maximals (X ∪ Y))
+ as [Hyp|Hyp]%elem_of_compute_maximals%elem_of_union;
+ first assumption;
+ [left|right];
+ apply compute_maximals_spec in Hx_in as [Hin Hmax];
+ apply compute_maximals_spec; (split; first assumption);
+ intros y Hy;
+ apply Hmax;
+ set_solver.
+ Qed.
+
+ Lemma compute_maximum_empty:
+ compute_maximum (∅: gset T) = None.
+ Proof. reflexivity. Qed.
+
+ Lemma compute_maximals_simgleton (t: T):
+ compute_maximals ({[ t ]}: gset T) = ({[ t ]}: gset T).
+ Proof.
+ unfold compute_maximals.
+ apply set_eq.
+ intros x; split.
+ - by intros [_ Hx_in]%elem_of_filter.
+ - intros ->%elem_of_singleton.
+ apply elem_of_filter; split.
+ + intros y ->%elem_of_singleton. apply TM_lt_irreflexive.
+ + by apply elem_of_singleton.
+ Qed.
+
+ Lemma compute_maximum_simgleton (t: T):
+ compute_maximum {[ t ]} = Some t.
+ Proof.
+ unfold compute_maximum.
+ by rewrite compute_maximals_simgleton, elements_singleton.
+ Qed.
+
+ Lemma compute_maximals_non_empty {X: gset T} {x: T}
+ (_: x ∈ X): compute_maximals X ≠∅.
+ Proof.
+ intros Hcm_empty.
+ pose proof (compute_maximals_empty X).
+ set_solver.
+ Qed.
+
+ Lemma set_singleton_eq (X: gset T) (x: T):
+ (x ∈ X ∧ (∀ y, y ∈ X → y = x)) ↔ X = {[ x ]}.
+ Proof. set_solver. Qed.
+
+ Lemma compute_maximum_non_empty (X: gset T):
+ (∀ (x y: T), x ∈ X → y ∈ X → x <_t y ∨ x =_t y ∨ y <_t x)
+ → (∀ (x y: T), x ∈ X → y ∈ X → x =_t y → x = y)
+ → (X ≠∅ ↔ (∃ (m: T), compute_maximum X = Some m)).
+ Proof.
+ intros Hcomp Hext. split.
+ - intros [m Hm_in]%set_choose_L.
+ pose proof (compute_maximals_non_empty Hm_in) as [o [Ho_in Ho_max]%compute_maximals_correct]%set_choose_L.
+ exists o.
+ unfold compute_maximum.
+ assert (compute_maximals X = {[ o ]}) as ->.
+ { apply set_singleton_eq.
+ split; first by apply compute_maximals_correct.
+ intros n [Hn_in Hn_max]%compute_maximals_correct.
+ pose proof (Hcomp o n Ho_in Hn_in) as [Himp | [Heq | Himp]].
+ - exfalso. by apply (Ho_max n).
+ - by apply Hext.
+ - exfalso. by apply (Hn_max o). }
+ by rewrite elements_singleton.
+ - intros [m [Hm_in Hm_max]%compute_maximum_correct];
+ first set_solver.
+ exact Hext.
+ Qed.
+
+ Lemma compute_maximum_empty' `{!LeibnizEquiv (gset T)} :
+ compute_maximum (∅: gset T) = None.
+ Proof.
+ unfold compute_maximum, compute_maximals.
+ rewrite filter_empty_L; last assumption.
+ by rewrite elements_empty.
+ Qed.
+End UsefulLemmas.
+
diff --git a/aneris/examples/crdt/statelib/time/time.v b/aneris/examples/crdt/statelib/time/time.v
new file mode 100644
index 0000000..374d392
--- /dev/null
+++ b/aneris/examples/crdt/statelib/time/time.v
@@ -0,0 +1,56 @@
+From stdpp Require Import gmap.
+From aneris.examples.crdt.spec Require Import crdt_time.
+From aneris.examples.crdt.statelib.proof Require Import utils.
+
+Section Time.
+ Definition ts_le (ts1 ts2 : Timestamp) : Prop :=
+ ts1 ⊆ ts2.
+
+ Definition ts_lt := strict ts_le.
+
+ Lemma ts_lt_irreflexive: ∀ x: Timestamp, ~ ts_lt x x.
+ Proof. by intros s [H H']. Qed.
+ Lemma ts_lt_trans: ∀ x y z, ts_lt x y → ts_lt y z → ts_lt x z.
+ Proof. set_solver. Qed.
+ Lemma ts_lt_TM_le: ∀ x x', ts_lt x x' → ts_le x x'.
+ Proof. exact strict_include. Qed.
+
+ Lemma ts_le_eq_or_lt: ∀ x x', ts_le x x' → x = x' ∨ ts_lt x x'.
+ Proof.
+ intros ???.
+ destruct (set_subseteq_inv x x' H);
+ [by right | left; by apply set_eq].
+ Qed.
+
+ Lemma ts_le_lt_trans:
+ ∀ t t' t'' : Timestamp,
+ ts_le t t' → ts_lt t' t'' → ts_lt t t''.
+ Proof. set_solver. Qed.
+
+ Lemma ts_lt_le_trans:
+ ∀ t t' t'' : Timestamp,
+ ts_lt t t' → ts_le t' t'' → ts_lt t t''.
+ Proof. set_solver. Qed.
+
+ Global Instance ts_le_trans: Transitive ts_le.
+ Proof. intros?. set_solver. Qed.
+ Global Instance ts_le_refl: Reflexive ts_le.
+ Proof. intros ?. set_solver. Qed.
+
+ Global Instance ts_lt_asym: Asymmetric ts_lt.
+ Proof. intros?. set_solver. Qed.
+
+ Global Instance timestamp_time : Log_Time :=
+ {| Time := Timestamp;
+ TM_le := ts_le;
+ TM_le_PO := set_subseteq_partialorder;
+ TM_lt := ts_lt;
+ TM_lt_irreflexive := ts_lt_irreflexive;
+ TM_lt_trans := ts_lt_trans;
+ TM_le_eq_or_lt := ts_le_eq_or_lt;
+ TM_lt_TM_le := ts_lt_TM_le;
+ TM_le_lt_trans := ts_le_lt_trans;
+ TM_lt_le_trans := ts_lt_le_trans
+ |}.
+
+End Time.
--
GitLab