Qcert.Basic.Util.RAssoc

Section RAssoc.

  Section assoc.
    Context {A B:Type}.
    Context (dec:∀ 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 : ∀ {l} {a b}, In (a,b) l → In a (domain l).

    Lemma in_domain_in : ∀ {l} {a}, In a (domain l) → ∃ b, In (a,b) l.

    Lemma lookup_none_nin : ∀ {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 : ∀ l {a:A} {b:B}, lookup l a = Some b → In (a,b) l.

    Lemma lookup_in_domain : ∀ 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 → ∃ 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 : ∀ {l} {a b c}, NoDup (domain l) → In (a,b) l → In (a,c) l → b = c.


    Lemma in_dom_lookup_strong : ∀ {l} {a:A}, In a (domain l) → {v | lookup l a = Some v}.

    Lemma in_dom_lookup : ∀ {l} {a:A}, In a (domain l) → ∃ v, lookup l a = Some v.

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

    Lemma in_lookup : ∀ {l} {a:A} {b0:B}, In (a,b0) l → ∃ v, lookup l a = Some v.

    Lemma in_lookup_nodup : ∀ {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 → ∀ v, update_first l a v = l.

    Lemma in_update_break {l a v} :
      lookup l a = Some v → ∀ vv,
                             ∃ 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:∀ 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:∀ 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.


  Lemma assoc_lookupr_app {A B:Type} (l1 l2:list (A×B)) x (dec:∀ 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:∀ 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:∀ x y, {x=y} + {x ≠ y}) :
    In a (domain l) → ∃ v, assoc_lookupr dec l a = Some v.

  Lemma assoc_lookupr_in {A B:Type} (l :list (A×B)) a b (dec:∀ 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 : ∀ 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:∀ 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:∀ 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:∀ 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.


  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)) :
      ∀ 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
      := ∀ (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
      := ∀ (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} :
      ∀ x y, NoDup (domain x) → {lookup_incl x y} + {¬ lookup_incl x y}.

    Lemma lookup_incl_dec {decb:EqDec B eq} :
      ∀ 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:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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:∀ 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)):
      (∀ 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:∀ 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.

    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.