Require Import Utf8 String.
Require Import List Coqlib Integers.

Definition incl {A} (P1 P2:A→Prop) :=
  ∀ a, P1 a → P2 a.
Notation "P1 ⊆ P2" := (∀ a, P1 a → P2 a) (at level 20).
Notation "x ∈ P" := (P x) (at level 19, only parsing).
Notation "'𝒫' A" := (A → Prop) (at level 0).
Notation "f ∘ g" := (fun x ⇒ f (g x)) (at level 40, left associativity).
Notation "X ∩ Y" := (fun x ⇒ X x ∧ Y x) (at level 19).
Notation "X ∪ Y" := (fun x ⇒ X x ∨ Y x) (at level 19).
Notation "∅" := (fun _ ⇒ False).

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

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)
}.
End Adom.
Export Adom.

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).

Section union_list.
Context {A B C:Type}.
Variable f : C → A.
Variable bot : A.
Variable union : A → A → A.
Variable gamma : A → B → Prop.
Variable union_correct : ∀ ab1 ab2 m,
  gamma ab1 m ∨ gamma ab2 m → gamma (union ab1 ab2) m.

Fixpoint union_list' (l:list A) : A :=
  match l with
    | nil ⇒ bot
    | a::nil ⇒ a
    | a::q ⇒ union 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
  | nil ⇒ bot
  | 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
  | nil ⇒ bot
  | a :: q ⇒ List.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 q ⇒ if 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'.