Mercurial > hg > Members > kono > Proof > galois
annotate Putil.agda @ 61:c16749815259
another shrink
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Mon, 24 Aug 2020 12:04:25 +0900 |
parents | 48926e810f5f |
children | a66f773330b4 |
rev | line source |
---|---|
48 | 1 module Putil where |
0 | 2 |
3 open import Level hiding ( suc ; zero ) | |
4 open import Algebra | |
5 open import Algebra.Structures | |
37 | 6 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ) |
41 | 7 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ) renaming ( <-cmp to <-fcmp ) |
0 | 8 open import Data.Fin.Permutation |
9 open import Function hiding (id ; flip) | |
10 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) | |
11 open import Function.LeftInverse using ( _LeftInverseOf_ ) | |
12 open import Function.Equality using (Π) | |
17 | 13 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) |
14 open import Data.Nat.Properties -- using (<-trans) | |
16 | 15 open import Relation.Binary.PropositionalEquality |
46 | 16 open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ) renaming (reverse to rev ) |
16 | 17 open import nat |
0 | 18 |
48 | 19 open import Symmetric |
0 | 20 |
21 | |
16 | 22 open import Relation.Nullary |
23 open import Data.Empty | |
17 | 24 open import Relation.Binary.Core |
25 open import fin | |
16 | 26 |
38 | 27 -- An inductive construction of permutation |
34 | 28 |
59 | 29 -- Todo |
30 -- | |
31 -- complete perm→FL | |
32 -- describe property of pprep and pswap | |
33 -- describe property of pins ( move 0 to any position) | |
34 -- describe property of shrink ( remove one column ) | |
35 -- prove FL→iso | |
36 -- prove FL←iso | |
37 -- prove FL enumerate all permutations | |
38 | |
48 | 39 -- we already have refl and trans in the Symmetric Group |
41 | 40 |
34 | 41 pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) |
42 pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
33 | 43 p→ : Fin (suc n) → Fin (suc n) |
34 | 44 p→ zero = zero |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
45 p→ (suc x) = suc ( perm ⟨$⟩ʳ x) |
33 | 46 |
34 | 47 p← : Fin (suc n) → Fin (suc n) |
48 p← zero = zero | |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
49 p← (suc x) = suc ( perm ⟨$⟩ˡ x) |
34 | 50 |
51 piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x | |
52 piso← zero = refl | |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
53 piso← (suc x) = cong (λ k → suc k ) (inverseʳ perm) |
33 | 54 |
34 | 55 piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x |
56 piso→ zero = refl | |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
57 piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) |
33 | 58 |
34 | 59 pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) |
60 pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
61 p→ : Fin (suc (suc n)) → Fin (suc (suc n)) | |
62 p→ zero = suc zero | |
63 p→ (suc zero) = zero | |
64 p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) | |
18 | 65 |
34 | 66 p← : Fin (suc (suc n)) → Fin (suc (suc n)) |
67 p← zero = suc zero | |
68 p← (suc zero) = zero | |
69 p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) | |
70 | |
71 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x | |
72 piso← zero = refl | |
73 piso← (suc zero) = refl | |
35 | 74 piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) |
16 | 75 |
34 | 76 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x |
77 piso→ zero = refl | |
78 piso→ (suc zero) = refl | |
35 | 79 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) |
34 | 80 |
81 -- enumeration | |
82 | |
44 | 83 psawpn : {n : ℕ} → 1 < n → Permutation n n |
84 psawpn {suc zero} (s≤s ()) | |
85 psawpn {suc n} (s≤s (s≤s x)) = pswap pid | |
34 | 86 |
35 | 87 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n |
88 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 | |
89 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n | |
90 pfill1 0 _ perm = perm | |
91 pfill1 (suc i) i<n perm = pfill1 i (≤to< i<n) (subst (λ k → Permutation k k ) (si-sn=i-n i<n ) ( pprep perm ) ) | |
34 | 92 |
48 | 93 -- |
94 -- psawpim (inseert swap at position m ) | |
95 -- not easy to write directory beacause left-inverse-of may contains Fin relations | |
96 -- | |
45 | 97 psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n |
98 psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) ) | |
99 | |
100 n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j | |
101 n≤ (zero) {j} = z≤n | |
102 n≤ (suc i) {j} = s≤s ( n≤ i ) | |
103 | |
104 lem0 : {n : ℕ } → n ≤ n | |
105 lem0 {zero} = z≤n | |
106 lem0 {suc n} = s≤s lem0 | |
107 | |
108 lem00 : {n m : ℕ } → n ≡ m → n ≤ m | |
109 lem00 refl = lem0 | |
44 | 110 |
111 -- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n) | |
112 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ? | |
113 | |
114 -- inductivley enmumerate permutations | |
115 -- from n-1 length create n length inserting new element at position m | |
116 | |
48 | 117 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] |
118 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) | |
119 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] | |
120 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] | |
45 | 121 |
48 | 122 pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) |
123 pins {_} {zero} _ = pid | |
124 pins {suc _} {suc zero} _ = pswap pid | |
125 pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where | |
126 pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) | |
127 pins1 _ zero _ = pid | |
128 pins1 zero _ _ = pid | |
129 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 ) | |
37 | 130 |
131 plist : {n : ℕ} → Permutation n n → List ℕ | |
132 plist {0} perm = [] | |
44 | 133 plist {suc j} perm = rev (plist1 j a<sa) where |
37 | 134 n = suc j |
135 plist1 : (i : ℕ ) → i < n → List ℕ | |
40 | 136 plist1 zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ {zero} (s≤s z≤n))) ∷ [] |
137 plist1 (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ≤ (s≤s lt))) ∷ plist1 i (<-trans lt a<sa) | |
37 | 138 |
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
139 data FL : (n : ℕ )→ Set where |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
140 f0 : FL 0 |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
141 _::_ : { n : ℕ } → Fin (suc n ) → FL n → FL (suc n) |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
142 |
50 | 143 open import logic |
144 | |
56 | 145 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] |
61 | 146 shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n |
147 shrink {n} perm p0=0 = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
148 shlem→ : (x : Fin (suc n) ) → perm ⟨$⟩ˡ x ≡ zero → x ≡ zero | |
149 shlem→ x px=0 = begin | |
150 x ≡⟨ sym ( inverseʳ perm ) ⟩ | |
151 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x) ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) px=0 ⟩ | |
152 perm ⟨$⟩ʳ zero ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) (sym p0=0) ⟩ | |
153 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero) ≡⟨ inverseʳ perm ⟩ | |
154 zero | |
155 ∎ where open ≡-Reasoning | |
54 | 156 |
61 | 157 shlem← : (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero |
158 shlem← x px=0 = begin | |
159 x ≡⟨ sym (inverseˡ perm ) ⟩ | |
160 perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x ) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) px=0 ⟩ | |
161 perm ⟨$⟩ˡ zero ≡⟨ p0=0 ⟩ | |
162 zero | |
163 ∎ where open ≡-Reasoning | |
54 | 164 |
61 | 165 sh2 : {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero |
166 sh2 {x} eq with shlem→ (suc x) eq | |
167 sh2 {x} eq | () | |
57 | 168 |
61 | 169 p→ : Fin n → Fin n |
170 p→ x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) | |
171 p→ x | zero | record { eq = e } = ⊥-elim ( sh2 {x} e ) | |
172 p→ x | suc t | _ = t | |
50 | 173 |
61 | 174 sh1 : {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero |
175 sh1 {x} eq with shlem← (suc x) eq | |
176 sh1 {x} eq | () | |
50 | 177 |
178 p← : Fin n → Fin n | |
61 | 179 p← x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) |
180 p← x | zero | record { eq = e } = ⊥-elim ( sh1 {x} e ) | |
181 p← x | suc t | _ = t | |
50 | 182 |
183 piso← : (x : Fin n ) → p→ ( p← x ) ≡ x | |
61 | 184 piso← x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) |
185 piso← x | zero | record { eq = e } = ⊥-elim ( sh1 {x} e ) | |
186 piso← x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) | |
187 piso← x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 e ) | |
188 piso← x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin | |
189 t1 | |
190 ≡⟨ plem0 plem1 ⟩ | |
52 | 191 x |
61 | 192 ∎ where |
193 open ≡-Reasoning | |
194 plem0 : suc t1 ≡ suc x → t1 ≡ x | |
195 plem0 refl = refl | |
196 plem1 : suc t1 ≡ suc x | |
197 plem1 = begin | |
198 suc t1 | |
199 ≡⟨ sym e1 ⟩ | |
200 Inverse.from perm Π.⟨$⟩ suc t | |
201 ≡⟨ cong (λ k → Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩ | |
202 Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x ) | |
203 ≡⟨ inverseˡ perm ⟩ | |
204 suc x | |
205 ∎ | |
50 | 206 |
207 piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x | |
61 | 208 piso→ x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) |
209 piso→ x | zero | record { eq = e } = ⊥-elim ( sh2 {x} e ) | |
210 piso→ x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t) | |
211 piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh1 e ) | |
212 piso→ x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin | |
213 t1 | |
214 ≡⟨ plem2 plem3 ⟩ | |
53 | 215 x |
61 | 216 ∎ where |
217 open ≡-Reasoning | |
218 plem2 : suc t1 ≡ suc x → t1 ≡ x | |
219 plem2 refl = refl | |
220 plem3 : suc t1 ≡ suc x | |
221 plem3 = begin | |
222 suc t1 | |
223 ≡⟨ sym e1 ⟩ | |
224 Inverse.to perm Π.⟨$⟩ suc t | |
225 ≡⟨ cong (λ k → Inverse.to perm Π.⟨$⟩ k ) (sym e0 ) ⟩ | |
226 Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x ) | |
227 ≡⟨ inverseʳ perm ⟩ | |
228 suc x | |
229 ∎ | |
57 | 230 |
231 FL→perm : {n : ℕ } → FL n → Permutation n n | |
232 FL→perm f0 = pid | |
233 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) | |
234 | |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
235 t40 = (# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
236 t4 = FL→perm ((# 2) :: t40 ) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
237 |
61 | 238 -- t1 = plist (shrink (pid {3} ∘ₚ (pins (n≤ 1))) refl) |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
239 t2 = plist ((pid {5} ) ∘ₚ transpose (# 2) (# 4)) ∷ plist (pid {5} ∘ₚ reverse ) ∷ [] |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
240 t3 = plist (FL→perm t40) -- ∷ plist (pprep (FL→perm t40)) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
241 -- ∷ plist ( pprep (FL→perm t40) ∘ₚ pins ( n≤ 0 {3} )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
242 -- ∷ plist ( pprep (FL→perm t40 )∘ₚ pins ( n≤ 1 {2} )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
243 -- ∷ plist ( pprep (FL→perm t40 )∘ₚ pins ( n≤ 2 {1} )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
244 -- ∷ plist ( pprep (FL→perm t40 )∘ₚ pins ( n≤ 3 {0} )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
245 ∷ plist ( FL→perm ((# 0) :: t40)) -- (0 ∷ 1 ∷ 2 ∷ []) ∷ |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
246 ∷ plist ( FL→perm ((# 1) :: t40)) -- (0 ∷ 2 ∷ 1 ∷ []) ∷ |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
247 ∷ plist ( FL→perm ((# 2) :: t40)) -- (1 ∷ 0 ∷ 2 ∷ []) ∷ |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
248 ∷ plist ( FL→perm ((# 3) :: t40)) -- (2 ∷ 0 ∷ 1 ∷ []) ∷ |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
249 -- ∷ plist ( FL→perm ((# 3) :: ((# 2) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) -- (1 ∷ 2 ∷ 0 ∷ []) ∷ |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
250 -- ∷ plist ( FL→perm ((# 3) :: ((# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) -- (2 ∷ 1 ∷ 0 ∷ []) ∷ |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
251 -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))))) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
252 -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) )) |
57 | 253 ∷ [] |
50 | 254 |
61 | 255 p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 |
256 p=0 perm = {!!} | |
58 | 257 |
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
258 perm→FL : {n : ℕ } → Permutation n n → FL n |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
259 perm→FL {zero} perm = f0 |
61 | 260 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
261 |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
262 -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
263 t5 = plist (t4) ∷ plist (flip t4) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
264 ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] ) |
61 | 265 ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] ) |
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
266 -- ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 1 ) )) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
267 ∷ plist (remove (# 0) t4 ) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
268 ∷ plist ( FL→perm t40 ) |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
269 ∷ [] |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
270 |
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
271 t6 = perm→FL t4 |
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
272 |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
273 FL→iso : {n : ℕ } → (fl : FL n ) → perm→FL ( FL→perm fl ) ≡ fl |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
274 FL→iso f0 = refl |
61 | 275 FL→iso (x :: fl) = {!!} -- with FL→iso fl |
276 -- ... | t = {!!} | |
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
277 |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
278 open _=p=_ |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
279 FL←iso : {n : ℕ } → (perm : Permutation n n ) → FL→perm ( perm→FL perm ) =p= perm |
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
280 FL←iso {0} perm = record { peq = λ () } |
61 | 281 FL←iso {suc n} perm = {!!} |
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
282 |
48 | 283 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) ) |
284 all-perm n = pls6 n where | |
38 | 285 lem1 : {i n : ℕ } → i ≤ n → i < suc n |
286 lem1 z≤n = s≤s z≤n | |
287 lem1 (s≤s lt) = s≤s (lem1 lt) | |
288 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n | |
289 lem2 i≤n = ≤-trans i≤n ( refl-≤s ) | |
40 | 290 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
48 | 291 pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x |
292 pls4 (suc i) n i≤n perm x = pls4 i n (≤-trans refl-≤s i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n ∷ x) | |
40 | 293 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
294 pls5 n [] x = x | |
295 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) | |
296 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) | |
297 pls6 zero = pid ∷ [] | |
48 | 298 pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first |
299 | |
300 pls : (n : ℕ ) → List (List ℕ ) | |
301 pls n = Data.List.map plist (all-perm n) where |