Library AssocList

Require Import Decidable.
Require Import FSetWeak.
Require Import List.

Require Import AdditionalTactics.
Require Import ListFacts.
Require Import FSetWeakDecide.

Implementation


We implement association lists as a functor over an implementation of finite sets of keys. This allows us to define a domain function on association lists that returns a finite set of keys, as opposed to, say, a list of keys. Note that the UsualDecidableType argument requires that equality on keys be eq (Coq's "built-in" equality) and decidable.

Note that our library has an implicit convention for the "normal form" of an association list. This normal form requires that a list be built only from nil (the empty list), one (the singleton list), and app (concatenation). Additionally, concatenations should be associated to the right and the list should not contain any nil terms, unless it is the empty list itself.

This allows association lists to be written in a slightly more uniform manner when compared to using both cons and app to build them. The downsides are that Coq's simpl tactic will simplify instances of one down to cons and that there are instances in which one needs to write association lists that are not in normal form (typically, some concatenation will need to be associated to the left). The simpl_alist and rewrite_alist tactics below are designed to minimize the impact of these downsides.

We have considered other alternative implementations, but the scheme described above seems to work the best in practice.

Module Make
  (X : UsualDecidableType)
  (Import KeySet : FSetWeakInterface.S with Module E := X).

  Module Import D := Decide KeySet.
  Module KeySetProperties := Properties KeySet.

Basic definitions


This section defines the following basic operations and predicates on association lists.

  • one: Constructs an association list consisting of exactly one binding.
  • map: Maps a function over the values in an association list.
  • dom: Computes the domain of an association list, i.e., the set consisting of its keys.
  • disjoint: Binary predicate that holds when the domains of two association lists are disjoint.
  • binds: Ternary predicate that holds when a key-value pair appears somewhere in an association list.
  • uniq: Unary predicate that holds when an association list binds any given key at most once. Note that uniq_push is defined in terms of one, due to our normal form for association lists.


Implicit arguments are declared by default for these definitions. We define some local notations to make the definition of uniq easier to read and to be consistent with the notations used in the rest of this library.

  Section Definitions.
    Variables A B C : Type.

    Definition one (C : Type) (item : C) : list C := cons item nil.

    Definition map (f : A -> B) (E : list (X.t*A)) : list (X.t*B) :=
      List.map (fun b => match b with (x, a) => (x, f a) end) E.

    Fixpoint dom (A : Type) (E : list (X.t*A)) {struct E} : KeySet.t :=
      match E with
        | nil => empty
        | (x, _) :: E' => add x (dom E')
      end.

    Definition disjoint (E : list (X.t*A)) (F : list (X.t*B)) : Prop :=
      Subset (inter (dom E) (dom F)) empty.

    Definition binds (x : X.t) (a : A) (E : list (X.t*A)) : Prop :=
      List.In (x, a) E.

    Notation Local "x ~ a" := (one (x, a)) (at level 68).
    Notation Local "x `notin` E" := (~ KeySet.In x E) (at level 69).

    Inductive uniq : list (X.t*A) -> Prop :=
      | uniq_nil :
          uniq nil
      | uniq_push : forall x a E,
          uniq E ->
          x `notin` dom E ->
          uniq ((x ~ a) ++ E).

  End Definitions.

Local notations


We make a local notation for one, and for operations and predicate on finite sets, in order to make the statements of the lemmas below more readable. The notations are local so that users of this functor may choose their own notations.

  Notation Local "[ i ]" := (one i).
  Notation Local "x ~ T" := (one (x, T)) (at level 68).

  Notation Local "E `union` F" :=
     (KeySet.union E F) (at level 69, right associativity).
  Notation Local "x `in` E" :=
     (KeySet.In x E) (at level 69).
  Notation Local "x `notin` E" :=
     (~ KeySet.In x E) (at level 69).
  Notation Local "E [=] F" :=
     (KeySet.Equal E F) (at level 70, no associativity).
  Notation Local "E [<=] F" :=
     (KeySet.Subset E F) (at level 70, no associativity).

List properties


The following block of properties is used mainly for rewriting association lists into the normal form described above. See the simpl_alist and rewrite_alist tactics below.

  Section ListProperties.
    Variables X : Type.
    Variables x y : X.
    Variables l l1 l2 l3 : list X.

    Lemma cons_app_one :
      cons x l = [ x ] ++ l.

    Lemma cons_app_assoc :
      (cons x l1) ++ l2 = cons x (l1 ++ l2).

    Lemma app_assoc :
      (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3).

    Lemma app_nil_1 :
      nil ++ l = l.

    Lemma app_nil_2 :
      l ++ nil = l.

    Lemma in_one :
      List.In x [ y ] <-> x = y.

    Lemma in_app :
      List.In x (l1 ++ l2) <-> List.In x l1 \/ List.In x l2.

  End ListProperties.

  Hint Rewrite cons_app_one cons_app_assoc app_assoc : rewr_list.
  Hint Rewrite app_nil_1 app_nil_2 : rewr_list.
  Hint Rewrite in_one in_app : rewr_list_in.

The following block of properties is an assortment of structural properties about lists.

  Section AssortedListProperties.
    Variables X : Type.
    Variables x y : X.
    Variables l l1 l2 l3 : list X.

    Lemma one_eq_app :
      [ x ] ++ l1 = l2 ++ l3 ->
      (exists qs, l2 = x :: qs /\ l1 = qs ++ l3) \/
      (l2 = nil /\ l3 = x :: l1).

    Lemma app_eq_one :
      l2 ++ l3 = [ x ] ++ l1 ->
      (exists qs, l2 = x :: qs /\ l1 = qs ++ l3) \/
      (l2 = nil /\ l3 = x :: l1).

    Lemma nil_neq_one_mid :
      nil <> l1 ++ [ x ] ++ l2.

    Lemma one_mid_neq_nil :
      l1 ++ [ x ] ++ l2 <> nil.

  End AssortedListProperties.

Properties of map and dom


The following lemmas are used mainly to simplify applications of map and dom to association lists. See also the simpl_alist and rewrite_alist tactics below.

  Section Properties.
    Variables A B : Type.
    Variables f : A -> B.
    Variables x : X.t.
    Variables b : A.
    Variables E F G : list (X.t*A).

    Lemma map_nil :
      map f nil = nil.

    Lemma map_cons :
      map f ((x, b) :: E) = (x, f b) :: map f E.

    Lemma map_one :
      map f (x ~ b) = (x ~ f b).

    Lemma map_app :
      map f (E ++ F) = map f E ++ map f F.

    Lemma dom_nil :
      (@dom A nil) = empty.

    Lemma dom_cons :
      dom ((x, b) :: E) [=] singleton x `union` dom E.

    Lemma dom_one :
      dom (x ~ b) [=] singleton x.

    Lemma dom_app :
      dom (E ++ F) [=] dom E `union` dom F.

    Lemma dom_map :
      dom (map f E) [=] dom E.

  End Properties.

  Hint Rewrite map_nil map_cons map_one map_app : rewr_map.
  Hint Rewrite dom_nil dom_cons dom_one dom_app dom_map : rewr_dom.

The simpl_alist tactic


The simpl_alist tactic rewrites association lists so that they are in the normal form described above. Similar to the simpl tactic, we define "in *" and "in H" variants of the tactic.

  Ltac simpl_alist :=
    autorewrite with rewr_list rewr_list_in rewr_map rewr_dom.
  Tactic Notation "simpl_alist" "in" hyp(H) :=
    autorewrite with rewr_list rewr_list_in rewr_map rewr_dom in H.
  Tactic Notation "simpl_alist" "in" "*" :=
    autorewrite with rewr_list rewr_list_in rewr_map rewr_dom in *.

The rewrite_alist tactic


The tactic (rewrite_alist E) replaces an association list in the conclusion of the goal with E. Suitability for replacement is determined by whether simpl_alist can put E and the chosen environment in the same normal form, up to convertibility's in Coq. We also define an "in H" variant that performs the replacement in a hypothesis H.

  Tactic Notation "rewrite_alist" constr(E) :=
    match goal with
      | |- context[?x] =>
        change x with E
      | |- context[?x] =>
        replace x with E;
          [ | try reflexivity; simpl_alist; reflexivity ]
    end.

  Tactic Notation "rewrite_alist" constr(E) "in" hyp(H) :=
    match type of H with
      | context[?x] =>
        change x with E in H
      | context[?x] =>
        replace x with E in H;
          [ | try reflexivity; simpl_alist; reflexivity ]
    end.

Basic facts about disjoint


  Section BasicDisjointFacts.
    Implicit Types A B C : Type.

    Lemma disjoint_sym_1 :
      forall A B (E : list (X.t*A)) (F : list (X.t*B)),
        disjoint E F ->
        disjoint F E.

    Lemma disjoint_sym :
      forall A B (E : list (X.t*A)) (F : list (X.t*B)),
      disjoint E F <-> disjoint F E.

    Lemma disjoint_one_1 :
      forall A B (x : X.t) (a : A) (F : list (X.t*B)),
      disjoint (x ~ a) F ->
      x `notin` dom F.

    Lemma disjoint_one_2 :
      forall A B (x : X.t) (a : A) (F : list (X.t*B)),
      x `notin` dom F ->
      disjoint (x ~ a) F.

    Lemma disjoint_one_l :
      forall A B (x : X.t) (a : A) (E : list (X.t*B)),
      disjoint (x ~ a) E <-> x `notin` dom E.

    Lemma disjoint_one_r :
      forall A B (x : X.t) (a : A) (E : list (X.t*B)),
      disjoint E (x ~ a) <-> x `notin` dom E.

    Lemma disjoint_app_1 :
      forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
      disjoint (E ++ F) G ->
      disjoint E G.

    Lemma disjoint_app_2 :
      forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
      disjoint (E ++ F) G ->
      disjoint F G.

    Lemma disjoint_app_3 :
      forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
      disjoint E G ->
      disjoint F G ->
      disjoint (E ++ F) G.

    Lemma disjoint_app_l :
      forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
      disjoint (E ++ F) G <-> disjoint E G /\ disjoint F G.

    Lemma disjoint_app_r :
      forall A B (E F : list (X.t*A)) (G : list (X.t*B)),
      disjoint G (E ++ F) <-> disjoint E G /\ disjoint F G.

    Lemma disjoint_map_1 :
      forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
      disjoint (map f E) F ->
      disjoint E F.

    Lemma disjoint_map_2 :
      forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
      disjoint E F ->
      disjoint (map f E) F.

    Lemma disjoint_map_l :
      forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
      disjoint (map f E) F <-> disjoint E F.

    Lemma disjoint_map_r :
      forall A B C (E : list (X.t*A)) (F : list (X.t*B)) (f : A -> C),
      disjoint F (map f E) <-> disjoint E F.

  End BasicDisjointFacts.

Basic facts about uniq


The following lemmas are facts about uniq with respect to the basic functions (one, app, and map) that can be used to build association lists.

  Section UniqProperties.
    Variables A B : Type.
    Variables f : A -> B.
    Variables x : X.t.
    Variables b : A.
    Variables E F G : list (X.t*A).

    Lemma uniq_one :
      uniq (x ~ b).

    Lemma uniq_app_1 :
      uniq (E ++ F) -> uniq E.

    Lemma uniq_app_2 :
      uniq (E ++ F) -> uniq F.

    Lemma uniq_app_3 :
      uniq (E ++ F) -> disjoint E F.

    Lemma uniq_app_4 :
      uniq E ->
      uniq F ->
      disjoint E F ->
      uniq (E ++ F).

    Lemma uniq_app :
      uniq (E ++ F) <-> uniq E /\ uniq F /\ disjoint E F.

    Lemma uniq_map_1 :
      uniq (map f E) ->
      uniq E.

    Lemma uniq_map_2 :
      uniq E ->
      uniq (map f E).

    Lemma uniq_map :
      uniq (map f E) <-> uniq E.

  End UniqProperties.

  Hint Rewrite
    disjoint_one_l disjoint_one_r
    disjoint_app_l disjoint_app_r
    disjoint_map_l disjoint_map_r
    uniq_app uniq_map
  : rewr_uniq.

The solve_uniq tactic


This tactic attempts to solve goals about uniq. Given its definition, it's likely to work only when the hypotheses in the goal already contain all the relevant uniq propositions. Thus, the tactic may not be generally useful. It is useful, however, for proving facts about uniq such as the ones below.

Implementation note: The second simpl_alist in the definition is because of disjoint_one_{l,r}. The "|| fail" at the end is so that in the case of failure, the error message reported to the user is not the one from fsetdec.

  Ltac solve_uniq :=
    try trivial;
    simpl_alist in *;
    autorewrite with rewr_uniq in *;
    simpl_alist in *;
    intuition (
      auto using uniq_nil, uniq_one ||
      (rewrite -> disjoint_sym; auto) ||
      (unfold disjoint in *; fsetdec))
    || fail.

Facts about uniq


  Section UniqDerived.
    Variables A : Type.
    Variables x y : X.t.
    Variables a b : A.
    Variables E F G : list (X.t*A).

    Lemma uniq_cons :
      uniq E ->
      x `notin` dom E ->
      uniq ((x, a) :: E).

    Lemma uniq_insert_mid :
      uniq (G ++ E) ->
      x `notin` dom (G ++ E) ->
      uniq (G ++ (x ~ a) ++ E).

    Lemma uniq_remove_mid :
      uniq (E ++ F ++ G) ->
      uniq (E ++ G).

    Lemma uniq_map_app_l : forall (f : A -> A),
      uniq (F ++ E) ->
      uniq (map f F ++ E).

    Lemma fresh_mid_tail :
      uniq (F ++ (x ~ a) ++ E) ->
      x `notin` dom E.

    Lemma fresh_mid_head :
      uniq (F ++ (x ~ a) ++ E) ->
      x `notin` dom E.

  End UniqDerived.

Basic facts about binds


The following lemmas are facts about binds with respect to the basic functions (one and app) that can be used to build association lists.

Note: map is treated further below.

  Section BindsProperties.
    Variables A : Type.
    Variables x y : X.t.
    Variables a b : A.
    Variables E F G : list (X.t*A).

    Lemma binds_nil :
      binds x a nil <-> False.

    Lemma binds_one_1 :
      x = y ->
      a = b ->
      binds x a (y ~ b).

    Lemma binds_one_2 :
      binds x a (y ~ b) ->
      x = y.

    Lemma binds_one_3 :
      binds x a (y ~ b) ->
      a = b.

    Lemma binds_one :
      binds x a (y ~ b) <-> x = y /\ a = b.

    Lemma binds_app_1 :
      binds x a E ->
      binds x a (E ++ F).

    Lemma binds_app_2 :
      binds x a F ->
      binds x a (E ++ F).

    Lemma binds_app_3 :
      binds x a (E ++ F) ->
      binds x a E \/ binds x a F.

    Lemma binds_app :
      binds x a (E ++ F) <-> binds x a E \/ binds x a F.

  End BindsProperties.

  Hint Rewrite binds_nil binds_one binds_app : rewr_binds.
  Hint Rewrite binds_nil binds_one : rewr_binds_uniq.

Additional lemmas and tactics for working with binds


  Section MoreBindsProperties.
    Variables A : Type.
    Variables x y : X.t.
    Variables a b : A.
    Variables E F G : list (X.t*A).

    Lemma binds_dom_contradiction: forall (E : list (X.t*A)),
      binds x a E ->
      x `notin` dom E ->
      False.

    Lemma binds_app_uniq :
      uniq (E ++ F) ->
      (binds x a (E ++ F) <->
        (binds x a E /\ x `notin` dom F) \/
        (binds x a F /\ x `notin` dom E)).

  End MoreBindsProperties.

  Hint Rewrite binds_app_uniq using solve_uniq : rewr_binds_uniq.

The apply_binds_dom_contradiction tactic solves a goal by applying the binds_dom_contradiction lemma. The tactic succeeds only if the the hypotheses of the lemma are immediately satisfied.

  Ltac apply_binds_dom_contradiction :=
    match goal with
      | H : binds ?x ?a ?E, J : ?x `notin` (dom ?E) |- _ =>
        assert False by apply (@binds_dom_contradiction _ _ _ _ H J);
        intuition
      | H : binds ?x ?a ?E, J : ?x `in` (dom ?E) -> False |- _ =>
        assert False by apply (@binds_dom_contradiction _ _ _ _ H J);
        intuition
    end.

The solve_binds tactic attempts to solve goals about binds. Given its definition, it's likely to work only when the hypotheses in the goal already contain all the relevant binds propositions. Thus, the tactic may not be generally useful. It is useful, however, for proving facts about binds such as the ones below.

  Ltac solve_binds :=
    simpl_alist in *;
    autorewrite with rewr_binds in *;
    intuition (auto || fsetdec || apply_binds_dom_contradiction)
    || fail.

The tactics analyze_binds and analyze_binds_uniq tactics take as an argument a hypotheses about binds and perform a case analysis based on the structure of the association list. In the case of analyze_binds_uniq, the analysis is performed assuming that the association list is uniq. The lemmas binds_app and binds_app_uniq are examples of such case analysis.

Implementation notes:

  • The initial calls to simpl_alist put the relevant association lists into normal form.
  • In the case of binds_app_uniq, we assert that the association list is uniq. This enables the autorewrite step to succeed.
  • Rather than work on H itself, we copy it and work on the copy. Thus, in instances where the analysis leaves unsolved subgoals, it is still possible to see the original hypothesis.
  • The rest of the tactic breaks apart the copy of H and tries several simple means for solving the resulting subgoals.

  Ltac analyze_binds H :=
    simpl_alist;
    simpl_alist in H;
    match type of H with
      | binds ?x ?a ?E =>
        let J := fresh in
        pose proof H as J;
        autorewrite with rewr_binds in J;
        simpl_alist in J;
        try (progress decompose [and or] J; clear J);
        try solve [trivial | discriminate | intuition | fsetdec]
    end.

  Ltac analyze_binds_uniq H :=
    simpl_alist;
    simpl_alist in H;
    match type of H with
      | binds ?x ?a ?E =>
        match goal with
          | H : uniq ?E |- _ => idtac
          | _ => assert (uniq E); [ try solve_uniq | ]
        end;
        let J := fresh in
        pose proof H as J;
        autorewrite with rewr_binds_uniq in J;
        simpl_alist in J;
        try (progress decompose [and or] J; clear J);
        try solve [trivial | discriminate | intuition | fsetdec]
    end.

Facts about binds


  Section BindsDerived.
    Variables A B : Type.
    Variables f : A -> B.
    Variables x y : X.t.
    Variables a b : A.
    Variables E F G : list (X.t*A).

    Lemma binds_dec :
      (forall a b : A, {a = b} + {a <> b}) ->
      {binds x a E} + {~ binds x a E}.

    Lemma binds_lookup_dec :
      decidable (exists a, binds x a E).

    Lemma binds_lookup_dec_specif :
      {a : A | binds x a E} + (forall a, ~ binds x a E).

    Lemma binds_map :
      binds x a E ->
      binds x (f a) (map f E).

    Lemma binds_map_inv :
      (forall a b, f a = f b -> a = b) ->
      binds x (f a) (map f E) ->
      binds x a E.

    Lemma binds_weaken :
      binds x a (E ++ G) ->
      binds x a (E ++ F ++ G).

    Lemma binds_mid_eq :
      binds x a (F ++ (x ~ b) ++ E) ->
      uniq (F ++ (x ~ b) ++ E) ->
      a = b.

    Lemma binds_remove_mid :
      binds x a (F ++ (y ~ b) ++ G) ->
      x <> y ->
      binds x a (F ++ G).

    Lemma binds_In : forall x a (E : list (X.t*A)),
      binds x a E ->
      x `in` dom E.

    Lemma binds_unique :
      binds x a E ->
      binds x b E ->
      uniq E ->
      a = b.

    Lemma fresh_app_l :
      uniq (F ++ E) ->
      binds x a E ->
      x `notin` dom F.

    Lemma fresh_app_r :
      uniq (F ++ E) ->
      binds x a F ->
      x `notin` dom E.

  End BindsDerived.

End Make.

This page has been generated by coqdoc