Mercurial > hg > Members > kono > Proof > galois

comparison Symmetric.agda @ 44:9ce6141ef479

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
start again
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 20 Aug 2020 21:59:22 +0900
parents 84c84695de94
children a3ee2ca4f07d
comparison
equal deleted inserted replaced
41:84c84695de94 44:9ce6141ef479
12 open import Function.LeftInverse using ( _LeftInverseOf_ ) 12 open import Function.LeftInverse using ( _LeftInverseOf_ )
13 open import Function.Equality using (Π) 13 open import Function.Equality using (Π)
14 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) 14 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n )
15 open import Data.Nat.Properties -- using (<-trans) 15 open import Data.Nat.Properties -- using (<-trans)
16 open import Relation.Binary.PropositionalEquality 16 open import Relation.Binary.PropositionalEquality
17 open import Data.List using (List; []; _∷_ ; length ; _++_ ) 17 open import Data.List using (List; []; _∷_ ; length ; _++_ ) renaming (reverse to rev )
18 open import nat 18 open import nat
19 19
20 fid : {p : ℕ } → Fin p → Fin p 20 fid : {p : ℕ } → Fin p → Fin p
21 fid x = x 21 fid x = x
22 22
120 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x 120 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
121 piso→ zero = refl 121 piso→ zero = refl
122 piso→ (suc zero) = refl 122 piso→ (suc zero) = refl
123 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) 123 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm)
124 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
175 -- enumeration 125 -- enumeration
176 126
177 psawpn : {n m : ℕ} → suc m < n → Permutation n n 127 psawpn : {n : ℕ} → 1 < n → Permutation n n
178 psawpn {suc zero} {m} (s≤s ()) 128 psawpn {suc zero} (s≤s ())
179 psawpn {suc n} {m} (s≤s (s≤s x)) = pswap pid 129 psawpn {suc n} (s≤s (s≤s x)) = pswap pid
180 130
181 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n 131 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n
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 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
183 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n 133 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n
184 pfill1 0 _ perm = perm 134 pfill1 0 _ perm = 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 ) ) 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 ) )
186 136
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
187 eperm : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n) 146 eperm : {n m : ℕ} → m ≤ n → Permutation n n → Permutation (suc n) (suc n)
188 eperm {0} {0} z≤n perm = pid 147 eperm {0} {0} z≤n perm = pid
189 eperm {suc n} {0} z≤n perm = pprep perm 148 eperm {suc n} {0} z≤n perm = pprep perm
190 eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pswap {0} pid ) (pprep perm) where 149 eperm {n} {suc m} (s≤s m<n) perm = eperm1 m 2 lemm3 (pprep perm) where
191 lemm3 : 2 + m ≤ suc n 150 lemm3 : 2 + m ≤ suc n
192 lemm3 = s≤s (s≤s m<n) 151 lemm3 = s≤s (s≤s m<n)
193 eperm1 : (m i : ℕ ) → i + m ≤ suc n → Permutation i i → Permutation (suc n)(suc n) → Permutation (suc n)(suc n) 152 eperm1 : (m i : ℕ ) → i + m ≤ suc n → Permutation (suc n)(suc n) → Permutation (suc n)(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) 153 eperm1 zero i i<ssm perm = perm ∘ₚ (psawpim {suc n} {i + m} {!!} {!!} ) --- 1 < i + m , i + m ≤ suc (suc n)
195 eperm1 (suc m) i i<ssm sw perm = eperm1 m (suc i) (lemm4 i<ssm ) (pprep sw) perm where 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
196 lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n 156 lemm4 : i + suc m ≤ suc n → suc i + m ≤ suc n
197 lemm4 lt = begin 157 lemm4 lt = begin
198 suc i + m ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩ 158 suc i + m ≡⟨ cong (λ k → suc k ) ( +-comm i _ ) ⟩
199 suc m + i ≡⟨ +-comm (suc m) _ ⟩ 159 suc m + i ≡⟨ +-comm (suc m) _ ⟩
200 i + suc m ≤⟨ lt ⟩ 160 i + suc m ≤⟨ lt ⟩
201 suc n 161 suc n
202 ∎ where open ≤-Reasoning 162 ∎ where open ≤-Reasoning
203 163
204 plist : {n : ℕ} → Permutation n n → List ℕ 164 plist : {n : ℕ} → Permutation n n → List ℕ
205 plist {0} perm = [] 165 plist {0} perm = []
206 plist {suc j} perm = plist1 j a<sa where 166 plist {suc j} perm = rev (plist1 j a<sa) where
207 n = suc j 167 n = suc j
208 plist1 : (i : ℕ ) → i < n → List ℕ 168 plist1 : (i : ℕ ) → i < n → List ℕ
209 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ [] 169 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
210 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) 170 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa)
171
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 ∷ []
211 176
212 test0 = plist (eperm {1} {0} z≤n pid) 177 test0 = plist (eperm {1} {0} z≤n pid)
213 test1 = plist (eperm {1} {1} (s≤s z≤n) pid) 178 test1 = plist (eperm {1} {1} (s≤s z≤n) pid)
214 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid ) 179 test = eperm {3} ( s≤s ( s≤s z≤n )) ( eperm (s≤s z≤n) pid )
215 test11 = plist (eperm {2} {0} z≤n (eperm {1} {0} z≤n pid)) 180 test11 = plist (eperm {2} {0} z≤n (eperm {1} {0} z≤n pid))
218 test22 = plist (eperm {2} {1} (s≤s z≤n) (eperm {1} {1} (s≤s z≤n) pid)) 183 test22 = plist (eperm {2} {1} (s≤s z≤n) (eperm {1} {1} (s≤s z≤n) pid))
219 test23 = plist (eperm {2} {2} (s≤s (s≤s z≤n)) (eperm {1} {0} z≤n pid)) 184 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)) 185 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 ∷ [] 186 test3 = test11 ∷ test12 ∷ test21 ∷ test22 ∷ test23 ∷ test24 ∷ []
222 187
223 NL : (n : ℕ ) → Set 188 lem0 : {n : ℕ } → n ≤ n
224 NL 0 = ℕ 189 lem0 {zero} = z≤n
225 NL (suc n) = List ( NL n ) 190 lem0 {suc n} = s≤s lem0
191
192 lem00 : {n m : ℕ } → n ≡ m → n ≤ m
193 lem00 refl = lem0
226 194
227 pls : (n : ℕ ) → List (List ℕ ) 195 pls : (n : ℕ ) → List (List ℕ )
228 pls n = Data.List.map plist (pls6 n) where 196 pls n = Data.List.map plist (pls6 n) where
229 lem1 : {i n : ℕ } → i ≤ n → i < suc n 197 lem1 : {i n : ℕ } → i ≤ n → i < suc n
230 lem1 z≤n = s≤s z≤n 198 lem1 z≤n = s≤s z≤n