Module Assoc

Require Import Coqlib List.

Section ASSOC.
  Variables A B: Type.

  Variable Aeq: forall (a1 a2: A), {a1=a2}+{a1<>a2}.

  Fixpoint get_assoc (l: list (A*B)) (b: A) : option B :=
    match l with
      nil => None
    | (k,v)::r => if Aeq k b then Some v else get_assoc r b
    end.

  Lemma get_assoc_in_fst:
    forall (l: list (A*B)) b r,
      get_assoc l b = Some r ->
      In b (map fst l).

  Lemma get_assoc_in:
    forall (l: list (A*B)) b r,
      get_assoc l b = Some r ->
      In (b,r) l.

  Lemma in_lnr_get_assoc:
    forall l b f,
      list_norepet (map fst l) ->
      In (b,f) l ->
      get_assoc l b = Some f.

End ASSOC.