Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 89:dcb4450680ab

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 Fri, 28 Aug 2020 13:33:35 +0900
parents 405c1f727ffe
children bb8c5b366219
comparison
equal deleted inserted replaced
88:405c1f727ffe 89:dcb4450680ab
103 lem0 {suc n} = s≤s lem0 103 lem0 {suc n} = s≤s lem0
104 104
105 lem00 : {n m : ℕ } → n ≡ m → n ≤ m 105 lem00 : {n m : ℕ } → n ≡ m → n ≤ m
106 lem00 refl = lem0 106 lem00 refl = lem0
107 107
108 plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ
109 plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ []
110 plist1 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 perm i (<-trans lt a<sa)
111
112 plist : {n : ℕ} → Permutation n n → List ℕ
113 plist {0} perm = []
114 plist {suc n} perm = rev (plist1 perm n a<sa)
115
108 -- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n) 116 -- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n)
109 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ? 117 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ?
110 118
111 -- inductivley enmumerate permutations 119 -- inductivley enmumerate permutations
112 -- from n-1 length create n length inserting new element at position m 120 -- from n-1 length create n length inserting new element at position m
113 121
114 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] 122 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ []
115 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) 123 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) 1 ∷ 0 ∷ 2 ∷ 3 ∷ []
116 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] 124 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] plist ( pins {3} (n≤ 2) ) 2 ∷ 0 ∷ 1 ∷ 3 ∷ []
117 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] 125 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] plist ( pins {3} (n≤ 3) ) 3 ∷ 0 ∷ 1 ∷ 2 ∷ []
118
119 pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) 126 pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
120 pins {_} {zero} _ = pid 127 pins {_} {zero} _ = pid
121 pins {suc _} {suc zero} _ = pswap pid 128 pins {suc _} {suc zero} _ = pswap pid
122 pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc (suc n)) lem0 where 129 pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where
123 pins1 : (j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) 130 pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n)))
124 pins1 zero _ = pid 131 pins1 _ zero _ = pid
125 pins1 (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 j (≤-trans si≤n refl-≤s ) 132 pins1 zero _ _ = pid
126 133 pins1 (suc i) (suc j) (s≤s si≤n) = psawpim {suc (suc (suc n))} {j} (s≤s (s≤s si≤n)) ∘ₚ pins1 i j (≤-trans si≤n refl-≤s )
127 plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ 134
128 plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] 135 pins' : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n)
129 plist1 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 perm i (<-trans lt a<sa) 136 pins' {_} {zero} _ = pid
130 137 pins' {suc n} {suc m} (s≤s m≤n) = permutation p← p→ record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
131 plist : {n : ℕ} → Permutation n n → List ℕ 138
132 plist {0} perm = [] 139 next : Fin (suc (suc n)) → Fin (suc (suc n))
133 plist {suc n} perm = rev (plist1 perm n a<sa) 140 next zero = suc zero
141 next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) refl-≤s )
142
143 p→ : Fin (suc (suc n)) → Fin (suc (suc n))
144 p→ x with <-cmp (toℕ x) (suc m)
145 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s a) (≤-trans (s≤s (s≤s m≤n) ) lem0 ))
146 ... | tri≈ ¬a b ¬c = zero
147 ... | tri> ¬a ¬b c = x
148
149 p← : Fin (suc (suc n)) → Fin (suc (suc n))
150 p← zero = fromℕ< (s≤s (s≤s m≤n))
151 p← (suc x) with <-cmp (toℕ x) (suc m)
152 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) refl-≤s )
153 ... | tri≈ ¬a b ¬c = suc x
154 ... | tri> ¬a ¬b c = suc x
155
156 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x
157 piso← = {!!}
158
159 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x
160 piso→ = {!!}
161
162 t7 = plist (pins' {3} (n≤ 3)) ∷ plist (flip ( pins' {3} (n≤ 3) )) ∷ plist ( pins' {3} (n≤ 3) ∘ₚ flip ( pins' {3} (n≤ 3))) ∷ []
163 t8 = {!!}
164
134 165
135 plist2 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ 166 plist2 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ
136 plist2 {n} perm zero _ = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ [] 167 plist2 {n} perm zero _ = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ []
137 plist2 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ʳ (fromℕ< (s≤s lt))) ∷ plist2 perm i (<-trans lt a<sa) 168 plist2 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ʳ (fromℕ< (s≤s lt))) ∷ plist2 perm i (<-trans lt a<sa)
138 169
343 ∎ 374 ∎
344 375
345 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm 376 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm
346 shrink-iso {n} {perm} = record { peq = λ q → refl } 377 shrink-iso {n} {perm} = record { peq = λ q → refl }
347 378
348 p01 : (perm : Permutation 1 1) → perm =p= pid
349 p01 perm = record { peq = p01e } where
350 p01e : (q : Fin 1) → (perm ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q)
351 p01e zero with perm ⟨$⟩ʳ zero
352 ... | zero = refl
353
354 p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
355 p=0 {zero} perm with p01 perm | p01 ( flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )))
356 ... | s | t = begin
357 ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0))
358 ≡⟨ peqˡ (presp (p01 perm) (p01 (flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ))))) (# 0) ⟩
359 (pid ∘ₚ pid ) ⟨$⟩ʳ (# 0)
360 ≡⟨⟩
361 # 0
362 ∎ where open ≡-Reasoning
363 p=0 {suc (zero)} perm with perm ⟨$⟩ʳ (# 0) | inspect ( _⟨$⟩ʳ_ perm ) (# 0)
364 ... | zero | record { eq = e } = begin
365 (perm ∘ₚ pid) ⟨$⟩ˡ (# 0)
366 ≡⟨⟩
367 perm ⟨$⟩ˡ (# 0)
368 ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (sym e ) ⟩
369 perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (# 0))
370 ≡⟨ inverseˡ perm ⟩
371 # 0
372 ∎ where open ≡-Reasoning
373 ... | suc zero | record { eq = e } = begin
374 (perm ∘ₚ pswap pid) ⟨$⟩ˡ (# 0)
375 ≡⟨⟩
376 perm ⟨$⟩ˡ (# 1)
377 ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) (sym e ) ⟩
378 perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (# 0))
379 ≡⟨ inverseˡ perm ⟩
380 # 0
381 ∎ where open ≡-Reasoning
382 p=0 {suc (suc n) } perm = p=01 (suc (suc n)) lem0 where
383 p=01 : (j : ℕ ) → j ≤ suc (suc n) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0
384 p=01 zero _ = {!!}
385 p=01 (suc j) (s≤s si≤n) = {!!}
386
387 FL→perm : {n : ℕ } → FL n → Permutation n n 379 FL→perm : {n : ℕ } → FL n → Permutation n n
388 FL→perm f0 = pid 380 FL→perm f0 = pid
389 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) 381 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x )
390 382
391 t40 = (# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) 383 t40 = (# 2) :: ( (# 1) :: (( # 0 ) :: f0 ))
409 ∷ [] 401 ∷ []
410 402
411 403
412 perm→FL : {n : ℕ } → Permutation n n → FL n 404 perm→FL : {n : ℕ } → Permutation n n → FL n
413 perm→FL {zero} perm = f0 405 perm→FL {zero} perm = f0
414 -- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) 406 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm)
415 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) 407 -- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) )
416 408
417 -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) )) 409 -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) ))
418 t5 = plist (t4) ∷ plist (flip t4) 410 t5 = plist (t4) ∷ plist (flip t4)
419 ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ< a<sa) ∷ [] ) 411 ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ< a<sa) ∷ [] )
420 ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] ) 412 ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] )