Library AdomLib
Inductive botlift (A:Type) : Type := Bot | NotBot (x:A).
Implicit Arguments Bot [A].
Notation "t +⊥" := (botlift t) (at level 39).
Definition bot {A: Type} (l: weak_lattice (A +⊥)) : A+⊥ := Bot.
Instance lift_bot_wl {A:Type} (l:weak_lattice A) : weak_lattice (A+⊥) :=
{ leb :=
(fun x y ⇒
match x, y with
| Bot, _ ⇒ true
| NotBot x, NotBot y ⇒ leb x y
| _, _ ⇒ false
end);
top := (NotBot top);
join :=
(fun x y ⇒
match x, y with
| Bot, _ ⇒ y
|_ , Bot ⇒ x
| NotBot x, NotBot y ⇒ NotBot (join x y)
end);
widen :=
(fun x y ⇒
match x, y with
| Bot, _ ⇒ y
|_ , Bot ⇒ x
| NotBot x, NotBot y ⇒ NotBot (widen x y)
end)
}.
Instance lift_gamma (A B: Type) (G: gamma_op A B) : gamma_op (A+⊥) B :=
(fun x ⇒
match x with
| Bot ⇒ fun _ ⇒ False
| NotBot x ⇒ γ x
end).
Definition lift_bot {A B:Type} WL G (l:adom A B WL G) : adom (A+⊥) B _ _.
Definition botbind {A B} (f: A → B+⊥) (a: A+⊥) : B+⊥ :=
match a with
| Bot ⇒ Bot
| NotBot x ⇒ f x
end.
Notation "'do' X <- A ; B" := (botbind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200)
: botbind_monad_scope.
Notation "'do_bot' X <- A ; B" := (botbind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200).
Lemma botbind_spec {A A' B B':Type} {GA: gamma_op A A'} {GB: gamma_op B B'} :
∀ f:A→B+⊥, ∀ x y, (∀ a, x ∈ γ a → y ∈ γ (f a)) →
(∀ a, x ∈ γ a → y ∈ γ (botbind f a)).
Definition botbind2 {A B C} (f: A → B → C+⊥) (a: A+⊥) (b: B+⊥) : C+⊥ :=
botbind (fun x ⇒ botbind (f x) b) a.
Lemma botbind2_spec {A A' B B' C C':Type} {AD:gamma_op A A'} {BD:gamma_op B B'} {CD:gamma_op C C'}:
∀ f:A→B→C+⊥, ∀ x y z, (∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (f x_ab y_ab)) →
(∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (botbind2 f x_ab y_ab)).
Definition botlift_fun1 {A B:Type} (f:A→B) (x:A+⊥) : B+⊥ :=
botbind (@NotBot _ ∘ f) x.
Lemma botlift_fun1_spec {A A' B B':Type} {AD:gamma_op A A'} {BD:gamma_op B B'}:
∀ f:A→B, ∀ x y, (∀ x_ab, x ∈ γ x_ab → y ∈ γ (f x_ab)) →
(∀ x_ab, x ∈ γ x_ab → y ∈ γ (botlift_fun1 f x_ab)).
Definition botlift_fun2 {A B C:Type} (f:A→B→C) (a:A+⊥) (b:B+⊥) : C+⊥ :=
botbind (fun x ⇒ botlift_fun1 (f x) b) a.
Lemma botlift_fun2_spec {A A' B B' C C':Type} {AD:gamma_op A A'} {BD:gamma_op B B'} {CD:gamma_op C C'}:
∀ f:A→B→C, ∀ x y z, (∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (f x_ab y_ab)) →
(∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (botlift_fun2 f x_ab y_ab)).
Instance bot_lift_toString A `{ToString A} : ToString (A+⊥) :=
{ to_string x := match x with
| Bot ⇒ "⊥"%string
| NotBot x' ⇒ to_string x'
end
}.
Lemma union_list_bot A B WL G {AD: adom A B WL G} (z: A) (l: list (A+⊥)) :
union_list (NotBot z) join l = Bot →
∀ x, List.In x l → x = Bot.
Lemma union_list_leb A (bot: A) join l (leb: A → A → bool) :
(∀ x a b, leb x a = true ∨ leb x b = true → leb x (join a b) = true) →
∀ x,
(l = nil → leb x bot = true) →
(∃ y, List.In y l ∧ leb x y = true) →
leb x (union_list bot join l) = true.
Implicit Arguments Bot [A].
Notation "t +⊥" := (botlift t) (at level 39).
Definition bot {A: Type} (l: weak_lattice (A +⊥)) : A+⊥ := Bot.
Instance lift_bot_wl {A:Type} (l:weak_lattice A) : weak_lattice (A+⊥) :=
{ leb :=
(fun x y ⇒
match x, y with
| Bot, _ ⇒ true
| NotBot x, NotBot y ⇒ leb x y
| _, _ ⇒ false
end);
top := (NotBot top);
join :=
(fun x y ⇒
match x, y with
| Bot, _ ⇒ y
|_ , Bot ⇒ x
| NotBot x, NotBot y ⇒ NotBot (join x y)
end);
widen :=
(fun x y ⇒
match x, y with
| Bot, _ ⇒ y
|_ , Bot ⇒ x
| NotBot x, NotBot y ⇒ NotBot (widen x y)
end)
}.
Instance lift_gamma (A B: Type) (G: gamma_op A B) : gamma_op (A+⊥) B :=
(fun x ⇒
match x with
| Bot ⇒ fun _ ⇒ False
| NotBot x ⇒ γ x
end).
Definition lift_bot {A B:Type} WL G (l:adom A B WL G) : adom (A+⊥) B _ _.
Definition botbind {A B} (f: A → B+⊥) (a: A+⊥) : B+⊥ :=
match a with
| Bot ⇒ Bot
| NotBot x ⇒ f x
end.
Notation "'do' X <- A ; B" := (botbind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200)
: botbind_monad_scope.
Notation "'do_bot' X <- A ; B" := (botbind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200).
Lemma botbind_spec {A A' B B':Type} {GA: gamma_op A A'} {GB: gamma_op B B'} :
∀ f:A→B+⊥, ∀ x y, (∀ a, x ∈ γ a → y ∈ γ (f a)) →
(∀ a, x ∈ γ a → y ∈ γ (botbind f a)).
Definition botbind2 {A B C} (f: A → B → C+⊥) (a: A+⊥) (b: B+⊥) : C+⊥ :=
botbind (fun x ⇒ botbind (f x) b) a.
Lemma botbind2_spec {A A' B B' C C':Type} {AD:gamma_op A A'} {BD:gamma_op B B'} {CD:gamma_op C C'}:
∀ f:A→B→C+⊥, ∀ x y z, (∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (f x_ab y_ab)) →
(∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (botbind2 f x_ab y_ab)).
Definition botlift_fun1 {A B:Type} (f:A→B) (x:A+⊥) : B+⊥ :=
botbind (@NotBot _ ∘ f) x.
Lemma botlift_fun1_spec {A A' B B':Type} {AD:gamma_op A A'} {BD:gamma_op B B'}:
∀ f:A→B, ∀ x y, (∀ x_ab, x ∈ γ x_ab → y ∈ γ (f x_ab)) →
(∀ x_ab, x ∈ γ x_ab → y ∈ γ (botlift_fun1 f x_ab)).
Definition botlift_fun2 {A B C:Type} (f:A→B→C) (a:A+⊥) (b:B+⊥) : C+⊥ :=
botbind (fun x ⇒ botlift_fun1 (f x) b) a.
Lemma botlift_fun2_spec {A A' B B' C C':Type} {AD:gamma_op A A'} {BD:gamma_op B B'} {CD:gamma_op C C'}:
∀ f:A→B→C, ∀ x y z, (∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (f x_ab y_ab)) →
(∀ x_ab y_ab, x ∈ γ x_ab → y ∈ γ y_ab → z ∈ γ (botlift_fun2 f x_ab y_ab)).
Instance bot_lift_toString A `{ToString A} : ToString (A+⊥) :=
{ to_string x := match x with
| Bot ⇒ "⊥"%string
| NotBot x' ⇒ to_string x'
end
}.
Lemma union_list_bot A B WL G {AD: adom A B WL G} (z: A) (l: list (A+⊥)) :
union_list (NotBot z) join l = Bot →
∀ x, List.In x l → x = Bot.
Lemma union_list_leb A (bot: A) join l (leb: A → A → bool) :
(∀ x a b, leb x a = true ∨ leb x b = true → leb x (join a b) = true) →
∀ x,
(l = nil → leb x bot = true) →
(∃ y, List.In y l ∧ leb x y = true) →
leb x (union_list bot join l) = true.
Module WProd.
Section lat.
Context {t1 t2 B: Type}.
Context WL1 G1 (lat1 : adom t1 B WL1 G1).
Context WL2 G2 (lat2 : adom t2 B WL2 G2).
Definition A: Type := (t1×t2)%type.
Definition leb: A → A → bool :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
(leb x1 y1
&&
leb x2 y2)%bool.
Definition top: A :=
(top, top).
Definition join: A → A → A :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
(join x1 y1,
join x2 y2).
Definition widen: A → A → A :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
(widen x1 y1,
widen x2 y2).
Definition gamma: A → B → Prop :=
fun x ⇒
let (x1,x2) := x in
γ x1 ∩ γ x2.
Lemma gamma_monotone: ∀ a1 a2,
leb a1 a2 = true → gamma a1 ⊆ gamma a2.
Lemma gamma_top: ∀ x, gamma top x.
Lemma join_sound: ∀ x y, gamma x ∪ gamma y ⊆ gamma (join x y).
Instance make_wl : weak_lattice A :=
{leb := leb;
top := top;
join := join;
widen := widen
}.
Lemma make : adom A B _ gamma.
End lat.
End WProd.
Section lat.
Context {t1 t2 B: Type}.
Context WL1 G1 (lat1 : adom t1 B WL1 G1).
Context WL2 G2 (lat2 : adom t2 B WL2 G2).
Definition A: Type := (t1×t2)%type.
Definition leb: A → A → bool :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
(leb x1 y1
&&
leb x2 y2)%bool.
Definition top: A :=
(top, top).
Definition join: A → A → A :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
(join x1 y1,
join x2 y2).
Definition widen: A → A → A :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
(widen x1 y1,
widen x2 y2).
Definition gamma: A → B → Prop :=
fun x ⇒
let (x1,x2) := x in
γ x1 ∩ γ x2.
Lemma gamma_monotone: ∀ a1 a2,
leb a1 a2 = true → gamma a1 ⊆ gamma a2.
Lemma gamma_top: ∀ x, gamma top x.
Lemma join_sound: ∀ x y, gamma x ∪ gamma y ⊆ gamma (join x y).
Instance make_wl : weak_lattice A :=
{leb := leb;
top := top;
join := join;
widen := widen
}.
Lemma make : adom A B _ gamma.
End lat.
End WProd.
Module WTensor.
Section lat.
Context {t1 t2 B1 B2: Type}.
Context WL1 G1 (lat1 : adom t1 B1 WL1 G1).
Context WL2 G2 (lat2 : adom t2 B2 WL2 G2).
Definition A: Type := (t1×t2)%type.
Definition B: Type := (B1×B2)%type.
Instance gamma : gamma_op A B :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
y1 ∈ γ x1 ∧ y2 ∈ γ x2.
Lemma gamma_monotone: ∀ a1 a2,
leb a1 a2 = true → gamma a1 ⊆ gamma a2.
Lemma gamma_top: ∀ x, gamma top x.
Lemma join_sound: ∀ x y, gamma x ∪ gamma y ⊆ gamma (join x y).
Lemma make : adom A B _ gamma.
Instance toString `{ToString t1} `{ToString t2} : ToString (t1 × t2) :=
{ to_string x := let '(a,b) := x in ("(" ++ to_string a ++ " ⊗ " ++ to_string b ++ ")")%string }.
End lat.
End WTensor.
Section lat.
Context {t1 t2 B1 B2: Type}.
Context WL1 G1 (lat1 : adom t1 B1 WL1 G1).
Context WL2 G2 (lat2 : adom t2 B2 WL2 G2).
Definition A: Type := (t1×t2)%type.
Definition B: Type := (B1×B2)%type.
Instance gamma : gamma_op A B :=
fun x y ⇒
let (x1,x2) := x in
let (y1,y2) := y in
y1 ∈ γ x1 ∧ y2 ∈ γ x2.
Lemma gamma_monotone: ∀ a1 a2,
leb a1 a2 = true → gamma a1 ⊆ gamma a2.
Lemma gamma_top: ∀ x, gamma top x.
Lemma join_sound: ∀ x y, gamma x ∪ gamma y ⊆ gamma (join x y).
Lemma make : adom A B _ gamma.
Instance toString `{ToString t1} `{ToString t2} : ToString (t1 × t2) :=
{ to_string x := let '(a,b) := x in ("(" ++ to_string a ++ " ⊗ " ++ to_string b ++ ")")%string }.
End lat.
End WTensor.
Module WPFun (P:TREE).
Module PP := Tree_Properties P.
Section lat.
Context {t0 B: Type}.
Context WL G (lat : adom t0 B WL G).
Definition t := P.t t0.
Definition bot : t+⊥ := Bot.
Definition top : t := (P.empty _).
Definition get (m: t) (r: P.elt) : t0 :=
match P.get r m with
| None ⇒ ⊤
| Some i ⇒ i
end.
Definition set (m: t) (r: P.elt) (i:t0) : t := P.set r i m.
Definition leb0 (m1 m2:t) : bool :=
PP.for_all m2 (fun x i2 ⇒ leb (get m1 x) i2).
Lemma leb_le: ∀ m1 m2,
leb0 m1 m2 = true → (∀ p, (get m1 p) ⊑ (get m2 p) = true
∨ get m2 p = ⊤).
Definition join : t → t → t :=
P.combine
(fun x y ⇒
match x, y with
| None, _ ⇒ None
|_ , None ⇒ None
| Some x, Some y ⇒ Some (join x y)
end).
Definition widen: t → t → t :=
P.combine
(fun x y ⇒
match x, y with
| None, _ ⇒ None
|_ , None ⇒ None
| Some x, Some y ⇒ Some (widen x y)
end).
Instance gamma : gamma_op t (P.elt → B) :=
fun m rs ⇒
∀ r, γ (get m r) (rs r).
Lemma gamma_monotone: ∀ x y,
leb0 x y = true →
gamma x ⊆ gamma y.
Lemma join_correct : ∀ (x y:t) b,
gamma x b ∨ gamma y b → gamma (join x y) b.
Instance make_wl : weak_lattice t :=
{ leb := leb0
; top := top
; join := join
; widen := widen
}.
Lemma make : adom t (P.elt → B) make_wl gamma.
Lemma gamma_set1 : ∀ (app:t) rs ab x,
γ app rs →
γ ab (rs x) →
γ (set app x ab) rs.
Lemma gamma_set2 : ∀ (app:t) rs ab v x,
γ app rs →
γ ab v →
γ (set app x ab) (fun p ⇒ if P.elt_eq p x then v else rs p).
Definition forget (app: t) (r: P.elt) : t := P.remove r app.
Lemma gamma_forget : ∀ (app:t) rs rs' x,
γ app rs →
(∀ y, x≠y → rs y = rs' y) →
γ (forget app x) rs'.
Lemma gamma_app: ∀ (m: t) (rs: P.elt → B),
γ m rs →
∀ r, γ (get m r) (rs r).
Instance toString `{ToString P.elt} `{ToString t0} : ToString (P.t t0) :=
(λ x, P.fold (λ s k v, s ++ "["++ to_string k ++ "↦" ++ to_string v ++"]" ) x "{" ++ "}")%string.
End lat.
End WPFun.
Module PP := Tree_Properties P.
Section lat.
Context {t0 B: Type}.
Context WL G (lat : adom t0 B WL G).
Definition t := P.t t0.
Definition bot : t+⊥ := Bot.
Definition top : t := (P.empty _).
Definition get (m: t) (r: P.elt) : t0 :=
match P.get r m with
| None ⇒ ⊤
| Some i ⇒ i
end.
Definition set (m: t) (r: P.elt) (i:t0) : t := P.set r i m.
Definition leb0 (m1 m2:t) : bool :=
PP.for_all m2 (fun x i2 ⇒ leb (get m1 x) i2).
Lemma leb_le: ∀ m1 m2,
leb0 m1 m2 = true → (∀ p, (get m1 p) ⊑ (get m2 p) = true
∨ get m2 p = ⊤).
Definition join : t → t → t :=
P.combine
(fun x y ⇒
match x, y with
| None, _ ⇒ None
|_ , None ⇒ None
| Some x, Some y ⇒ Some (join x y)
end).
Definition widen: t → t → t :=
P.combine
(fun x y ⇒
match x, y with
| None, _ ⇒ None
|_ , None ⇒ None
| Some x, Some y ⇒ Some (widen x y)
end).
Instance gamma : gamma_op t (P.elt → B) :=
fun m rs ⇒
∀ r, γ (get m r) (rs r).
Lemma gamma_monotone: ∀ x y,
leb0 x y = true →
gamma x ⊆ gamma y.
Lemma join_correct : ∀ (x y:t) b,
gamma x b ∨ gamma y b → gamma (join x y) b.
Instance make_wl : weak_lattice t :=
{ leb := leb0
; top := top
; join := join
; widen := widen
}.
Lemma make : adom t (P.elt → B) make_wl gamma.
Lemma gamma_set1 : ∀ (app:t) rs ab x,
γ app rs →
γ ab (rs x) →
γ (set app x ab) rs.
Lemma gamma_set2 : ∀ (app:t) rs ab v x,
γ app rs →
γ ab v →
γ (set app x ab) (fun p ⇒ if P.elt_eq p x then v else rs p).
Definition forget (app: t) (r: P.elt) : t := P.remove r app.
Lemma gamma_forget : ∀ (app:t) rs rs' x,
γ app rs →
(∀ y, x≠y → rs y = rs' y) →
γ (forget app x) rs'.
Lemma gamma_app: ∀ (m: t) (rs: P.elt → B),
γ m rs →
∀ r, γ (get m r) (rs r).
Instance toString `{ToString P.elt} `{ToString t0} : ToString (P.t t0) :=
(λ x, P.fold (λ s k v, s ++ "["++ to_string k ++ "↦" ++ to_string v ++"]" ) x "{" ++ "}")%string.
End lat.
End WPFun.
Option type.
Inductive toplift (A: Type) := All | Just : A → toplift A.
Notation "x +⊤" := (toplift x) (at level 39).
Definition toplift_bind {A B: Type} (f: A → B+⊤) (x: A+⊤) : B+⊤ :=
match x with
| All ⇒ All
| Just x' ⇒ f x'
end.
Notation "'do' X <- A ; B" := (toplift_bind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200)
: top_monad_scope.
Notation "'do_top' X <- A ; B" := (toplift_bind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200).
Lemma top_bind_case A B (a: A+⊤) (f: A → B+⊤) :
∀ P : B+⊤ → Prop,
P All →
(∀ a', a = Just a' → P (f a')) →
P (do_top x <- a; f x).
Definition top_lift {A B: Type} (f: A → B) : A+⊤ → B+⊤ :=
toplift_bind (fun x ⇒ Just (f x)).
Definition top_bind2 {A B C: Type} (f: A → B → C+⊤) (x: A+⊤) (y: B+⊤) : C+⊤ :=
match x, y with
| All, _ | _, All ⇒ All
| Just x', Just y' ⇒ f x' y'
end.
Definition top_lift2 {A B C: Type} (f: A → B → C) : A+⊤ → B+⊤ → C+⊤ :=
top_bind2 (fun x y ⇒ Just (f x y)).
Definition top_leb {A: Type} (leb: A → A → bool) (x y: A+⊤) : bool :=
match x, y with
| _, All ⇒ true
| All, Just _ ⇒ false
| Just x', Just y' ⇒ leb x' y'
end.
Definition flat_top_leb {A} (beq: A → A → bool) (x y: A+⊤) : bool :=
match x, y with
| _, All ⇒ true
| All, _ ⇒ false
| Just x', Just y' ⇒ beq x' y'
end.
Definition flat_top_join {A} beq (x y: A+⊤) : A +⊤ := if flat_top_leb beq x y then y else All.
Local Instance flat_top_wlat A beq : weak_lattice (A+⊤) :=
{| leb := flat_top_leb beq
; top := All
; join := flat_top_join beq
; widen := flat_top_join beq
|}.
Instance top_toString A `{ToString A} : ToString (A+⊤) :=
{ to_string x := match x with
| All ⇒ "⊤"%string
| Just y ⇒ to_string y
end
}.
Notation "x +⊤" := (toplift x) (at level 39).
Definition toplift_bind {A B: Type} (f: A → B+⊤) (x: A+⊤) : B+⊤ :=
match x with
| All ⇒ All
| Just x' ⇒ f x'
end.
Notation "'do' X <- A ; B" := (toplift_bind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200)
: top_monad_scope.
Notation "'do_top' X <- A ; B" := (toplift_bind (fun X ⇒ B) A)
(at level 200, X ident, A at level 100, B at level 200).
Lemma top_bind_case A B (a: A+⊤) (f: A → B+⊤) :
∀ P : B+⊤ → Prop,
P All →
(∀ a', a = Just a' → P (f a')) →
P (do_top x <- a; f x).
Definition top_lift {A B: Type} (f: A → B) : A+⊤ → B+⊤ :=
toplift_bind (fun x ⇒ Just (f x)).
Definition top_bind2 {A B C: Type} (f: A → B → C+⊤) (x: A+⊤) (y: B+⊤) : C+⊤ :=
match x, y with
| All, _ | _, All ⇒ All
| Just x', Just y' ⇒ f x' y'
end.
Definition top_lift2 {A B C: Type} (f: A → B → C) : A+⊤ → B+⊤ → C+⊤ :=
top_bind2 (fun x y ⇒ Just (f x y)).
Definition top_leb {A: Type} (leb: A → A → bool) (x y: A+⊤) : bool :=
match x, y with
| _, All ⇒ true
| All, Just _ ⇒ false
| Just x', Just y' ⇒ leb x' y'
end.
Definition flat_top_leb {A} (beq: A → A → bool) (x y: A+⊤) : bool :=
match x, y with
| _, All ⇒ true
| All, _ ⇒ false
| Just x', Just y' ⇒ beq x' y'
end.
Definition flat_top_join {A} beq (x y: A+⊤) : A +⊤ := if flat_top_leb beq x y then y else All.
Local Instance flat_top_wlat A beq : weak_lattice (A+⊤) :=
{| leb := flat_top_leb beq
; top := All
; join := flat_top_join beq
; widen := flat_top_join beq
|}.
Instance top_toString A `{ToString A} : ToString (A+⊤) :=
{ to_string x := match x with
| All ⇒ "⊤"%string
| Just y ⇒ to_string y
end
}.
Partial order with partial least upper bound.
LocalRecord pre_lattice t :=
{ pl_leb : t → t → bool
; pl_join : t → t → t+⊤
; pl_widen: t → t → t+⊤
}.
Instance toplift_gamma t B (GAMMA: gamma_op t B) : gamma_op (t+⊤) B :=
λ x, match x with All ⇒ λ _, True | Just y ⇒ γ y end.
Record pre_lattice_spec t B (PL: pre_lattice t) (GAMMA: gamma_op t B) : Prop :=
{ pl_gamma_monotone: ∀ x y : t, pl_leb PL x y = true →
∀ b : B, γ x b → γ y b
; pl_join_sound: ∀ x y: t, (γ x ∪ γ y) ⊆ γ (pl_join PL x y)
}.
Instance weak_lattice_of_pre_lattice t (PL: pre_lattice t) : weak_lattice (t+⊤) :=
let join f x y :=
match x, y with
| All, _
| _, All ⇒ All
| Just x', Just y' ⇒ f x' y'
end in
{| leb := flat_top_leb (pl_leb PL)
; top := All
; join := join (pl_join PL)
; widen:= join (pl_widen PL)
|}.
Lemma adom_of_pre_lattice t B (PL: pre_lattice t) G (PLP: pre_lattice_spec PL G)
: adom (t+⊤) B (weak_lattice_of_pre_lattice PL) (toplift_gamma G).
Definition flat_pre_lattice T (beq: T → T → bool ) : pre_lattice T :=
{| pl_leb := beq
; pl_join x y := if beq x y then Just x else All
; pl_widen x y := if beq x y then Just x else All
|}.
Lemma flat_pre_lattice_correct T B beq (BEQ: ∀ x y, beq x y = true → x = y)
(G: gamma_op T B) : pre_lattice_spec (flat_pre_lattice beq) G.
Local Open Scope top_monad_scope.
Definition product_pre_lattice {A B} (PA: pre_lattice A) (PB: pre_lattice B) : pre_lattice (A × B) :=
{| pl_leb x x' := let '(a,b) := x in let '(a',b') := x' in
pl_leb PA a a' && pl_leb PB b b'
; pl_join x x' := let '(a,b) := x in let '(a',b') := x' in
do α <- pl_join PA a a';
do β <- pl_join PB b b';
Just (α, β)
; pl_widen x x' := let '(a,b) := x in let '(a',b') := x' in
do α <- pl_widen PA a a';
do β <- pl_widen PB b b';
Just (α, β)
|}.
Instance pair_gamma {A B Ca Cb} (GA: gamma_op A Ca) (GB: gamma_op B Cb) : gamma_op (A × B) (Ca × Cb) :=
λ x x', let '(a, b) := x in let '(a', b') := x' in
a' ∈ γ(a) ∧ b' ∈ γ(b).
Lemma product_pre_lattice_correct {A B Ca Cb} {PA: pre_lattice A} {PB: pre_lattice B} (GA: gamma_op A Ca) (GB: gamma_op B Cb) (HA: pre_lattice_spec PA GA) (HB: pre_lattice_spec PB GB) : pre_lattice_spec (product_pre_lattice PA PB) (pair_gamma GA GB).
Module WPFun2 (T:TREE).
Module P := Tree_Properties T.
Section elt.
Context (elt B: Type)
(PL: pre_lattice elt)
(elt_gamma: gamma_op elt B)
(PLP: pre_lattice_spec PL elt_gamma).
Definition t : Type := T.t elt.
Definition get (p: T.elt) (x: t) : elt+⊤ :=
match T.get p x with
| Some r ⇒ Just r
| None ⇒ All
end.
Definition set (x:t) (p: T.elt) (v: elt+⊤) : t :=
match v with
| All ⇒ T.remove p x
| Just v' ⇒ T.set p v' x
end.
Lemma gsspec x p v p' :
get p' (set x p v) = if T.elt_eq p' p then v else get p' x.
Definition leb : t → t → bool :=
λ x y,
P.for_all y (λ a s, match T.get a x with
| Some a' ⇒ pl_leb PL a' s
| None ⇒ false
end).
Lemma leb_le (x y: t) :
leb x y = true ↔
∀ p : T.elt, flat_top_leb (pl_leb PL) (get p x) (get p y) = true.
Lemma leb_refl
(H: ∀ x, pl_leb PL x x = true)
(x: t) : leb x x = true.
Definition join f : t → t → t :=
T.combine (λ u v, match u, v with
| None, _
| _, None ⇒ None
| Some u', Some v' ⇒
match f u' v' with
| Just r ⇒ Some r
| All ⇒ None
end
end).
Lemma join_monotone f x a b :
(∀ u v, pl_leb PL u v = true →
(∀ w v', f v w = Just v' → pl_leb PL u v' = true)
∧ (∀ w v', f w v = Just v' → pl_leb PL u v' = true)) →
leb x a = true ∨ leb x b = true →
leb x (join f a b) = true.
Instance wlat : weak_lattice t :=
{| leb := leb
; top := T.empty _
; join := join (pl_join PL)
; widen := join (pl_widen PL)
|}.
Instance gamma : gamma_op t (T.elt → B) :=
λ x y, ∀ e, y e ∈ γ (get e x).
Lemma gamma_set x a b p v :
γ x a →
γ v (b p) →
(∀ q, q ≠ p → a q = b q) →
γ (set x p v) b.
Lemma gamma_forget x a b p :
γ x a →
(∀ q, q ≠ p → a q = b q) →
γ (set x p All) b.
Lemma adom : adom t (T.elt → B) wlat gamma.
Instance toString `{ToString T.elt} `{ToString elt} : ToString (T.t elt) :=
(λ x, T.fold (λ s k v, s ++ "["++ to_string k ++ "↦" ++ to_string v ++"]" ) x "{" ++ "}")%string.
End elt.
Opaque get. Opaque set.
End WPFun2.