Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 87:c68956f6c3ad

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
tc fix
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 27 Aug 2020 11:44:58 +0900
parents c5329963c583
children 405c1f727ffe
comparison
equal deleted inserted replaced
86:c5329963c583 87:c68956f6c3ad
208 toℕ (suc (fromℕ< i<sn)) 208 toℕ (suc (fromℕ< i<sn))
209 ∎ ) where open ≡-Reasoning 209 ∎ ) where open ≡-Reasoning
210 pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) 210 pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) )
211 pleq2 = headeq eq 211 pleq2 = headeq eq
212 212
213 pprep-cong : {n : ℕ} → (x y : Permutation n n ) → x =p= y → pprep x =p= pprep y 213 pprep-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y
214 pprep-cong {n} x y x=y = {!!} where 214 pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where
215 pprep-cong02 : (x : Permutation 1 1 ) → (q : Fin 1) → (x ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) 215 pprep-cong1 : (q : Fin (suc n)) → (pprep x ⟨$⟩ʳ q) ≡ (pprep y ⟨$⟩ʳ q)
216 pprep-cong02 x zero with x ⟨$⟩ʳ zero | inspect (_⟨$⟩ʳ_ x) zero 216 pprep-cong1 zero = refl
217 ... | zero | record { eq = e } = refl 217 pprep-cong1 (suc q) = begin
218 pprep-cong01 : (x : Permutation 1 1 ) → x =p= pid 218 pprep x ⟨$⟩ʳ suc q
219 pprep-cong01 x = record { peq = pprep-cong02 x } 219 ≡⟨⟩
220 pprep-cong0 : (n : ℕ) → (x : Permutation (suc n) (suc n) ) → toℕ (x ⟨$⟩ʳ fromℕ< a<sa ) ≡ n 220 suc ( x ⟨$⟩ʳ q )
221 pprep-cong0 zero x = begin 221 ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩
222 toℕ (x ⟨$⟩ʳ fromℕ< a<sa) 222 suc ( y ⟨$⟩ʳ q )
223 ≡⟨⟩ 223 ≡⟨⟩
224 toℕ (x ⟨$⟩ʳ zero) 224 pprep y ⟨$⟩ʳ suc q
225 ≡⟨ cong (λ k → toℕ k) (pprep-cong02 x zero) ⟩ 225 ∎ where open ≡-Reasoning
226 toℕ {suc zero} zero 226
227 ≡⟨⟩ 227 pprep-dist : {n : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y)
228 zero 228 pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where
229 ∎ where open ≡-Reasoning 229 pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q)
230 pprep-cong0 (suc n) x = {!!} 230 pprep-dist1 zero = refl
231 t1 = plist0 (pprep (pid {3})) 231 pprep-dist1 (suc q) = cong ( λ k → suc k ) refl
232 pprep-cong1 : (n : ℕ) → (x : Permutation n n ) → plist0 (pprep x) ≡ n ∷ plist0 x 232
233 pprep-cong1 zero x = refl 233 pswap-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pswap x =p= pswap y
234 pprep-cong1 (suc n) x = {!!} 234 pswap-cong {n} {x} {y} x=y = record { peq = pswap-cong1 } where
235 pswap-cong1 : (q : Fin (suc (suc n))) → (pswap x ⟨$⟩ʳ q) ≡ (pswap y ⟨$⟩ʳ q)
236 pswap-cong1 zero = refl
237 pswap-cong1 (suc zero) = refl
238 pswap-cong1 (suc (suc q)) = begin
239 pswap x ⟨$⟩ʳ suc (suc q)
240 ≡⟨⟩
241 suc (suc (x ⟨$⟩ʳ q))
242 ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩
243 suc (suc (y ⟨$⟩ʳ q))
244 ≡⟨⟩
245 pswap y ⟨$⟩ʳ suc (suc q)
246 ∎ where open ≡-Reasoning
247
248 pswap-dist : {n : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y)
249 pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where
250 pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q)
251 pswap-dist1 zero = refl
252 pswap-dist1 (suc zero) = refl
253 pswap-dist1 (suc (suc q)) = cong ( λ k → suc (suc k) ) refl
235 254
236 data FL : (n : ℕ )→ Set where 255 data FL : (n : ℕ )→ Set where
237 f0 : FL 0 256 f0 : FL 0
238 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n) 257 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
239 258