Library Atom


Require Import Arith.
Require Import DecidableTypeEx.
Require Import List.
Require Import Max.

Main definition (and implementation)


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 module type ATOM, defined below, is compatible with UsualDecidableType.

Module Type ATOM.
  Parameter t : Set.

  Definition eq := @eq t.
  Definition eq_refl := @refl_equal t.
  Definition eq_sym := @sym_eq t.
  Definition eq_trans := @trans_eq t.

  Parameter eq_dec : ∀ x y : t, {x = y} + {xy}.

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

End ATOM.

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

Module AtomImpl : ATOM.


End AtomImpl.

Auxiliary definitions


We give more suggestive names to some of the constants provided by the AtomImpl module.

Definition atom : Set :=
  AtomImpl.t.

Definition eq_atom_dec : ∀ (x y : atom), {x = y} + {xy} :=
  AtomImpl.eq_dec.

Hint Resolve eq_atom_dec.

This page has been generated by coqdoc