Require Import Atoms.
Require Import Axioms.
|
The main purpose of this file is to provide an implementation of the
following module signature. We use modules here to purposefully keep the
implementation opaque.
We then prove a variety of theorems from the signature (see below). |
Module Type PermutationsAbstraction.
Section PermutationDefinitions.
permt A is the type of permutations of atoms of type A.
|
Parameter permt : AtomT -> Set.
Variable A : AtomT.
| Apply a permutation to an atom. |
Parameter perma : permt A -> A -> A.
| Identity permutation. |
Parameter pid : permt A.
| Inverse of a permutation. |
Parameter pinv : permt A -> permt A.
| Compose two permutations. |
Parameter pcompose : permt A -> permt A -> permt A.
| Extend a permutation by a swap. |
Parameter pextend : (A * A) -> permt A -> permt A.
End PermutationDefinitions.
Implicit Arguments perma [A].
Implicit Arguments pid [A].
Implicit Arguments pinv [A].
Implicit Arguments pcompose [A].
Implicit Arguments pextend [A].
Notation "[]" := (pid) : perms_scope.
Arguments Scope perma [_ perms_scope _ _].
Arguments Scope pinv [_ perms_scope].
Arguments Scope pcompose [_ perms_scope perms_scope].
Arguments Scope pextend [_ _ perms_scope].
Notation "p @ a" :=
(perma p a)
(at level 65, right associativity) : perms_scope.
Notation "- p" :=
(pinv p)
(at level 35, right associativity) : perms_scope.
Notation "p :++ q" :=
(pcompose p q)
(at level 60, right associativity) : perms_scope.
Notation "x :+ p" :=
(pextend x p)
(at level 60, right associativity) : perms_scope.
Notation "[ x ; .. ; y ]" := (pextend x .. (pextend y pid) ..) : perms_scope.
Bind Scope perms_scope with permt.
Open Scope perms_scope.
| Basic properties of permutations. |
Section PermutationBaseProperties.
Variable A : AtomT.
Axiom perma_id :
forall a : A, [] @ a = a.
Axiom perma_inverse :
forall (p : permt A) (a : A), (- p) @ p @ a = a.
Axiom perma_compose :
forall (p q : permt A) (a : A), (p :++ q) @ a = p @ q @ a.
Axiom perma_eq :
forall (p q : permt A), (forall a, p @ a = q @ a) -> p = q.
Axiom perma_extend :
forall (p : permt A) (ab : A * A) (c : A),
(ab :+ p) @ c = swapa A ab (p @ c).
End PermutationBaseProperties.
Hint Resolve perma_id perma_inverse perma_compose perma_extend : nominal.
Hint Rewrite perma_id perma_inverse perma_compose perma_extend : nominal.
End PermutationsAbstraction.
Implementation of atom permutations |
Module PermutationsImplementation : PermutationsAbstraction.
| We hide the implementation for documentation purposes. Note that we need extensional equality on functions and proof irrelevance here. |
End PermutationsImplementation.
Export PermutationsImplementation.
Theorems about atom permutations |
Section PermutationEqualities.
Variable A : AtomT.
Lemma perma_double_inv_eq : forall (p : permt A), - - p = p.
Lemma perma_compose_inv_eq : forall (p : permt A), -p :++ p = [].
Lemma perma_compose_inv_eq' : forall (p : permt A), p :++ -p = [].
Lemma perma_inverse' : forall (p : permt A) a, p @ -p @ a = a.
Lemma perma_inv_id : forall (a : A), (- []) @ a = a.
Lemma perma_inv_id_eq : - [] = ([] : permt A).
Lemma perma_injective :
forall (p : permt A) (a b : A),
p @ a = p @ b -> a = b.
Lemma perma_inv_compose :
forall (p q : permt A) a, - (p :++ q) @ a = (-q) :++ (-p) @ a.
Lemma perma_inv_compose_eq :
forall (p q : permt A), - (p :++ q) = (-q) :++ (-p).
Lemma perma_swap_commute :
forall (p : permt A) (a b : A),
p :++ [(a,b)] = [(p @ a, p @ b)] :++ p.
Lemma perma_swap_same : forall (a b : A), [(a, a)] @ b = b.
Lemma perma_swap_same_eq : forall (a b : A), [(a, a)] = [].
Lemma perma_swap_invol :
forall (ab : A * A) (c : A), [ab] @ [ab] @ c = c.
Lemma perma_swap_invol_eq :
forall (ab : A * A), [ab] :++ [ab] = [].
Lemma perma_swap_switch :
forall (a b c : A), [(a, b)] @ c = [(b, a)] @ c.
Lemma perma_swap_switch_eq :
forall (a b : A), [(a, b)] = [(b, a)].
Lemma perma_inv_swap :
forall (ab : A * A) (c : A), (- [ab]) @ c = [ab] @ c.
Lemma perma_inv_swap_eq :
forall (ab : A * A), - [ab] = [ab].
Lemma perma_swap_distrib :
forall ab (c d x : A),
[ab] @ [(c,d)] @ x =
[(swapa A ab c, swapa A ab d)] @ [ab] @ x.
End PermutationEqualities.
Hint Resolve perma_double_inv_eq : nominal.
Hint Rewrite perma_double_inv_eq : nominal.
Hint Resolve perma_compose_inv_eq perma_compose_inv_eq': nominal.
Hint Rewrite perma_compose_inv_eq perma_compose_inv_eq': nominal.
Hint Resolve perma_inverse' : nominal.
Hint Rewrite perma_inverse' : nominal.
Hint Resolve perma_inv_id perma_inv_id_eq : nominal.
Hint Rewrite perma_inv_id perma_inv_id_eq : nominal.
Hint Immediate perma_injective : nominal.
Hint Resolve perma_inv_compose perma_inv_compose_eq : nominal.
Hint Rewrite perma_inv_compose perma_inv_compose_eq : nominal.
Hint Resolve perma_swap_commute : nominal.
Hint Resolve perma_swap_same perma_swap_same_eq : nominal.
Hint Rewrite perma_swap_same perma_swap_same_eq : nominal.
Hint Resolve perma_swap_invol perma_swap_invol_eq : nominal.
Hint Rewrite perma_swap_invol perma_swap_invol_eq : nominal.
Hint Resolve perma_swap_switch perma_swap_switch_eq : nominal.
Hint Resolve perma_inv_swap perma_inv_swap_eq : nominal.
Hint Rewrite perma_inv_swap perma_inv_swap_eq : nominal.
Hint Resolve perma_swap_distrib : nominal.