association lists
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].