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.