From 099eb48af7f8891c87df6ed838ae24e8828b6d62 Mon Sep 17 00:00:00 2001
From: Zhen Zhang <izgzhen@gmail.com>
Date: Fri, 9 Sep 2016 11:39:15 +0200
Subject: [PATCH] cleanups
---
srv.v | 15 ---------------
sync.v | 2 +-
2 files changed, 1 insertion(+), 16 deletions(-)
diff --git a/srv.v b/srv.v
index ed42605..c6ec99e 100644
--- a/srv.v
+++ b/srv.v
@@ -34,22 +34,7 @@ Definition mk_srv : val :=
release "l";;
"ret".
-(* play with some algebraic structure to see what fit ... *)
-
Definition srvR := prodR fracR (dec_agreeR val).
-
-Lemma srv_coincide: ∀ (x1 x2: val) (q1 q2: Qp), ✓ ((q1, DecAgree x1) ⋅ (q2, DecAgree x2)) → x1 = x2.
-Proof.
- intros x1 x2 q1 q2 H. destruct (decide (x1 = x2))=>//.
- exfalso. destruct H as [H1 H2].
- simpl in H2. apply dec_agree_op_inv in H2.
- by inversion H2.
-Qed.
-
-Lemma srv_update: ∀ (x1 x2: val), (1%Qp, DecAgree x1) ~~> (1%Qp, DecAgree x2).
-Proof. intros. by apply cmra_update_exclusive. Qed.
-
-(* define the gFunctors *)
Class srvG Σ := FlatG { srv_tokG :> inG Σ srvR }.
Definition srvΣ : gFunctors := #[GFunctor (constRF srvR)].
diff --git a/sync.v b/sync.v
index 0d40bb0..9b6111d 100644
--- a/sync.v
+++ b/sync.v
@@ -106,7 +106,7 @@ Section generic.
Definition gFrag (γ: gname) g : iProp Σ := own γ (gFragR g).
Definition gFull (γ: gname) g : iProp Σ := own γ (gFullR g).
- Global Instance frag_timeless γ g: TimelessP (@own Σ syncR sync_tokG γ (gFragR g)).
+ Global Instance frag_timeless γ g: TimelessP (gFrag γ g).
Proof. apply _. Qed.
Global Instance full_timeless γ g: TimelessP (gFull γ g).
--
GitLab