Mercurial > hg > Members > kono > Proof > galois
annotate Putil.agda @ 58:80d61b6776d3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 23 Aug 2020 20:07:23 +0900 |
| parents | 518d364a58a3 |
| children | afa989a4b7e9 |
| 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 |
| 48 | 29 -- we already have refl and trans in the Symmetric Group |
| 41 | 30 |
| 34 | 31 pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) |
| 32 pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
| 33 | 33 p→ : Fin (suc n) → Fin (suc n) |
| 34 | 34 p→ zero = zero |
| 35 p→ (suc x) = suc ( perm ⟨$⟩ˡ x) | |
| 33 | 36 |
| 34 | 37 p← : Fin (suc n) → Fin (suc n) |
| 38 p← zero = zero | |
| 39 p← (suc x) = suc ( perm ⟨$⟩ʳ x) | |
| 40 | |
| 41 piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x | |
| 42 piso← zero = refl | |
| 35 | 43 piso← (suc x) = cong (λ k → suc k ) (inverseˡ perm) |
| 33 | 44 |
| 34 | 45 piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x |
| 46 piso→ zero = refl | |
| 35 | 47 piso→ (suc x) = cong (λ k → suc k ) (inverseʳ perm) |
| 33 | 48 |
| 34 | 49 pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) |
| 50 pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
| 51 p→ : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 52 p→ zero = suc zero | |
| 53 p→ (suc zero) = zero | |
| 54 p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) | |
| 18 | 55 |
| 34 | 56 p← : Fin (suc (suc n)) → Fin (suc (suc n)) |
| 57 p← zero = suc zero | |
| 58 p← (suc zero) = zero | |
| 59 p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) | |
| 60 | |
| 61 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x | |
| 62 piso← zero = refl | |
| 63 piso← (suc zero) = refl | |
| 35 | 64 piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) |
| 16 | 65 |
| 34 | 66 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x |
| 67 piso→ zero = refl | |
| 68 piso→ (suc zero) = refl | |
| 35 | 69 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) |
| 34 | 70 |
| 71 -- enumeration | |
| 72 | |
| 44 | 73 psawpn : {n : ℕ} → 1 < n → Permutation n n |
| 74 psawpn {suc zero} (s≤s ()) | |
| 75 psawpn {suc n} (s≤s (s≤s x)) = pswap pid | |
| 34 | 76 |
| 35 | 77 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n |
| 78 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 | |
| 79 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n | |
| 80 pfill1 0 _ perm = perm | |
| 81 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 | 82 |
| 48 | 83 -- |
| 84 -- psawpim (inseert swap at position m ) | |
| 85 -- not easy to write directory beacause left-inverse-of may contains Fin relations | |
| 86 -- | |
| 45 | 87 psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n |
| 88 psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) ) | |
| 89 | |
| 90 n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j | |
| 91 n≤ (zero) {j} = z≤n | |
| 92 n≤ (suc i) {j} = s≤s ( n≤ i ) | |
| 93 | |
| 94 lem0 : {n : ℕ } → n ≤ n | |
| 95 lem0 {zero} = z≤n | |
| 96 lem0 {suc n} = s≤s lem0 | |
| 97 | |
| 98 lem00 : {n m : ℕ } → n ≡ m → n ≤ m | |
| 99 lem00 refl = lem0 | |
| 44 | 100 |
| 101 -- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n) | |
| 102 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ? | |
| 103 | |
| 104 -- inductivley enmumerate permutations | |
| 105 -- from n-1 length create n length inserting new element at position m | |
| 106 | |
| 48 | 107 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] |
| 108 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) | |
| 109 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] | |
| 110 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] | |
| 45 | 111 |
| 48 | 112 pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) |
| 113 pins {_} {zero} _ = pid | |
| 114 pins {suc _} {suc zero} _ = pswap pid | |
| 115 pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where | |
| 116 pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) | |
| 117 pins1 _ zero _ = pid | |
| 118 pins1 zero _ _ = pid | |
| 119 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 | 120 |
| 121 plist : {n : ℕ} → Permutation n n → List ℕ | |
| 122 plist {0} perm = [] | |
| 44 | 123 plist {suc j} perm = rev (plist1 j a<sa) where |
| 37 | 124 n = suc j |
| 125 plist1 : (i : ℕ ) → i < n → List ℕ | |
| 40 | 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) | |
| 37 | 128 |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
129 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
|
130 f0 : FL 0 |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
131 _::_ : { 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
|
132 |
| 50 | 133 open import logic |
| 134 | |
| 56 | 135 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] |
| 51 | 136 shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (fromℕ n) ≡ fromℕ n → Permutation n n |
| 54 | 137 shrink {n} perm pn=n = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where |
| 138 | |
| 139 sh3 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ˡ (fin+1 x)) ≡ n ) | |
| 140 sh3 x eq = ⊥-elim ( nat-≡< sh31 fin<n ) where | |
| 141 sh31 : toℕ x ≡ n | |
| 142 sh31 = begin | |
| 143 toℕ x | |
| 55 | 144 ≡⟨ sym fin+1-toℕ ⟩ |
| 54 | 145 toℕ (fin+1 x) |
| 146 ≡⟨ cong (λ k → toℕ k ) (sym ( inverseʳ perm)) ⟩ | |
| 147 toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fin+1 x))) | |
| 55 | 148 ≡⟨ cong (λ k → toℕ (perm ⟨$⟩ʳ k )) (sym (toℕ→from eq)) ⟩ |
| 54 | 149 toℕ (perm ⟨$⟩ʳ fromℕ n) |
| 150 ≡⟨ cong ( λ k → toℕ (perm ⟨$⟩ʳ k )) (sym pn=n) ⟩ | |
| 151 toℕ (perm ⟨$⟩ʳ (perm ⟨$⟩ˡ (fromℕ n) )) | |
| 152 ≡⟨ cong (λ k → toℕ k ) ( inverseʳ perm ) ⟩ | |
| 153 toℕ (fromℕ n) | |
| 55 | 154 ≡⟨ toℕ-fromℕ _ ⟩ |
| 54 | 155 n |
| 156 ∎ where | |
| 157 open ≡-Reasoning | |
| 158 | |
| 159 sh4 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ʳ (fin+1 x)) ≡ n ) | |
| 160 sh4 x eq = ⊥-elim ( nat-≡< sh41 fin<n ) where | |
| 161 sh41 : toℕ x ≡ n | |
| 162 sh41 = begin | |
| 163 toℕ x | |
| 55 | 164 ≡⟨ sym fin+1-toℕ ⟩ |
| 54 | 165 toℕ (fin+1 x) |
| 166 ≡⟨ cong (λ k → toℕ k ) (sym ( inverseˡ perm)) ⟩ | |
| 167 toℕ (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ (fin+1 x))) | |
| 55 | 168 ≡⟨ cong (λ k → toℕ (perm ⟨$⟩ˡ k )) (sym (toℕ→from eq)) ⟩ |
| 54 | 169 toℕ ((perm ⟨$⟩ˡ fromℕ n)) |
| 170 ≡⟨ cong (λ k → toℕ k) pn=n ⟩ | |
| 171 toℕ (fromℕ n) | |
| 55 | 172 ≡⟨ toℕ-fromℕ _ ⟩ |
| 54 | 173 n |
| 174 ∎ where | |
| 175 open ≡-Reasoning | |
| 176 | |
| 57 | 177 sh5 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ˡ (fin+1 x)) > n ) |
| 178 sh5 x lt = ⊥-elim ( nat-≤> lt (fin<n {suc n} {perm ⟨$⟩ˡ (fin+1 x)})) | |
| 179 | |
| 180 sh6 : (x : Fin n) → ¬ ( toℕ (perm ⟨$⟩ʳ (fin+1 x)) > n ) | |
| 181 sh6 x lt = ⊥-elim ( nat-≤> lt (fin<n {suc n} {perm ⟨$⟩ʳ (fin+1 x)})) | |
| 182 | |
| 51 | 183 shlem→ : (x : Fin n ) → toℕ (perm ⟨$⟩ˡ (fin+1 x)) < n |
| 184 shlem→ x with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 x))) n | |
| 185 shlem→ x | tri< a ¬b ¬c = a | |
| 54 | 186 shlem→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b ) |
| 57 | 187 shlem→ x | tri> ¬a ¬b c = ⊥-elim ( sh5 x c ) |
| 50 | 188 |
| 51 | 189 shlem← : (x : Fin n) → toℕ (perm ⟨$⟩ʳ (fin+1 x)) < n |
| 190 shlem← x with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x))) n | |
| 191 shlem← x | tri< a ¬b ¬c = a | |
| 54 | 192 shlem← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b ) |
| 57 | 193 shlem← x | tri> ¬a ¬b c = ⊥-elim ( sh6 x c ) |
| 50 | 194 |
| 51 | 195 p→ : (x : Fin n ) → Fin n |
| 196 p→ x = fromℕ≤ (shlem→ x) | |
| 50 | 197 |
| 198 p← : Fin n → Fin n | |
| 51 | 199 p← x = fromℕ≤ (shlem← x) |
| 50 | 200 |
| 52 | 201 ff : { x y n : ℕ } → (x ≡ y ) → (x<n : x < n) → (y<n : y < n) → fromℕ≤ x<n ≡ fromℕ≤ y<n |
| 202 ff refl _ _ = lemma10 refl | |
| 203 | |
| 204 -- a : (toℕ (Inverse.to perm Π.⟨$⟩ fin+1 x)) < n | |
| 205 -- a₁ : (toℕ (Inverse.from perm Π.⟨$⟩ fin+1 (fromℕ≤ a))) < n | |
| 50 | 206 piso← : (x : Fin n ) → p→ ( p← x ) ≡ x |
| 51 | 207 piso← x with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 x))) n |
| 52 | 208 piso← x | tri< a ¬b ¬c with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 (fromℕ≤ a)))) n |
| 209 piso← x | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = begin | |
| 210 fromℕ≤ a₁ | |
| 211 ≡⟨ ff sh1 a₁ (toℕ<n x) ⟩ | |
| 212 fromℕ≤ (toℕ<n x) | |
| 213 ≡⟨ fromℕ≤-toℕ _ _ ⟩ | |
| 214 x | |
| 215 ∎ where | |
| 216 open ≡-Reasoning | |
| 217 sh1 : toℕ (Inverse.from perm Π.⟨$⟩ fin+1 (fromℕ≤ a)) ≡ toℕ x | |
| 218 sh1 = begin | |
| 219 toℕ (Inverse.from perm Π.⟨$⟩ fin+1 (fromℕ≤ a)) | |
| 53 | 220 ≡⟨ cong (λ k → toℕ (Inverse.from perm Π.⟨$⟩ k)) (fin+1≤ a ) ⟩ |
| 221 toℕ (Inverse.from perm Π.⟨$⟩ (fromℕ≤ (<-trans a a<sa ) )) | |
| 222 ≡⟨ cong (λ k → toℕ (Inverse.from perm Π.⟨$⟩ k)) (fromℕ≤-toℕ (Inverse.to perm Π.⟨$⟩ (fin+1 x)) (<-trans a a<sa) ) ⟩ | |
| 52 | 223 toℕ (Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ (fin+1 x) )) |
| 53 | 224 ≡⟨ cong (λ k → toℕ k) (inverseˡ perm) ⟩ |
| 52 | 225 toℕ (fin+1 x) |
| 53 | 226 ≡⟨ fin+1-toℕ ⟩ |
| 52 | 227 toℕ x |
| 228 ∎ | |
| 57 | 229 piso← x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( sh3 (fromℕ≤ a) b ) |
| 230 piso← x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( sh5 _ c ) | |
| 54 | 231 piso← x | tri≈ ¬a b ¬c = ⊥-elim ( sh4 x b ) |
| 57 | 232 piso← x | tri> ¬a ¬b c = ⊥-elim ( sh6 x c ) |
| 50 | 233 |
| 234 piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x | |
| 53 | 235 piso→ x with <-cmp (toℕ (perm ⟨$⟩ˡ (fin+1 x))) n |
| 236 piso→ x | tri< a ¬b ¬c with <-cmp (toℕ (perm ⟨$⟩ʳ (fin+1 (fromℕ≤ a)))) n | |
| 237 piso→ x | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = begin | |
| 238 fromℕ≤ a₁ | |
| 239 ≡⟨ ff sh2 a₁ (toℕ<n x) ⟩ | |
| 240 fromℕ≤ (toℕ<n x) | |
| 241 ≡⟨ fromℕ≤-toℕ _ _ ⟩ | |
| 242 x | |
| 243 ∎ where | |
| 244 open ≡-Reasoning | |
| 245 sh2 : toℕ (Inverse.to perm Π.⟨$⟩ fin+1 (fromℕ≤ a)) ≡ toℕ x | |
| 246 sh2 = begin | |
| 247 toℕ (Inverse.to perm Π.⟨$⟩ fin+1 (fromℕ≤ a)) | |
| 248 ≡⟨ cong (λ k → toℕ (Inverse.to perm Π.⟨$⟩ k)) (fin+1≤ a ) ⟩ | |
| 249 toℕ (Inverse.to perm Π.⟨$⟩ (fromℕ≤ (<-trans a a<sa ) )) | |
| 250 ≡⟨ cong (λ k → toℕ (Inverse.to perm Π.⟨$⟩ k)) (fromℕ≤-toℕ (Inverse.from perm Π.⟨$⟩ (fin+1 x)) (<-trans a a<sa) ) ⟩ | |
| 251 toℕ (Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ (fin+1 x) )) | |
| 252 ≡⟨ cong (λ k → toℕ k) (inverseʳ perm) ⟩ | |
| 253 toℕ (fin+1 x) | |
| 254 ≡⟨ fin+1-toℕ ⟩ | |
| 255 toℕ x | |
| 256 ∎ | |
| 57 | 257 piso→ x | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim ( sh4 (fromℕ≤ a) b ) |
| 258 piso→ x | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim ( sh6 _ c ) | |
| 54 | 259 piso→ x | tri≈ ¬a b ¬c = ⊥-elim ( sh3 x b ) |
| 57 | 260 piso→ x | tri> ¬a ¬b c = ⊥-elim ( sh5 x c ) |
| 261 | |
| 262 FL→perm : {n : ℕ } → FL n → Permutation n n | |
| 263 FL→perm f0 = pid | |
| 264 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) | |
| 265 | |
| 266 t1 = plist (shrink (pid {3} ∘ₚ (pins (n≤ 1))) refl) | |
| 58 | 267 t3 = plist (pid {4} ) |
| 268 ∷ plist ( FL→perm ((# 0) :: ((# 0) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) -- (0 ∷ 1 ∷ 2 ∷ []) ∷ | |
| 57 | 269 ∷ plist ( FL→perm ((# 1) :: ((# 0) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) -- (0 ∷ 2 ∷ 1 ∷ []) ∷ |
| 270 ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) -- (1 ∷ 0 ∷ 2 ∷ []) ∷ | |
| 271 ∷ plist ( FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) -- (2 ∷ 0 ∷ 1 ∷ []) ∷ | |
| 272 ∷ plist ( FL→perm ((# 1) :: ((# 2) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) -- (1 ∷ 2 ∷ 0 ∷ []) ∷ | |
| 273 ∷ plist ( FL→perm ((# 1) :: ((# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) -- (2 ∷ 1 ∷ 0 ∷ []) ∷ | |
| 274 ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))))) | |
| 275 ∷ plist ( (flip (FL→perm ((# 1) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 1) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) )) | |
| 276 ∷ [] | |
| 50 | 277 |
| 58 | 278 t4 = FL→perm ((# 1) :: ((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) )) |
| 279 -- t5 = plist t4 ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 3 ) )) | |
| 280 t5 = plist (flip t4) | |
| 281 ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ≤ a<sa) ∷ [] ) | |
| 282 ∷ ( toℕ (t4 ⟨$⟩ʳ fromℕ≤ ( fin<n {_} {(t4 ⟨$⟩ˡ fromℕ≤ a<sa)})) ∷ [] ) | |
| 283 ∷ plist (shrink ( t4 ∘ₚ flip (pins ( n≤ 3 ) ) ) refl ) | |
| 284 ∷ plist ( FL→perm (((# 1) :: ( (# 1) :: (( # 0 ) :: f0 )) ))) | |
| 285 ∷ [] | |
| 286 | |
| 287 | |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
288 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
|
289 perm→FL {zero} perm = f0 |
| 58 | 290 perm→FL {suc n} perm = (perm ⟨$⟩ˡ fromℕ≤ a<sa ) :: perm→FL ( shrink fl1 fl4 ) where |
| 291 fl2 : Fin (suc n) | |
| 292 fl2 = perm ⟨$⟩ʳ fromℕ≤ (fin<n {suc n} {perm ⟨$⟩ˡ fromℕ≤ a<sa} ) | |
| 293 fl3 : toℕ fl2 < n | |
| 294 fl3 = {!!} | |
| 50 | 295 fl1 : Permutation (suc n) (suc n) |
| 58 | 296 fl1 = perm ∘ₚ pinv ( pins fl3 ) |
| 297 fl4 : (fl1 ⟨$⟩ˡ fromℕ n) ≡ fromℕ n | |
| 298 fl4 = {!!} | |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
299 |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
300 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
|
301 FL→iso f0 = refl |
| 58 | 302 FL→iso (x :: fl) = {!!} |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
303 |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
304 open _=p=_ |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
305 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
|
306 FL←iso {0} perm = record { peq = λ () } |
| 58 | 307 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
|
308 |
| 48 | 309 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) ) |
| 310 all-perm n = pls6 n where | |
| 38 | 311 lem1 : {i n : ℕ } → i ≤ n → i < suc n |
| 312 lem1 z≤n = s≤s z≤n | |
| 313 lem1 (s≤s lt) = s≤s (lem1 lt) | |
| 314 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n | |
| 315 lem2 i≤n = ≤-trans i≤n ( refl-≤s ) | |
| 40 | 316 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
| 48 | 317 pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x |
| 318 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 | 319 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
| 320 pls5 n [] x = x | |
| 321 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) | |
| 322 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) | |
| 323 pls6 zero = pid ∷ [] | |
| 48 | 324 pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first |
| 325 | |
| 326 pls : (n : ℕ ) → List (List ℕ ) | |
| 327 pls n = Data.List.map plist (all-perm n) where |