Commit 5c00b6bf authored by Hai Dang's avatar Hai Dang
Browse files

removed some warnings

parent cc9827c0
......@@ -5,12 +5,12 @@ Canonical Structure natProtocol : protocolT := ProtocolT _ le.
Instance natPrt_facts : protocol_facts (natProtocol).
Proof. esplit; apply _. Qed.
Canonical Structure boolProtocol : protocolT := ProtocolT bool (implb).
Definition boolProtocol : protocolT := ProtocolT _ implb.
Instance boolPrt_facts : protocol_facts (boolProtocol).
Proof. esplit; try apply _; [by intros []|by intros [] [] []]. Qed.
Canonical Structure unitProtocol : protocolT := ProtocolT unit (λ _ _, True).
Definition unitProtocol : protocolT := ProtocolT unit (λ _ _, True).
Instance unitPrt_facts : protocol_facts (unitProtocol).
Proof. esplit; apply _. Qed.
\ No newline at end of file
......@@ -33,6 +33,53 @@ Import uPred.
Specifically, they are always fixed to a certain view.
*)
Canonical Structure RCULinkProtocol : protocolT
:= ProtocolT (list AbsLoc) suffix.
Instance RCULinkPrt_facts : protocol_facts (RCULinkProtocol).
Proof. esplit; apply _. Qed.
Canonical Structure RCUCounterProtocol : protocolT
:= ProtocolT (RCUData * nat)
(λ p1 p2, (p1 = p2) (p1.1 p2.1 (p1.2 < p2.2)%nat)).
Instance RCUCounterPrt_facts : protocol_facts (RCUCounterProtocol).
Proof.
esplit; try apply _.
- by left.
- intros ? ? ? [|[]] [|[]]; subst.
+ by left.
+ by right.
+ by right.
+ right. split; by etrans.
Qed.
Record RCUGhost :=
mkRCUGhost {
lhd :> loc;
history :> gname;
wxtok :> gname;
rxtok :> gname;
txtok :> gname;
}.
Canonical Structure RCUGhostC := leibnizC RCUGhost.
Definition RCUGhost_to_tuple : RCUGhost _
:= λ al, match al with mkRCUGhost l h w r t => (l,h,w,r,t) end.
Definition tuple_to_RCUGhost : _ RCUGhost
:= λ t, match t with (l,h,w,r,t) => mkRCUGhost l h w r t end.
Instance RCUGhost_EqDec : EqDecision RCUGhost :=
inj_dec_eq RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
Proof. by destruct 0. Qed.
Instance RCUGhost_Countable: Countable RCUGhost :=
inj_countable RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
Proof. by destruct 0. Qed.
Section RCU.
Context (n: positive).
......@@ -139,51 +186,6 @@ Section RCU.
["np"]_na <- "p'" ;;
#0.
Canonical Structure RCULinkProtocol : protocolT
:= ProtocolT (list AbsLoc) suffix.
Instance RCULinkPrt_facts : protocol_facts (RCULinkProtocol).
Proof. esplit; apply _. Qed.
Canonical Structure RCUCounterProtocol : protocolT
:= ProtocolT (RCUData * nat)
(λ p1 p2, (p1 = p2) (p1.1 p2.1 (p1.2 < p2.2)%nat)).
Instance RCUCounterPrt_facts : protocol_facts (RCUCounterProtocol).
Proof.
esplit; try apply _.
- by left.
- intros ? ? ? [|[]] [|[]]; subst.
+ by left.
+ by right.
+ by right.
+ right. split; by etrans.
Qed.
Record RCUGhost :=
mkRCUGhost {
lhd :> loc;
history :> gname;
wxtok :> gname;
rxtok :> gname;
txtok :> gname;
}.
Canonical Structure RCUGhostC := leibnizC RCUGhost.
Definition RCUGhost_to_tuple : RCUGhost _
:= λ al, match al with mkRCUGhost l h w r t => (l,h,w,r,t) end.
Definition tuple_to_RCUGhost : _ RCUGhost
:= λ t, match t with (l,h,w,r,t) => mkRCUGhost l h w r t end.
Global Instance RCUGhost_EqDec : EqDecision RCUGhost :=
inj_dec_eq RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
Proof. by destruct 0. Qed.
Global Instance RCUGhost_Countable: Countable RCUGhost :=
inj_countable RCUGhost_to_tuple (Some tuple_to_RCUGhost) _.
Proof. by destruct 0. Qed.
(* There are n+1 pieces, n for readers, and 1 for writer *)
Local Notation nf := (1 / (n+1))%Qp.
......
......@@ -230,7 +230,7 @@ Structure type_ofe :=
type_of_ofe : TTag ;
_ : ttagged (type_of_ofe) = ofe_car ofe_of_ofe
}.
Arguments type_of_ofe _.
(* Arguments type_of_ofe _. *)
Definition type_of_eq (to : type_ofe) : ttagged (type_of_ofe to) = ofe_car (ofe_of_ofe to) := ltac:(by destruct to).
Program Canonical type_of_interp Σ Prtcl : type_ofe :=
mkto (ointerp (interpC Σ Prtcl)) (tinterp (bool -> loc -> pr_state Prtcl -> Z -> @vPred Σ)) (Logic.eq_refl).
......@@ -337,7 +337,7 @@ Ltac unfold_lemma int :=
end
in unfold_lemma int.
Notation unf_int int := (ltac:(let e := unfold_lemma int in refine e)).
Notation unf_int int := (ltac:(let e := unfold_lemma int in refine e)) (only parsing).
Notation "'[rec' F ]" := (funC_fix _ (F : _ -> _) _).
......
......@@ -92,7 +92,7 @@ Arguments st_view [_] _ /.
(* Arguments sts.tok [_] _ /. *)
Arguments gpsG _ _ _ : clear implicits.
(* Arguments gpsG _ _ _ _ _ : clear implicits. *)
Arguments stateR _ _.
(* Arguments stateR _ _. *)
Section Setup.
......
......@@ -72,26 +72,26 @@ Lemma wp_bindi {E e} Ki Φ :
Proof. exact: weakestpre.wp_bind. Qed.
Instance uPred_entails_Proper {M} :
( T, Proper ((=) ==> () ==> iff) (@uPred_holds M T))
-> Proper (() ==> () ==> iff) (@uPred_entails M).
Proof.
intros. constructor; intros.
- rewrite -H0 -H1 //.
- rewrite H0 H1 //.
Qed.
(* Instance uPred_entails_Proper {M} : *)
(* ( T, Proper ((=) ==> () ==> iff) (@uPred_holds M T)) *)
(* -> Proper (() ==> () ==> iff) (@uPred_entails M). *)
(* Proof. *)
(* intros. constructor; intros. *)
(* - rewrite -H0 -H1 //. *)
(* - rewrite H0 H1 //. *)
(* Qed. *)
Lemma option_fmap_pair {A B : Type} {f o} {b b' : B} {a' : A} :
(λ a : A, (f a, b)) <$> o = Some (a', b') -> b' = b.
Proof. by destruct o => //= [[? ->]]. Qed.
Lemma foldl_pair {A B C : Type} {f : (A * C) -> B -> (A * C)} {ac} {l} :
( x y, (f y x) = ((f y x).1, y.2)) ->
foldl f ac l = ((foldl f ac l).1, snd ac).
Proof.
move => H. move : ac. elim: l => [//|? l /= IH].
- exact: surjective_pairing.
- move => ac. by rewrite H -IH.
Qed.
(* Lemma option_fmap_pair {A B : Type} {f o} {b b' : B} {a' : A} : *)
(* (λ a : A, (f a, b)) <$> o = Some (a', b') -> b' = b. *)
(* Proof. by destruct o => //= [[? ->]]. Qed. *)
(* Lemma foldl_pair {A B C : Type} {f : (A * C) -> B -> (A * C)} {ac} {l} : *)
(* ( x y, (f y x) = ((f y x).1, y.2)) -> *)
(* foldl f ac l = ((foldl f ac l).1, snd ac). *)
(* Proof. *)
(* move => H. move : ac. elim: l => [//|? l /= IH]. *)
(* - exact: surjective_pairing. *)
(* - move => ac. by rewrite H -IH. *)
(* Qed. *)
(* Lemma wp_thread (E : coPset) *)
(* (Φ : ra_lang.val iProp Σ) e: *)
......
......@@ -2,6 +2,8 @@ From igps.examples Require Import message_passing unit_token.
From igps.gps Require Import shared inst_shared.
From igps Require Import adequacy.
Section MP.
Let Σ : gFunctors := #[ baseΣ;
gpsΣ protocols.boolProtocol _ ;
gps_agreeΣ protocols.boolProtocol _;
......@@ -28,9 +30,11 @@ Proof.
last iMod (persistor_init with "PS") as (?) "#Pers".
{ by auto. }
iModIntro.
iApply (message_passing_spec with "* [%] PS Seen Pers").
iApply (message_passing_spec with "[%] PS Seen Pers").
{ reflexivity. }
iNext. iViewUp. iIntros (v) "? %". by subst.
Qed.
Print Assumptions message_passing.
\ No newline at end of file
Print Assumptions message_passing.
End MP.
\ No newline at end of file
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment