Require Import String.
Require Import List.
Require Import Sumbool.
Require Import Bool.
Require Import Permutation.
Require Import Morphisms.
Require Import Setoid.
Require Import EquivDec.
Require Import Equivalence.
Require Import Peano_dec.
Require Import Ascii.
Require Import CoqLibAdd.
Require Import ListAdd.
Require Import StringAdd.
Require Import Lift.

Section Assoc.

Association lists

  
  Section Defn.
    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.
    Definition codomain (l:list (A*B)) := map (@snd A B) l.

    Definition map_codomain {A B C} (f:B->C) (l:list (A*B)) : list (A*C)
      := map (fun b => (fst b, f (snd 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 codomain_nil (l:list (A*B)) :
      codomain l = nil <-> l = nil.

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

    Lemma codomain_rev (l:list (A*B)) : codomain (rev l) = rev (codomain 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_codom {l : list (A * B)} {a : A} {b : B} :
      In (a, b) l -> In b (codomain 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.

    Local Hint Constructors NoDup : qcert.
    
    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').

    Lemma lookup_split {l:list (A*B)} {a b} :
      lookup l a = Some b ->
      exists l1 l2 : list (A*B), l = l1 ++ (a,b) :: l2 /\ ~ In a (domain l1).

    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.

    Local Hint Resolve in_dom_lookup_strong in_dom : qcert.
    Lemma in_lookup_strong : forall {l} {a:A} {b0:B}, In (a,b0) l -> {v | lookup l a = Some v}.

    Local Hint Resolve in_dom_lookup in_dom : qcert.

    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 in_in_split_domain_or (l:list (list (A*B))) a :
      (exists l1 la l2, l = l1++la::l2 /\ In a (domain la) /\ ~ In a (domain (concat l1)))
      \/ Forall (fun x => ~ In a (domain x)) l.

    Lemma in_in_split_domain_first {l:list (list (A*B))} {a} :
      In a (domain (concat l)) ->
      exists l1 la l2, l = l1++la::l2 /\ In a (domain la) /\ ~ In a (domain (concat l1)).

    Lemma update_app_in (l1 l2:list (A*B)) v d :
      In v (domain l1) ->
      update_first (l1++l2) v d = update_first l1 v d ++ l2.

    Lemma update_app_nin (l1 l2:list (A*B)) v d :
      ~ In v (domain l1) ->
      update_first (l1++l2) v d = l1 ++ update_first l2 v d.

    Lemma update_app_nin2 (l1 l2:list (A*B)) v d :
      ~ In v (domain l2) ->
      update_first (l1++l2) v d = update_first l1 v d ++ l2.

    Lemma update_first_concat_disjoint_push (ls:list (list (A*B))) v d:
      all_disjoint (map domain ls) ->
      (update_first (concat ls) v d) =
      (concat (map (fun x => update_first x v d) ls)).

    Lemma Forall_update_first P (l:list (A*B)) x v :
      Forall P l ->
      P (x,v) ->
      Forall P (update_first l x v).

    Lemma update_first_in_or {l : list (A * B)} {z} {x} {v} :
      In z (update_first l x v) ->
      In z l \/ z = (x,v).

    Lemma update_first_update_first_eq (l:list (A*B)) v d1 d2 :
      update_first (update_first l v d1) v d2 = update_first l v d2.
    
    Lemma update_first_update_first_neq_swap (l:list (A*B)) v1 d1 v2 d2 :
      v1 <> v2 ->
      update_first (update_first l v1 d1) v2 d2 =
      update_first (update_first l v2 d2) v1 d1.

    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_update_eq_in {l:list (A*B)} {a} {n:B} :
      In a (domain l) ->
      lookup (update_first l a n) a = Some n.
    
    Lemma lookup_update_neq {l a a'} {n:B} : a<>a' -> lookup (update_first l a n) a' = lookup l a'.

    Lemma in_update_break_first {l:list (A*B)} {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
          /\ ~ In a (domain l1).

    Lemma in_domain_split_or (l:list (A*B)) a :
      (exists l1 b l2, l = l1++(a,b)::l2 /\ ~ In a (domain l1))
      \/ ~ In a (domain l).

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

  Lemma map_codomain_update_first {A B C} (f:B->C) dec (l:list (A*B)) v d :
    map_codomain f (update_first dec l v d) =
    update_first dec (map_codomain f l) v (f d).


  Lemma Forall2_lookup_none {K A B} {P:A->B->Prop}
        {l : list (K * A)} {l' : list (K * B)} :
    (Forall2
       (fun (d : K * A) (r : K * B) =>
          fst d = fst r /\ P (snd d) (snd r)) l l') ->
    forall {dec s},
      lookup dec l' s = None ->
      lookup dec l s = None.

  Lemma Forall2_lookup_some {K A B} {P:A->B->Prop}
        {l : list (K * A)} {l' : list (K * B)} :
    (Forall2
       (fun (d : K * A) (r : K * B) =>
          fst d = fst r /\ P (snd d) (snd r)) l l') ->
    forall {dec} {s:K} {d':B},
      lookup dec l' s = Some d' ->
      (exists d'', lookup dec l s = Some d'' /\ P d'' d').

  Lemma Forall2_lookup_some_with_key {K A B} {P:K->A->B->Prop}
        {l : list (K * A)} {l' : list (K * B)} :
    (Forall2
       (fun (d : K * A) (r : K * B) =>
          fst d = fst r /\ P (fst d) (snd d) (snd r)) l l') ->
    forall {dec} {s:K} {d':B},
      lookup dec l' s = Some d' ->
      (exists d'', lookup dec l s = Some d'' /\ P s d'' d').
  Lemma lookup_map_same_domain {A B C:Type} dec
        (f:(A*B)->(A*C)) l v :
    domain l = domain (map f l) ->
    lookup dec (map f l) v = lift (fun x => snd (f (v,x))) (lookup dec l v).

  Lemma lookup_map_codomain {A B C:Type} dec (f:B->C) (l:list (A*B)) v :
    lookup dec (map_codomain f l) v = lift f (lookup dec l v).

  Lemma lookup_map_codomain_unfolded {A B C:Type} dec (f:B->C) (l:list (A*B)) v :
    lookup dec (map (fun b => (fst b, f (snd b))) l) v = lift f (lookup dec l v).

  Lemma domain_map_codomain {A B C} (f:B->C) (l:list (A*B)) :
    domain (map_codomain f l) = domain l.

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

  Lemma cut_down_to_lookup_some
        {A B} {dec:EqDec A eq}
        (l:list (A*B)) l2 a y :
    lookup dec (cut_down_to l l2) a = Some y ->
    lookup dec l a = Some y /\ In a l2 .

  Lemma cut_down_to_lookup_in
        {A B} {dec:EqDec A eq}
        (l:list (A*B)) l2 a :
    In a l2 ->
    lookup dec (cut_down_to l l2) a = lookup dec l a.

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

  Lemma cut_down_to_incl
        {A B} {dec:EqDec A eq}
        (l:list (A*B)) (l2:list A) :
    incl (cut_down_to l l2) l.
  
  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.

  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.

  Lemma Forall2_lookupr_none {K A B} {P:A->B->Prop} {l : list (K * A)} {l' : list (K * B)} :
    (Forall2
       (fun (d : K * A) (r : K * B) =>
          fst d = fst r /\ P (snd d) (snd r)) l l') ->
    forall {Q1 Q2} {dec s},
      @assoc_lookupr K B Q1 Q2 dec l' s = None ->
      assoc_lookupr dec l s = None.

  Lemma Forall2_lookupr_some {K A B} {P:A->B->Prop} {l : list (K * A)} {l' : list (K * B)} :
    (Forall2
       (fun (d : K * A) (r : K * B) =>
          fst d = fst r /\ P (snd d) (snd r)) l l') ->
    forall {Q1 Q2} {dec} {s:K} {d':B},
      @assoc_lookupr K B Q1 Q2 dec l' s = Some d' ->
      (exists d'', assoc_lookupr dec l s = Some d'' /\ P d'' d').

  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.

  Local Hint Resolve NoDup_app_inv : qcert.

  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)) :
    List.length (domain l) = List.length l.
  
  Lemma domain_app {A B:Type} (l₁ l₂:list (A*B)) :
    domain (l₁ ++ l₂) = domain l₁ ++ domain l₂.

  Lemma codomain_length {A B:Type} (l:list (A*B)) :
    List.length (codomain l) = List.length l.
  
  Lemma codomain_app {A B:Type} (l₁ l₂:list (A*B)) :
    codomain (l₁ ++ l₂) = codomain l₁ ++ codomain l₂.

  Lemma app_inv_head_domain {A B:Type} {l1 l2 l1' l2' : list (A*B)} :
    l1 ++ l2 = l1' ++ l2' ->
    domain l1' = domain l1 ->
    l1 = l1' /\ l2 = l2'.
  
  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.

    Local Hint Constructors NoDup : qcert.

    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.

    Global Instance lookup_equiv_lookup
      : Proper (lookup_equiv ==> eq ==> eq) (@lookup A B dec).

    Lemma lookup_equiv_cons_same {l1 l2:list (A*B)} :
      lookup_equiv l1 l2 ->
      forall a,
        lookup_equiv (a::l1) (a::l2).

    Lemma lookup_equiv_app {l1 l2 l1' l2':list (A*B)} :
      lookup_equiv l1 l1' ->
      lookup_equiv l2 l2' ->
      lookup_equiv (l1++l2) (l1'++l2').

    Lemma lookup_equiv_appl_same {l1 l2:list (A*B)} :
      lookup_equiv l1 l2 ->
      forall l,
        lookup_equiv (l++l1) (l++l2).

    Lemma lookup_equiv_appr_same {l1 l2:list (A*B)} :
      lookup_equiv l1 l2 ->
      forall l,
        lookup_equiv (l1++l) (l2++l).

    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 cut_down_to_lookup_incl
          (l:list (A*B)) (l2:list A) :
      lookup_incl (cut_down_to l l2) l.

    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.

    Lemma update_first_NoDup_perm_invs (f g:B->B) {l1 l2} {a:A} {v1 v2:B} :
      NoDup (domain l1) ->
      Permutation (update_first dec l1 a (f v1)) (update_first dec l2 a (g v2)) ->
      lookup dec l1 a = Some v1 ->
      lookup dec l2 a = Some v2 ->
      (forall x y, f x = g y -> x = y) ->
      Permutation l1 l2 /\ v1 = v2 /\ f v1 = g v2.

    Lemma assoc_lookupr_lookup_nodup x (ls:list (A*B)):
      NoDup (domain ls) ->
      assoc_lookupr dec ls x = lookup dec ls x.

    Lemma NoDup_lookup_equiv_equivlist (l1 l2:list (A*B)) :
      NoDup (domain l1) ->
      NoDup (domain l2) ->
      lookup_equiv l1 l2 ->
      equivlist l1 l2.

    Lemma NoDup_lookup_equiv_Permutation (l1 l2:list (A*B)) :
      NoDup (domain l1) ->
      NoDup (domain l2) ->
      lookup_equiv l1 l2 ->
      Permutation l1 l2.
    
    Definition assoc_lookupr_equiv
               (l1 l2:list (A*B))
      := forall x : A, assoc_lookupr dec l1 x = assoc_lookupr dec l2 x.

    Global Instance assoc_lookupr_equiv_equiv : Equivalence (assoc_lookupr_equiv).

    Global Instance assoc_lookupr_equiv_app:
      Proper (assoc_lookupr_equiv ==> assoc_lookupr_equiv ==> assoc_lookupr_equiv) (@app (A*B)).

    Lemma assoc_lookupr_equiv_cons_in (s:A) (d:B) l :
      In s (domain l) ->
      assoc_lookupr_equiv l ((s, d) :: l).

  End lookup_eq.

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

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

  Section Lookup_equiv_on.

    Definition lookup_equiv_on {A B} {dec:EqDec A eq}
               (dom:list A) (l1 l2:list (A*B))
      := forall x, In x dom -> lookup dec l1 x = lookup dec l2 x.
    
    Lemma cut_down_to_lookup_equiv_on {A B} {dec:EqDec A eq}
          (l:list (A*B)) l2 :
      lookup_equiv_on l2 (cut_down_to l l2) l.
    
    Lemma lookup_equiv_on_is_cut_down_equiv {A B} {dec:EqDec A eq}
          (dom:list A) (l1 l2:list (A*B))
      : lookup_equiv_on dom l1 l2
        <->
        lookup_equiv (cut_down_to l1 dom) (cut_down_to l2 dom).

    Global Instance lookup_equiv_on_equiv {A B} {dec:EqDec A eq} l
      : Equivalence (@lookup_equiv_on A B dec l).

    Lemma lookup_equiv_on_lookup_equiv {A B : Type} (dec : EqDec A eq)
          (l1 l2 : list (A * B)) :
      lookup_equiv l1 l2 <-> (forall dom, lookup_equiv_on dom l1 l2).

    Lemma lookup_equiv_on_dom_incl {A B} {dec:EqDec A eq}
          (dom1 dom2:list A) (l1 l2:list (A*B))
      : incl dom2 dom1 ->
        lookup_equiv_on dom1 l1 l2 ->
        lookup_equiv_on dom2 l1 l2.

    Lemma lookup_equiv_on_dom_app_f {A B} {dec:EqDec A eq}
          {dom1 dom2:list A} {l1 l2:list (A*B)}
      : lookup_equiv_on dom1 l1 l2 ->
        lookup_equiv_on dom2 l1 l2 ->
        lookup_equiv_on (dom1++dom2) l1 l2.
    
    Lemma lookup_equiv_on_dom_app {A B} {dec:EqDec A eq}
          (dom1 dom2:list A) (l1 l2:list (A*B))
      : lookup_equiv_on (dom1++dom2) l1 l2 ->
        lookup_equiv_on dom1 l1 l2
        /\ lookup_equiv_on dom2 l1 l2.

    Lemma lookup_equiv_on_cons_same {A B} {dec:EqDec A eq} {l} {l1 l2:list (A*B)} :
      lookup_equiv_on l l1 l2 ->
      forall a,
        lookup_equiv_on l (a::l1) (a::l2).

    Global Instance lookup_equiv_on_incl_prop {A B} {dec:EqDec A eq} :
      Proper ((@incl A) --> eq ==> eq ==> Basics.impl) (@lookup_equiv_on A B dec).

    Lemma lookup_equiv_on_update_first {A B} {dec:EqDec A eq} fvs (l₁ l₂:list (A*B)) v d :
      lookup_equiv_on fvs l₁ l₂ ->
      lookup_equiv_on fvs (update_first equiv_dec l₁ v d)
                      (update_first equiv_dec l₂ v d).

  End Lookup_equiv_on.

  Section alldisjoint.
    
    Lemma all_disjoint_domain_has_same_eq {A B} {ls:list (list (A*B))} :
      all_disjoint (map domain ls) ->
      forall l1 l2,
        In l1 ls ->
        In l2 ls ->
        forall x,
          In x (domain l1) -> In x (domain l2) -> l1 = l2.

  End alldisjoint.

  Section concat.

    Lemma concat_lookup_some_break {A B:Type} {dec:EqDec A eq} {ls:list (list (A*B))} {x:A} {v:B} :
      lookup dec (List.concat ls) x = Some v ->
      exists ll1 ll ll2, ls = ll1++ll::ll2
                         /\ lookup dec ll x = Some v
                         /\ ~ In x (domain (concat ll1)).

  End concat.

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