Library Maps

Require Import List TheoryList.
Require Import ListUtil Tactics.

Set Implicit Arguments.

Axiom ext_eq : forall (S T : Set) (f g : S -> T),
  (forall x, f x = g x) -> f = g.

Module Type EQ.
  Parameter dom : Set.
  Parameter dom_eq_dec : forall (x y : dom), {x = y} + {x <> y}.
End EQ.

Module Type MAP.
   Variable dom : Set.

  Parameter map : Set -> Set.

  Parameter init : forall (ran : Set), ran -> map ran.
  Parameter sel : forall (ran : Set), map ran -> dom -> ran.
  Parameter upd : forall (ran : Set), map ran -> dom -> ran -> map ran.

  Axiom sel_init : forall (ran : Set) (v : ran) a,
    sel (init v) a = v.

  Axiom sel_upd : forall (ran : Set) (m : map ran) a v a',
    (a = a' /\ sel (upd m a v) a' = v)
    \/ (a <> a' /\ sel (upd m a v) a' = sel m a').

  Axiom sel_upd_eq : forall (ran : Set) (m : map ran) a v,
    sel (upd m a v) a = v.

  Axiom sel_upd_neq : forall (ran : Set) (m : map ran) a v a',
    a <> a'
    -> sel (upd m a v) a' = sel m a'.

  Axiom upd_self : forall (ran : Set) (m : map ran) a,
    upd m a (sel m a) = m.
End MAP.

Module FuncMap (Param : EQ) : MAP with Definition dom := Param.dom.
  Import Param.

   Section Map.
     Variable ran : Set.

    Definition map := dom -> ran.

    Definition init (r : ran) : map :=
      fun _ => r.
    Definition sel (m : map) (d : dom) : ran :=
      m d.
    Definition upd (m : map) (d : dom) (r : ran) : map :=
      fun d' =>
        if dom_eq_dec d d'
          then r
          else m d'.

    Theorem sel_init : forall v a,
      sel (init v) a = v.

    Theorem sel_upd : forall m a v a',
      (a = a' /\ sel (upd m a v) a' = v)
      \/ (a <> a' /\ sel (upd m a v) a' = sel m a').

    Theorem sel_upd_eq : forall m a v,
      sel (upd m a v) a = v.

    Theorem sel_upd_neq : forall m a v a',
      a <> a'
      -> sel (upd m a v) a' = sel m a'.

    Theorem upd_self : forall m a,
      upd m a (sel m a) = m.
   End Map.

  Definition dom := dom.
End FuncMap.

Module Type SET.
   Variable dom : Set.

  Parameter set : Set.

  Parameter empty : set.
  Parameter In : dom -> set -> bool.
  Parameter add : set -> dom -> set.
  Parameter remove : set -> dom -> set.
  Parameter union : set -> set -> set.
  Parameter intersect : set -> set -> set.

  Parameter incl : set -> set -> bool.
  Parameter elems : set -> list dom.
  
  Axiom In_add : forall s v v',
    In v' (add s v) = true
    <-> v = v' \/ In v' s = true.

  Axiom In_add_eq : forall s v,
    In v (add s v) = true.

  Axiom In_add_neq : forall s v v',
    v <> v'
    -> In v' (add s v) = In v' s.

  Axiom In_union : forall s s' v,
    In v (union s s') = true
    -> In v s = true \/ In v s' = true.

  Axiom In_union' : forall s s' v,
    In v s = true
    -> In v s' = true
    -> In v (union s s') = true.

  Axiom union_idempotent : forall s,
    union s s = s.

  Axiom In_intersect : forall v s' s,
    In v (intersect s s') = true
    -> In v s = true /\ In v s' = true.

  Axiom In_intersect' : forall v s' s,
    In v (intersect s s') = false
    -> In v s = false \/ In v s' = false.

  Axiom incl_ok : forall s1 s2,
    incl s1 s2 = true <-> (forall x, In x s1 = true -> In x s2 = true).

  Axiom incl_empty : forall s,
    incl empty s = true.

  Axiom In_empty : forall x,
    In x empty = false.

  Axiom incl_refl : forall s,
    incl s s = true.
  
  Axiom incl_false : forall s1 s2,
    incl s1 s2 = false
    -> exists x, In x s1 = true /\ In x s2 = false.

  Axiom incl_trans : forall s1 s2,
    incl s1 s2 = true
    -> forall s3, incl s2 s3 = true
      -> incl s1 s3 = true.

  Axiom incl_In : forall s1 s2,
    incl s1 s2 = true
    -> forall x, In x s1 = true
      -> In x s2 = true.

  Axiom incl_union_left : forall s1 s2,
    incl s1 (union s1 s2) = true.

  Axiom incl_union_right : forall s1 s2,
    incl s2 (union s1 s2) = true.

  Axiom elems_ok : forall s x,
    List.In x (elems s) <-> In x s = true.

  Axiom elems_remove : forall s x ls,
    elems s = x :: ls
    -> elems (remove s x) = ls.

  Axiom In_remove : forall x x' s,
    In x s = true
    -> x <> x'
    -> In x (remove s x') = true.
End SET.

Module ListSet (Param : EQ) : SET with Definition dom := Param.dom.
  Import Param.

   Section Map.
    Definition set := list dom.

    Definition empty : set := nil.

    Definition In (v : dom) (s : set) : bool :=
      if In_eq_dec dom_eq_dec v s
        then true
        else false.

    Definition add (s : set) (v : dom) : set :=
      if In_eq_dec dom_eq_dec v s
        then s
        else v :: s.

    Fixpoint remove (s : set) (v : dom) {struct s} : set :=
      match s with
        | nil => nil
        | v' :: s' =>
          if dom_eq_dec v v'
            then s'
            else v' :: remove s' v
      end.

    Fixpoint union (s1 s2 : set) {struct s1} : set :=
      match s1 with
        | nil => s2
        | v :: s1' => add (union s1' s2) v
      end.

    Fixpoint intersect (s1 s2 : set) {struct s1} : set :=
      match s1 with
        | nil => nil
        | v :: s1' =>
          if In_eq_dec dom_eq_dec v s2
            then v :: intersect s1' s2
            else intersect s1' s2
      end.

    Definition incl (s1 s2 : set) : bool :=
      if incl_eq_dec dom_eq_dec s1 s2
        then true
        else false.
    Definition elems (s : set) : list dom := s.

    Theorem In_add : forall s v v',
      In v' (add s v) = true
      <-> v = v' \/ In v' s = true.

    Theorem In_add_eq : forall s v,
      In v (add s v) = true.

    Theorem In_add_neq : forall s v v',
      v <> v'
      -> In v' (add s v) = In v' s.

    Theorem In_union : forall s s' v,
      In v (union s s') = true
      -> In v s = true \/ In v s' = true.

    Theorem In_union' : forall s s' v,
      In v s = true
      -> In v s' = true
      -> In v (union s s') = true.

    Theorem incl_ok : forall s1 s2,
      incl s1 s2 = true <-> (forall x, In x s1 = true -> In x s2 = true).

    Lemma union_idempotent' : forall s s',
      List.incl s s'
      -> union s s' = s'.

    Theorem In_intersect : forall v s' s,
      In v (intersect s s') = true
      -> In v s = true /\ In v s' = true.

    Theorem In_intersect' : forall v s' s,
      In v (intersect s s') = false
      -> In v s = false \/ In v s' = false.

    Theorem union_idempotent : forall s,
      union s s = s.

    Theorem incl_empty : forall s,
      incl empty s = true.

    Theorem In_empty : forall x,
      In x empty = false.

    Theorem incl_refl : forall s,
      incl s s = true.

    Theorem incl_false : forall s1 s2,
      incl s1 s2 = false
      -> exists x, In x s1 = true /\ In x s2 = false.

    Theorem incl_trans : forall s1 s2,
      incl s1 s2 = true
      -> forall s3, incl s2 s3 = true
        -> incl s1 s3 = true.

    Theorem incl_In : forall s1 s2,
      incl s1 s2 = true
      -> forall x, In x s1 = true
        -> In x s2 = true.

    Theorem incl_union_left : forall s1 s2,
      incl s1 (union s1 s2) = true.

    Theorem incl_union_right : forall s1 s2,
      incl s2 (union s1 s2) = true.

    Theorem elems_ok : forall s x,
      List.In x (elems s) <-> In x s = true.

    Theorem elems_remove : forall s x ls,
      elems s = x :: ls
      -> elems (remove s x) = ls.

    Theorem In_remove : forall x x' s,
      In x s = true
      -> x <> x'
      -> In x (remove s x') = true.

   End Map.

  Definition dom := dom.
End ListSet.

Index
This page has been generated by coqdoc