Top.Util.Atom

Support for atoms, i.e., objects with decidable equality. We provide here the ability to generate an atom fresh for any finite collection, e.g., the lemma atom_fresh_for_set, and a tactic to pick an atom fresh for the current proof context.

Authors: Arthur Charguéraud and Brian Aydemir.

Implementation note: In older versions of Coq, OrderedTypeEx redefines decimal constants to be integers and not natural numbers. The following scope declaration is intended to address this issue. In newer versions of Coq, the declaration should be benign.

Definition

Atoms are structureless objects such that we can always generate one fresh from a finite collection. Equality on atoms is eq and decidable. We use Coq's module system to make abstract the implementation of atoms. The Export AtomImpl line below allows us to refer to the type atom and its properties without having to qualify everything with "AtomImpl.".

Module Type ATOM.

  Parameter atom : Set.

  Parameter atom_fresh_for_list :
    ∀ (xs : list atom), {x : atom | ¬ List.In x xs }.

  Declare Module Atom_as_OT : UsualOrderedType with Definition t := atom.

  Parameter eq_atom_dec : ∀ x y : atom, {x = y } + {x ≠ y }.

End ATOM.

The implementation of the above interface is hidden for documentation purposes.

Module AtomImpl : ATOM.

End AtomImpl.

Finite sets of atoms

Definitions

Module AtomSet : FiniteSets.S with Module E := Atom_as_OT :=
FiniteSets.Make Atom_as_OT.

The type atoms is the type of finite sets of atoms.

Notation atoms := AtomSet.F.t.

Basic operations on finite sets of atoms are available, in the remainder of this file, without qualification. We use Import instead of Export in order to avoid unnecessary namespace pollution.

We instantiate two modules which provide useful lemmas and tactics work working with finite sets of atoms.

Module AtomSetDecide := FSetDecide.Decide AtomSet.F.
Module AtomSetNotin := FSetNotin.Notin AtomSet.F.
Module AtomSetFacts := FSetFacts.Facts AtomSet.F.
Module AtomSetProperties := FSetProperties.Properties AtomSet.F.

Tactics for working with finite sets of atoms

The tactic fsetdec is a general purpose decision procedure for solving facts about finite sets of atoms.

The tactic notin_simpl simplifies all hypotheses of the form (~ In x F), where F is constructed from the empty set, singleton sets, and unions.

The tactic notin_solve, solves goals of the form (~ In x F), where F is constructed from the empty set, singleton sets, and unions. The goal must be provable from hypothesis of the form simplified by notin_simpl.

Lemmas for working with finite sets of atoms

We make some lemmas about finite sets of atoms available without qualification by using abbreviations.

Notation eq_if_Equal := AtomSet.eq_if_Equal.
Notation notin_empty := AtomSetNotin.notin_empty.
Notation notin_singleton := AtomSetNotin.notin_singleton.
Notation notin_singleton_rw := AtomSetNotin.notin_singleton_rw.
Notation notin_union := AtomSetNotin.notin_union.

Additional properties

One can generate an atom fresh for a given finite set of atoms.

Lemma atom_fresh_for_set : ∀ L : atoms, { x : atom | ¬ In x L }.

Additional tactics

Picking a fresh atom

We define three tactics which, when combined, provide a simple mechanism for picking a fresh atom. We demonstrate their use below with an example, the example_pick_fresh tactic.

(gather_atoms_with F) returns the union of (F x), where x ranges over all objects in the context such that (F x) is well typed. The return type of F should be atoms. The complexity of this tactic is due to the fact that there is no support in Ltac for folding a function over the context.

(beautify_fset V) takes a set V built as a union of finite sets and returns the same set with empty sets removed and union operations associated to the right. Duplicate sets are also removed from the union.

The tactic (pick fresh Y for L) takes a finite set of atoms L and a fresh name Y, and adds to the context an atom with name Y and a proof that (~ In Y L), i.e., that Y is fresh for L. The tactic will fail if Y is already declared in the context.

Tactic Notation "pick" "fresh" ident(Y) "for" constr(L) :=
  let Fr := fresh "Fr" in
  let L := beautify_fset L in
  (destruct (atom_fresh_for_set L) as [Y Fr]).

Demonstration

The example_pick_fresh tactic below illustrates the general pattern for using the above three tactics to define a tactic which picks a fresh atom. The pattern is as follows:

Repeatedly invoke gather_atoms_with, using functions with different argument types each time.
Union together the result of the calls, and invoke (pick fresh ... for ...) with that union of sets.

Lemma example_pick_fresh_use : ∀ (x y z : atom) (L1 L2 L3: atoms), True.
Proof.
intros x y z L1 L2 L3. example_pick_fresh k.

At this point in the proof, we have a new atom k and a hypothesis Fr : ¬ In k (union L1 (union L2 (union L3 (union (singleton x) (union (singleton y) (singleton z)))))).

trivial.
Qed.

Definition disjoint (xs : atoms) (ys: atoms) : Prop :=
AtomSet.F.Empty (AtomSet.F.inter xs ys).

Notation "a `disjoint` b" := (disjoint a b) (at level 1) : metatheory_scope.