Commit d76571ee authored by Hai Dang's avatar Hai Dang

some cleanup

parent b2105b84
Pipeline #33556 passed with stage
in 3 minutes and 57 seconds
......@@ -211,5 +211,5 @@ End LocBlock.
Program Instance lblock_allocator `{@StateFacts lblock _ state} : Allocator lblock state :=
{| alloc := lblock_alloc;
dealloc := lblock_dealloc; |}.
Next Obligation. intros. inversion H0. by apply MAX. Qed.
Next Obligation. intros. inversion H0. by apply ALLOC. Qed.
Next Obligation. intros ????? Hl ??. inversion Hl. by apply MAX. Qed.
Next Obligation. intros ????? Hl ??. inversion Hl. by apply ALLOC. Qed.
......@@ -22,7 +22,7 @@ Section Memory.
end.
Global Instance baseMsg_dec_eq : EqDecision baseMessage.
Proof. refine (@inj_eq_dec _ _ _ _bMsg_to_tuple _); intros [][]; cbv; congruence. Qed.
Proof. solve_decision. Qed.
Global Instance baseMsg_countable : Countable baseMessage.
Proof. refine (inj_countable _bMsg_to_tuple (Some _tuple_to_bMsg) _); by intros []. Qed.
......@@ -39,9 +39,9 @@ Section Memory.
PartialOrder (() : SqSubsetEq baseMessage).
Proof.
constructor; [constructor|]; [done|..].
- intros [][][] [??] [??]. simpl in *.
- intros [][][] [][]. simpl in *.
constructor; [by subst|by etrans].
- intros [][] [??Le1][??Le2]. simpl in *. subst.
- intros [][] [][]. simpl in *. subst.
f_equal. by apply : (anti_symm ()).
Qed.
......
......@@ -44,8 +44,8 @@ Section Thread.
PartialOrder (() : SqSubsetEq global).
Proof.
constructor; [constructor|]; [done|..].
- intros [][][] [??] [??]. constructor; intros; by etrans.
- intros [][] [??][??]. simpl in *. f_equal; [|done|]; by apply : anti_symm.
- intros [][][] [][]. constructor; intros; by etrans.
- intros [][] [][]. simpl in *. f_equal; [|done|]; by apply : anti_symm.
Qed.
Record config_wf' c := {
......@@ -65,8 +65,8 @@ Section Thread.
PartialOrder (() : SqSubsetEq config).
Proof.
split; [split|]; [done|..].
- intros [][][] [??] [??]. split; by etrans.
- intros [][] [??][??]. simpl in *. f_equal; by apply : anti_symm.
- intros [][][] [][]. split; by etrans.
- intros [][] [][]. simpl in *. f_equal; by apply : anti_symm.
Qed.
(** Thread-local non-promising steps *)
......
......@@ -111,7 +111,7 @@ Section ThreadView.
split; [by split|] => ??? [????] [????]. constructor; by etrans.
Qed.
Next Obligation.
move => [????????] [????????] [????] [????]. apply threadView_eq; by apply: (anti_symm ()).
intros [][][][]. apply threadView_eq; by apply: (anti_symm ()).
Qed.
Next Obligation.
move => ??. split; simpl; try solve_lat.
......@@ -122,7 +122,7 @@ Section ThreadView.
move => ?. rewrite lookup_join. by apply lat_join_sqsubseteq_r.
Qed.
Next Obligation.
move => ??? [????] [????]. split; simpl; try solve_lat.
intros ??? [][]. split; simpl; try solve_lat.
move => ?. rewrite lookup_join. apply lat_join_lub; auto.
Qed.
Next Obligation.
......@@ -134,7 +134,7 @@ Section ThreadView.
move => ?. rewrite lookup_meet. by apply lat_meet_sqsubseteq_r.
Qed.
Next Obligation.
move => ??? [????] [????]. split; simpl; try solve_lat.
intros ??? [][]. split; simpl; try solve_lat.
move => ?. rewrite lookup_meet. apply lat_meet_glb; auto.
Qed.
......
......@@ -7,7 +7,12 @@ Section Val.
Inductive isval : (v : val), Prop := val_is_val v : isval (VVal v).
Lemma NEqADVal : AVal DVal. Proof. by inversion 1. Qed.
Lemma NEqADVal : AVal DVal. Proof. congruence. Qed.
Global Instance val_dec_eq : EqDecision val.
Proof. solve_decision. Qed.
Global Instance val_inhabited : Inhabited val := populate AVal.
Section ValCount.
Definition _val_to_sum (v : val): _ :=
......@@ -24,12 +29,6 @@ Section Val.
end.
End ValCount.
Global Instance val_dec_eq : EqDecision val.
Proof. refine (@inj_eq_dec _ _ _ _val_to_sum _); intros [] []; cbn; congruence. Qed.
Global Instance val_countable : Countable val.
Proof. refine (inj_countable _val_to_sum (Some _sum_to_val) _); by intros []. Qed.
Global Instance val_inhabited : Inhabited val.
Proof. exact : populate AVal. Qed.
End Val.
From orc11 Require Export location.
Set Default Proof Using "Type".
Notation time := (positive).
Notation time_id := (positive).
Notation time := (positive) (only parsing).
Notation time_id := (positive) (only parsing).
Notation time_ids := (gset time_id).
Instance time_ids_Countable : Countable time_ids.
Proof.
refine (inj_countable (mapset.mapset_car) (Some mapset.Mapset) _);
by move => [].
Qed.
Record timeInfo : Type := mkTimeInfo {
twrite : time;
tawrite: time_ids;
......@@ -23,6 +17,9 @@ Notation "[{ t , wa , rn , ra }]" :=
(at level 20, format "[{ t , wa , rn , ra }]",
t at level 21, wa at level 21, rn at level 21, ra at level 21) : stdpp_scope.
Instance timeInfo_dec_eq : EqDecision timeInfo.
Proof. solve_decision. Qed.
Section timeInfoCountable.
Definition _ti_tuple : Type := time * time_ids * time_ids * time_ids.
Definition _ti_to_tuple (ti: timeInfo) : _ti_tuple :=
......@@ -33,11 +30,6 @@ Section timeInfoCountable.
end.
End timeInfoCountable.
Instance timeInfo_dec_eq : EqDecision timeInfo.
Proof.
refine (@inj_eq_dec _ _ _ _ti_to_tuple _). intros [] []; cbv; congruence.
Qed.
Instance timeInfo_countable : Countable timeInfo.
Proof.
refine (inj_countable _ti_to_tuple (Some _tuple_to_ti) _); by intros [].
......@@ -62,13 +54,13 @@ Qed.
Next Obligation.
move => [????] [????] [?[?[??]]] [?[?[??]]]. f_equal; by apply : anti_symm.
Qed.
Next Obligation. move => [????] [????]. repeat split; simpl; solve_lat. Qed.
Next Obligation. move => [????] [????]. repeat split; simpl; solve_lat. Qed.
Next Obligation. intros [] []. repeat split; simpl; solve_lat. Qed.
Next Obligation. intros [] []. repeat split; simpl; solve_lat. Qed.
Next Obligation.
move => [????] [????] [????] [?[?[??]]] [?[?[??]]]. repeat split; solve_lat.
Qed.
Next Obligation. move => [????] [????]. repeat split; simpl; solve_lat. Qed.
Next Obligation. move => [????] [????]. repeat split; simpl; solve_lat. Qed.
Next Obligation. intros [] []. repeat split; simpl; solve_lat. Qed.
Next Obligation. intros [] []. repeat split; simpl; solve_lat. Qed.
Next Obligation.
move => [????] [????] [????] [?[?[??]]] [?[?[??]]]. repeat split; solve_lat.
Qed.
......@@ -83,8 +75,7 @@ Section View.
Context `{LocFacts loc}.
Definition view := gmap loc timeInfo.
(* FIXME this is not canonical, as it overlaps [gmap_Lat]. *)
Canonical Structure view_Lat := gmap_Lat loc timeInfo_Lat.
Definition view_Lat := gmap_Lat loc timeInfo_Lat.
Implicit Types (V: view).
Definition view_lookup_write: Lookup loc time view
......@@ -338,11 +329,11 @@ Section ViewLookup_more.
Proof.
rewrite {1}/sqsubseteq /lat_sqsubseteq /= /option_sqsubseteq.
split.
- destruct (V1 !! l) as [[????]|] eqn:Eq1;
destruct (V2 !! l) as [[????]|] eqn:Eq2;
- destruct (V1 !! l) as [[]|] eqn:Eq1;
destruct (V2 !! l) as [[]|] eqn:Eq2;
simplify_view; cbn; try done.
- destruct (V1 !! l) as [[????]|] eqn:Eq1;
destruct (V2 !! l) as [[????]|] eqn:Eq2;
- destruct (V1 !! l) as [[]|] eqn:Eq1;
destruct (V2 !! l) as [[]|] eqn:Eq2;
simplify_view; cbn; try done. intuition.
Qed.
End ViewLookup_more.
......@@ -351,10 +342,10 @@ Instance twrite_sqsubseteq_proper: Proper (sqsubseteq ==> sqsubseteq) twrite.
Proof. solve_proper. Qed.
Instance tawrite_sqsubseteq_proper: Proper (sqsubseteq ==> sqsubseteq) tawrite.
Proof. by intros [][] [?[?[??]]]. Qed.
Proof. by intros [][] [?[?[]]]. Qed.
Instance tnread_sqsubseteq_proper: Proper (sqsubseteq ==> sqsubseteq) tnread.
Proof. by intros [][] [?[?[??]]]. Qed.
Proof. by intros [][] [?[?[]]]. Qed.
Instance taread_sqsubseteq_proper: Proper (sqsubseteq ==> sqsubseteq) taread.
Proof. by intros [][] [?[?[??]]]. Qed.
Proof. by intros [][] [?[?[]]]. Qed.
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