Mercurial > hg > Members > kono > Proof > galois

comparison Symmetric.agda @ 41:84c84695de94

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 20 Aug 2020 14:13:08 +0900
parents e87ed47742b1
children 25273e17a018 9ce6141ef479
comparison
equal deleted inserted replaced
40:e87ed47742b1 41:84c84695de94
2 2
3 open import Level hiding ( suc ; zero ) 3 open import Level hiding ( suc ; zero )
4 open import Algebra 4 open import Algebra
5 open import Algebra.Structures 5 open import Algebra.Structures
6 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ) 6 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ )
7 open import Data.Fin.Properties hiding ( <-cmp ; <-trans ; ≤-trans ) 7 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp )
8 open import Data.Product 8 open import Data.Product
9 open import Data.Fin.Permutation 9 open import Data.Fin.Permutation
10 open import Function hiding (id ; flip) 10 open import Function hiding (id ; flip)
11 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) 11 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_)
12 open import Function.LeftInverse using ( _LeftInverseOf_ ) 12 open import Function.LeftInverse using ( _LeftInverseOf_ )
78 open import Relation.Binary.Core 78 open import Relation.Binary.Core
79 open import fin 79 open import fin
80 80
81 -- An inductive construction of permutation 81 -- An inductive construction of permutation
82 82
83 -- we already have refl and trans
84
83 pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) 85 pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n)
84 pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where 86 pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
85 p→ : Fin (suc n) → Fin (suc n) 87 p→ : Fin (suc n) → Fin (suc n)
86 p→ zero = zero 88 p→ zero = zero
87 p→ (suc x) = suc ( perm ⟨$⟩ˡ x) 89 p→ (suc x) = suc ( perm ⟨$⟩ˡ x)
118 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x 120 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
119 piso→ zero = refl 121 piso→ zero = refl
120 piso→ (suc zero) = refl 122 piso→ (suc zero) = refl
121 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) 123 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm)
122 124
125 Finnm : {n m : ℕ } → Fin (n + m) ≡ Fin (m + n)
126 Finnm {n} {m} = cong (λ k → Fin k ) (+-comm n _ )
127
128 Finnmconv : {n m : ℕ } → Fin (m + n) → Fin (n + m)
129 Finnmconv {n} {m} x = subst (λ k → Fin k ) (+-comm m _) x
130
131 m+n→n : {n m : ℕ } → (x : Fin (n + m)) → toℕ x < n → Fin n
132 m+n→n x x<n = fromℕ≤ x<n
133
134 n→m+n : {n m : ℕ } → (x : Fin n) → Fin (n + m)
135 n→m+n {n} {m} x = Finnmconv {n} {m} (raise m x )
136
137 m+n→m : {n m : ℕ } → (x : Fin (n + m)) → n ≤ toℕ x → Fin m
138 m+n→m x n<x = reduce≥ x n<x
139
140 m→m+n : {n m : ℕ } → (x : Fin m) → Fin (n + m)
141 m→m+n {zero} {m} x = x
142 m→m+n {suc n} {m} x = suc (m→m+n x)
143
144 lem0 : {n : ℕ } → n ≤ n
145 lem0 {zero} = z≤n
146 lem0 {suc n} = s≤s lem0
147
148 lem00 : {n m : ℕ } → n ≡ m → n ≤ m
149 lem00 refl = lem0
150
151 pconcat : {n m : ℕ } → Permutation n n → Permutation m m → Permutation (n + m) (n + m)
152 pconcat {n} {m} p q = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where
153 p→ : Fin (n + m) → Fin (n + m)
154 p→ x with <-cmp (toℕ x ) n
155 p→ x | tri< a ¬b ¬c = n→m+n (p ⟨$⟩ˡ (m+n→n x a ))
156 p→ x | tri≈ ¬a b ¬c = m→m+n (q ⟨$⟩ˡ (m+n→m x (lem00 (sym b)) ) )
157 p→ x | tri> ¬a ¬b c = m→m+n (q ⟨$⟩ˡ (m+n→m x (≤to< c) ))
158
159 p← : Fin (n + m) → Fin (n + m)
160 p← x with <-cmp (toℕ x ) n
161 p← x | tri< a ¬b ¬c = n→m+n (p ⟨$⟩ʳ (m+n→n x a ))
162 p← x | tri≈ ¬a b ¬c = m→m+n (q ⟨$⟩ʳ (m+n→m x (lem00 (sym b))))
163 p← x | tri> ¬a ¬b c = m→m+n (q ⟨$⟩ʳ (m+n→m x (≤to< c)) )
164
165 piso← : (x : Fin (n + m) ) → p→ ( p← x ) ≡ x
166 piso← x with <-cmp (toℕ x ) n
167 piso← x | tri< a ¬b ¬c = ?
168 piso← x | tri≈ ¬a b ¬c = ?
169 piso← x | tri> ¬a ¬b c = ?
170
171 piso→ : (x : Fin (n + m) ) → p← ( p→ x ) ≡ x
172 piso→ = {!!}
173
174
123 -- enumeration 175 -- enumeration
124 176
125 psawpn : {n m : ℕ} → suc m < n → Permutation n n 177 psawpn : {n m : ℕ} → suc m < n → Permutation n n
126 psawpn {suc zero} {m} (s≤s ()) 178 psawpn {suc zero} {m} (s≤s ())
127 psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid 179 psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid
130 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 182 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
131 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n 183 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n
132 pfill1 0 _ perm = perm 184 pfill1 0 _ perm = perm
133 pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) ) 185 pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) )
134 186
135 eperm : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n) 187 eperm : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
136 eperm {zero} () 188 eperm {0} {0} z≤n perm = pid
137 eperm {n} {0} (s≤s z≤n) perm = pprep perm 189 eperm {suc n} {0} z≤n perm = pprep perm
138 eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where 190 eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where
139 lemm3 : 2 + m ≤ suc n 191 lemm3 : 2 + m ≤ suc n
140 lemm3 = ≤-trans (s≤s m<n) refl-≤s 192 lemm3 = s≤s (s≤s m<n)
141 eperm1 : (m i : ℕ ) → i + m ≤ suc n → Permutation i i → Permutation (suc n)(suc n)→ Permutation (suc n)(suc n) 193 eperm1 : (m i : ℕ ) → i + m ≤ suc n → Permutation i i → Permutation (suc n)(suc n) → Permutation (suc n)(suc n)
142 eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill (subst (λ k → k ≤ suc n) (+-comm i _) i<ssm) sw ) -- i + zero ≤ suc (suc n) → i ≤ suc (suc n) 194 eperm1 zero i i<ssm sw perm = perm ∘ₚ ( pfill (subst (λ k → k ≤ suc n) (+-comm i _) i<ssm) sw ) -- i + zero ≤ suc (suc n) → i ≤ suc (suc n)
143 eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where 195 eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where
144 lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n 196 lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
145 lemm4 lt = begin 197 lemm4 lt = begin
146 suc i + m ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩ 198 suc i + m ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
147 suc m + i ≡⟨ +-comm (suc m) _ ⟩ 199 suc m + i ≡⟨ +-comm (suc m) _ ⟩
148 i + suc m ≤⟨ lt ⟩ 200 i + suc m ≤⟨ lt ⟩
149 suc n 201 suc n
150 ∎ where open ≤-Reasoning 202 ∎ where open ≤-Reasoning
151 203
152
153 finpid : (n i : ℕ ) → i < n → List (Fin n)
154 finpid (suc n) zero _ = fromℕ≤ {zero} (s≤s z≤n) ∷ []
155 finpid (suc n) (suc i) (s≤s lt) = fromℕ≤ (s≤s lt) ∷ finpid (suc n) i (<-trans lt a<sa)
156
157 fpid : (n : ℕ ) → List (Fin n)
158 fpid 0 = []
159 fpid (suc j) = finpid (suc j) j a<sa where
160
161 plist : {n : ℕ} → Permutation n n → List ℕ 204 plist : {n : ℕ} → Permutation n n → List ℕ
162 plist {0} perm = [] 205 plist {0} perm = []
163 plist {suc j} perm = plist1 j a<sa where 206 plist {suc j} perm = plist1 j a<sa where
164 n = suc j 207 n = suc j
165 plist1 : (i : ℕ ) → i < n → List ℕ 208 plist1 : (i : ℕ ) → i < n → List ℕ
166 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ [] 209 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
167 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) 210 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa)
168 211
212 test0 = plist (eperm {1} {0} z≤n pid)
213 test1 = plist (eperm {1} {1} (s≤s z≤n) pid)
169 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid ) 214 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
170 test10 = plist (eperm {2} {0} ( s≤s z≤n) pid) 215 test11 = plist (eperm {2} {0} z≤n (eperm {1} {0} z≤n pid))
171 test11 = plist (eperm {2} {0} ( s≤s z≤n) (eperm {1} {0} (s≤s z≤n) pid)) 216 test12 = plist (eperm {2} {0} z≤n (eperm {1} {1} (s≤s z≤n) pid))
172 test20 = plist (eperm {2} {1} (s≤s ( s≤s z≤n)) pid) 217 test21 = plist (eperm {2} {1} (s≤s z≤n) (eperm {1} {0} z≤n pid))
173 test21 = plist (eperm {2} {1} (s≤s ( s≤s z≤n)) (eperm {1} {0} (s≤s z≤n) pid)) 218 test22 = plist (eperm {2} {1} (s≤s z≤n) (eperm {1} {1} (s≤s z≤n) pid))
174 test3 = test10 ∷ test11 ∷ test20 ∷ test21 ∷ [] 219 test23 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {0} z≤n pid))
220 test24 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {1} (s≤s z≤n) pid))
221 test3 = test11 ∷ test12 ∷ test21 ∷ test22 ∷ test23 ∷ test24 ∷ []
175 222
176 NL : (n : ℕ ) → Set 223 NL : (n : ℕ ) → Set
177 NL 0 = ℕ 224 NL 0 = ℕ
178 NL (suc n) = List ( NL n ) 225 NL (suc n) = List ( NL n )
179 226
180 pls : (n : ℕ ) → List (List ℕ ) 227 pls : (n : ℕ ) → List (List ℕ )
181 pls n = Data.List.map plist (pls6 n) where 228 pls n = Data.List.map plist (pls6 n) where
182 lem0 : {n : ℕ } → n ≤ n
183 lem0 {zero} = z≤n
184 lem0 {suc n} = s≤s lem0
185 lem1 : {i n : ℕ } → i ≤ n → i < suc n 229 lem1 : {i n : ℕ } → i ≤ n → i < suc n
186 lem1 z≤n = s≤s z≤n 230 lem1 z≤n = s≤s z≤n
187 lem1 (s≤s lt) = s≤s (lem1 lt) 231 lem1 (s≤s lt) = s≤s (lem1 lt)
188 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n 232 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
189 lem2 i≤n = ≤-trans i≤n ( refl-≤s ) 233 lem2 i≤n = ≤-trans i≤n ( refl-≤s )
190 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) 234 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n))
191 pls4 zero n i≤n perm x = pid ∷ x 235 pls4 zero n i≤n perm x = pid ∷ x
192 pls4 (suc i) n i≤n perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (eperm {n} {i} i≤n perm ∷ x) 236 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)
193 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) 237 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n))
194 pls5 n [] x = x 238 pls5 n [] x = x
195 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) 239 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y)
196 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) 240 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n))
197 pls6 zero = pid ∷ [] 241 pls6 zero = pid ∷ []