|
7
|
1 module Symmetric where
|
|
0
|
2
|
|
|
3 open import Level hiding ( suc ; zero )
|
|
|
4 open import Algebra
|
|
|
5 open import Algebra.Structures
|
|
37
|
6 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ )
|
|
41
|
7 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
|
|
3
|
8 open import Data.Product
|
|
0
|
9 open import Data.Fin.Permutation
|
|
|
10 open import Function hiding (id ; flip)
|
|
|
11 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
|
|
|
12 open import Function.LeftInverse using ( _LeftInverseOf_ )
|
|
|
13 open import Function.Equality using (Π)
|
|
17
|
14 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
|
|
|
15 open import Data.Nat.Properties -- using (<-trans)
|
|
16
|
16 open import Relation.Binary.PropositionalEquality
|
|
44
|
17 open import Data.List using (List; []; _∷_ ; length ; _++_ ) renaming (reverse to rev )
|
|
16
|
18 open import nat
|
|
0
|
19
|
|
|
20 fid : {p : ℕ } → Fin p → Fin p
|
|
|
21 fid x = x
|
|
|
22
|
|
|
23 -- Data.Fin.Permutation.id
|
|
|
24 pid : {p : ℕ } → Permutation p p
|
|
|
25 pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
|
|
|
26
|
|
|
27 -- Data.Fin.Permutation.flip
|
|
|
28 pinv : {p : ℕ } → Permutation p p → Permutation p p
|
|
|
29 pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
|
|
|
30
|
|
3
|
31 record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where
|
|
|
32 field
|
|
|
33 peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
|
|
0
|
34
|
|
3
|
35 open _=p=_
|
|
0
|
36
|
|
3
|
37 prefl : {p : ℕ } { x : Permutation p p } → x =p= x
|
|
|
38 peq (prefl {p} {x}) q = refl
|
|
1
|
39
|
|
3
|
40 psym : {p : ℕ } { x y : Permutation p p } → x =p= y → y =p= x
|
|
|
41 peq (psym {p} {x} {y} eq ) q = sym (peq eq q)
|
|
1
|
42
|
|
3
|
43 ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y → y =p= z → x =p= z
|
|
|
44 peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
|
|
0
|
45
|
|
7
|
46 Symmetric : ℕ → Group Level.zero Level.zero
|
|
|
47 Symmetric p = record {
|
|
0
|
48 Carrier = Permutation p p
|
|
3
|
49 ; _≈_ = _=p=_
|
|
0
|
50 ; _∙_ = _∘ₚ_
|
|
|
51 ; ε = pid
|
|
|
52 ; _⁻¹ = pinv
|
|
3
|
53 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
|
|
|
54 isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
|
|
0
|
55 ; ∙-cong = presp }
|
|
|
56 ; assoc = passoc }
|
|
3
|
57 ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } )) }
|
|
|
58 ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))
|
|
|
59 ; ⁻¹-cong = λ i=j → record { peq = λ q → p-inv i=j q }
|
|
0
|
60 }
|
|
|
61 } where
|
|
3
|
62 presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
|
|
|
63 presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
|
|
|
64 lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
|
|
|
65 lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
|
|
|
66 passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p= (x ∘ₚ (y ∘ₚ z))
|
|
|
67 passoc x y z = record { peq = λ q → refl }
|
|
|
68 p-inv : {i j : Permutation p p} → i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
|
|
|
69 p-inv {i} {j} i=j q = begin
|
|
4
|
70 i ⟨$⟩ˡ q ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j) ) ⟩
|
|
|
71 i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (peq i=j _ )) ⟩
|
|
|
72 i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i ⟩
|
|
|
73 j ⟨$⟩ˡ q
|
|
3
|
74 ∎ where open ≡-Reasoning
|
|
0
|
75
|
|
16
|
76 open import Relation.Nullary
|
|
|
77 open import Data.Empty
|
|
17
|
78 open import Relation.Binary.Core
|
|
|
79 open import fin
|
|
16
|
80
|
|
38
|
81 -- An inductive construction of permutation
|
|
34
|
82
|
|
41
|
83 -- we already have refl and trans
|
|
|
84
|
|
34
|
85 pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n)
|
|
|
86 pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
|
|
33
|
87 p→ : Fin (suc n) → Fin (suc n)
|
|
34
|
88 p→ zero = zero
|
|
|
89 p→ (suc x) = suc ( perm ⟨$⟩ˡ x)
|
|
33
|
90
|
|
34
|
91 p← : Fin (suc n) → Fin (suc n)
|
|
|
92 p← zero = zero
|
|
|
93 p← (suc x) = suc ( perm ⟨$⟩ʳ x)
|
|
|
94
|
|
|
95 piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x
|
|
|
96 piso← zero = refl
|
|
35
|
97 piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm)
|
|
33
|
98
|
|
34
|
99 piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
|
|
|
100 piso→ zero = refl
|
|
35
|
101 piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm)
|
|
33
|
102
|
|
34
|
103 pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n ))
|
|
|
104 pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
|
|
|
105 p→ : Fin (suc (suc n)) → Fin (suc (suc n))
|
|
|
106 p→ zero = suc zero
|
|
|
107 p→ (suc zero) = zero
|
|
|
108 p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) )
|
|
18
|
109
|
|
34
|
110 p← : Fin (suc (suc n)) → Fin (suc (suc n))
|
|
|
111 p← zero = suc zero
|
|
|
112 p← (suc zero) = zero
|
|
|
113 p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) )
|
|
|
114
|
|
|
115 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
|
|
|
116 piso← zero = refl
|
|
|
117 piso← (suc zero) = refl
|
|
35
|
118 piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm)
|
|
16
|
119
|
|
34
|
120 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
|
|
|
121 piso→ zero = refl
|
|
|
122 piso→ (suc zero) = refl
|
|
35
|
123 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm)
|
|
34
|
124
|
|
|
125 -- enumeration
|
|
|
126
|
|
44
|
127 psawpn : {n : ℕ} → 1 < n → Permutation n n
|
|
|
128 psawpn {suc zero} (s≤s ())
|
|
|
129 psawpn {suc n} (s≤s (s≤s x)) = pswap pid
|
|
34
|
130
|
|
35
|
131 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n
|
|
|
132 pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m<n n m ) (subst (λ k → Permutation k k ) (n-n-m=m m≤n ) perm) where
|
|
|
133 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n
|
|
|
134 pfill1 0 _ perm = perm
|
|
|
135 pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )
|
|
34
|
136
|
|
44
|
137 psawpim : {n m : ℕ} → 1 < m → m ≤ n → Permutation n n
|
|
|
138 psawpim {n} {m} 1<m m≤n = pfill m≤n ( psawpn 1<m )
|
|
|
139
|
|
|
140 -- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n)
|
|
|
141 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ?
|
|
|
142
|
|
|
143 -- inductivley enmumerate permutations
|
|
|
144 -- from n-1 length create n length inserting new element at position m
|
|
|
145
|
|
41
|
146 eperm : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
|
|
|
147 eperm {0} {0} z≤n perm = pid
|
|
|
148 eperm {suc n} {0} z≤n perm = pprep perm
|
|
44
|
149 eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pprep perm) where
|
|
37
|
150 lemm3 : 2 + m ≤ suc n
|
|
41
|
151 lemm3 = s≤s (s≤s m<n)
|
|
44
|
152 eperm1 : (m i : ℕ ) → i + m ≤ suc n → Permutation (suc n)(suc n) → Permutation (suc n)(suc n)
|
|
|
153 eperm1 zero i i<ssm perm = perm ∘ₚ (psawpim {suc n} {i + m} {!!} {!!} ) --- 1 < i + m , i + m ≤ suc (suc n)
|
|
|
154 -- m<n : m ≤ n , i<ssm : i + zero ≤ suc (suc n)
|
|
|
155 eperm1 (suc m) i i<ssm perm = eperm1 m (suc i) (lemm4 i<ssm ) perm where
|
|
37
|
156 lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
|
|
|
157 lemm4 lt = begin
|
|
|
158 suc i + m ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
|
|
|
159 suc m + i ≡⟨ +-comm (suc m) _ ⟩
|
|
|
160 i + suc m ≤⟨ lt ⟩
|
|
|
161 suc n
|
|
|
162 ∎ where open ≤-Reasoning
|
|
|
163
|
|
|
164 plist : {n : ℕ} → Permutation n n → List ℕ
|
|
|
165 plist {0} perm = []
|
|
44
|
166 plist {suc j} perm = rev (plist1 j a<sa) where
|
|
37
|
167 n = suc j
|
|
|
168 plist1 : (i : ℕ ) → i < n → List ℕ
|
|
40
|
169 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
|
|
|
170 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa)
|
|
37
|
171
|
|
44
|
172 testp = plist (psawpim {6} {4} (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))))
|
|
|
173 testi00 = plist(pid {3} ) -- 0 ∷ 1 ∷ 2 ∷ []
|
|
|
174 testi = plist (pid {3} ∘ₚ psawpim {3} {2} (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n))) -- 0 ∷ 2 ∷ 1 ∷ [] -- 1 ∷ 0 ∷ 2 ∷ []
|
|
|
175 testi0 = plist (pid {3} ∘ₚ psawpim {3} {3} (s≤s (s≤s z≤n)) (s≤s ( s≤s (s≤s z≤n)))) -- 1 ∷ 0 ∷ 2 ∷ [] -- 1 ∷ 2 ∷ 0 ∷ []
|
|
|
176
|
|
41
|
177 test0 = plist (eperm {1} {0} z≤n pid)
|
|
|
178 test1 = plist (eperm {1} {1} (s≤s z≤n) pid)
|
|
37
|
179 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
|
|
41
|
180 test11 = plist (eperm {2} {0} z≤n (eperm {1} {0} z≤n pid))
|
|
|
181 test12 = plist (eperm {2} {0} z≤n (eperm {1} {1} (s≤s z≤n) pid))
|
|
|
182 test21 = plist (eperm {2} {1} (s≤s z≤n) (eperm {1} {0} z≤n pid))
|
|
|
183 test22 = plist (eperm {2} {1} (s≤s z≤n) (eperm {1} {1} (s≤s z≤n) pid))
|
|
|
184 test23 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {0} z≤n pid))
|
|
|
185 test24 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {1} (s≤s z≤n) pid))
|
|
|
186 test3 = test11 ∷ test12 ∷ test21 ∷ test22 ∷ test23 ∷ test24 ∷ []
|
|
38
|
187
|
|
44
|
188 lem0 : {n : ℕ } → n ≤ n
|
|
|
189 lem0 {zero} = z≤n
|
|
|
190 lem0 {suc n} = s≤s lem0
|
|
|
191
|
|
|
192 lem00 : {n m : ℕ } → n ≡ m → n ≤ m
|
|
|
193 lem00 refl = lem0
|
|
38
|
194
|
|
|
195 pls : (n : ℕ ) → List (List ℕ )
|
|
40
|
196 pls n = Data.List.map plist (pls6 n) where
|
|
38
|
197 lem1 : {i n : ℕ } → i ≤ n → i < suc n
|
|
|
198 lem1 z≤n = s≤s z≤n
|
|
|
199 lem1 (s≤s lt) = s≤s (lem1 lt)
|
|
|
200 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
|
|
|
201 lem2 i≤n = ≤-trans i≤n ( refl-≤s )
|
|
40
|
202 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n))
|
|
|
203 pls4 zero n i≤n perm x = pid ∷ x
|
|
41
|
204 pls4 (suc i) n i≤n perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {i} (≤-trans refl-≤s i≤n ) perm ∷ x)
|
|
40
|
205 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n))
|
|
|
206 pls5 n [] x = x
|
|
|
207 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y)
|
|
|
208 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n))
|
|
|
209 pls6 zero = pid ∷ []
|
|
|
210 pls6 (suc n) = pls5 (suc n) (pls6 n) []
|
