Module LatticeSignatures

Require Import Utf8.
Require Import List Maps Coqlib.

Definition incl {A} (P1 P2:A->Prop) :=
  forall a, P1 a -> P2 a.
Notation "P1 ⊆ P2" := (forall 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 99, 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.
Unset Elimination Schemes.
Class adom (A:Type) (B:Type) : Type := {
  leb: A -> A -> bool;
  top: A;
  join: A -> A -> A;
  widen: A -> A -> A;
  
  gamma: A -> ℘ B;
  gamma_monotone: forall {a1} {a2},
    leb a1 a2 = true -> gamma a1 ⊆ gamma a2;
  gamma_top: forall x, x ∈ gamma top;
  join_sound: ∀ x y, gamma x ∪ gamma y ⊆ gamma (join x y)
}.
End Adom.
Export Adom.
Hint Resolve @gamma_monotone @gamma_top.

Set Implicit Arguments.
Inductive botlift (A:Type) : Type := Bot | NotBot (x:A).
Implicit Arguments Bot [A].
Notation "t +⊥" := (botlift t) (at level 39).

Definition bot {A B: Type} (l:adom (A +⊥) B) : A+⊥ := Bot.

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).
Notation γ := gamma.

Instance lift_bot {A B:Type} (l:adom A B) : adom (A+⊥) B :=
{ 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);
  gamma :=
    (fun x =>
      match x with
      | Bot => fun _ => False
        | NotBot x => gamma x
      end)
}.

Definition botlift_fun1 {A B:Type} (f:A->B) (x:A+⊥) : B+⊥ :=
  match x with
    | Bot => Bot
    | NotBot x => NotBot (f x)
  end.

Definition botlift_fun2 {A B C:Type} (f:A->B->C) (x:A+⊥) (y:B+⊥) : C+⊥ :=
  match x, y with
    | Bot, _
    | _, Bot => Bot
    | NotBot x, NotBot y => NotBot (f x y)
  end.

Definition botlift_prop {A B: Type} (f: A → ℘ B) : A+⊥ → ℘ B :=
  fun a => match a with Bot => ∅ | NotBot a' => f a' end.

Section union_list.
Context {A B:Type}.
Variable bot : A.
Variable union : A -> A -> A.
Variable gamma : A -> B -> Prop.
Variable union_correct : forall 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 : forall l ab m,
  In ab l ->
  m ∈ gamma ab ->
  m ∈ gamma (union_list l).

End union_list.

Module WProd.
Section lat.
  Context {t1 t2 B: Type}.
  Variable lat1 : adom t1 B.
  Variable lat2 : adom t2 B.
  
  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
      gamma x1 ∩ gamma x2.

  Lemma gamma_monotone: forall a1 a2,
    leb a1 a2 = true -> gamma a1 ⊆ gamma a2.
  
  Lemma gamma_top: forall x, gamma top x.

  Lemma join_sound: forall x y, gamma x ∪ gamma y ⊆ gamma (join x y).

  Instance make : adom A B :=
   {leb := leb;
    top := top;
    join := join;
    widen := widen;
    gamma := gamma;
    gamma_monotone := gamma_monotone;
    gamma_top := gamma_top
   ;join_sound := join_sound
   }.

End lat.
End WProd.

Module WPFun (P:TREE).
Module PP_Prop := Tree_Properties P.

Section lat.
Context {t0 B: Type}.
Variable lat : adom t0 B.

Definition A := P.t t0.
Definition t := (P.t t0)+⊥.

Definition bot : t := Bot.

Definition topA : A := (P.empty _).
Definition top : t := NotBot topA.

Definition getA (m: A) (r: P.elt) : t0 :=
  match P.get r m with
    | None => ⊤
    | Some i => i
  end.

Definition get (app: t) (r: P.elt) : t0+⊥ :=
  match app with
    | Bot => Bot
    | NotBot m =>
      match P.get r m with
        | None => NotBot (⊤)
        | Some i => NotBot i
      end
  end.

Definition set (app: t) (r: P.elt) (i:t0+⊥) : t :=
  match i with
    | Bot => Bot
    | NotBot i =>
      match app with
        | Bot => Bot
        | NotBot m => NotBot (P.set r i m)
      end
  end.

Definition p_forall {A:Type} (m:P.t A) (f:P.elt->A->bool) : bool :=
  P.fold (fun b0 p a => b0 && f p a)%bool m true.


Lemma p_forall_correct1 : forall A (f:P.elt->A->bool) m,
  p_forall m f = true ->
  forall n ins, P.get n m = Some ins -> f n ins = true.

Lemma p_forall_correct2 : forall A (f:P.elt->A->bool) m,
  (forall n ins, P.get n m = Some ins -> f n ins = true) ->
  p_forall m f = true.

Lemma p_forall_correct : forall A (f:P.elt->A->bool) m,
  p_forall m f = true <->
  (forall n ins, P.get n m = Some ins -> f n ins = true).


Definition leb0 (m1 m2:A) : bool :=
    p_forall m2
    (fun x i2 =>
          match get (NotBot m1) x with
            | Bot => true
            | NotBot i1 => leb i1 i2
          end).

  Lemma leb_le: forall m1 m2,
    leb0 m1 m2 = true -> (forall p, (get (NotBot m1) p) ⊑ (get (NotBot m2) p) = true
                                \/ get (NotBot m2) p = ⊤).

  Definition joinA : A -> A -> A :=
    P.combine
     (fun x y =>
       match x, y with
         | None, _ => None
           |_ , None => None
         | Some x, Some y => Some (join x y)
       end).

  Definition widenA: A -> A -> A :=
    P.combine
    (fun x y =>
      match x, y with
        | None, _ => None
          |_ , None => None
        | Some x, Some y => Some (widen x y)
      end).

    Definition gamma (m: A) (rs: P.elt -> B) : Prop :=
    forall r, gamma (get (NotBot m) r) (rs r).
  
  Lemma gamma_monotone: forall x y,
    leb0 x y = true ->
    gamma x ⊆ gamma y.

  Section join_correct.
    Variable Ljoin_correct: forall x y:t0, forall b,
      γ x b \/ γ y b -> γ (x ⊔ y) b.

    Lemma join_correct : forall (x y:A) b,
      gamma x b \/ gamma y b -> gamma (joinA x y) b.
  End join_correct.

  Instance make : adom A (P.elt -> B) :=
   {leb := leb0;
    top := topA;
    join := joinA;
    widen := widenA;
    gamma := gamma;
    gamma_monotone := gamma_monotone
   ;join_sound := join_correct join_sound
   }.

  Instance makebot: adom t (P.elt -> B) := lift_bot make.

Lemma gamma_set1 : forall (app:t) rs ab x,
  γ app rs ->
  γ ab (rs x) ->
  γ (set app x ab) rs.

Lemma gamma_set2 : forall (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 :=
  match app with
    | Bot => Bot
    | NotBot m => NotBot (P.remove r m)
  end.

Lemma gamma_forget : forall (app:t) rs rs' x,
  γ app rs ->
  (forall y, x<>y -> rs y = rs' y) ->
  γ (forget app x) rs'.

Lemma gamma_app: forall (m: t) (rs: P.elt -> B),
  γ m rs ->
  forall r, γ (get m r) (rs r).
Hint Resolve gamma_app.

End lat.

End WPFun.

Class EqDec (T: Type) := eq_dec : ∀ x y : T, { x = y } + { x ≠ y }.
Instance PosEqDec : EqDec positive := peq.

Definition upd `{X: Type} `{EqDec X} {Y} (f: X → Y) (p: X) (v:Y) :=
  fun q => if eq_dec p q 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'.