Library Support


Require Import Axioms.

Require Export Swaps.

Support





Section Support.




Variable AR : AtomT.

Variable X : Set.

Variable S : SwapT AR X.




Definition supports (E : aset AR) (x : X) : Prop :=

  forall (a b : atom AR), ~ In a E -> ~ In b E -> swap S (a, b) x = x.




Definition fresh (a : atom AR) (x : X) : Prop :=

  exists E : aset AR, supports E x /\ ~ In a E.




Lemma swap_non_supports :

  forall (F : aset AR) (a b : atom AR) (x : X),

  supports F x -> ~ In a F -> ~ In b F -> swap S (a, b) x = x.




Lemma supports_subset :

  forall (E F : aset AR) (x : X),

  supports E x -> Subset E F -> supports F x.




Lemma supports_intersection :

  forall (E F : aset AR) (x : X),

  supports E x -> supports F x -> supports (intersection E F) x.




Hint Resolve supports_intersection : nominal.




Lemma supports_to_fresh :

  forall (E : aset AR) (a : atom AR) (x : X),

  supports E x -> ~ In a E -> fresh a x.




Lemma swap_fresh_atoms :

  forall (a b : atom AR) (x : X),

  fresh a x -> fresh b x -> swap S (a, b) x = x.




End Support.




Implicit Arguments supports [AR X].

Implicit Arguments fresh [AR X].




Hint Resolve swap_non_supports : nominal.

Hint Resolve supports_subset : nominal.

Hint Resolve supports_intersection : nominal.

Hint Resolve supports_to_fresh : nominal.

Hint Resolve swap_fresh_atoms : nominal.

Hint Rewrite swap_fresh_atoms using (auto with nominal; fail) : nominal.

Support for atoms





Lemma supports_atom :

  forall (A : AtomT) (a : atom A), supports (mkAtomSwap A) (singleton a) a.




Hint Resolve supports_atom : nominal.




Lemma fresh_atom_from_neq :

  forall (A : AtomT) (a a' : atom A), a <> a' -> fresh (mkAtomSwap A) a a'.




Hint Resolve fresh_atom_from_neq : nominal.




Lemma swap_not_in_set :

  forall (A : AtomT) (E : aset A) (a b c : atom A),

  ~ In a E ->

  ~ In b E ->

  ~ In c E ->

  ~ In (swap (mkAtomSwap A) (a, b) c) E.




Hint Resolve swap_not_in_set : nominal.

Additional theorems.





Section GeneralTheorems.




Variable AR : AtomT.

Variable X : Set.

Variable XS : SwapT AR X.




Lemma swap_fresh :

  forall a cd x, fresh XS a x -> fresh XS (swapa AR cd a) (swap XS cd x). Lemma unswap_fresh :

  forall a cd x, fresh XS (swapa AR cd a) (swap XS cd x) -> fresh XS a x.




End GeneralTheorems.




Hint Resolve swap_fresh : nominal.

Hint Immediate unswap_fresh : nominal.




Section FunctionTheorems.




Variables AR : AtomT.

Variables X Y : Set.

Variables XS : SwapT AR X.

Variables YS : SwapT AR Y.




Lemma function_supports :

  forall (F : aset AR) (f : X -> Y),

  (forall a b x, ~ In a F -> ~ In b F ->

    swap YS (a, b) (f x) = f (swap XS (a, b) x)) ->

  supports (XS ^-> YS) F f.




Lemma application_supports :

  forall (F : aset AR) (f : X -> Y) (x : X),

  supports (XS ^-> YS) F f ->

  supports XS F x ->

  supports YS F (f x).




Lemma application_fresh :

  forall (a : AR) (f : X -> Y) (x : X),

  fresh (XS ^-> YS) a f -> fresh XS a x -> fresh YS a (f x).




End FunctionTheorems.




Section MajorTheorems.




Variables AR : AtomT.

Variables X : Set.

Variables XS : SwapT AR X.




Theorem function_constancy_v1 :

  forall (F : aset AR) (f : AR -> X),

  supports (mkAtomSwap AR ^-> XS) F f ->

  forall (a : AR), ~ In a F -> fresh XS a (f a) ->

  forall (b : AR), ~ In b F -> f a = f b.




Theorem function_constancy_v2 :

  forall (F : aset AR) (f : AR -> X),

  supports (mkAtomSwap AR ^-> XS) F f ->

  (exists a : AR, ~ In a F /\ fresh XS a (f a)) ->

  forall a b : AR, ~ In a F -> ~ In b F -> f a = f b.




End MajorTheorems.

Index

This page has been generated by coqdoc