# Library Psets

``` Require Import List. Require Import Atoms. Require Import Axioms. Require Import Permutations. ```
 A `PsetT` record is the evidence that we can define permutations over a type `X`. Both `perm_id` and `perm_compose` are standard axioms of group actions (in this case, of permutations acting on `X`).
``` Record PsetT (A : AtomT) (X : Set) : Set := mkPset {   perm : permt A -> X -> X;   perm_id : forall x, perm [] x = x;   perm_compose :     forall p q x, perm (p :++ q) x = perm p (perm q x) }. Implicit Arguments mkPset [A X]. Implicit Arguments perm [A X]. Implicit Arguments perm_id [A X]. Implicit Arguments perm_compose [A X]. Hint Resolve perm_id perm_compose : nominal. Hint Rewrite perm_id perm_compose : nominal. ```

``` Section BasicPsetTheorems.    Variable A : AtomT.    Variable X : Set.    Variable P : PsetT A X.   Lemma perm_eq : forall p q x, p = q -> perm P p x = perm P q x.    Hint Resolve perm_eq : nominal.   Lemma perm_inv : forall p x, perm P (-p) (perm P p x) = x.   Lemma perm_inv' : forall p x, perm P (p) (perm P (-p) x) = x.   Lemma perm_injective :     forall p x y, perm P p x = perm P p y -> x = y.   Lemma perm_swap_same :     forall a x, perm P [(a, a)] x = x.   Lemma perm_swap_invol :     forall ab x, perm P [ab] (perm P [ab] x) = x.   Lemma perm_swap_move :     forall ab x y, x = perm P [ab] y -> perm P [ab] x = y.   Lemma perm_swap_move' :     forall ab x y, perm P [ab] x = y -> x = perm P [ab] y.   Lemma perm_swap_switch :     forall a b x, perm P [(a, b)] x = perm P [(b, a)] x. End BasicPsetTheorems. Hint Resolve perm_inv perm_inv' : nominal. Hint Rewrite perm_inv perm_inv' : nominal. Hint Immediate perm_injective : nominal. Hint Resolve perm_swap_same perm_swap_invol : nominal. Hint Rewrite perm_swap_same perm_swap_invol : nominal. Hint Immediate perm_swap_move perm_swap_move' : nominal. Hint Resolve perm_swap_switch : nominal. ```

## Support

``` ```
 We define what it means for a finite set of atoms to support an element of a pset.
``` Section Support.    Variable A : AtomT.    Variable X : Set.    Variable P : PsetT A X.   Definition supports (F : aset A) (x : X) :=     forall a b, ~ In a F -> ~ In b F -> perm P [(a, b)] x = x.   Lemma swap_non_supports :     forall F x a b, supports F x -> ~ In a F -> ~ In b F ->     perm P [(a, b)] x = x.   Lemma Subset_supports :     forall (E F : aset A) (x : X),     supports E x -> Subset E F -> supports F x.   Lemma intersection_supports :     forall (E F : aset A) (x : X),     supports E x -> supports F x -> supports (intersection E F) x. End Support. Implicit Arguments supports [A X]. Implicit Arguments swap_non_supports [A X]. Hint Resolve swap_non_supports : nominal. Hint Resolve Subset_supports intersection_supports : nominal. ```

## Identity permutation

``` Section IdPermutations.    Variable A : AtomT.    Variable X : Set.   Definition mkIdPset : PsetT A X :=     mkPset (fun _ x => x) (fun _ => refl_equal _) (fun _ _ _ => refl_equal _). End IdPermutations. ```

## Permutations on atoms

``` Section AtomPermutations.    Variable A : AtomT.   Definition mkAtomPset :=     mkPset (@perma A) (perma_id A) (perma_compose A).   Lemma supports_atom :     forall a : A, supports mkAtomPset (singleton a) a.   Lemma perm_atom : forall p a, perm mkAtomPset p a = p @ a. End AtomPermutations. Implicit Arguments perm_atom [A]. Hint Resolve supports_atom : nominal. ```

## Permutations on pairs

``` Section PairPermutations.    Variable A : AtomT.    Variables X Y : Set.    Variables (XP : PsetT A X) (YP : PsetT A Y).   Definition perm_on_pair (p : permt A) (xy : X * Y) :=     let (x, y) := xy in (perm XP p x, perm YP p y).   Definition mkPairPset : PsetT A (X * Y).   Lemma perm_pair :     forall p x y, perm mkPairPset p (x, y) = (perm XP p x, perm YP p y).   Lemma supports_pair :     forall x y F G,     supports XP F x ->     supports YP G y ->     supports mkPairPset (union F G) (x, y). End PairPermutations. Implicit Arguments mkPairPset [A X Y]. Notation "X ^* Y" := (mkPairPset X Y) (at level 50, left associativity). Hint Resolve perm_pair supports_pair : nominal. Hint Rewrite perm_pair : nominal. ```

## Permutations on lists

``` Section ListPermutations.    Variable A : AtomT.    Variable X : Set.    Variable P : PsetT A X.   Fixpoint perm_on_list (p : permt A) (xs : list X) {struct xs} : list X :=     match xs with       | nil => nil       | y :: ys => (perm P p y) :: (perm_on_list p ys)     end.   Definition mkListPset : PsetT A (list X).   Lemma perm_list_nil : forall p, perm mkListPset p nil = nil.   Lemma perm_list_cons :     forall p x xs,     perm mkListPset p (x :: xs) = perm P p x :: perm mkListPset p xs.   Lemma perm_list_In :     forall xs x p,     List.In x xs -> List.In (perm P p x) (perm mkListPset p xs).   Lemma perm_list_In' :     forall xs x p,     List.In (perm P p x) (perm mkListPset p xs) -> List.In x xs.   Lemma perm_list_not_In :     forall xs x p,     ~ List.In x xs -> ~ List.In (perm P p x) (perm mkListPset p xs).   Lemma perm_list_not_In' :     forall xs x p,     ~ List.In (perm P p x) (perm mkListPset p xs) -> ~ List.In x xs.   Lemma supports_list_nil : supports mkListPset empty nil.   Lemma supports_list_cons :     forall F G x xs, supports P F x -> supports mkListPset G xs ->     supports mkListPset (union F G) (x :: xs). End ListPermutations. Implicit Arguments mkListPset [A X]. Hint Resolve perm_list_nil perm_list_cons : nominal. Hint Rewrite perm_list_nil perm_list_cons : nominal. Hint Resolve perm_list_In perm_list_In' : nominal. Hint Resolve perm_list_not_In perm_list_not_In' : nominal. Hint Resolve supports_list_nil supports_list_cons : nominal. ```

## Permutations on finite sets

``` Section FiniteSetPermutations.    Variable A : AtomT.    Variable X : Set.    Variable E : ExtFset X.    Variable P : PsetT A X.   Definition perm_on_extFset (p : permt A) (F : extFset E) :=     map (fun x => perm P p x) F.   Lemma perm_on_extFset_In_raw :     forall x F p, In x F -> In (perm P p x) (perm_on_extFset p F).    Hint Resolve perm_on_extFset_In_raw : nominal.   Definition mkExtFsetPset : PsetT A (extFset E).   Lemma perm_extFset_In :     forall x F p, In x F -> In (perm P p x) (perm mkExtFsetPset p F).   Lemma perm_extFset_In' :     forall x F p, In (perm P p x) (perm mkExtFsetPset p F) -> In x F.   Lemma perm_extFset_neg_In :     forall x F p, ~ In x F -> ~ In (perm P p x) (perm mkExtFsetPset p F).   Lemma perm_extFset_neg_In' :     forall x F p, ~ In (perm P p x) (perm mkExtFsetPset p F) -> ~ In x F.   Lemma perm_extFset_empty : forall p, perm mkExtFsetPset p empty = empty.   Lemma perm_extFset_add :     forall x F p,     perm mkExtFsetPset p (add x F) = add (perm P p x) (perm mkExtFsetPset p F).   Lemma perm_extFset_singleton :     forall x p,     perm mkExtFsetPset p (singleton x) = singleton (perm P p x).   Lemma perm_extFset_union :     forall p G F,     perm mkExtFsetPset p (union G F) =     union (perm mkExtFsetPset p G) (perm mkExtFsetPset p F).   Lemma perm_extFset_diff :     forall p G F,     perm mkExtFsetPset p (diff G F) =     diff (perm mkExtFsetPset p G) (perm mkExtFsetPset p F).   Lemma perm_extFset_remove :     forall p x F,     perm mkExtFsetPset p (remove x F) =     remove (perm P p x) (perm mkExtFsetPset p F).   Lemma perm_extFset_Subset :     forall p G F, Subset G F ->     Subset (perm mkExtFsetPset p G) (perm mkExtFsetPset p F).   Lemma swap_not_in_set :     forall (a c d : A) (F : aset A),     ~ In a F -> ~ In c F -> ~ In d F -> ~ In ([(c,d)] @ a) F.   Lemma swap_not_in_set' :     forall (a c d : A) (F : aset A),     ~ In a F -> ~ In c F -> ~ In d F -> ~ In (perm (mkAtomPset A) [(c,d)] a) F. End FiniteSetPermutations. Implicit Arguments mkExtFsetPset [A X]. Implicit Arguments perm_extFset_In [A X E x F]. Implicit Arguments perm_extFset_In' [A X E x F]. Implicit Arguments perm_extFset_neg_In [A X E x F]. Implicit Arguments perm_extFset_neg_In' [A X E x F]. Hint Resolve perm_extFset_In : nominal. Hint Resolve perm_extFset_neg_In : nominal. Hint Immediate perm_extFset_In' : nominal. Hint Immediate perm_extFset_neg_In' : nominal. Hint Resolve perm_extFset_empty perm_extFset_add : nominal. Hint Rewrite perm_extFset_empty perm_extFset_add : nominal. Hint Resolve perm_extFset_singleton perm_extFset_union : nominal. Hint Rewrite perm_extFset_singleton perm_extFset_union : nominal. Hint Resolve perm_extFset_diff perm_extFset_remove : nominal. Hint Rewrite perm_extFset_diff perm_extFset_remove : nominal. Hint Resolve perm_extFset_Subset : nominal. Hint Resolve swap_not_in_set swap_not_in_set' : nominal. ```

## Freshness as a predicate

``` Section Fresh.    Variable A : AtomT.    Variable X : Set.    Variable P : PsetT A X.   Lemma perm_supports :     forall F x p,     supports P F x ->     supports P (perm (mkExtFsetPset (asetR A) (mkAtomPset A)) p F) (perm P p x).   Lemma perm_supports' :     forall F x p,     supports P (perm (mkExtFsetPset (asetR A) (mkAtomPset A)) p F) (perm P p x) ->     supports P F x.   Definition freshP (a : A) (x : X) :=     exists F : aset A, ~ In a F /\ supports P F x.   Lemma freshP_from_supports :     forall a x F, ~ In a F -> supports P F x -> freshP a x.   Lemma perm_freshP :     forall a x p, freshP a x -> freshP (perm (mkAtomPset A) p a) (perm P p x).   Lemma perm_freshP' :     forall a x p, freshP (perm (mkAtomPset A) p a) (perm P p x) -> freshP a x.   Lemma swap_freshP_atoms :     forall a b x, freshP a x -> freshP b x -> perm P [(a,b)] x = x. End Fresh. Implicit Arguments freshP [A X]. Hint Resolve perm_supports : nominal. Hint Immediate perm_supports' : nominal. Hint Resolve perm_freshP : nominal. Hint Immediate perm_freshP' : nominal. Section FreshFacts.    Variable A : AtomT.   Lemma freshP_atom :     forall a b, a <> b -> freshP (mkAtomPset A) a b. End FreshFacts. Hint Resolve freshP_from_supports : nominal. Hint Resolve freshP_atom : nominal. ```

## Permutations on functions

``` Section FunctionPermutations.    Variable A : AtomT.    Variables X Y : Set.    Variables (XP : PsetT A X) (YP : PsetT A Y).   Definition perm_on_fun (p : permt A) (f : X -> Y) :=     fun x => perm YP p (f (perm XP (-p) x)).   Definition mkFunPset : PsetT A (X -> Y).   Lemma perm_fun :     forall f p, perm mkFunPset p f = fun x => perm YP p (f (perm XP (-p) x)).   Lemma perm_app :     forall f x p, perm YP p (f x) = (perm mkFunPset p f) (perm XP p x).   Lemma supports_fun :     forall (F : aset A) (f : X -> Y),     (forall a b x, ~ In a F -> ~ In b F ->       perm YP [(a, b)] (f x) = f (perm XP [(a, b)] x)) ->     supports mkFunPset F f.   Lemma supports_application :     forall f x F G,     supports mkFunPset F f ->     supports XP G x ->     supports YP (union F G) (f x).   Lemma freshP_application :     forall f x a, freshP mkFunPset a f -> freshP XP a x -> freshP YP a (f x). End FunctionPermutations. Implicit Arguments mkFunPset [A X Y]. Notation "X ^-> Y" := (mkFunPset X Y) (at level 90, right associativity). Hint Resolve perm_fun perm_app : nominal. Hint Resolve supports_fun : nominal. Hint Resolve supports_application freshP_application : nominal. Section FunctionPermutationFacts.    Variable A : AtomT.    Variables X Y : Set.    Variables (XP : PsetT A X) (YP : PsetT A Y).   Theorem function_constancy_v1 :     forall (F : aset A) (f : A -> X),     supports (mkAtomPset A ^-> XP) F f ->       forall (a : A), ~ In a F -> freshP XP a (f a) ->       forall (b : A), ~ In b F -> f a = f b.   Theorem function_constancy_v2 :     forall (F : aset A) (f : A -> X),     supports (mkAtomPset A ^-> XP) F f ->     (exists a : A, ~ In a F /\ freshP XP a (f a)) ->     forall a b : A, ~ In a F -> ~ In b F -> f a = f b. End FunctionPermutationFacts. Hint Immediate function_constancy_v1 function_constancy_v2 : nominal. ```
Index