module NomSet where
open import Basics
open import Atoms
open import Perms
open import PermProp
open import Nom
NominalPerm : Nominal
NominalPerm = record { Aₛ = Perm
; ≈ₐ = pEquiv
; eq≈ₐ = pEquiv≡
; Act = PPAct
; res = λ {π₁ π₂ p₁ p₂} → λ π₁≈π₂ → λ p₁≈p₂ → resPP π₁ π₂ p₁ p₂ π₁≈π₂ p₁≈p₂
; p₁p₂↠ = λ p₁ p₂ → (λ {p} → sym (p₁++p₂≡p₂p₁p p₂ p₁ p))
; ι↠ = λ {p} → ιp p
; some_supp = λ p → (flatten p)
; suppAx = λ p → λ b c → λ b∉p → λ c∉p → (λ {a} → πsuppAx p b c b∉p c∉p a)
}
data Sig (A : Set) : Set where
base : (a : A) → Sig A
build : (n : ℕ) → Vec (Sig A) n → Sig A
VecAct : (N : Nominal) → Perm → (n : ℕ) → Vec (Sig (Aₛ N)) n → Vec (Sig (Aₛ N)) n
SigAct : (N : Nominal) → Perm → Sig (Aₛ N) → Sig (Aₛ N)
VecAct N π zero [] = []
VecAct N π (succ n) (x :: xs) = (SigAct N π x) :: (VecAct N π n xs)
SigAct N π (base a) = base ((Act N) π a)
SigAct N π (build n xs) = build n (VecAct N π n xs)
Vecsupp : (N : Nominal) → (n : ℕ) → Vec (Sig (Aₛ N)) n → List Atom
Sigsupp : (N : Nominal) → Sig (Aₛ N) → List Atom
Vecsupp N zero [] = []
Vecsupp N (succ n) (x :: xs) = (Sigsupp N x) ++ (Vecsupp N n xs)
Sigsupp N (base a) = (some_supp N) a
Sigsupp N (build n xs) = Vecsupp N n xs
Vecι : (n : ℕ) → (v : Vec (Sig (Aₛ NominalAtom)) n) → VecAct NominalAtom ι n v ≡ v
Sigι : (s : Sig (Aₛ NominalAtom)) → SigAct NominalAtom ι s ≡ s
Vecι zero [] = refl
Vecι (succ n) (x :: xs) = cong₂ (λ v w → v :: w) (Sigι x) (Vecι n xs)
Sigι (base a) = refl
Sigι (build n xs) = cong (λ w → build n w) (Vecι n xs)
Vecp₁p₂ : (p₁ p₂ : Perm) → (n : ℕ) → (v : Vec (Sig (Aₛ NominalAtom)) n) → (VecAct NominalAtom p₁ n (VecAct NominalAtom p₂ n v)) ≡ (VecAct NominalAtom (p₂ ++ p₁) n v)
Sigp₁p₂ : (p₁ p₂ : Perm) → (s : Sig (Aₛ NominalAtom)) → (SigAct NominalAtom p₁ (SigAct NominalAtom p₂ s)) ≡ (SigAct NominalAtom (p₂ ++ p₁) s)
Vecp₁p₂ p₁ p₂ zero [] = refl
Vecp₁p₂ p₁ p₂ (succ n) (x :: xs) = cong₂ (λ v w → v :: w) (Sigp₁p₂ p₁ p₂ x) (Vecp₁p₂ p₁ p₂ n xs)
Sigp₁p₂ p₁ p₂ (base a) = cong (λ w → base w) ((p₁p₂↠ NominalAtom) p₁ p₂ {a})
Sigp₁p₂ p₁ p₂ (build n xs) = cong (λ w → build n w) (Vecp₁p₂ p₁ p₂ n xs)
VecsuppAx : (b c : Atom) → (n : ℕ) → (v : Vec (Sig (Aₛ NominalAtom)) n) → b ∉ Vecsupp NominalAtom n v → c ∉ Vecsupp NominalAtom n v → VecAct NominalAtom [ ( b , c ) ] n v ≡ v
SigsuppAx : (b c : Atom) → (s : Sig (Aₛ NominalAtom)) → b ∉ Sigsupp NominalAtom s → c ∉ Sigsupp NominalAtom s → SigAct NominalAtom [ ( b , c ) ] s ≡ s
VecsuppAx b c zero [] b∉v c∉v = refl
VecsuppAx b c (succ n) (x :: xs) b∉v c∉v = cong₂ (λ i j → i :: j) (SigsuppAx b c x (∉⊆₁ {Sigsupp NominalAtom x}{Vecsupp NominalAtom n xs} b b∉v)
(∉⊆₁ {Sigsupp NominalAtom x}{Vecsupp NominalAtom n xs} c c∉v))
(VecsuppAx b c n xs (∉⊆₂ {Sigsupp NominalAtom x}{Vecsupp NominalAtom n xs} b b∉v)
(∉⊆₂ {Sigsupp NominalAtom x}{Vecsupp NominalAtom n xs} c c∉v))
SigsuppAx b c (base a) b∉s c∉s = cong (λ w → base w) ((suppAx NominalAtom) a b c b∉s c∉s)
SigsuppAx b c (build n xs) b∉s c∉s = cong (λ w → build n w) (VecsuppAx b c n xs b∉s c∉s)
VecPre₂ : (n : ℕ) → (π₁ π₂ : Perm) → (v₁ v₂ : Vec (Sig (Aₛ NominalAtom)) n) → (π₁≈π₂ : pEquiv π₁ π₂) → v₁ ≡ v₂ → (VecAct NominalAtom π₁ n v₁) ≡ (VecAct NominalAtom π₂ n v₂)
SigPre₂ : (π₁ π₂ : Perm) → (s₁ s₂ : Sig (Aₛ NominalAtom)) → (π₁≈π₂ : pEquiv π₁ π₂) → s₁ ≡ s₂ → (SigAct NominalAtom π₁ s₁) ≡ (SigAct NominalAtom π₂ s₂)
VecPre₂ zero π₁ π₂ [] [] π₁≈π₂ refl = refl
VecPre₂ (succ n) π₁ π₂ (x :: xs) (.x :: .xs) π₁≈π₂ refl = cong₂ (λ i j → i :: j) (SigPre₂ π₁ π₂ x x π₁≈π₂ refl)(VecPre₂ n π₁ π₂ xs xs π₁≈π₂ refl)
SigPre₂ π₁ π₂ (base a) (base .a) π₁≈π₂ refl = cong (λ w → base w) ((res NominalAtom) {π₁}{π₂}{a}{a} π₁≈π₂ refl)
SigPre₂ π₁ π₂ (build n xs) (build .n .xs) π₁≈π₂ refl = cong (λ w → build n w)(VecPre₂ n π₁ π₂ xs xs π₁≈π₂ refl)
SigNomAtom : Nominal
SigNomAtom = record { Aₛ = Sig (Aₛ NominalAtom)
; ≈ₐ = _≡_
; eq≈ₐ = aEquiv≡ (Sig (Aₛ NominalAtom))
; Act = λ π → λ ν → SigAct NominalAtom π ν
; res = λ {π₁}{π₂}{ν₁}{ν₂} → λ π₁≈π₂ → λ ν₁≡ν₂ → SigPre₂ π₁ π₂ ν₁ ν₂ π₁≈π₂ ν₁≡ν₂
; p₁p₂↠ = λ p₁ p₂ → λ {ν} → Sigp₁p₂ p₁ p₂ ν
; ι↠ = λ {ν} → Sigι ν
; some_supp = λ ν → Sigsupp NominalAtom ν
; suppAx = λ ν → λ b c → λ b∉ν → λ c∉ν → SigsuppAx b c ν b∉ν c∉ν
}
ℕNom : Nominal
ℕNom = record {Aₛ = ℕ
; ≈ₐ = _≡_
; eq≈ₐ = aEquiv≡ ℕ
; Act = λ π → λ n → n
; res = λ π₁≈π₂ → λ n₁≡n₂ → n₁≡n₂
; p₁p₂↠ = λ p₁ p₂ → λ {n} → (Reflex (aEquiv≡ ℕ)) {n}
; ι↠ = λ {n} → (Reflex (aEquiv≡ ℕ)) {n}
; some_supp = λ n → []
; suppAx = λ n → λ b c b∉n c∉n → (Reflex (aEquiv≡ ℕ)) {n}
}
data _≺_ {A : Set} (a : A) : List A → Set where
a≺a : ∀ {as} → a ≺ (a :: as)
a≺as : ∀ {as}{b : A} → a ≺ as → a ≺ (b :: as)
record ≺rel (A : Set)(L₁ : List A)(L₂ : List A) : Set where
constructor L₁◯L₂
field
L₁⊆L₂ : ∀ {a : A} → (a ≺ L₁) → (a ≺ L₂)
L₂⊆L₁ : ∀ {a : A} → (a ≺ L₂) → (a ≺ L₁)
open ≺rel public
≺eq : (A : Set) → isEquivalence (List A) (≺rel A)
≺eq A = record { Reflex = λ {l} → L₁◯L₂ (λ a≺l → a≺l) (λ a≺l → a≺l)
; Symm = λ l₁≈l₂ → L₁◯L₂ (L₂⊆L₁ l₁≈l₂) (L₁⊆L₂ l₁≈l₂)
; Trans = λ l₁≈l₂ l₂≈l₃ → L₁◯L₂ (λ a≺l → (L₁⊆L₂ l₂≈l₃) ((L₁⊆L₂ l₁≈l₂) a≺l)) (λ a≺l → (L₂⊆L₁ l₁≈l₂) ((L₂⊆L₁ l₂≈l₃) a≺l))
}
ActList : (π : Perm) → List Atom → List Atom
ActList π [] = []
ActList π (n :: ns) = (PermAct π n) :: (ActList π ns)
l₁≡l₂⇒l₁≈l₂ : {A : Set}{L₁ L₂ : List A} → L₁ ≡ L₂ → ≺rel A L₁ L₂
l₁≡l₂⇒l₁≈l₂ {A}{L₁}{.L₁} refl = L₁◯L₂ (λ a≺l → a≺l) (λ a≺l → a≺l)
a≺l⇒πa≺πl : {a : Atom}{l : List Atom} → (π₁ π₂ : Perm) → (pEquiv π₁ π₂) → a ≺ l → (PermAct π₁ a) ≺ (ActList π₂ l)
a≺l⇒πa≺πl {a}{.a :: as} π₁ π₂ π₁≈π₂ a≺a rewrite π₁≈π₂ {a} = a≺a
a≺l⇒πa≺πl {a}{b :: as} π₁ π₂ π₁≈π₂ (a≺as aas) rewrite (π₁≈π₂ {b}) = a≺as (a≺l⇒πa≺πl π₁ π₂ π₁≈π₂ aas)
aL₁≡aL₂ : {L₁ L₂ : List Atom} → (a : Atom) → L₁ ≡ L₂ → a ≺ L₁ → a ≺ L₂
aL₁≡aL₂ a refl a≺l = a≺l
a₁L≡a₂L : {L : List Atom}{a₁ a₂ : Atom} → a₁ ≡ a₂ → a₁ ≺ L → a₂ ≺ L
a₁L≡a₂L refl a≺l = a≺l
π⁻¹πList : {L : List Atom} → (π : Perm) → ActList (invPerm π) (ActList π L) ≡ L
π⁻¹πList {[]} π = refl
π⁻¹πList {x :: xs} π = cong₂ (λ v w → v :: w) ((PermAct (invPerm π) (PermAct π x)) ≡< sym (p₁++p₂≡p₂p₁ {x} π (invPerm π)) >
((PermAct (π ++ (invPerm π)) x ) ≡< p∘p⁻¹Act π {x} > (x ▪))) (π⁻¹πList {xs} π)
πa≺πl⇒a≺l : {a : Atom}{L : List Atom} → (π : Perm) → a ≺ (ActList π L) → (PermAct (invPerm π) a) ≺ L
πa≺πl⇒a≺l {a}{l} π πa≡πx = aL₁≡aL₂ (PermAct (invPerm π) a) (π⁻¹πList {l} π) (a≺l⇒πa≺πl (invPerm π) (invPerm π) (P≡≈ (invPerm π)) πa≡πx)
ActListRes : {L₁ L₂ : List Atom}{π₁ π₂ : Perm} → (π₁≈π₂ : pEquiv π₁ π₂) → (L₁≈L₂ : ≺rel Atom L₁ L₂) → ≺rel Atom (ActList π₁ L₁) (ActList π₂ L₂)
ActListRes {L₁}{L₂}{π₁}{π₂} π₁≈π₂ L₁≈L₂ = L₁◯L₂ (λ {a} π₁a≺π₁L₁ → a₁L≡a₂L (ππ⁻¹a≡a π₁ a) (a≺l⇒πa≺πl π₁ π₂ π₁≈π₂ ((L₁⊆L₂ L₁≈L₂) (πa≺πl⇒a≺l π₁ π₁a≺π₁L₁))))
(λ {a} π₂a≺π₂L₂ → a₁L≡a₂L (ππ⁻¹a≡a π₂ a) (a≺l⇒πa≺πl π₂ π₁ (λ {w} → sym (π₁≈π₂ {w})) ((L₂⊆L₁ L₁≈L₂) (πa≺πl⇒a≺l π₂ π₂a≺π₂L₂))))
suppAxList : (l : List Atom) → (b c : Atom) → b ∉ l → c ∉ l → ActList [(b , c)] l ≡ l
suppAxList [] b c b∉[] c∉[] = refl
suppAxList (a :: as) b c (a∉as b∉as a≠b) (a∉as c∉as a≠c) rewrite (swapabc≡c b c a a≠b a≠c) = cong (λ w → a :: w) (suppAxList as b c b∉as c∉as)
p₁p₂↠List : (l : List Atom) → (p₁ p₂ : Perm) → ActList p₁ (ActList p₂ l) ≡ ActList (p₂ ++ p₁) l
p₁p₂↠List [] p₁ p₂ = refl
p₁p₂↠List (a :: as) p₁ p₂ rewrite (p₁p₂↠ NominalAtom) p₁ p₂ {a} = cong (λ w → (PermAct (p₂ ++ p₁) a) :: w) (p₁p₂↠List as p₁ p₂)
ι↠List : (l : List Atom) → ActList ι l ≡ l
ι↠List [] = refl
ι↠List (a :: as) rewrite (ι↠ NominalAtom) {a} = cong (λ w → a :: w) (ι↠List as)
NomListAtom : Nominal
NomListAtom = record { Aₛ = List Atom
; ≈ₐ = ≺rel Atom
; eq≈ₐ = ≺eq Atom
; Act = ActList
; res = λ π₁≈π₂ l₁≈l₂ → ActListRes π₁≈π₂ l₁≈l₂
; p₁p₂↠ = λ p₁ p₂ {l} → l₁≡l₂⇒l₁≈l₂ (p₁p₂↠List l p₁ p₂)
; ι↠ = λ {l} → l₁≡l₂⇒l₁≈l₂ (ι↠List l)
; some_supp = λ l → l
; suppAx = λ l b c b∉l c∉l → l₁≡l₂⇒l₁≈l₂ (suppAxList l b c b∉l c∉l)
}