# Library Atoms

``` Require Import OrderedType. Require Import OrderedTypeEx. Require Import Arith. Require Import AuxLib. Require Export ExtFset. Require Import ExtFsetImpl. ```

## Atoms

``` ```
 `A : AtomT` is a record containing the fundamental properties of atoms in a nominal setting.
``` Record AtomT : Type := mkAtom {   atom : Set;   asetR : ExtFset atom;   aset := extFset asetR;   atom_eqdec : forall (a b : atom), {a = b} + {a <> b};   atom_infinite : forall (S : aset), { a : atom | ~ In a S } }. Hint Resolve atom_eqdec : nominal. ```
 Declare `atom` as a coercion. For example, if we have `tmvar : AtomT`, then we can say `a b : tmvar` instead of `a b : atom tmvar`.
``` Coercion atom : AtomT >-> Sortclass. ```

## Infrastructure for reasoning about atoms

``` ```
 This tactic splits the proof into the cases where `a = b` and `a <> b`. Then it eliminates situations where one of these statements contradicts other information in the environment using the `congruence` tactic. In the case of `a = b`, we rewrite instances of `a` in the goal to `b`. The first argument to `atom_eqdec` is inferable since the types of `a` and `b` must already be in the context.
``` Section AtomComparisons.    Variable A : AtomT.    Variables a b : atom A.    Variable X : Set.    Variables x1 x2 : X.    Ltac compare_atoms H a b :=     case (atom_eqdec _ a b); intro H; congruence.   Lemma atom_eqdec_eq :     a = b -> (if atom_eqdec A a b then x1 else x2) = x1.   Lemma atom_eqdec_neq :     a <> b -> (if atom_eqdec A a b then x1 else x2) = x2.   Lemma atom_eqdec_contract :     x1 = x2 -> (if atom_eqdec A a b then x1 else x2) = x1. End AtomComparisons. Hint Immediate atom_eqdec_eq atom_eqdec_neq atom_eqdec_contract : nominal. Hint Rewrite atom_eqdec_eq using congruence : nominal. Hint Rewrite atom_eqdec_neq using congruence : nominal. Hint Rewrite atom_eqdec_contract using congruence : nominal. ```
 `atom_eqdec_simpl` performs all reductions of conditionals on atom equality (in the goal or context) for which the relationship of the atoms is inferrable from the context using the `congruence` tactic.
``` Ltac atom_eqdec_simpl :=   repeat (     match goal with     | |- context [if atom_eqdec _ ?a ?b then _ else _] =>         (rewrite (@atom_eqdec_eq _ a b);           [idtac | solve [congruence]]) ||         (rewrite (@atom_eqdec_neq _ a b);           [idtac | solve [congruence]]) ||         (rewrite (@atom_eqdec_contract _ a b);           [idtac | solve [congruence]])     | H : context [if atom_eqdec _ ?a ?b then _ else _] |- _ =>         (rewrite (@atom_eqdec_eq _ a b) in H;           [idtac | solve [congruence]]) ||         (rewrite (@atom_eqdec_neq _ a b) in H;           [idtac | solve [congruence]]) ||         (rewrite (@atom_eqdec_contract _ a b) in H;           [idtac | solve [congruence]])     end). ```
 `atom_eqdec_case H a b` is guaranteed to reduce all subexpressions of the form `if atom_eqdec A a b then _ else _`, splitting the goal into two cases whenever the equality of `a` and `b` cannot be determined from the context using the `congruence` tactic. If the goal is split, the name `H` will be used for the new assumption about the relationship between `a` and `b`.
``` Ltac atom_eqdec_case H a b :=   match goal with   | |- context [if atom_eqdec _ a b then _ else _] =>       repeat (         (rewrite (@atom_eqdec_eq _ a b);         [idtac | solve [congruence]]) ||         (rewrite (@atom_eqdec_neq _ a b);         [idtac | solve [congruence]]) ||         (rewrite (@atom_eqdec_contract _ a b);         [idtac | solve [congruence]])       );       try match goal with       | |- context [if atom_eqdec _ a b then _ else _] =>           case (atom_eqdec _ a b); intro H       end   end. ```

## Definition and properties of swapping

``` Section AtomSwapping.    Variable A : AtomT.    Variables a b c : atom A.   Definition swapa (s : atom A * atom A) (c : atom A) :=     let (a, b) := s in     if atom_eqdec _ a c then b     else if atom_eqdec _ b c then a     else c.   Lemma swapa_left :     swapa (a, b) a = b.   Lemma swapa_left' :     a = c -> swapa (a, b) c = b.   Lemma swapa_right :     swapa (a, b) b = a.   Lemma swapa_right' :     b = c -> swapa (a, b) c = a.   Lemma swapa_neither :     a <> c -> b <> c -> swapa (a, b) c = c. End AtomSwapping. Implicit Arguments swapa_left [A]. Implicit Arguments swapa_left' [A]. Implicit Arguments swapa_right [A]. Implicit Arguments swapa_right' [A]. Implicit Arguments swapa_neither [A]. Hint Rewrite swapa_left : nominal. Hint Rewrite swapa_left' using congruence : nominal. Hint Rewrite swapa_right : nominal. Hint Rewrite swapa_right' using congruence : nominal. Hint Rewrite swapa_neither using congruence : nominal. ```
 `swapa_simpl_once` and `swapa_simpl_hyp` are just auxilary tactics.
``` Ltac swapa_simpl_once a b c :=   (rewrite (@swapa_left' _ a b c);     [idtac | solve [congruence]]) ||   (rewrite (@swapa_right' _ a b c);     [idtac | solve [congruence]]) ||   (rewrite (@swapa_neither _ a b c);     [idtac | solve [congruence] | solve [congruence]]). Ltac swapa_simpl_hyp H a b c :=   (rewrite (@swapa_left' _ a b c) in H;     [idtac | solve [congruence]]) ||   (rewrite (@swapa_right' _ a b c) in H;     [idtac | solve [congruence]]) ||   (rewrite (@swapa_neither _ a b c) in H;     [idtac | solve [congruence] | solve [congruence]]). ```
 `swapa_simpl` performs all reductions of atom swaps (in the goal or assumptions) for which the result is inferrable from the context using the `congruence` tactic.
``` Ltac swapa_simpl :=   repeat (     match goal with     | |- context [swapa _ (?a, ?b) ?c] =>         swapa_simpl_once a b c     | H : context [swapa _ (?a, ?b) ?c] |- _ =>         swapa_simpl_hyp H a b c     end). ```
 `swapa_case H1 H2 a b c` will reduce all expressions of the form `swapa _ (a, b) c` in the goal to either `a`, `b`, or `c`, splitting the goal as necessary, when the relationships between `a` and `c` and between `b` and `c` cannot be inferred from the context. `H1` will be used as the name for a newly introduced assumption about the relationship between `a` and `c`, and respectively `H2` for `b` and `c`. Also, any additional reductions of atom swaps that are inferrable from the context will be performed.
``` Ltac swapa_case H1 H2 a b c :=   swapa_simpl;   try match goal with   | |- context [swapa _ (a, b) c] =>       case (atom_eqdec _ a c); intro H1; try congruence;       swapa_simpl;       try match goal with       | |- context [swapa _ (a, b) c] =>           case (atom_eqdec _ b c); intro H2; try congruence;           swapa_simpl       end   end. Section BasicAtomSwappingProperties.    Variable A : AtomT.    Variables s : A * A.    Variables a b c d e: A.   Lemma swapa_same :     swapa A (a, a) b = b.   Lemma swapa_invol :     swapa A s (swapa A s c) = c.   Lemma swapa_distrib :     swapa A s (swapa A (c, d) e) =     swapa A (swapa A s c, swapa A s d) (swapa A s e). End BasicAtomSwappingProperties. Implicit Arguments swapa_same [A]. Implicit Arguments swapa_invol [A]. Implicit Arguments swapa_distrib [A]. Hint Resolve swapa_same swapa_invol swapa_distrib : nominal. Hint Rewrite swapa_same swapa_invol : nominal. Section MoreAtomSwappingProperties.    Variable A : AtomT.    Variables s : A * A.    Variables x y z : A.   Lemma swapa_injective : swapa A s x = swapa A s y -> x = y.   Lemma swapa_switch : swapa A (x, y) z = swapa A (y, x) z. End MoreAtomSwappingProperties. Hint Immediate swapa_injective : nominal. ```

## Implementing atoms

``` ```
 Keep opaque our means for constructing `AtomT` records. The opaque nature of atoms is for convinience; since we don't declare any axioms based on this fact, our development doesn't become unsound if we make them transparent.
``` Module Type AtomImplementationSig. Parameter mkAtomRec : nat -> AtomT. End AtomImplementationSig. Module AtomImplementation : AtomImplementationSig. ```
 We hide the implementation for documentation purposes. Indirectly, we require proof irrelevance here.
``` End AtomImplementation. Export AtomImplementation. ```
Index
This page has been generated by coqdoc