module FreshNom where
{-
This file develops the properties of the freshness relation.
-}
open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
open import Nomfs
open import CatDef
-----------------------------------------------------------------------------------------
--Freshness relation
----------------------------------------------------------------------------------------
record # {X : Nominal}(a : Atom)(x : Aₛ X) : Set where
constructor fresh
field
new : Atom
notin : new ∉ (some_supp X) x
fixed : (≈ₐ X) ((Act X) [ ( a , new ) ] x) x
open # public
---------------------------------------------------------------------------------------
--Separated Product
---------------------------------------------------------------------------------------
record SepPro (X : Nominal) : Set where
constructor SP
field
Xelem : Aₛ X
Aelem : Atom
freshCon : # {X} Aelem Xelem
open SepPro public
-----------------------------------------------------------------------------------
--equivalence relation on Separated product
-----------------------------------------------------------------------------------
SepPro≈ : (X : Nominal) → Rel (SepPro X)
SepPro≈ X x₁a₁ x₂a₂ = ((≈ₐ X) (Xelem x₁a₁) (Xelem x₂a₂)) × ((Aelem x₁a₁) ≡ (Aelem x₂a₂))
------------------------------------------------------------------------------------
--Some/any theorem
-----------------------------------------------------------------------------------
Some/any : {X : Nominal} → (x : Aₛ X) → (a b : Atom) → b ∉ (some_supp X) x → (≈ₐ X) ((Act X) [ (a , b) ] x) x → (c : Atom) → (c ∉ (some_supp X) x) → (≈ₐ X) ((Act X) [ (a , c) ] x) x
Some/any {X} x a b b∉x abx≈x c c∉x with AtEqDec c a | AtEqDec c b
Some/any {X} x a b b∉x abx≈x .a c∉x | yes refl | _ = ((Act X) [ (a , a) ] x)
≣< ((Act X) ι x) and x by (≈ₐ X) as (eq≈ₐ X) on
((res X) (aa≈ι a) (≈≡ (eq≈ₐ X) {x}{x} refl)) >
(((Act X) ι x)
≣< x and x by (≈ₐ X) as (eq≈ₐ X) on
((ι↠ X) {x}) >
((x by (≈ₐ X) as (eq≈ₐ X) ▴ )))
Some/any {X} x a b b∉x abx≈x .b c∉x | no _ | yes refl = abx≈x
Some/any {X} x a b b∉x abx≈x c c∉x | no c≠a | no c≠b = ((Act X) [ (a , c) ] x) ≣< ((Act X) ([(a , b)] ++ ([(b , c)] ++ [(a , b)])) x) and x by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → (ac≈ab+bc+ab a b c c≠a c≠b) {x}) (≈≡ (eq≈ₐ X) {x}{x} refl)) >
(((Act X) ([(a , b)] ++ ([(b , c)] ++ [(a , b)])) x)
≣< ((Act X) ([(b , c)] ++ [(a , b)]) ((Act X) [(a , b)] x)) and x by (≈ₐ X) as (eq≈ₐ X) on
((isEquivalence.Symm (eq≈ₐ X)) ((p₁p₂↠ X) ([(b , c)] ++ [(a , b)]) [(a , b)])) >
(((Act X) ([(b , c)] ++ [(a , b)]) ((Act X) [(a , b)] x))
≣< ((Act X) ([(b , c)] ++ [(a , b)]) x) and x by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → P≡≈ ([(b , c)] ++ [(a , b)]) {x}) (abx≈x)) >
(((Act X) ([(b , c)] ++ [(a , b)]) x)
≣< ((Act X) [(a , b)] ((Act X) [(b , c)] x)) and x by (≈ₐ X) as (eq≈ₐ X) on
((isEquivalence.Symm (eq≈ₐ X)) ((p₁p₂↠ X) [(a , b)] [(b , c)])) >
(((Act X) [(a , b)] ((Act X) [(b , c)] x))
≣< ((Act X) [(a , b)] x) and x by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {x} → P≡≈ [(a , b)] {x}) ((suppAx X) x b c b∉x c∉x)) >
(((Act X) [(a , b)] x)
≣< x and x by (≈ₐ X) as (eq≈ₐ X) on abx≈x >
((x by (≈ₐ X) as (eq≈ₐ X) ▴ )))))))
Some⇒any : {X : Nominal}{x : Aₛ X}{a : Atom} → (a#x : # {X} a x) → (c : Atom) → (c ∉ (some_supp X) x) → # {X} a x
Some⇒any {X}{x}{a} a#x c c∉x = fresh c c∉x (Some/any {X} x a (new a#x) (notin a#x) (fixed a#x) c c∉x)
-----------------------------------------------------------------------------------------------------------------------------
--# is an equivariant relation
----------------------------------------------------------------------------------------------------------------------------
osup : {X : Nominal} → (π : Perm) → (x : Aₛ X) → Atom
osup {X} π x = outside ((flatten π) ++ (((some_supp X) x) ++ ((some_supp X) ((Act X) π x))))
esup : {X : Nominal} → (π : Perm) → (x : Aₛ X) → List Atom
esup {X} π x = (flatten π) ++ (((some_supp X) x) ++ ((some_supp X) ((Act X) π x)))
#eq : (X : Nominal) → EqCon (Prod NominalAtom X) (λ ax → # {X} (proj₁ ax) (proj₂ ax))
#eq X π (a , x) a#x = fresh (osup {X} π x)
(∉⊆₂ {(some_supp X) x}{(some_supp X)((Act X) π x)}
(osup {X} π x)
(∉⊆₂ {flatten π}{((some_supp X) x) ++ ((some_supp X) ((Act X) π x))}
(osup {X} π x)
(outside∉ (esup {X} π x))))
(((Act X) [((PermAct π a) , (osup {X} π x))]
((Act X) π x)
≣< ((Act X) (π ++ [((PermAct π a) , (osup {X} π x))]) x) and ((Act X) π x) by (≈ₐ X) as (eq≈ₐ X) on
((p₁p₂↠ X) [((PermAct π a) , (osup {X} π x))] π) >
(((Act X) (π ++ [((PermAct π a) , (osup {X} π x))]) x)
≣< ((Act X) ([(a , (osup {X} π x))] ++ π) x) and ((Act X) π x) by (≈ₐ X) as (eq≈ₐ X) on
((res X)(πabπ≈πab π a (osup {X} π x)
(∉⊆₁ {flatten π}{((some_supp X) x) ++ ((some_supp X)((Act X) π x))}
(osup {X} π x)(outside∉ (esup {X} π x))))
(≈≡ (eq≈ₐ X) {x}{x} refl)) >
(((Act X) ([(a , (osup {X} π x))] ++ π) x)
≣< ((Act X) π ((Act X) [(a , (osup {X} π x))] x)) and ((Act X) π x) by (≈ₐ X) as (eq≈ₐ X) on
((isEquivalence.Symm (eq≈ₐ X))((p₁p₂↠ X) π [(a , (osup {X} π x))])) >
(((Act X) π ((Act X) [(a , (osup {X} π x))] x))
≣< ((Act X) π x) and ((Act X) π x) by (≈ₐ X) as (eq≈ₐ X) on
((res X) (P≡≈ π)(fixed (Some⇒any {X = X} a#x (osup {X} π x)
(∉⊆₁ {(some_supp X) x}{(some_supp X) ((Act X) π x)}
(osup {X} π x)(∉⊆₂ {flatten π}{((some_supp X) x) ++ ((some_supp X) ((Act X) π x))}
(osup {X} π x) (outside∉ (esup {X} π x))))))) >
(((Act X) π x) by (≈ₐ X) as (eq≈ₐ X) ▴))))))
a₁a₂#x : {X : Nominal}{x : Aₛ X} → (a₁ a₂ : Atom) → a₁ ≡ a₂ → # {X} a₁ x → # {X} a₂ x
a₁a₂#x a .a refl a#x = a#x
#feq : (X : Nominal) → EqCon (NomExp NominalAtom X) (λ F → ∀ (a : Atom) → # {X} a ((ffun F) a))
#feq X π F a#fa = λ a → let iπa = (PermAct (invPerm π) a) in let ππ⁻¹af = #eq X π (iπa , ((ffun F) iπa)) (a#fa iπa) in a₁a₂#x (PermAct π iπa) a (ππ⁻¹a≡a π a) ππ⁻¹af
ℝX : (X : Nominal) → Nominal
ℝX X = NomSubEq (NomExp NominalAtom X) (λ F → ∀ (a : Atom) → # {X} a ((ffun F) a)) (#feq X)
ActSepPro : (X : Nominal) → Perm → SepPro X → SepPro X
ActSepPro X π X₁ = record {Xelem = (Act X) π (Xelem X₁)
; Aelem = PermAct π (Aelem X₁)
; freshCon = #eq X π ((Aelem X₁) , (Xelem X₁)) (freshCon X₁)
}
--------------------------------------------------------------------------------------------------------------------------------------------
--Separated Product Functor
--------------------------------------------------------------------------------------------------------------------------------------------
_*A : (X : Nominal) → Nominal
X *A = record { Aₛ = SepPro X
; ≈ₐ = SepPro≈ X
; eq≈ₐ = record { Reflex = λ {x₁} → ((Reflex (eq≈ₐ X)) {Xelem x₁} , ((Aelem x₁) ▪))
; Symm = λ {x₁ x₂} → λ x₁≈x₂ → ((Symm (eq≈ₐ X)) (proj₁ x₁≈x₂) , sym (proj₂ x₁≈x₂))
; Trans = λ {x₁ x₂ x₃} → λ x₁≈x₂ → λ x₂≈x₃ → ((Trans (eq≈ₐ X)) (proj₁ x₁≈x₂) (proj₁ x₂≈x₃) , ((Aelem x₁) ≡< proj₂ x₁≈x₂ > (proj₂ x₂≈x₃)))
}
; Act = λ π → λ x → ActSepPro X π x
; res = λ {π₁ π₂ x₁ x₂} → λ π₁≈π₂ → λ x₁≈x₂ → ((res X) {π₁} {π₂} {Xelem x₁} {Xelem x₂} π₁≈π₂ (proj₁ x₁≈x₂) ,
(PermAct π₁ (Aelem x₁) ≡< cong (λ w → PermAct π₁ w) (proj₂ x₁≈x₂) > (PermAct π₁ (Aelem x₂) ≡< π₁≈π₂ {Aelem x₂} > (PermAct π₂ (Aelem x₂)) ▪)))
; p₁p₂↠ = λ π π' → (λ {x} → (((p₁p₂↠ X) π π' {Xelem x}) , (sym (p₁++p₂≡p₂p₁ {Aelem x} π' π))))
; ι↠ = λ {x} → ((ι↠ X) {Xelem x} , refl)
; some_supp = λ x → ((some_supp X) (Xelem x)) ++ [ (Aelem x) ]
; suppAx = λ x → λ b c → λ b∉x → λ c∉x → ((suppAx X) (Xelem x) b c (∉⊆₁ b b∉x) (∉⊆₁ c c∉x) ,
bc∉suppa (Aelem x) b c (∉⊆₂ {(some_supp X) (Xelem x)}{[ (Aelem x) ]} b b∉x) (∉⊆₂ {(some_supp X) (Xelem x)}{[ (Aelem x) ]} c c∉x))
}
osupf : (X Y : Nominal) → (F : Equivar X Y) → (x : Aₛ X) → List Atom
osupf X Y F x = ((some_supp Y) ((ufun F) x)) ++ ((some_supp X) x)
X*A⟶Y*A : (X Y : Nominal) → (F : Equivar X Y) → Equivar (X *A) (Y *A)
X*A⟶Y*A X Y F = record {ufun = λ x₁ → record {Xelem = (ufun F)(Xelem x₁)
; Aelem = Aelem x₁
; freshCon = fresh
(outside (osupf X Y F (Xelem x₁)))
(∉⊆₁ {(some_supp Y)((ufun F)(Xelem x₁))}{(some_supp X)(Xelem x₁)}
(outside (osupf X Y F (Xelem x₁)))
(outside∉ (osupf X Y F (Xelem x₁))))
((Act Y) [(Aelem x₁ , (outside (osupf X Y F (Xelem x₁))))] ((ufun F)(Xelem x₁))
≣< ((ufun F)((Act X) [(Aelem x₁ , (outside (osupf X Y F (Xelem x₁))))] (Xelem x₁))) and ((ufun F)(Xelem x₁)) by (≈ₐ Y) as (eq≈ₐ Y) on
((equiv F) [(Aelem x₁ , (outside (osupf X Y F (Xelem x₁))))] (Xelem x₁)) >
(((ufun F)((Act X) [(Aelem x₁ , (outside (osupf X Y F (Xelem x₁))))] (Xelem x₁)))
≣< ((ufun F)(Xelem x₁)) and ((ufun F)(Xelem x₁)) by (≈ₐ Y) as (eq≈ₐ Y) on
((eqi≈ F) (fixed (Some⇒any {X = X} (freshCon x₁)(outside (osupf X Y F (Xelem x₁)))
(∉⊆₂ {(some_supp Y)((ufun F)(Xelem x₁))}{(some_supp X)(Xelem x₁)}
(outside (osupf X Y F (Xelem x₁)))
(outside∉ (osupf X Y F (Xelem x₁))))))) >
(((ufun F)(Xelem x₁)) by (≈ₐ Y) as (eq≈ₐ Y) ▴)))
}
; eqi≈ = λ {x₁}{x₂} → λ x₁≈x₂ → (((eqi≈ F){Xelem x₁}{Xelem x₂}(proj₁ x₁≈x₂)) , (proj₂ x₁≈x₂))
; equiv = λ π → λ x → (((equiv F) π (Xelem x)) , ((PermAct π (Aelem x)) ▪))
}
NomSep : Functor NomCat NomCat
NomSep = record { onObj = λ X → X *A
; onMor = λ X Y → λ F → X*A⟶Y*A X Y F
; res≈ = λ X Y → λ F G → λ F≈G → λ x → ((F≈G (Xelem x)) , ((Aelem x) ▪))
; onId = λ X → λ x → (((isEquivalence.Reflex (eq≈ₐ X)) {Xelem x}) , ((Aelem x) ▪))
; onComp = λ X Y Z → λ F G → λ x → (((isEquivalence.Reflex (eq≈ₐ Z)) {((ufun G) ∘ (ufun F))(Xelem x)}) , ((Aelem x) ▪))
}
-------------------------------------------------------------------------------------------------------------------------------------------
--Properties of Freshness
------------------------------------------------------------------------------------------------------------------------------------------
a#fx : {X Y : Nominal}{f : (Aₛ (NomExp X Y))}{x : (Aₛ X)}{a : Atom} → # {NomExp X Y} a f → # {X} a x → # {Y} a ((ffun f) x)
a#fx {X}{Y}{f}{x}{a} a#f a#x = let y = (ffun f) x in let fₛ = (some_supp (NomExp X Y)) f in let xₛ = (some_supp X) x in let yₛ = (some_supp Y) y in
let bₛ = xₛ ++ yₛ in let cₛ = fₛ ++ bₛ in let b = outside cₛ in let b∉fxy = outside∉ cₛ in let b∉f = ∉⊆₁ {fₛ}{bₛ} b b∉fxy in
let b∉xy = ∉⊆₂ {fₛ}{bₛ} b b∉fxy in let b∉x = ∉⊆₁ {xₛ}{yₛ} b b∉xy in let b∉y = ∉⊆₂ {xₛ}{yₛ} b b∉xy in
let abf≈f = fixed (Some⇒any {X = NomExp X Y} a#f b b∉f) in let abx≈x = fixed (Some⇒any {X = X} a#x b b∉x) in
let abfx≈fx = ((Act Y) [(a , b)] y)
≣< ((Act Y) [(a , b)] ((ffun f) ((Act X) [(a , b)] x))) and y by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → P≡≈ [(a , b)] {w}) ((feqi≈ f) ((Symm (eq≈ₐ X)) abx≈x))) >
(((Act Y) [(a , b)] ((ffun f) ((Act X) [(a , b)] x)))
≣< y and y by (≈ₐ Y) as (eq≈ₐ Y) on (abf≈f x) >
(y by (≈ₐ Y) as (eq≈ₐ Y) ▴)) in fresh b b∉y abfx≈fx
ffs : {X Y : Nominal}{f : Funfs X Y}{a : Atom} → (a ∉ (fsupp f)) → (∀ (x : Aₛ X) → ((≈ₐ Y) ((Act Y) [(a , a)] ((ffun f) ((Act X) [(a , a)] x))) ((ffun f) x))) → # {NomExp X Y} a f
ffs {X}{Y}{f}{a} a∉f aafx = fresh a a∉f (λ x → aafx x)
a#fxEq : {X Y : Nominal}{f : Equivar X Y}{x : (Aₛ X)}{a : Atom} → # {X} a x → # {Y} a ((ufun f) x)
a#fxEq {X}{Y}{f}{x}{a} a#x = let fₛ = Eq2fs f in let a#f = ffs {X}{Y}{fₛ}{a} a∉[] (λ x → aax≈x fₛ x a) in a#fx a#f a#x where
aax≈x : {X Y : Nominal}(f : Funfs X Y)(x : Aₛ X)(a : Atom) → (≈ₐ Y) ((Act Y) [(a , a)] ((ffun f) ((Act X) [(a , a)] x))) ((ffun f) x)
aax≈x {X}{Y} f x a = let afx = (Act Y) [(a , a)] ((ffun f) ((Act X) [(a , a)] x)) in let fx = (ffun f) x in
let afx≈fx = afx ≣< ((Act Y) ι ((ffun f) ((Act X) [(a , a)] x))) and fx by (≈ₐ Y) as (eq≈ₐ Y) on
((res Y) (λ {w} → aa≈ι a) (≈≡ (eq≈ₐ Y) {(ffun f) ((Act X) [(a , a)] x)}{(ffun f) ((Act X) [(a , a)] x)} refl)) >
(((Act Y) ι ((ffun f) ((Act X) [(a , a)] x)))
≣< ((ffun f) ((Act X) [(a , a)] x)) and fx by (≈ₐ Y) as (eq≈ₐ Y) on
((ι↠ Y) {(ffun f) ((Act X) [(a , a)] x)}) >
(((ffun f) ((Act X) [(a , a)] x))
≣< ((ffun f) ((Act X) ι x)) and fx by (≈ₐ Y) as (eq≈ₐ Y) on
((feqi≈ f) ((res X) (λ {w} → aa≈ι a {w}) (≈≡ (eq≈ₐ X) {x}{x} refl))) >
(((ffun f) ((Act X) ι x))
≣< fx and fx by (≈ₐ Y) as (eq≈ₐ Y) on
((feqi≈ f) ((ι↠ X) {x})) >
(fx by (≈ₐ Y) as (eq≈ₐ Y) ▴)))) in afx≈fx
Freshness : {X : Nominal}{b c : Atom} → (f : (Aₛ (NomExp NominalAtom X))) → (∀ {a : Atom} → (a ∉ (fsupp f)) → (a ∉ ((some_supp X) ((ffun f) a)))) → b ∉ (fsupp f) → c ∉ (fsupp f) → (≈ₐ X)((ffun f) b)((ffun f) c)
Freshness {X}{b}{c} f a∉f⇒a∉fa b∉f c∉f = let fb = (ffun f) b in let fc = (ffun f) c in let fₛ = (fsupp f) in let bₛ = (some_supp X) fb in let cₛ = (some_supp X) fc in
let uₛ = bₛ ++ cₛ in let vₛ = fₛ ++ uₛ in let a = outside vₛ in let a∉fbc = outside∉ vₛ in let a∉f = ∉⊆₁ {fₛ}{uₛ} a a∉fbc in
let a∉bc = ∉⊆₂ {fₛ}{uₛ} a a∉fbc in let a∉fb = ∉⊆₁ {bₛ}{cₛ} a a∉bc in let a∉fc = ∉⊆₂ {bₛ}{cₛ} a a∉bc in let fa = (ffun f) a in
let b∉fb = a∉f⇒a∉fa b∉f in let c∉fc = a∉f⇒a∉fa c∉f in let abf≈fa = (fsuppAx f) a b a∉f b∉f a in let acf≈fa = (fsuppAx f) a c a∉f c∉f a in
let fb≈fa = fb ≣< ((Act X) [(a , b)] fb) and fa by (≈ₐ X) as (eq≈ₐ X) on ((Symm (eq≈ₐ X)) ((suppAx X) fb a b a∉fb b∉fb)) >
(((Act X) [(a , b)] fb) ≣< ((Act X) [(a , b)] ((ffun f) (PermAct [(a , b)] a))) and fa by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {w} → P≡≈ [(a , b)] {w}) ((feqi≈ f) (sym (swapaba≡b a b)))) >
(((Act X) [(a , b)] ((ffun f) (PermAct [(a , b)] a)))
≣< fa and fa by (≈ₐ X) as (eq≈ₐ X) on abf≈fa >
(fa by (≈ₐ X) as (eq≈ₐ X) ▴))) in
let fc≈fa = fc ≣< ((Act X) [(a , c)] fc) and fa by (≈ₐ X) as (eq≈ₐ X) on ((Symm (eq≈ₐ X)) ((suppAx X) fc a c a∉fc c∉fc)) >
(((Act X) [(a , c)] fc) ≣< ((Act X) [(a , c)] ((ffun f) (PermAct [(a , c)] a))) and fa by (≈ₐ X) as (eq≈ₐ X) on
((res X) (λ {w} → P≡≈ [(a , c)] {w}) ((feqi≈ f) (sym (swapaba≡b a c)))) >
(((Act X) [(a , c)] ((ffun f) (PermAct [(a , c)] a)))
≣< fa and fa by (≈ₐ X) as (eq≈ₐ X) on acf≈fa >
(fa by (≈ₐ X) as (eq≈ₐ X) ▴))) in (Trans (eq≈ₐ X)) fb≈fa ((Symm (eq≈ₐ X)) fc≈fa)
------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------