Require Export list_support.

Section Assoc.
  Variable A B : Type.
  Variable aeq : eq_type A.
  Variable beq : eq_type B.

  Fixpoint assoc(l : list (A × B))(a : A) : option B :=
    match l with
      | [] ⇒ None
      | ab :: l ⇒ if aeq a (fst ab) then Some (snd ab) else assoc l a
    end.

  Fixpoint rassoc(l : list (A × B))(b : B) : option A :=
    match l with
      | [] ⇒ None
      | ab :: l ⇒ if beq b (snd ab) then Some (fst ab) else rassoc l b
    end.

  Lemma assoc_cons_split :
    ∀(P : option B → Prop)(a1 a2 : A)(b : B)(l : list (A × B)),
      (a1 = a2 → P (Some b)) →
      (a1 ≠ a2 → P (assoc l a2)) →
        P (assoc ((a1, b) :: l) a2).

  Lemma assoc_cons_first :
    ∀(a : A)(b : B)(l : list (A × B)),
      assoc ((a, b) :: l) a = Some b.

  Lemma assoc_cons_tail :
    ∀(a1 a2 : A)(b : B)(l : list (A × B)),
      a1 ≠ a2 →
        assoc ((a1, b) :: l) a2 = assoc l a2.

  Lemma rassoc_cons_split :
    ∀(P : option A → Prop)(a : A)(b1 b2 : B)(l : list (A × B)),
      (b1 = b2 → P (Some a)) →
      (b1 ≠ b2 → P (rassoc l b2)) →
        P (rassoc ((a, b1) :: l) b2).

  Lemma rassoc_cons_first :
    ∀(a : A)(b : B)(l : list (A × B)),
      rassoc ((a, b) :: l) b = Some a.

  Lemma rassoc_cons_tail :
    ∀(a : A)(b1 b2 : B)(l : list (A × B)),
      b1 ≠ b2 →
        rassoc ((a, b1) :: l) b2 = rassoc l b2.

  Lemma rassoc_assoc_none :
    ∀(l : list (A × B))(a : A)(b : B),
      rassoc l b = None →
        assoc l a ≠ Some b.

  Lemma assoc_rassoc_some :
    ∀(l : list (A × B))(a : A)(b : B),
      assoc l a = Some b →
        is_some (rassoc l b).

  Lemma assoc_append_split :
    ∀(P : option B → Prop)(l1 l2 : list (A × B))(a : A),
      (is_some (assoc l1 a) → P (assoc l1 a)) →
      (is_none (assoc l1 a) → P (assoc l2 a)) →
        P (assoc (l1 ++ l2) a).

  Lemma assoc_map_split :
    ∀(C : Type)(f : C → A × B)(l : list C)(a : A),
      (assoc (map f l) a = None ∧ ∀(c : C), In c l → fst (f c) ≠ a)
      ∨
      ∃(c : C), In c l ∧
        fst (f c) = a ∧ assoc (map f l) a = Some (snd (f c)).

  Definition injective_assoc(l : list (A × B)) : Prop :=
    ∀(a1 a2 : A),
      assoc l a1 = assoc l a2 →
      is_some (assoc l a1) →
        a1 = a2.

  Lemma injective_assoc_empty : injective_assoc [].

  Lemma injective_assoc_cons_different :
    ∀(l : list (A × B))(a : A)(b : B),
      injective_assoc l →
      (∀(a : A), assoc l a ≠ Some b) →
        injective_assoc ((a, b) :: l).

  Lemma injective_assoc_cons_rassoc :
    ∀(l : list (A × B))(a : A)(b : B),
      injective_assoc l →
      rassoc l b = None →
        injective_assoc ((a, b) :: l).

  Lemma injective_assoc_append :
    ∀(l1 l2 : list (A × B)),
      injective_assoc l1 →
      injective_assoc l2 →
      (∀(a1 a2 : A),
             is_some (assoc l1 a1) →
               assoc l1 a1 ≠ assoc l2 a2) →
        injective_assoc (l1 ++ l2).

  Inductive assoc_mapping : list (A × B) → Prop :=
    | assoc_mapping_nil : assoc_mapping []
    | assoc_mapping_cons :
        ∀(a : A)(b : B)(l : list (A × B)),
          assoc_mapping l →
            is_none (assoc l a) → assoc_mapping ((a, b) :: l).

  Lemma assoc_mapping_tail :
    ∀(a : A)(b : B)(l : list (A × B)),
      assoc_mapping ((a, b) :: l) →
        assoc_mapping l.

  Lemma assoc_mapping_cons_first :
    ∀(a : A)(b : B)(l : list (A × B)),
      assoc_mapping ((a, b) :: l) →
        is_none (assoc l a).

  Lemma rassoc_assoc_some :
    ∀(l : list (A × B))(a : A)(b : B),
      assoc_mapping l →
      rassoc l b = Some a →
        assoc l a = Some b.

  Lemma injective_assoc_tail :
    ∀(a : A)(b : B)(l : list (A × B)),
      assoc_mapping ((a, b) :: l) →
      injective_assoc ((a, b) :: l) →
        injective_assoc l.

  Lemma assoc_rassoc_inj_some :
    ∀(l : list (A × B))(a : A)(b : B),
      assoc_mapping l →
      injective_assoc l →
      assoc l a = Some b →
        rassoc l b = Some a.

  Lemma assoc_In : ∀(l : list (A × B))(a : A)(b : B),
    assoc l a = Some b → In (a, b) l.

  Lemma assoc_In_rev : ∀(l : list (A × B))(a : A)(b : B),
    assoc_mapping l →
    In (a, b) l →
      assoc l a = Some b.

  Lemma incl_assoc_some :
    ∀(l1 l2 : list (A × B))(a : A),
      assoc_mapping l2 →
      incl l1 l2 →
      is_some (assoc l1 a) →
        is_some (assoc l2 a).

  Definition assoc_disjoint_keys(l1 l2 : list (A × B)) : Prop :=
    ∀(a : A),
      (is_some (assoc l1 a) → is_none (assoc l2 a)) ∧
      (is_some (assoc l2 a) → is_none (assoc l1 a)).

  Lemma assoc_disjoint_keys_right_tail :
    ∀(a : A)(b : B)(l1 l2 : list (A × B)),
      assoc_disjoint_keys l1 ((a, b) :: l2) →
        assoc_disjoint_keys l1 l2.

End Assoc.

Implicit Arguments assoc [A B].
Implicit Arguments rassoc [A B].
Implicit Arguments assoc_map_split [A B C].
Implicit Arguments injective_assoc [A B].
Implicit Arguments assoc_mapping [A B].
Implicit Arguments assoc_mapping_tail [A B].
Implicit Arguments assoc_mapping_cons_first [A B].
Implicit Arguments assoc_disjoint_keys [A B].
Implicit Arguments assoc_disjoint_keys_right_tail [A B].

Section Assoc_2.
  Variable A : Type.
  Variable aeq : eq_type A.

  Lemma assoc_swap_pairs :
    ∀(B : Type)(l : list (B × A))(a : A),
      assoc aeq (swap_pairs l) a = rassoc aeq l a.

  Lemma assoc_map_pair :
    ∀(B C : Type)(f : A × B → C)
          (l : list (A × B))(a : A),
      assoc aeq (map (fun(ab : A × B) ⇒ (fst ab, f ab)) l) a =
        match assoc aeq l a with
          | Some b ⇒ Some (f (a, b))
          | None ⇒ None
        end.

  Fixpoint apply_assoc_map(m : list (A × A))(l : list A) : list A :=
    match l with
      | [] ⇒ []
      | a :: l ⇒
        (match assoc aeq m a with
           | Some a' ⇒ a'
           | None ⇒ a
         end
        ) :: (apply_assoc_map m l)
    end.

  Lemma In_apply_assoc_map_member :
    ∀(m : list (A × A))(a1 a2 : A)(l : list A),
      In a1 l →
      assoc aeq m a1 = Some a2 →
        In a2 (apply_assoc_map m l).

  Lemma In_apply_assoc_map_non_member :
    ∀(m : list (A × A))(a : A)(l : list A),
      In a l →
      assoc aeq m a = None →
        In a (apply_assoc_map m l).

  Lemma In_apply_assoc_map_destruct :
    ∀(m : list (A × A))(a : A)(l : list A),
      In a (apply_assoc_map m l) →
        (∃(a' : A), assoc aeq m a' = Some a ∧ In a' l) ∨
        (assoc aeq m a = None ∧ In a l).

  Lemma apply_assoc_map_support :
    ∀(m : list (A × A))(l : list A),
      incl (apply_assoc_map m l) (apply_assoc_map m (list_support aeq l)).

  Lemma apply_assoc_map_append :
    ∀(m : list (A × A))(l1 l2 : list A),
      apply_assoc_map m (l1 ++ l2) =
        (apply_assoc_map m l1) ++ (apply_assoc_map m l2).

  Lemma apply_assoc_map_flatten :
    ∀(m : list (A × A))(ll : list (list A)),
      apply_assoc_map m (flatten ll) =
        flatten (map (apply_assoc_map m) ll).

End Assoc_2.

Implicit Arguments assoc_map_pair [A B C].
Implicit Arguments apply_assoc_map [A].