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.
Basic properties about psets |
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.