Module RAssoc

Require Import List.
Require Import Sumbool.
Require Import Bool.

Require Import Permutation.
Require Import Equivalence.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Peano_dec.

Require Import RUtil RList RString.

Section RAssoc.

  Section assoc.
    Context {A B:Type}.
    Context (dec:forall a a':A, {a=a'} + {a<>a'}).

    Fixpoint lookup l a : option B
      := match l with
           | nil => None
           | (f',v')::os => if dec a f' then Some v' else lookup os a
         end.

    Fixpoint update_first l a n : list (A*B)
      := match l with
           | nil => nil
           | (f',v')::os => if dec a f' then (a,n)::os else (f',v')::(update_first os a n)
         end.

    Definition domain (l:list (A*B)) := map (@fst A B) l.

    Lemma domain_eq (l:list (A*B)) : domain l = map fst l.
    
    Lemma domain_nil (l:list (A*B)) :
      domain l = nil <-> l = nil.

    Lemma domain_rev (l:list (A*B)) : domain (rev l) = rev (domain l).

    Lemma domain_update_first l a v: domain (update_first l a v) = domain l.

    Lemma map_eta_fst_domain l :
      (map (fun x : A * B => fst x) l) = domain l.

    Lemma in_dom : forall {l} {a b}, In (a,b) l -> In a (domain l).

    Lemma in_domain_in : forall {l} {a}, In a (domain l) -> exists b, In (a,b) l.

    Lemma lookup_none_nin : forall {l} {a:A}, lookup l a = None -> ~ In a (domain l).

   Lemma lookup_nin_none {l x} : ~ In x (domain l) -> lookup l x = None.

    Lemma NoDup_domain_NoDup {l} : NoDup (domain l) -> NoDup l.

    Lemma lookup_in : forall l {a:A} {b:B}, lookup l a = Some b -> In (a,b) l.

    Lemma lookup_in_domain : forall l {a:A} {b:B}, lookup l a = Some b -> In a (domain l).

    Lemma lookup_to_front {l a x} : lookup l a = Some x -> exists l', Permutation l ((a,x)::l').

    Global Instance dom_perm : Proper (@Permutation (A*B) ==> @Permutation A) domain.

    Global Instance perm_nodup :Proper (@Permutation (A) ==> iff) (@NoDup A).

    Lemma nodup_in_eq : forall {l} {a b c}, NoDup (domain l) -> In (a,b) l -> In (a,c) l -> b = c.


    Lemma in_dom_lookup_strong : forall {l} {a:A}, In a (domain l) -> {v | lookup l a = Some v}.

    Lemma in_dom_lookup : forall {l} {a:A}, In a (domain l) -> exists v, lookup l a = Some v.

    Lemma in_lookup_strong : forall {l} {a:A} {b0:B}, In (a,b0) l -> {v | lookup l a = Some v}.

    Lemma in_lookup : forall {l} {a:A} {b0:B}, In (a,b0) l -> exists v, lookup l a = Some v.

    Lemma in_lookup_nodup : forall {l} {a:A} {b:B}, NoDup (domain l) -> In (a,b) l -> lookup l a = Some b.

    Lemma nin_update {l a} : lookup l a = None -> forall v, update_first l a v = l.

    Lemma in_update_break {l a v} :
      lookup l a = Some v -> forall vv,
                             exists l1 l2, l = l1++(a,v)::l2 /\
                                           update_first l a vv = l1++(a,vv)::l2.

    Lemma lookup_some_nodup_perm {l l'} a v:
      NoDup (domain l) ->
      Permutation l l' ->
      lookup l a = Some v ->
      lookup l' a = Some v.

    Lemma lookup_none_perm {l l'} a :
      Permutation l l' ->
      lookup l a = None ->
      lookup l' a = None.

    Lemma update_first_NoDup_perm_proper {l l'} a v :
      NoDup (domain l) ->
      Permutation l l' ->
      Permutation (update_first l a v) (update_first l' a v).

    Lemma lookup_app {l1 l2} x:
      lookup (l1++l2) x =
      match lookup l1 x with
        | Some y => Some y
        | None => lookup l2 x
      end.

    Lemma lookup_app_in {l1 l2} a b :
      lookup (l1++l2) a = Some b -> In (a,b) l1 \/ In (a,b) l2.
        
    Lemma domain_cons a (l:list (A*B)) :
      domain (a::l) = (fst a)::domain l.
    
  End assoc.

  Lemma cut_down_to_incl_to
        {A B} {dec:EqDec A eq}
        (l:list (A*B)) l2 :
    incl (domain (cut_down_to l l2)) l2.
  
  Lemma incl_domain_cut_down_incl
        {A B} {dec:EqDec A eq}
        (l:list (A*B)) l2 :
    incl l2 (domain l) ->
    incl l2 (domain (cut_down_to l l2)).

  Global Instance domain_incl_proper A B : Proper (@incl (A*B) ==> @incl A) (@domain A B).

  Fixpoint assoc_lookupr {A B:Type} {P Q:A->A->Prop} (eqd:forall a a':A, {P a a'} + {Q a a'}) (l:list (A*B)) (a:A) : option B
    := match l with
       | nil => None
       | cons (a',d) r2 =>
         match assoc_lookupr eqd r2 a with
         | Some d' => Some d'
         | None =>
           if eqd a a'
           then Some d
           else None
         end
       end.
  
  Fixpoint projectr {A B:Type} {P Q:A->A->Prop} (eqd:forall a a':A, {P a a'} + {Q a a'}) (l:list (A*B)) (ats:list A) : list (option (A*B)) :=
    match ats with
    | nil => nil
    | cons a ats' =>
      match assoc_lookupr eqd l a with
      | Some d => (Some (a,d)) :: (projectr eqd l ats')
      | None => None :: (projectr eqd l ats')
      end
    end.

  Require Import Permutation.

  Lemma assoc_lookupr_app {A B:Type} (l1 l2:list (A*B)) x (dec:forall x y, {x=y} + {x <> y}) :
    assoc_lookupr dec (l1++l2) x =
    match assoc_lookupr dec l2 x with
    | Some y => Some y
    | None => assoc_lookupr dec l1 x
    end.

  Lemma assoc_lookupr_lookup
        {A B} dec x (ls:list (A*B)):
    assoc_lookupr dec ls x = lookup dec (rev ls) x.
  
  Lemma lookup_assoc_lookupr
        {A B} dec x (ls:list (A*B)):
    lookup dec ls x = assoc_lookupr dec (rev ls) x.

  Lemma in_dom_lookupr_strong {A B:Type} (l:list (A*B)) a (dec:forall x y, {x=y} + {x <> y}) :
    In a (domain l) -> {v|assoc_lookupr dec l a = Some v}.

  Lemma in_dom_lookupr {A B:Type} (l:list (A*B)) a (dec:forall x y, {x=y} + {x <> y}) :
    In a (domain l) -> exists v, assoc_lookupr dec l a = Some v.

  Lemma assoc_lookupr_in {A B:Type} (l :list (A*B)) a b (dec:forall x y, {x=y} + {x <> y}) :
    assoc_lookupr dec l a = Some b -> In (a,b) l.

  Lemma assoc_lookupr_none_nin {A B}
         (dec : forall x0 y : A, {x0 = y} + {x0 <> y}) {l x} :
    assoc_lookupr dec l x = (@None B) -> ~ In x (domain l).

  Lemma assoc_lookupr_nodup_perm {A B:Type} (l l':list (A*B)) x (dec:forall x y, {x=y} + {x <> y}) :
    NoDup (domain l) -> Permutation l l' -> assoc_lookupr dec l x = assoc_lookupr dec l' x.

  Lemma in_split_strong {A:Type} `{EqDec A eq} {x} {l:list A} : In x l -> {l1:list A & {l2:list A | l = l1 ++ x::l2}}.

  Lemma assoc_lookupr_nin_none {A B:Type} (l:list (A*B)) x (dec:forall x y, {x=y} + {x <> y}) : ~ In x (domain l) -> assoc_lookupr dec l x = None.

  Lemma in_assoc_lookupr_nodup {A B:Type} (l:list (A*B)) a b (dec:forall x y, {x=y} + {x <> y}):
    NoDup (domain l) -> In (a,b) l -> assoc_lookupr dec l a = Some b.

  Definition permutation_dec {A:Type} `{EqDec A eq} (l l':list A)
    : {Permutation l l'} + {~Permutation l l'}.

  Lemma permutation_prover {A:Set} {dec:EqDec A eq}
           (l1 l2:list A)
           (pf:holds (permutation_dec l1 l2)) :
              Permutation l1 l2.

  Lemma NoDup_app_inv {A:Type} {a b:list A} : NoDup (a++b) -> NoDup a.

  Hint Resolve NoDup_app_inv.

  Lemma NoDup_app_inv2 {A:Type} {a b:list A} : NoDup (a++b) -> NoDup b.

  Lemma domain_length {A B:Type} (l:list (A*B)) :
    length (domain l) = length l.
  
  Lemma domain_app {A B:Type} (l₁ l₂:list (A*B)) :
    domain (l₁ ++ l₂) = domain l₁ ++ domain l₂.

  Section distinctdom.
    Fixpoint bdistinct_domain {A B} {R} `{dec:EqDec A R} (l:list (A*B)) :=
      match l with
      | nil => nil
      | x :: l' =>
        let dl' := bdistinct_domain l' in
        if (existsb (fun z => (fst x) ==b (fst z)) dl') then
          dl' else x::dl'
      end.

    Lemma bdistinct_domain_NoDup {A B} {dec:EqDec A eq} (l:list (A*B)) :
      NoDup (domain (bdistinct_domain l)).

    Lemma bdistinct_domain_domain_equiv {A B} {dec:EqDec A eq} (l:list (A*B)) :
      equivlist (domain (bdistinct_domain l)) (domain l).

    Lemma bdistinct_rev_domain_equivlist {A B} {dec:EqDec A eq} (l:list (A*B)) :
      equivlist ((domain l)) (domain (bdistinct_domain (rev l))).

    Lemma bdistinct_domain_assoc_lookupr {A B} {dec:EqDec A eq} (l:list (A*B)) :
      forall x,
        assoc_lookupr dec (bdistinct_domain l) x
        = assoc_lookupr dec l x.

  End distinctdom.
  
  Section lookup_eq.
    Context {A B:Type}.
    Context {dec:EqDec A eq}.

    Definition lookup_incl (l1 l2:list (A*B)) : Prop
      := forall (x:A) (y:B), lookup dec l1 x = Some y ->
                             lookup dec l2 x = Some y.

    Global Instance lookup_incl_pre : PreOrder lookup_incl.
      
    Definition lookup_equiv (l1 l2:list (A*B)) : Prop
      := forall (x:A), lookup dec l1 x = lookup dec l2 x.

    Global Instance lookup_equiv_equiv : Equivalence lookup_equiv.

    Global Instance lookup_incl_equiv : subrelation lookup_equiv lookup_incl.

    Global Instance lookup_incl_part : PartialOrder lookup_equiv lookup_incl.

    Lemma lookup_incl_dec_nodup {decb:EqDec B eq} :
      forall x y, NoDup (domain x) -> {lookup_incl x y} + {~ lookup_incl x y}.

    Lemma lookup_incl_dec {decb:EqDec B eq} :
      forall x y, {lookup_incl x y} + {~ lookup_incl x y}.

    Instance lookup_equiv_eqdec {decb:EqDec B eq} :
      EqDec (list (A*B)) lookup_equiv.

    Lemma lookup_incl_cons_l_nin (l1 l2:list (A*B)) x y :
      lookup_incl l1 l2 ->
      ~ In x (domain l1) ->
      lookup_incl l1 ((x,y)::l2).

    Lemma lookup_remove_duplicate l v x l' x' l'' :
      lookup_equiv
        (l ++ (v,x)::l' ++ (v,x')::l'')
        (l ++ (v,x)::l' ++ l'').

    Lemma lookup_remove_nin l v0 (x:B) l' v :
      v <> v0 ->
      lookup dec (l ++ (v0,x) :: l') v = lookup dec (l ++ l') v.

    Lemma lookup_swap_neq l1 v1 x1 v2 x2 l2 :
      v1 <> v2 ->
      lookup_equiv
        (l1++(v1,x1)::(v2,x2)::l2)
        (l1++(v2,x2)::(v1,x1)::l2).

    Lemma lookup_equiv_perm_nodup {l1 l2} :
      NoDup (domain l1) ->
      Permutation l1 l2 ->
      lookup_equiv l1 l2.

  End lookup_eq.

  Lemma assoc_lookupr_lookup_nodup {A B} dec x (ls:list (A*B)):
    NoDup (domain ls) ->
      assoc_lookupr dec ls x = lookup dec ls x.
  
    Lemma remove_domain_filter {A B} `{dec:EqDec A eq} s l:
    remove equiv_dec s (domain l) =
    domain (filter (fun x : A * B => s <>b fst x) l).
  
   Lemma fold_left_remove_all_nil_in_not_inv {B} {x ps l}:
     In x (fold_left
        (fun (h : list nat) (xy : nat * B) =>
         remove_all (fst xy) h)
        ps l) ->
     ~ In x (domain ps).

   Lemma fold_left_remove_all_nil_in {B} {x ps l}:
     In x l ->
     ~ In x (domain ps) ->
     In x (fold_left
        (fun (h : list nat) (xy : nat * B) =>
         remove_all (fst xy) h)
        ps l).

     Definition swap {A B} (xy:A*B) := (snd xy, fst xy).

  Section swap.
    Lemma swap_idempotent {A B} (a:A*B) : swap (swap a) = a.
  
    Lemma in_swap {A B} x (l:list (A*B)):
      In x (map swap l) <-> In (swap x) l.

    Lemma in_swap_in {A B} x (l:list (A*B)):
      In (swap x) (map swap l) <-> In x l.
    
  End swap.

  Section ldiff.

    Fixpoint lookup_diff {A B C:Type} (dec:forall a a':A, {a=a'} + {a<>a'}) (l₁:list (A*B)) (l₂:list (A*C)) :=
      match l₁ with
        | nil => nil
        | x::xs => match lookup dec l₂ (fst x) with
                     | None => x::lookup_diff dec xs l₂
                     | Some _ => lookup_diff dec xs l₂
                   end
      end.

    Lemma lookup_diff_none1 {A B C:Type} (dec:forall a a':A, {a=a'} + {a<>a'}) {l₁:list(A*B)} (l₂:list (A*C)) {x} :
      lookup dec l₁ x = None ->
      lookup dec (lookup_diff dec l₁ l₂) x = None.

    Lemma lookup_diff_none2 {A B C:Type} (dec:forall a a':A, {a=a'} + {a<>a'}) (l₁:list (A*B)) {l₂:list (A*C)} {x} :
      lookup dec l₂ x = None ->
      lookup dec (lookup_diff dec l₁ l₂) x = lookup dec l₁ x.

    Lemma lookup_diff_some2 {A B C:Type} (dec:forall a a':A, {a=a'} + {a<>a'}) (l₁:list(A*B)) {l₂:list (A*C)} {x t} :
      lookup dec l₂ x = Some t ->
      lookup dec (lookup_diff dec l₁ l₂) x = None.

    Lemma lookup_diff_inv {A B C} (dec:forall a a':A, {a=a'} + {a<>a'})
          x (l1:list (A*B)) (l2:list (A*C)):
      In x (lookup_diff dec l1 l2) ->
      In x l1 /\ ~ In (fst x) (domain l2).

    Lemma lookup_diff_nilr {A B C:Type}
          (dec:forall a a':A, {a=a'} + {a<>a'})
          (l₁:list (A*B)) :
      (lookup_diff dec l₁ (@nil (A*C))) = l₁.

    Lemma NoDup_lookup_diff {A B:Type} (dec:forall a a':A, {a=a'} + {a<>a'})
          {r₁ r₂:list (A*B)} :
      NoDup (domain r₁) -> NoDup (domain (lookup_diff dec r₁ r₂)).

    Lemma lookup_diff_domain_bounded {A B C} dec l₁ l₂ :
      incl (domain l₁) (domain l₂) ->
      @lookup_diff A B C dec l₁ l₂ = nil.

    Lemma lookup_diff_bounded {A B} dec l₁ l₂ :
      incl l₁ l₂ ->
      @lookup_diff A B B dec l₁ l₂ = nil.

    Lemma lookup_diff_same_domain2 {A B C D} dec (l1:list (A*B)) (l2:list (A*C)) (l3:list (A*D)) :
      equivlist (domain l2) (domain l3) ->
      lookup_diff dec l1 l2 = lookup_diff dec l1 l3.

    Lemma map_lookup_diff {A B C} dec (f:A*B->A*C) (l1:list (A*B)) (l2:list (A*C)):
      (forall a, fst a = fst (f a)) ->
      map f (lookup_diff dec l1 l2) = lookup_diff dec (map f l1) l2.

    Lemma lookup_diff_disjoint
          {A B:Type}
          (dec:forall a a':A, {a=a'} + {a<>a'})
          (l₁ l₂:list (A*B)) :
      disjoint (domain (lookup_diff dec l₁ l₂)) (domain l₂).
    
  End ldiff.

  Section substlist.
    
    Definition substlist_subst {A} {dec:EqDec A eq}
               (substlist:list (A*A)) (inp:A)
      := match lookup equiv_dec substlist inp with
         | Some x => x
         | None => inp
         end.
    
  End substlist.

  Section conv.
    Require Import List Ascii String.
    Import ListNotations.
    
    Definition ascii_mk_lower_substtable
      := [("A", "a");("B", "b");("C", "c");("D", "d");("E", "e")
          ;("F", "f");("G", "g");("H", "h");("I", "i");("J", "j")
          ;("K", "k");("L", "l");("M", "m");("N", "n");("O", "o")
          ;("P", "p");("Q", "q");("R", "r");("S", "s");("T", "t")
          ;("U", "u");("V", "v");("W", "w");("X", "x");("Y", "y")
          ;("Z", "z")]%char.

    Definition ascii_mk_lower (c:ascii) : ascii
      := substlist_subst ascii_mk_lower_substtable c.

    Definition mk_lower (s:string) : string
      := map_string ascii_mk_lower s.

  End conv.
  
End RAssoc.