Commit 68f95e02 by Jacques-Henri Jourdan

extension -> sqle

parent 1d375f24
Pipeline #4740 passed with stages
in 5 minutes 43 seconds
......@@ -77,13 +77,13 @@ Lemma Some_inv_wf `{Wellformed A} (a : A) {_: WellformedResolver (Some a)}
: WellformedResolver a.
Proof. done. Qed.
(** Extension and Join typeclasses, from iGPS development **)
(** Sqle and Join typeclasses **)
Class Extension A := extension : relation A.
Instance: Params (@extension) 2.
Infix "⊑" := extension (at level 70) : C_scope.
Notation "(⊑)" := extension (only parsing) : C_scope.
Notation "( X ⊑)" := (extension X) (only parsing) : C_scope.
Class Sqle A := sqle : relation A.
Instance: Params (@sqle) 2.
Infix "⊑" := sqle (at level 70) : C_scope.
Notation "(⊑)" := sqle (only parsing) : C_scope.
Notation "( X ⊑)" := (sqle X) (only parsing) : C_scope.
Notation "(⊑ X )" := (λ Y, Y X) (only parsing) : C_scope.
Infix "⊑*" := (Forall2 ()) (at level 70) : C_scope.
Notation "(⊑*)" := (Forall2 ()) (only parsing) : C_scope.
......@@ -92,11 +92,11 @@ Infix "⊑1*" := (Forall2 (λ p q, p.1 ⊑ q.1)) (at level 70) : C_scope.
Infix "⊑2*" := (Forall2 (λ p q, p.2 q.2)) (at level 70) : C_scope.
Infix "⊑1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : C_scope.
Infix "⊑2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : C_scope.
Instance Extension_Rewrite `{Extension T} : @RewriteRelation T ().
Instance sqle_Rewrite `{Sqle T} : @RewriteRelation T ().
Infix "⊏" := (strict extension) (at level 70) : C_scope.
Notation "(⊏)" := (strict extension) (only parsing) : C_scope.
Notation "( X ⊏)" := (extension X) (only parsing) : C_scope.
Infix "⊏" := (strict sqle) (at level 70) : C_scope.
Notation "(⊏)" := (strict sqle) (only parsing) : C_scope.
Notation "( X ⊏)" := (sqle X) (only parsing) : C_scope.
Notation "(⊏ X )" := (λ Y, Y X) (only parsing) : C_scope.
Infix "⊏*" := (Forall2 ()) (at level 70) : C_scope.
Notation "(⊏*)" := (Forall2 ()) (only parsing) : C_scope.
......@@ -105,7 +105,7 @@ Infix "⊏1*" := (Forall2 (λ p q, p.1 ⊏ q.1)) (at level 70) : C_scope.
Infix "⊏2*" := (Forall2 (λ p q, p.2 q.2)) (at level 70) : C_scope.
Infix "⊏1**" := (Forall2 (λ p q, p.1 * q.1)) (at level 70) : C_scope.
Infix "⊏2**" := (Forall2 (λ p q, p.2 * q.2)) (at level 70) : C_scope.
Instance Strict_Extension_Rewrite `{Extension T} : @RewriteRelation T ().
Instance Strict_sqle_Rewrite `{Sqle T} : @RewriteRelation T ().
(** Join Typeclasses **)
......@@ -122,10 +122,10 @@ Infix "⊔**" := (zip_with (zip_with (⊔)))
Infix "⊔*⊔**" := (zip_with (prod_zip () (*)))
(at level 50, left associativity) : C_scope.
Class JoinSemiLattice A `{Extension A, Join A} : Prop := {
Class JoinSemiLattice A `{Sqle A, Join A} : Prop := {
join_semi_lattice_pre :>> PreOrder ();
join_ext_l X Y : X X Y;
join_ext_r X Y : Y X Y;
join_sqle_l X Y : X X Y;
join_sqle_r X Y : Y X Y;
join_least X Y Z : X Z Y Z X Y Z
}.
......@@ -142,11 +142,11 @@ Ltac solve_jsl :=
| |- _ _ = _ => auto with jsl
end.
Hint Extern 0 (?x ?x) => reflexivity : jsl.
Hint Extern 0 (?x ?x _) => apply join_ext_l : jsl.
Hint Extern 0 (?x _ ?x) => apply join_ext_r : jsl.
Hint Extern 0 (?x ?x _) => apply join_sqle_l : jsl.
Hint Extern 0 (?x _ ?x) => apply join_sqle_r : jsl.
Hint Extern 2 (_ _ _) => apply join_least : jsl.
Hint Resolve join_ext_l : jsl.
Hint Resolve join_ext_r : jsl.
Hint Resolve join_sqle_l : jsl.
Hint Resolve join_sqle_r : jsl.
Hint Resolve join_least : jsl.
Lemma join_idempotent
......@@ -154,7 +154,7 @@ Lemma join_idempotent
: R x (x x).
Proof.
eapply anti_symm; eauto.
- by eapply join_ext_l.
- by eapply join_sqle_l.
- by eapply join_least.
Qed.
......@@ -162,11 +162,11 @@ Hint Extern 1 (?x = ?x ⊔ ?x) => apply join_idempotent : jsl.
Hint Extern 2 (_ = _ _) => apply (anti_symm ()) : jsl.
Hint Extern 2 (_ _ = _) => symmetry; apply (anti_symm ()) : jsl.
Instance JSL_Comm `{E : Extension A} `{J : Join A} `{@PartialOrder A ()}
Instance JSL_Comm `{E : Sqle A} `{J : Join A} `{@PartialOrder A ()}
`{@JoinSemiLattice A E J} : @Comm A _ (=) ().
Proof. move => ? ?. solve_jsl. Qed.
Instance JSL_Assoc `{E : Extension A} `{J : Join A} `{@PartialOrder A ()}
Instance JSL_Assoc `{E : Sqle A} `{J : Join A} `{@PartialOrder A ()}
`{@JoinSemiLattice A E J} : @Assoc A (=) ().
Proof.
move => ? ? ?.
......@@ -182,47 +182,47 @@ Instance JSL_join_proper `{JoinSemiLattice A}
: Proper (() ==> () ==> ()) ().
Proof. intros ? ? ? ? ? ?. apply join_least; etrans; eauto with jsl. Qed.
Lemma join_ext_mono_r `{JoinSemiLattice A}
Lemma join_sqle_mono_r `{JoinSemiLattice A}
(m1 m2 m3 : A) (Ex: m1 m2) :
m1 m3 m2 m3.
Proof.
apply join_least.
- etrans; last apply join_ext_l. done.
- apply join_ext_r.
- etrans; last apply join_sqle_l. done.
- apply join_sqle_r.
Qed.
Lemma join_ext_mono_l `{JoinSemiLattice A}
Lemma join_sqle_mono_l `{JoinSemiLattice A}
(m1 m2 m3 : A) (Ex: m1 m2) :
m3 m1 m3 m2.
Proof.
apply join_least.
- apply join_ext_l.
- etrans; last apply join_ext_r. done.
- apply join_sqle_l.
- etrans; last apply join_sqle_r. done.
Qed.
Lemma join_ext_eq_r `{JoinSemiLattice A} `{AntiSymm A (=) ()}
x y (Ext: x y) :
Lemma join_sqle_eq_r `{JoinSemiLattice A} `{AntiSymm A (=) ()}
x y (Sqle: x y) :
x y = y.
Proof.
apply : anti_symm; first by apply join_least.
apply join_ext_r.
apply join_sqle_r.
Qed.
Lemma join_ext_eq_l `{JoinSemiLattice A} `{AntiSymm A (=) ()}
x y (Ext: x y) :
Lemma join_sqle_eq_l `{JoinSemiLattice A} `{AntiSymm A (=) ()}
x y (Sqle: x y) :
y x = y.
Proof.
apply : anti_symm; first by apply join_least.
apply join_ext_l.
apply join_sqle_l.
Qed.
(** Extension and Join instances for product **)
(** Sqle and Join instances for product **)
Instance prod_Extension `{Extension A} `{Extension B} : Extension (A * B)
Instance prod_sqle `{Sqle A} `{Sqle B} : Sqle (A * B)
:= λ p1 p2, p1.1 p2.1 p1.2 p2.2.
Instance prod_PreOrder
`{Extension A} `{Extension B} `{PreOrder A ()} `{PreOrder B ()}
`{Sqle A} `{Sqle B} `{PreOrder A ()} `{PreOrder B ()}
: @PreOrder (A * B) ().
Proof.
econstructor.
......@@ -232,7 +232,7 @@ Proof.
+ by apply (PreOrder_Transitive _ _ _ H12 H22).
Qed.
Instance prod_PartialOrder `{Extension A} `{Extension B} `{PartialOrder A ()}
Instance prod_PartialOrder `{Sqle A} `{Sqle B} `{PartialOrder A ()}
`{PartialOrder B ()} : @PartialOrder (A * B) ().
Proof.
econstructor.
......@@ -252,9 +252,9 @@ Proof.
- move => ? ?; split => /=; solve_jsl.
- move => ? ? ? [? ?] [? ?]. split => /=; solve_jsl.
Qed.
Instance prod_extension_dec
`{Extension A} `{ a a' : A, Decision (a a')}
`{Extension B} `{ a a' : B, Decision (a a')} :
Instance prod_sqle_dec
`{Sqle A} `{ a a' : A, Decision (a a')}
`{Sqle B} `{ a a' : B, Decision (a a')} :
ab ab' : (A * B), Decision (ab ab').
Proof.
move => ab ab'.
......@@ -264,9 +264,9 @@ Proof.
Qed.
(** Extension and Join instances for option **)
(** Sqle and Join instances for option **)
Instance option_Extension `{Extension T} : Extension (option T) :=
Instance option_sqle `{Sqle T} : Sqle (option T) :=
λ o1 o2, match o1 with
| None => True
| Some t1 => match o2 with
......@@ -293,7 +293,7 @@ Proof. by move => [?|]. Qed.
Instance join_left_None `{Join T} : LeftId eq None join.
Proof. by move => [?|]. Qed.
Instance option_PreOrder `{Extension T} `{PreOrder T ()} : @PreOrder (option T) ().
Instance option_PreOrder `{Sqle T} `{PreOrder T ()} : @PreOrder (option T) ().
Proof.
econstructor.
- move => ?; cbv; repeat case_match; last auto.
......@@ -302,7 +302,7 @@ Proof.
exact: PreOrder_Transitive.
Qed.
Instance option_PartialOrder `{Extension T} `{PartialOrder T ()}
Instance option_PartialOrder `{Sqle T} `{PartialOrder T ()}
: @PartialOrder (option T) ().
Proof.
econstructor.
......@@ -310,11 +310,11 @@ Proof.
- move => [?|] [?|] //; cbv => ? ?. f_equal. exact: anti_symm.
Qed.
Instance option_Reflexive `{Extension T} `{Reflexive T ()}
Instance option_Reflexive `{Sqle T} `{Reflexive T ()}
: @Reflexive (option T) ().
Proof. move => ?. cbv. by case_match. Qed.
Instance option_AntiSymm `{Extension T} `{AntiSymm T (=) ()}
Instance option_AntiSymm `{Sqle T} `{AntiSymm T (=) ()}
: AntiSymm (=) (() : relation (option T)).
Proof.
move => ? ?; cbv; repeat case_match => //; move => H1 H2. apply/f_equal.
......@@ -326,7 +326,7 @@ Proof.
move => ? ?; cbv; repeat case_match => //. f_equal. by apply comm.
Qed.
Instance option_Total `{Extension T} `{Total T ()}: (@Total (option T) ()).
Instance option_Total `{Sqle T} `{Total T ()}: (@Total (option T) ()).
Proof.
move => [?|] [?|]; eauto with jsl.
- by right.
......@@ -339,17 +339,17 @@ Proof.
econstructor.
- exact: option_PreOrder.
- move => ? ?. cbv; repeat case_match => //; simplify_option_eq.
+ by apply join_ext_l.
+ by apply join_sqle_l.
+ by apply PreOrder_Reflexive.
- move => ? ?. cbv; repeat case_match => //; simplify_option_eq.
+ by apply join_ext_r.
+ by apply join_sqle_r.
+ by apply PreOrder_Reflexive.
- move => ? ? ?; cbv; repeat case_match => //; simplify_option_eq.
by apply join_least.
Qed.
Instance option_extension_dec
`{Extension A} `{ a a' : A, Decision (a a')} :
Instance option_sqle_dec
`{Sqle A} `{ a a' : A, Decision (a a')} :
oa oa' : (option A), Decision (oa oa').
Proof.
move => [oa|] [oa'|].
......@@ -363,22 +363,22 @@ Instance option_equiv_reflexive `{Equiv A} `{Reflexive A equiv} :
@Reflexive (option A) equiv.
Proof. intros [|]; by constructor. Qed.
Instance option_ext_proper `{Extension A} `{Equiv A} `{!Equivalence (@equiv A _)}
`{!Proper (() ==> () ==> iff) (@extension A _)}:
Proper (() ==> () ==> iff) (@extension (option A) _).
Instance option_sqle_proper `{Sqle A} `{Equiv A} `{!Equivalence (@equiv A _)}
`{!Proper (() ==> () ==> iff) (@sqle A _)}:
Proper (() ==> () ==> iff) (@sqle (option A) _).
Proof.
move=>[?|][?|]EQ1[?|][?|]EQ2//=; inversion_clear EQ1; inversion_clear EQ2.
rewrite /extension /=. by setoid_subst.
rewrite /sqle /=. by setoid_subst.
Qed.
Instance option_equiv_AntiSymm `{Extension A} `{Equiv A} `{@AntiSymm A () ()}
Instance option_equiv_AntiSymm `{Sqle A} `{Equiv A} `{@AntiSymm A () ()}
: AntiSymm () (() : relation (option A)).
Proof.
move => ??; cbv; do 2 case_match => //; move => ??; constructor.
by apply (anti_symm ()).
Qed.
(** Extension and Join instances for gmap **)
(** Sqle and Join instances for gmap **)
Instance gmap_Join `{Countable K} `{Join A} : Join (gmap K A) :=
union_with (λ a1 a2, Some $ a1 a2).
......@@ -400,10 +400,10 @@ Proof.
move => ? ? ?. f_equal. by apply assoc.
Qed.
Instance gmap_Extension `{Countable K} `{Extension A} : Extension (gmap K A)
Instance gmap_sqle `{Countable K} `{Sqle A} : Sqle (gmap K A)
:= λ f1 f2, k, f1 !! k f2 !! k.
Instance gmap_PreOrder `{Countable K} `{Extension A} `{PreOrder A ()}
Instance gmap_PreOrder `{Countable K} `{Sqle A} `{PreOrder A ()}
: @PreOrder (gmap K A) ().
Proof.
econstructor.
......@@ -411,7 +411,7 @@ Proof.
- move => ? ? ? ? ? ?. by etransitivity; eauto.
Qed.
Instance gmap_PartialOrder `{Countable K} `{Extension A} `{PartialOrder A ()}
Instance gmap_PartialOrder `{Countable K} `{Sqle A} `{PartialOrder A ()}
: @PartialOrder (gmap K A) ().
Proof.
econstructor.
......@@ -423,13 +423,13 @@ Instance gmap_JSL `{Countable K} `{JoinSemiLattice A} : JoinSemiLattice (gmap K
Proof.
econstructor.
- exact: gmap_PreOrder.
- move => ? ? ?. rewrite lookup_join. by apply join_ext_l.
- move => ? ? ?. rewrite lookup_join. by apply join_ext_r.
- move => ? ? ?. rewrite lookup_join. by apply join_sqle_l.
- move => ? ? ?. rewrite lookup_join. by apply join_sqle_r.
- move => ? ? ? ? ? ?. rewrite lookup_join. by apply join_least.
Qed.
Instance gmap_extension_dec
`{Countable K} `{Extension A} `{ a a' : A, Decision (a a')} :
Instance gmap_sqle_dec
`{Countable K} `{Sqle A} `{ a a' : A, Decision (a a')} :
f f' : (gmap K A), Decision (f f').
Proof.
move => f f'.
......@@ -441,26 +441,26 @@ Proof.
- right.
apply not_set_Forall_Exists in N;
last eauto with typeclass_instances.
case : N => x [/elem_of_dom [a ?]] NExt ?.
by apply NExt.
case : N => x [/elem_of_dom [a ?]] NSqle ?.
by apply NSqle.
Qed.
Instance gmap_ext_proper `{Countable K} `{Extension A} `{Equiv A}
Instance gmap_sqle_proper `{Countable K} `{Sqle A} `{Equiv A}
`{!Equivalence (@equiv A _)}
`{!Proper (() ==> () ==> iff) (@extension A _)}:
Proper (() ==> () ==> iff) (@extension (gmap K A) _).
Proof. rewrite /extension /gmap_Extension=>??????. by setoid_subst. Qed.
`{!Proper (() ==> () ==> iff) (@sqle A _)}:
Proper (() ==> () ==> iff) (@sqle (gmap K A) _).
Proof. rewrite /sqle /gmap_sqle=>??????. by setoid_subst. Qed.
Instance gmap_equiv_ext_antisymm `{Countable K} `{Extension A} `{Equiv A}
Instance gmap_equiv_sqle_antisymm `{Countable K} `{Sqle A} `{Equiv A}
`{@AntiSymm A equiv ()}
: AntiSymm (@equiv (gmap K A) _) (@extension (gmap K A) _).
: AntiSymm (@equiv (gmap K A) _) (@sqle (gmap K A) _).
Proof. move => ?? E1 E2 ?. apply (anti_symm ()); [apply E1|apply E2]. Qed.
Instance gmap_ext_dom_proper `{Countable K} `{Extension A}:
Proper ((@extension (gmap K A) _) ==> ()) (dom (gset K)).
Instance gmap_sqle_dom_proper `{Countable K} `{Sqle A}:
Proper ((@sqle (gmap K A) _) ==> ()) (dom (gset K)).
Proof.
move => m1 m2 Ext k /elem_of_dom [a Eqa].
specialize (Ext k). rewrite Eqa in Ext.
move => m1 m2 Sqle k /elem_of_dom [a Eqa].
specialize (Sqle k). rewrite Eqa in Sqle.
destruct (m2 !! k) as [|] eqn:Eq2; last done.
apply elem_of_dom. by eexists.
Qed.
......@@ -473,9 +473,9 @@ Proof.
case (m1 !! k) => [v1|]; case (m2 !! k) => [v2|] /=; naive_solver.
Qed.
(** Extension and Join instances for Qp **)
(** Sqle and Join instances for Qp **)
Instance Qp_Extension : Extension Qp := ()%Qc.
Instance Qp_sqle : Sqle Qp := ()%Qc.
Instance Qp_Reflexive : Reflexive ()%Qp.
Proof. exact: Qcle_refl. Qed.
......@@ -516,10 +516,10 @@ Qed.
Instance gmap_key_filter `{Countable K} {A} : Filter K (gmap K A) :=
λ P _, filter (λ kv, P (kv.1)).
(* We restrict these to extensions to avoid divergence. *)
Instance flip_total `{Extension A} : Total () Total (flip ()).
(* We restrict these to s to avoid divergence. *)
Instance flip_total `{Sqle A} : Total () Total (flip ()).
Proof. move=>Ht x y. destruct (Ht y x); auto. Qed.
Instance flip_ext_antisymm `{Extension A} :
Instance flip_sqle_antisymm `{Sqle A} :
AntiSymm (=) () AntiSymm (=) (flip ()).
Proof. move=>?????. by apply (anti_symm ()). Qed.
......
......@@ -3,7 +3,7 @@ From promising Require Export base.
Inductive memOrder := | Plain | Relaxed | StrongRelaxed | AcqRel | SeqCst .
Instance memOrder_ext : Extension memOrder :=
Instance memOrder_sqle : Sqle memOrder :=
λ o1 o2,
match o1, o2 with
| Plain, _ => True
......@@ -32,7 +32,7 @@ Proof.
- move => [] []; firstorder.
Qed.
Instance memOrder_extension_dec : o1 o2 : memOrder, Decision (o1 o2).
Instance memOrder_sqle_dec : o1 o2 : memOrder, Decision (o1 o2).
Proof. move => [] []; firstorder. Qed.
Instance memOrder_join : Join memOrder :=
......
......@@ -36,7 +36,7 @@ Section Memory.
: WellformedResolver (m.(mrel)).
Proof. apply HW. Qed.
Global Instance baseMessage_ext : Extension baseMessage := eq.
Global Instance baseMessage_sqle : Sqle baseMessage := eq.
(* ======================================================================== *)
(** Cells are containers of messages per location,
......@@ -111,7 +111,7 @@ Section Memory.
C !! t' = C' !! t'.
Proof. inversion ADD. by rewrite lookup_insert_ne. Qed.
Lemma cell_addins_ext t m C C'
Lemma cell_addins_sqle t m C C'
(WF: wf C) (ADD: cell_addins t m C C') (WFt: wf (m.(mfrom),t]):
C C'.
Proof.
......@@ -201,7 +201,7 @@ Section Memory.
|rewrite lookup_insert_ne; last auto].
* apply adjacent_interval_disj.
* move => HL. rewrite TEQ.
apply (interval_ext_disj _ (m'.(mfrom), to']).
apply (interval_sqle_disj _ (m'.(mfrom), to']).
{ by apply WF. }
{ split; first done. by apply Qclt_le_weak. }
+ case (decide (to1 = to')) => [?|?];
......@@ -212,17 +212,17 @@ Section Memory.
rewrite lookup_insert_ne; last auto]).
* move => [<-] _. simpl. symmetry. apply adjacent_interval_disj.
* move => HL ?. rewrite lookup_insert_ne in HL; last auto.
apply (interval_ext_disj _ (m'.(mfrom), to']).
apply (interval_sqle_disj _ (m'.(mfrom), to']).
{ by apply WF. }
{ rewrite -TEQ. split; last done. by apply Qclt_le_weak. }
* move => HL [<-] _. rewrite TEQ.
symmetry. apply (interval_ext_disj _ (m'.(mfrom), to']).
symmetry. apply (interval_sqle_disj _ (m'.(mfrom), to']).
{ by apply WF. }
{ split; first done. by apply Qclt_le_weak. }
* case (decide (to2 = to')) => [?|?];
[subst to2; rewrite lookup_insert => HL [<-] _|
rewrite lookup_insert_ne; [apply WF|auto]].
symmetry. apply (interval_ext_disj _ (m'.(mfrom), to']).
symmetry. apply (interval_sqle_disj _ (m'.(mfrom), to']).
{ by apply WF. }
{ split; last done. rewrite -TEQ. by apply Qclt_le_weak. }
Qed.
......@@ -489,7 +489,7 @@ Section Memory.
case_match => Eqv.
eexists. eexists. repeat split; eauto.
- apply (cell_head_lookup (flip ())). by eauto.
- eapply (cell_head_top (flip (@extension Qp Qp_Extension))). by eauto.
- eapply (cell_head_top (flip (@sqle Qp Qp_sqle))). by eauto.
Qed.
Lemma cell_deallocated_correct2 C:
......@@ -983,10 +983,10 @@ Section Memory.
(** Proper instances *)
Global Instance closed_timemap_downclosed:
Proper ((@extension timeMap _) ==> (@eq memory) ==> flip impl) ().
Proper ((@sqle timeMap _) ==> (@eq memory) ==> flip impl) ().
Proof.
move => T1 T2 Ext M1 M2 -> In l t Eq2.
move : Ext => /(_ l). rewrite Eq2.
move => T1 T2 Sqle M1 M2 -> In l t Eq2.
move : Sqle => /(_ l). rewrite Eq2.
destruct (T2 !! l) as [to|] eqn:HT2; rewrite HT2; last done.
cbn => Le.
destruct (In _ _ HT2) as [m [to' [Le' Eq]]].
......@@ -994,15 +994,15 @@ Section Memory.
Qed.
Global Instance closed_view_downclosed:
Proper ((@extension view _) ==> (@eq memory) ==> flip impl) ().
Proper ((@sqle view _) ==> (@eq memory) ==> flip impl) ().
Proof.
move => ?? [Ext1 Ext2] ??-> [??]. split; by [rewrite Ext1|rewrite Ext2].
move => ?? [Sqle1 Sqle2] ??-> [??]. split; by [rewrite Sqle1|rewrite Sqle2].
Qed.
Global Instance opt_closed_view_downclosed:
Proper ((@extension (option view) _) ==> (@eq memory) ==> flip impl) ().
Proper ((@sqle (option view) _) ==> (@eq memory) ==> flip impl) ().
Proof.
move => [V1|] [V2|] Ext ??-> // In. move : Ext In. cbn => -> //.
move => [V1|] [V2|] Sqle ??-> // In. move : Sqle In. cbn => -> //.
Qed.
Lemma closed_timemap_wf_view (V : view) M (WF: wf V) (HC: V.(rlx) M):
......
......@@ -272,13 +272,13 @@ Section Wellformedness.
- eapply sc_fence_step_closed_sc; eauto. apply WF.
Qed.
(* threadView extension *)
Lemma acq_fence_step_tview_ext 𝓥 𝓥'
(* threadView sqle *)
Lemma acq_fence_step_tview_sqle 𝓥 𝓥'
(ACQ: acq_fence_step 𝓥 𝓥') (WF: wf 𝓥) :
𝓥 𝓥'.
Proof. inversion ACQ. constructor; [done|by apply WF|done]. Qed.
Lemma rel_fence_step_tview_ext L1 L2
Lemma rel_fence_step_tview_sqle L1 L2
(REL: rel_fence_step L1 L2) (WF: wf L1.(tv)) :
L1.(tv) L2.(tv).
Proof.
......@@ -296,7 +296,7 @@ Section Wellformedness.
by eexists.
Qed.
Lemma sc_fence_helper_tview_ext 𝓥 𝓥' 𝓢 𝓢'
Lemma sc_fence_helper_tview_sqle 𝓥 𝓥' 𝓢 𝓢'
(SC: sc_fence_helper 𝓥 𝓢 𝓥' 𝓢') (WF: wf 𝓥) :
𝓥 𝓥'.
Proof.
......@@ -304,7 +304,7 @@ Section Wellformedness.
set T' := 𝓥.(acq).(rlx) 𝓢.
set V' := mkView T' T'.
have ?: acq 𝓥 V'.
{ constructor; simpl; (etrans; last apply join_ext_l); [apply WF|done]. }
{ constructor; simpl; (etrans; last apply join_sqle_l); [apply WF|done]. }
rewrite EQSC; constructor; simpl; last done.
- move => l.
case (decide (l dom (gset _) T'))
......@@ -315,50 +315,50 @@ Section Wellformedness.
rewrite HE; last done. cbn. etrans; [apply WF|done].
+ destruct (rel 𝓥 !! l) as [t|] eqn:HRel; last done.
exfalso. apply NIn. rewrite gmap_join_dom_union elem_of_union. left.
apply (gmap_ext_dom_proper _ _ (view_ext_rlx _ _ (tview_wf_cur_acq _ WF))).
apply (gmap_sqle_dom_proper _ _ (view_sqle_rlx _ _ (tview_wf_cur_acq _ WF))).
apply (tview_wf_rel_dom _ WF), elem_of_dom. by eexists.
- etrans; [apply WF|done].
Qed.
Lemma sc_fence_step_tview_ext L1 𝓢1 L2 𝓢2
Lemma sc_fence_step_tview_sqle L1 𝓢1 L2 𝓢2
(SC: sc_fence_step L1 𝓢1 L2 𝓢2) (WF: wf L1.(tv)):
L1.(tv) L2.(tv).
Proof. inversion SC. by eapply sc_fence_helper_tview_ext. Qed.
Proof. inversion SC. by eapply sc_fence_helper_tview_sqle. Qed.
Lemma alloc_step_tview_ext 𝓥1 M1 l n 𝑚s 𝓥2 M2
Lemma alloc_step_tview_sqle 𝓥1 M1 l n 𝑚s 𝓥2 M2
(ALLOC: alloc_step 𝓥1 M1 l n 𝑚s 𝓥2 M2) :
𝓥1 𝓥2.
Proof. inversion ALLOC. by eapply alloc_helper_tview_ext. Qed.
Proof. inversion ALLOC. by eapply alloc_helper_tview_sqle. Qed.
Lemma dealloc_step_tview_ext 𝓥1 M1 l n 𝑚s 𝓥2 M2
Lemma dealloc_step_tview_sqle 𝓥1 M1 l n 𝑚s 𝓥2 M2
(DEALLOC: dealloc_step 𝓥1 M1 l n 𝑚s 𝓥2 M2):
𝓥1 𝓥2.
Proof. inversion DEALLOC. by eapply alloc_helper_tview_ext. Qed.
Proof. inversion DEALLOC. by eapply alloc_helper_tview_sqle. Qed.
Lemma read_step_tview_ext L1 M1 𝑚 o L2
Lemma read_step_tview_sqle L1 M1 𝑚 o L2
(READ: read_step L1 M1 𝑚 o L2) :
L1.(tv) L2.(tv).
Proof. inversion READ. by eapply read_helper_tview_ext. Qed.
Proof. inversion READ. by eapply read_helper_tview_sqle. Qed.
Lemma write_step_tview_ext L1 M1 𝑚 o b L2 M2
Lemma write_step_tview_sqle L1 M1 𝑚 o b L2 M2
(WRITE: write_step L1 M1 𝑚 o b L2 M2):
L1.(tv) L2.(tv).
Proof. inversion WRITE. by eapply write_helper_tview_ext. Qed.
Proof. inversion WRITE. by eapply write_helper_tview_sqle. Qed.
Lemma program_step_tview_ext b c1 ev c2
Lemma program_step_tview_sqle b c1 ev c2
(STEP: program_step b c1 ev c2) (WF: wf c1.(lc).(tv)):
c1.(lc).(tv) c2.(lc).(tv).
Proof.
inversion STEP; [..|by subst].
- by eapply alloc_step_tview_ext.
- by eapply dealloc_step_tview_ext.
- by eapply read_step_tview_ext.
- by eapply write_step_tview_ext.
- etrans; [by eapply read_step_tview_ext|by eapply write_step_tview_ext].
- by apply acq_fence_step_tview_ext.
- by apply rel_fence_step_tview_ext.
- by eapply sc_fence_step_tview_ext.
- by eapply sc_fence_step_tview_ext.
- by eapply alloc_step_tview_sqle.
- by eapply dealloc_step_tview_sqle.
- by eapply read_step_tview_sqle.
- by eapply write_step_tview_sqle.
- etrans; [by eapply read_step_tview_sqle|by eapply write_step_tview_sqle].
- by apply acq_fence_step_tview_sqle.
- by apply rel_fence_step_tview_sqle.
- by eapply sc_fence_step_tview_sqle.
- by eapply sc_fence_step_tview_sqle.
Qed.
(* promises sub *)
......@@ -1249,7 +1249,7 @@ Section Steps.
have ?: Some t ({[l := t]}: timeMap) !! l by rewrite lookup_insert.
move => [<-].
case_match; case_match => /=;
rewrite ?lookup_join; do ? (etrans; last apply join_ext_r); done.
rewrite ?lookup_join; do ? (etrans; last apply join_sqle_r); done.
Qed.
Lemma write_new_mview_closed o l (t t' : time) v 𝓥 M1 C V'
......@@ -1275,8 +1275,8 @@ Section Steps.
- apply CLOSED in Eqt1 as [m2 [t2 Eqt2]].
exists m2, t2. by rewrite (lookup_mem_first_ne l l1) //. }
have ?: 𝓥.(cur) M2.
{ constructor; last done. have Ext := (tview_wf_cur _ WF).
rewrite /wf /view_wf in Ext. by rewrite Ext. }
{ constructor; last done. have Sqle := (tview_wf_cur _ WF).
rewrite /wf /view_wf in Sqle. by rewrite Sqle. }
case_match; last done.
case_match.
- have CLOSED0: v0 M1.
......@@ -1292,8 +1292,8 @@ Section Steps.
exists m2, t2. by rewrite (lookup_mem_first_ne l l1). }
have ?: v0 M2.
{ constructor; last done.
have Ext := (tview_wf_rel _ WF) l. rewrite Heqo0 in Ext.
cbn in Ext. rewrite /wf /view_wf in Ext. by rewrite Ext. }
have Sqle := (tview_wf_rel _ WF) l. rewrite Heqo0 in Sqle.
cbn in Sqle. rewrite /wf /view_wf in Sqle. by rewrite Sqle. }
case_match; simpl; apply join_closed_view;
[done|by apply join_closed_view|done|done].
- case_match; simpl; [by apply join_closed_view|done].
......
......@@ -28,10 +28,10 @@ Qed.
Lemma interval_elem_ub (lb ub: time) (Lt: wf (lb, ub]): ub (lb, ub].
Proof. done. Qed.
Instance interval_ext : Extension interval :=
Instance interval_sqle : Sqle interval :=
λ il ir, low ir low il high il high ir.
Lemma interval_ext_in il ir t:
Lemma interval_sqle_in il ir t:
il ir t il t ir.
Proof. move => [??] [??].
split.
......@@ -48,10 +48,10 @@ Proof. move => ?? H ???. by eapply H. Qed.
Lemma adjacent_interval_disj t1 t2 t3: (t1, t2] (t2, t3].
Proof. move => t [_ /Qclt_not_le Le] [// ?]. Qed.
Lemma interval_ext_disj i1 i2 i3: i2 i3 i1 i2 i1 i3.
Lemma interval_sqle_disj i1 i2 i3: i2 i3 i1 i2 i1 i3.
Proof.
move => Disj ? ? ? ?.
eapply Disj; eauto. by eapply interval_ext_in.
eapply Disj; eauto. by eapply interval_sqle_in.
Qed.
Lemma interval_disjoint_ub_neq l1 u1 l2 u2
......
......@@ -38,14 +38,14 @@ Section ThreadView.
: WellformedResolver (𝓥.(rel) !! l).
Proof. by apply tview_wf_rel. Qed.
Record tview_ext' 𝓥1 𝓥2 :=
mkTViewExt {
tview_ext_rel : 𝓥1.(rel) 𝓥2.(rel);
tview_ext_cur : 𝓥1.(cur) 𝓥2.(cur);
tview_ext_acq : 𝓥1.(acq) 𝓥2.(acq);
Record tview_sqle' 𝓥1 𝓥2 :=
mkTViewSqle {
tview_sqle_rel : 𝓥1.(rel) 𝓥2.(rel);
tview_sqle_cur : 𝓥1.(cur) 𝓥2.(cur);
tview_sqle_acq : 𝓥1.(acq) 𝓥2.(acq);
}.