Require Import List.

Variable KEY : Set.
Variable VAL : Set.

(* == Egalité décidable sur KEY *)
Variable eqb_key : KEY -> KEY -> bool.

Axiom eqb_key_is_eq : forall (k k':KEY),
    (eqb_key k k')=true <-> k=k'.

Lemma eq_eqb_key: forall (k k':KEY), (k = k') -> (eqb_key k k' = true).
Proof.
  Admitted.

Lemma eqb_key_eq: forall (k k':KEY), (eqb_key k k' = true) -> (k = k').
Proof.
  Admitted.

Lemma not_eq_eqb_key: forall k k':KEY, (k <> k') -> (eqb_key k k' = false).
Proof.
  Admitted.

Lemma eqb_key_false_eq : forall k k':KEY, (eqb_key k k' = false) -> (k <> k').
Proof.
  Admitted.

Lemma eqb_key_refl: forall k : KEY,
 eqb_key k k = true.
Proof.
  Admitted.

Lemma eq_key_dec: forall (k k':KEY), (k=k') \/ (k<>k').
Proof.
  Admitted.
    
(* == Listes d'association *)
Definition alist := list (KEY * VAL).

Fixpoint assoc (k:KEY) (kvs:alist) : option (KEY * VAL) :=
match kvs with
| nil => None
| (k',v)::kvs => if (eqb_key k k') then (Some (k',v))
                 else assoc k kvs
end. 

Lemma eq_some_eq : forall (T:Type) (x y:T),
    Some x = Some y -> x = y.
Proof.
Admitted.

(* -- Correction *)
Lemma assoc_some_in : forall (k:KEY) (v:VAL) (kvs:alist),
    (assoc k kvs) = Some (k,v) -> (In (k,v) kvs).
Proof.
  Admitted.

Lemma assoc_none_tl : forall (k:KEY) (a:(KEY*VAL)) (kvs:alist),
    (assoc k (a::kvs)) = None -> (assoc k kvs) = None.
Proof.
Admitted.

Lemma assoc_none_in : forall (k:KEY) (v:VAL) (kvs:alist),
    (assoc k kvs) = None -> not (In (k,v) kvs).
Proof.
Admitted.

(* -- Complétude *)
Lemma in_assoc_none: forall (k:KEY) (kvs:alist),
    (forall (v:VAL), not (In (k,v) kvs)) -> (assoc k kvs) = None.
Proof.
Admitted.

Lemma in_assoc_some : forall (k:KEY) (v:VAL) (kvs:alist),
    (In (k,v) kvs) -> (exists (v:VAL), (assoc k kvs) = Some (k,v)).
Proof.
Admitted.

(* == Modification de liaison *)
Fixpoint aset (k:KEY) (v:VAL) (kvs:alist) : option alist :=
  match kvs with
  | nil => None
  | ((k',v')::kvs) => if (eqb_key k k')
               then Some ((k,v)::kvs)
               else match (aset k v kvs) with
                    | None => None
                    | Some kvs' => Some ((k',v')::kvs')
                    end
  end.

(* -- Correction *)
Lemma aset_tl : forall (k k':KEY) (v v':VAL) (kvs kvs':alist),
    (k <> k') -> (aset k v ((k',v')::kvs)) = Some ((k',v')::kvs')
    -> (aset k v kvs) = Some kvs'.
Proof.
Admitted.

Lemma aset_none_assoc : forall (k:KEY), forall (v:VAL), forall (kvs:alist),
        (aset k v kvs) = None -> (assoc k kvs) = None.
Proof.
Admitted.

Corollary aset_none_in : forall (k:KEY), forall (v:VAL), forall (kvs:alist),
        (aset k v kvs) = None -> forall (v:VAL), not (In (k,v) kvs).
Proof.
  intros.
  apply assoc_none_in.
  apply aset_none_assoc with (v:=v).
  assumption.
Qed.

Lemma aset_eqb_true : forall (k k':KEY) (v v':VAL) (kvs kvs':alist),
    (eqb_key k k' = true) -> (aset k v ((k',v')::kvs)) = (Some kvs')
    -> kvs' = (k,v)::kvs.
Proof.
Admitted.

Lemma aset_eqb_false : forall (k k':KEY) (v v':VAL) (kvs kvs':alist),
    (eqb_key k k' = false) -> (aset k v ((k',v')::kvs)) = (Some kvs')
    -> exists (kvs'':alist), kvs' = ((k',v')::kvs'').
Proof.
Admitted.

Lemma aset_some_assoc : forall (k:KEY), forall (v:VAL), forall (kvs kvs':alist),
        (aset k v kvs) = Some kvs' -> assoc k kvs' = Some (k,v).
Proof.
Admitted.

(* -- Complétude *)
Lemma assoc_none_aset : forall (k:KEY) (kvs:alist),
    (assoc k kvs) = None -> forall (v:VAL), (aset k v kvs) = None.
Proof.
Admitted.

Lemma assoc_some_aset : forall (k:KEY) (v:VAL) (kvs:alist),
    (assoc k kvs) = Some (k,v) ->
    forall (v':VAL), exists (kvs':alist), (aset k v' kvs) = Some kvs'.
Proof.
Admitted.