Commit cf17ca4c authored by Hai Dang's avatar Hai Dang

update to support iris.dev and coq.dev

parent 0652693e
Pipeline #14282 failed with stage
in 15 minutes and 59 seconds
......@@ -74,13 +74,12 @@ Section hashtable.
Definition const := 654435761.
Instance hf1 : hash_fun := { size := Z.to_nat 16384; hash i := Z.to_nat ((i * const) mod 16384) }.
Proof.
- hnf.
by apply (Z2Nat.inj_le 1 16384); compute.
- intro.
lapply (Z_mod_lt (i * const) 16384); last by compute.
by intros []; split; [apply (Z2Nat.inj_le 0) | apply (Z2Nat.inj_lt _ 16384)].
Program Instance hf1 : hash_fun :=
{ size := Z.to_nat 16384; hash i := Z.to_nat ((i * const) mod 16384) }.
Next Obligation. hnf. by apply (Z2Nat.inj_le 1 16384); compute. Defined.
Next Obligation.
intro. lapply (Z_mod_lt (i * const) 16384); last by compute.
by intros []; split; [apply (Z2Nat.inj_le 0) | apply (Z2Nat.inj_lt _ 16384)].
Defined.
Definition integer_hash : val := λ: "i", "i" * #654435761.
......@@ -182,30 +181,35 @@ Qed.
Instance zero_unit : Unit ZC := 0.
Instance zero_join : Join zero_ord :=
Program Instance zero_join : Join zero_ord :=
{ join a b := if decide (a = 0) then Some b else if decide (b = 0) then Some a
else if decide (a = b) then Some a else None }.
Proof.
- constructor; first constructor; repeat intro; unfold zero_ord in *; auto.
+ destruct H, H0; subst; auto.
+ destruct H, H0; subst; auto.
- constructor; auto.
- intros.
destruct (decide (a = 0)), (decide (b = 0)); last (destruct (decide (a = b))); inversion H;
subst; eauto; destruct (decide (c = 0)); subst; eauto; try done.
destruct (decide _); last destruct (decide _); inversion H0; subst; do 2 eexists; eauto;
destruct (decide _); auto; rewrite decide_left; auto.
- repeat intro.
Next Obligation.
constructor; first constructor; repeat intro; unfold zero_ord in *; auto.
- destruct H, H0; subst; auto.
- destruct H, H0; subst; auto. Qed.
Next Obligation. constructor; auto. Qed.
Next Obligation. intros ???? ?. simpl.
destruct (decide (a = 0)), (decide (b = 0)); last (destruct (decide (a = b)));
intros H; inversion H;
subst; eauto; destruct (decide (c = 0)); subst; eauto; try done.
destruct (decide _); last destruct (decide _); intros H0; inversion H0; subst;
do 2 eexists; eauto;
destruct (decide _); auto; rewrite decide_left; auto. Qed.
Next Obligation.
repeat intro.
destruct (decide _), (decide _); subst; auto.
destruct (decide _), (decide _); subst; auto; done.
- intros.
unfold zero_ord.
destruct (decide _); subst; auto.
destruct (decide _); last destruct (decide _); inversion H; auto.
- unfold zero_ord; intros; destruct (decide _); auto.
destruct H; [contradiction | subst].
destruct (decide _); auto.
rewrite decide_left; auto.
destruct (decide _), (decide _); subst; auto; done. Qed.
Next Obligation.
intros ???. simpl.
unfold zero_ord.
destruct (decide _); subst; auto.
destruct (decide _); last destruct (decide _); intros H; inversion H; auto. Qed.
Next Obligation.
unfold zero_ord; intros; destruct (decide _); auto.
destruct H; [contradiction | subst].
destruct (decide _); auto.
rewrite decide_left; auto.
Qed.
Section Interpretation.
......
......@@ -98,34 +98,39 @@ Qed.
End gmaps.
Instance hist_join (A : ofeT) {D : OfeDiscrete A} {L : LeibnizEquiv A} {U : Unit A} `{EqDecision A} : Join
(fun (a b : gmapC nat A) => map_subseteq(M := gmap nat)(A := A) a b) :=
Program Instance hist_join (A : ofeT) {D : OfeDiscrete A} {L : LeibnizEquiv A}
{U : Unit A} `{EqDecision A} :
Join (fun (a b : gmapC nat A) => map_subseteq(M := gmap nat)(A := A) a b) :=
{ join (m1 m2 : gmapC nat A) := if decide (compatible m1 m2)
then Some (union m1 m2) else None }.
Proof.
- repeat intro.
rewrite lookup_empty; destruct (a !! i) eqn: Ha; rewrite Ha; done.
- intros ?????; destruct (decide _); last discriminate.
destruct (decide _); last discriminate.
intros Ha Hb; inversion Ha; inversion Hb; subst.
exists (a d).
destruct (decide _).
split; auto.
assert (compatible b a) by (rewrite comm; done).
destruct (decide _).
rewrite fin_maps.Assoc_instance_0 (compatible_union_comm b a); auto.
{ contradiction n; apply compatible_union_assoc; auto.
rewrite compatible_union_comm; auto. }
{ contradiction n.
eapply compatible_subset; eauto.
apply (map_union_subseteq_l a b). }
- repeat intro.
destruct (decide _), (decide _); auto; first (rewrite compatible_union_comm; auto);
contradiction n; rewrite compatible_comm; auto.
- intros.
destruct (decide _); inversion H; subst.
apply (map_union_subseteq_l a b).
- intros.
destruct (decide _); [|contradiction n; apply subset_compatible; auto].
apply f_equal, (map_subseteq_union a b); auto.
Qed.
Next Obligation.
repeat intro.
rewrite lookup_empty; destruct (a !! i) eqn: Ha; rewrite Ha; done. Qed.
Next Obligation.
intros ??????????. simpl.
destruct (decide _); last discriminate.
destruct (decide _); last discriminate.
intros Ha Hb; inversion Ha; inversion Hb; subst.
exists (a d).
destruct (decide _).
split; auto.
assert (compatible b a) by (rewrite comm; done).
destruct (decide _).
rewrite fin_maps.Assoc_instance_0 (compatible_union_comm b a); auto.
{ contradiction n; apply compatible_union_assoc; auto.
rewrite compatible_union_comm; auto. }
{ contradiction n.
eapply compatible_subset; eauto.
apply (map_union_subseteq_l a b). } Qed.
Next Obligation.
repeat intro.
destruct (decide _), (decide _); auto; first (rewrite compatible_union_comm; auto);
contradiction n; rewrite compatible_comm; auto. Qed.
Next Obligation.
intros ????????. simpl.
destruct (decide _); intros H; inversion H; subst.
apply (map_union_subseteq_l a b). Qed.
Next Obligation.
intros. simpl.
destruct (decide _); [|contradiction n; apply subset_compatible; auto].
apply f_equal, (map_subseteq_union a b); auto. Qed.
......@@ -31,7 +31,6 @@ Program Definition read : val := @RecV <> "n" (λ: "out",
let: "v" := ["n" + #version]_at in
if: "v" = "snap" then #() else "f" #()) #()) _.
Next Obligation.
Proof.
apply I.
Qed.
......@@ -42,7 +41,6 @@ Program Definition write : val := @RecV <> "n" (λ: "in",
["n" + #data + "i"]_at <- ["in" + "i"]_na);;
["n" + #version]_at <- ("v" + #2)) _.
Next Obligation.
Proof.
apply I.
Qed.
......@@ -53,7 +51,6 @@ Program Definition make_node : val := @RecV <> <>
["n" + #data + "i"]_na <- #0);;
"n") _.
Next Obligation.
Proof.
apply I.
Qed.
......@@ -82,19 +79,15 @@ Instance versionPrt_facts : protocol_facts versionProtocol.
Proof. esplit; apply _.
Qed.
Instance version_join : Join le := { join a b := Some (max a b) }.
Proof.
- apply Nat.le_0_l.
- intros ????? Hc He; inversion Hc; inversion He; subst.
do 2 eexists; eauto.
by rewrite Max.max_assoc (Max.max_comm a b).
- intros ??.
by rewrite Max.max_comm.
- intros ??? X; inversion X.
apply Nat.le_max_l.
- intros.
by rewrite Max.max_r.
Qed.
Program Instance version_join : Join le := { join a b := Some (max a b) }.
Next Obligation. apply Nat.le_0_l. Qed.
Next Obligation.
intros ????? Hc He; inversion Hc; inversion He; subst.
do 2 eexists; eauto.
by rewrite Max.max_assoc (Max.max_comm a b). Qed.
Next Obligation. intros ??. by rewrite Max.max_comm. Qed.
Next Obligation. intros ??? X; inversion X. apply Nat.le_max_l. Qed.
Next Obligation. intros. simpl. by rewrite Max.max_r. Qed.
Definition log_latest {A} (m : gmap nat A) n v := m !! n = Some v /\
forall n', is_Some (m !! n') <-> even n' = true /\ (n' <= n)%nat.
......
......@@ -30,9 +30,8 @@ Section RCUData.
Proof. intros [] []; naive_solver. Qed.
Global Instance AbsLoc_eqdec : EqDecision AbsLoc := inj_eq_dec AbsLoc_to_sum.
Global Instance AbsLoc_countable: Countable AbsLoc
:= inj_countable AbsLoc_to_sum (Some sum_to_AbsLoc) _.
Proof. by destruct 0. Qed.
Global Instance AbsLoc_countable: Countable AbsLoc.
Proof. refine (inj_countable AbsLoc_to_sum (Some sum_to_AbsLoc) _); by intros []. Qed.
Definition RCUInfo : Type := list (aloc * loc * gname).
Definition RCUHist : Type := list (aloc * AbsLoc).
......
......@@ -241,7 +241,7 @@ Section RAMachine.
_ : pairwise_disj msgs
}.
Definition memory_ok : M, pairwise_disj M.(msgs) := ltac:(by destruct 0).
Definition memory_ok : M, pairwise_disj M.(msgs) := ltac:(by intros []).
Program Definition add_ins (M : memory) m : MS_msg_disj M m -> memory :=
fun H => mkMemory (msgs M {[m]}) _.
......@@ -302,7 +302,7 @@ Section RAMachine.
move => ? ? /elem_of_empty [].
Qed.
Global Instance state_Inhabited : Inhabited state := _.
Global Instance state_Inhabited : Inhabited state.
Proof.
do 2!econstructor; exact: inhabitant.
Qed.
......@@ -938,16 +938,16 @@ Section RAMachine.
simpl in HAcc; try by (simplify_option_eq; tauto);
try (rewrite LT in LV; inversion LV; subst; clear LV);
(apply Lt in LT || apply Lt in LV); try by [].
- move => m /elem_of_union [|/elem_of_singleton ->] /=;
last (by inversion 0);
move => In Eq; move : (DInv _ In Eq); intros [[HMax]|];
- move => m /elem_of_union [|/elem_of_singleton ->] /= In;
last (by inversion In);
move => Eq; move : (DInv _ In Eq); intros [[HMax]|];
[left|right; exact: dealloc_inv_helper1].
case: (decide (x0 = mloc m)) => [Eqx0|NEqx0];
last exact: dealloc_inv_helper2.
subst. exfalso. eapply max_D_not_allocated => //.
- move => m /elem_of_union [|/elem_of_singleton ->] /=;
last (by inversion 0);
move => In Eq; move : (DInv _ In Eq); intros [[HMax]|];
- move => m /elem_of_union [|/elem_of_singleton ->] /= In;
last (by inversion In);
move => Eq; move : (DInv _ In Eq); intros [[HMax]|];
[left|right; exact: dealloc_inv_helper1].
case: (decide (x0 = mloc m)) => [Eqx0|NEqx0];
last exact: dealloc_inv_helper2.
......
......@@ -63,13 +63,13 @@ Section Exclusive.
iIntros (?) "[H _] /=". iDestruct "H" as (?) "?". iExists _. eauto.
Qed.
Global Instance valloc_local_timeless Σ h : Timeless (@valloc_local Σ h).
Global Instance valloc_local_timeless h : Timeless (@valloc_local Σ h).
Proof.
rewrite valloc_local_eq /valloc_local_def /= /Timeless. iStartProof (uPred _).
iIntros (?) "/=". iApply timeless.
Qed.
Global Instance valloc_local_Persistent Σ h : Persistent (@valloc_local Σ h).
Global Instance valloc_local_Persistent h : Persistent (@valloc_local Σ h).
Proof.
rewrite valloc_local_eq /valloc_local_def /= /Persistent. iStartProof (uPred _).
iIntros (?) "/=". iApply persistent.
......
......@@ -39,14 +39,12 @@ Section Definitions.
Proof. by intros [] [] ?; simplify_eq/=. Qed.
Global Instance Val_dec_eq : EqDecision Val := inj_eq_dec val_to_sum.
Global Instance Val_countable : Countable Val :=
inj_countable val_to_sum (Some sum_to_val) _.
Proof. by destruct 0. Qed.
Global Instance Val_countable : Countable Val.
Proof. refine (inj_countable val_to_sum (Some sum_to_val) _); by intros []. Qed.
Global Instance msg_dec_eq : EqDecision message := inj_eq_dec msg_to_tuple.
Global Instance msg_countable : Countable message :=
inj_countable msg_to_tuple (Some tuple_to_msg) _.
Proof. by destruct 0. Qed.
Global Instance msg_countable : Countable message.
Proof. refine (inj_countable msg_to_tuple (Some tuple_to_msg) _); by intros []. Qed.
Implicit Type (x t : positive) (R V : View) (m : message).
......@@ -89,9 +87,8 @@ Section Definitions.
Proof. intros [] []; naive_solver. Qed.
Global Instance access_dec_eq : EqDecision access | 20 := inj_eq_dec acc_to_sum.
Global Instance access_countable : Countable access | 20 :=
inj_countable acc_to_sum (Some sum_to_acc) _.
Proof. by destruct 0. Qed.
Global Instance access_countable : Countable access | 20.
Proof. refine (inj_countable acc_to_sum (Some sum_to_acc) _); by intros []. Qed.
End Glue.
......
Markdown is supported
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