Library d3

Listes d'association

Require Import List.

Domaines abstraits pour les clefs et les valeurs
Variable KEY : Set.
Variable VAL : Set.

Egalité booléenne sur le domaine KEY


Axiome

Variable eqb_key : KEY → KEY → bool.

Axiom eqb_key_is_eq : ∀ (k k':KEY),
    (eqb_key k k')=true ↔ k=k'.

Equivalence égalité booléenne et égalité propositionnelle

On se donne les deux sens de l'axiome eqb_key_is_eq
Lemma eq_eqb_key: ∀ (k k':KEY), (k = k') → (eqb_key k k' = true).
Proof.
  intros k k'.
  elim (eqb_key_is_eq k k').
  auto.
Qed.

Lemma eqb_key_eq: ∀ (k k':KEY), (eqb_key k k' = true) → (k = k').
Proof.
  intros k k'.
  elim (eqb_key_is_eq k k').
  auto.
Qed.

Contraposée
Lemma not_eq_eqb_key: ∀ k k':KEY, (k ≠ k') → (eqb_key k k' = false).
Proof.
  intros.
  case_eq (eqb_key k k').
  - intros H'.
    exfalso.
    apply H.
    apply eqb_key_eq.
    assumption.
  - trivial.
Qed.

Lemma eqb_key_false_eq : ∀ k k':KEY, (eqb_key k k' = false) → (k ≠ k').
Proof.
 intros.
 intro.  rewrite (eq_eqb_key k k' H0) in H.
 discriminate.
Qed.

Réflexivité

Lemma eqb_key_refl: ∀ k : KEY,
 eqb_key k k = true.
Proof.
  intro.
  apply eq_eqb_key.
  reflexivity.
Qed.

Décidabilité de l'égalité propositionnelle

Lemma eq_key_dec: ∀ (k k':KEY), (k=k') ∨ (k≠k').
Proof.
  intros.
  case_eq (eqb_key k k').
  - intro.
    left.
    exact (eqb_key_eq k k' H).
  - intro.
    right.
    exact (eqb_key_false_eq k k' H).
Qed.

Listes d'association

Definition alist := list (KEY × VAL).

Fonction assoc

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.

Injectivité de Some
Lemma eq_some_eq : ∀ (T:Type) (x y:T),
    Some x = Some y → x = y.
Proof.
  intros.
  inversion H.
  trivial.
Qed.

Correction
Lemma assoc_some_in : ∀ (k:KEY) (v:VAL) (kvs:alist),
    (assoc k kvs) = Some (k,v) → (In (k,v) kvs).
Proof.
  induction kvs.
  - simpl.
    intro.
    discriminate.
  - destruct a.
    simpl.
    case (eqb_key k k0).
    + intro.
      left.
      apply eq_some_eq.
      assumption.
    + intro.
      right.
      apply IHkvs.
      assumption.
Qed.

Lemma assoc_none_tl : ∀ (k:KEY) (a:(KEY×VAL)) (kvs:alist),
    (assoc k (a::kvs)) = None → (assoc k kvs) = None.
Proof.
  intros.
  destruct a.
  case_eq (eqb_key k k0).
  + intro.
    simpl in H.
    rewrite H0 in H.
    discriminate.
  + intro.
    simpl in H.
    rewrite H0 in H.
    assumption.
Qed.

Lemma assoc_none_in : ∀ (k:KEY) (v:VAL) (kvs:alist),
    (assoc k kvs) = None → not (In (k,v) kvs).
Proof.
  induction kvs.
  - intro.
    simpl.
    intro.
    assumption.
  - destruct a.
    intro.
    intro.
    elim H0.
    + intro.
      injection H1.
      intros.
      rewrite H3 in H.
      simpl in H.
      rewrite eqb_key_refl in H.
      discriminate.
    + apply IHkvs.
      apply assoc_none_tl with (a:=(k0,v0)).
      assumption.
Qed.

Complétude

Lemma in_assoc_none: ∀ (k:KEY) (kvs:alist),
    (∀ (v:VAL), not (In (k,v) kvs)) → (assoc k kvs) = None.
Proof.
  induction kvs.
  - intro.
    trivial.
  - destruct a.
    intro.
    case_eq (eqb_key k k0).
    + intro.
      exfalso.
      apply H with (v0:=v).
      rewrite (eqb_key_eq k k0 H0).
      simpl.
      left.
      trivial.
    + intro.
      simpl.
      rewrite H0.
      apply IHkvs.
      intro.
      intro.
      apply H with (v0:=v0).
      simpl.
      right.
      assumption.
Qed.

Lemma in_assoc_some : ∀ (k:KEY) (v:VAL) (kvs:alist),
    (In (k,v) kvs) → (∃ (v:VAL), (assoc k kvs) = Some (k,v)).
Proof.
Admitted.

Modification de liaison. Fonction aset

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 : ∀ (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 : ∀ (k:KEY), ∀ (v:VAL), ∀ (kvs:alist),
        (aset k v kvs) = None → (assoc k kvs) = None.
Proof.
Admitted.

Corollary aset_none_in : ∀ (k:KEY), ∀ (v:VAL), ∀ (kvs:alist),
        (aset k v kvs) = None → ∀ (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 : ∀ (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 : ∀ (k k':KEY) (v v':VAL) (kvs kvs':alist),
    (eqb_key k k' = false) → (aset k v ((k',v')::kvs)) = (Some kvs')
    → ∃ (kvs'':alist), kvs' = ((k',v')::kvs'').
Proof.
Admitted.

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

Complétude
Lemma assoc_none_aset : ∀ (k:KEY) (kvs:alist),
    (assoc k kvs) = None → ∀ (v:VAL), (aset k v kvs) = None.
Proof.
Admitted.

Lemma assoc_some_aset : ∀ (k:KEY) (v:VAL) (kvs:alist),
    (assoc k kvs) = Some (k,v) →
    ∀ (v':VAL), ∃ (kvs':alist), (aset k v' kvs) = Some kvs'.
Proof.
Admitted.