Mercurial > hg > Members > kono > Proof > galois

comparison Putil.agda @ 49:8b3b95362ca9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
remove (fromℕ≤ a<sa) perm is no good
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 22 Aug 2020 19:55:41 +0900
parents ac2f21a2d467
children ddec1ef4f5e4
comparison
equal deleted inserted replaced
48:ac2f21a2d467 49:8b3b95362ca9
124 n = suc j 124 n = suc j
125 plist1 : (i : ℕ ) → i < n → List ℕ 125 plist1 : (i : ℕ ) → i < n → List ℕ
126 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ [] 126 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ []
127 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) 127 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa)
128 128
129 data FL : (n : ℕ )→ Set where
130 f0 : FL 0
131 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n)
132
133 perm→FL : {n : ℕ } → Permutation n n → FL n
134 perm→FL {zero} perm = f0
135 perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL {n} ( remove (fromℕ≤ a<sa) perm )
136
137 FL→perm : {n : ℕ } → FL n → Permutation n n
138 FL→perm f0 = pid
139 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x )
140
141 FL→iso : {n : ℕ } → (fl : FL n ) → perm→FL ( FL→perm fl ) ≡ fl
142 FL→iso f0 = refl
143 FL→iso (x :: fl) with FL→iso fl
144 ... | t = {!!}
145
146 open _=p=_
147 FL←iso : {n : ℕ } → (perm : Permutation n n ) → FL→perm ( perm→FL perm ) =p= perm
148 FL←iso {0} perm = record { peq = λ () }
149 FL←iso {suc n} perm = {!!} where
150 fl0 : {n : ℕ } → (fl : FL n ) → {!!}
151 fl0 = {!!}
152
129 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) ) 153 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) )
130 all-perm n = pls6 n where 154 all-perm n = pls6 n where
131 lem1 : {i n : ℕ } → i ≤ n → i < suc n 155 lem1 : {i n : ℕ } → i ≤ n → i < suc n
132 lem1 z≤n = s≤s z≤n 156 lem1 z≤n = s≤s z≤n
133 lem1 (s≤s lt) = s≤s (lem1 lt) 157 lem1 (s≤s lt) = s≤s (lem1 lt)