# Library LatticeSignatures

Lattice signatures.

Require Import Utf8 String.
Require Import List Coqlib Integers.

Definition incl {A} (P1 P2:AProp) :=
a, P1 aP2 a.
Notation "P1 ⊆ P2" := ( a, P1 aP2 a) (at level 20).
Notation "x ∈ P" := (P x) (at level 19, only parsing).
Notation "'𝒫' A" := (AProp) (at level 0).
Notation "f ∘ g" := (fun xf (g x)) (at level 40, left associativity).
Notation "X ∩ Y" := (fun xX x Y x) (at level 19).
Notation "X ∪ Y" := (fun xX x Y x) (at level 19).
Notation "∅" := (fun _False).

# Definition of an abstract domain

Module Adom. Class weak_lattice (A: Type) : Type := {
leb: AAbool;
top: A;
join: AAA;
widen: AAA
}.

Class gamma_op (A B: Type) : Type := γ : A𝒫 B.

Record adom (A B:Type)`(weak_lattice A)`(gamma_op A B) : Prop := {
gamma_monotone: a1 a2,
leb a1 a2 = trueγ a1 γ a2;
gamma_top: x, x γ top;
join_sound: x y, γ x γ y γ (join x y)
}.

Notation "x ⊑ y" := (leb x y) (at level 39).
Notation "x ⊔ y" := (join x y) (at level 40).
Notation "x ∇ y" := (widen x y) (at level 40).
Notation "⊤" := top (at level 40).

# Union of a list of abstract values

Section union_list.
Context {A B C:Type}.
Variable f : CA.
Variable bot : A.
Variable union : AAA.
Variable gamma : ABProp.
Variable union_correct : ab1 ab2 m,
gamma ab1 m gamma ab2 mgamma (union ab1 ab2) m.

Fixpoint union_list' (l:list A) : A :=
match l with
| nilbot
| a::nila
| a::qunion a (union_list' q)
end.

Lemma union_list'_correct : l ab m,
In ab l
m gamma ab
m gamma (union_list' l).

Definition union_list (l: list A) : A :=
match l with
| nilbot
| a::q
List.fold_left union q a
end.

Lemma union_list_correct : l ab m,
In ab l
m gamma ab
m gamma (union_list l).

Definition union_list_map (l: list C) : A :=
match l with
| nilbot
| a :: qList.fold_left (λ u x, union u (f x)) q (f a)
end.

Lemma union_list_map_correct l :
union_list_map l = union_list (map f l).

End union_list.

Class EqDec (T: Type) := eq_dec : x y : T, { x = y } + { x y }.

Lemma eq_dec_true {T: Type} `{E: EqDec} x (A B: T):
(if eq_dec x x then A else B) = A.
Lemma eq_dec_false {T: Type} `{E: EqDec} {x y}:
x y
A B : T,
(if eq_dec x y then A else B) = B.

Instance PosEqDec : EqDec positive := peq.
Instance ZEqDec : EqDec Z := zeq.
Instance IntEqDec : @EqDec Integers.int.

Instance ProdEqDec {X Y: Type} `{EqDec X} `{EqDec Y} : EqDec (X × Y).

Definition upd `{X: Type} `{EqDec X} {Y} (f: X Y) (p: X) (v:Y) :=
fun qif eq_dec q p then v else f q.

Lemma upd_s `{X: Type} `{EqDec X} {Y} (f: X Y) p v:
(upd f p v) p = v.

Lemma upd_o `{X: Type} `{EqDec X} {Y} (f: X Y) p v p' :
p' p (upd f p v) p' = f p'.