Notations for finite sets of atoms

Common set operations and constants may be written using more convenient notations.

We define some abbreviations for the empty set, singleton sets, and the union of two sets.

Open the notation scopes declared above.

Environments

We can use our implementation of association lists (in AssocList) to implement association lists whose keys are atoms. Thanks to parameter inlining, the types in the instantiated functor will all use atom for the type for keys.

We provide alternative names for the tactics on association lists to reflect our use of association lists for environments.

As an alternative to the x ¬ a notation, we also provide more list-like notation for writing association lists consisting of a single binding. Implementation note: The following notation overlaps with the standard recursive notation for lists, e.g., the one found in the Program library of Coq's standard library.

Cofinite quantification

Consider a rule H (equivalently, constructor, lemma, etc.) whose type begins with ∀ L, ... and contains hypotheses of the form (∀ y, y `notin` L → ...). The tactic (pick fresh x excluding F and apply H) applies H to the current goal, instantiating H's first argument (L) with the finite set of atoms F. In each new subgoal of the form (∀ y, y `notin` F → ...), the atom y is introduced as x, and (y `notin` F) is introduced using a generated name. If we view H as a rule that uses cofinite quantification, the tactic can be read as picking a sufficiently fresh atom to open a term with.

The following variant of the tactic excludes the set of atoms returned by the gather_atoms tactic. Redefine gather_atoms if you wish to modify the behavior of this tactic.

Lemma aliases

A number of useful lemmas are given standardized, if somewhat unintuitive, names. Here, we define some intuitive aliases for them.

Hints

The next block of hints is to help auto discharge many of the inequality and freshness goals that arise in programming language metatheory proofs. Implementation note (BEA): The eassumption step is intended to address those cases where eauto tries to use a cofinite rule. The pattern goes something like this:

• Apply a cofinite rule with no idea what "L" should be. This adds a hypothesis x `notin` ?1 to the context.
• Apply the IH.
• eassumption resolves the x `notin` L obligation of the IH against the previously introduced x `notin` ?1 hypothesis.

This ensures that the autorewrite step does not trigger an infinite loop.

The next block of hints are occasionally useful when reasoning about finite sets. In some instances, they obviate the need to use auto with set.

Decidable equality

We prefer that "==" refer to decidable equality at eq, as defined by the EqDec_eq class from the CoqEqDec library.

Ott compatibility

Implementation note (BEA): The following definitions make this library usable with the output of Ott's locally nameless backend. They may disappear or change as Ott changes.