Mercurial > hg > Members > kono > Proof > galois
annotate Putil.agda @ 91:482ef04890f8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 29 Aug 2020 07:48:45 +0900 |
| parents | bb8c5b366219 |
| children | 2e5d0b142eca |
| rev | line source |
|---|---|
| 90 | 1 {-# OPTIONS --allow-unsolved-metas #-} |
| 48 | 2 module Putil where |
| 0 | 3 |
| 4 open import Level hiding ( suc ; zero ) | |
| 5 open import Algebra | |
| 6 open import Algebra.Structures | |
| 37 | 7 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ) |
| 90 | 8 open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ) renaming ( <-cmp to <-fcmp ) |
| 0 | 9 open import Data.Fin.Permutation |
| 10 open import Function hiding (id ; flip) | |
| 11 open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) | |
| 12 open import Function.LeftInverse using ( _LeftInverseOf_ ) | |
| 13 open import Function.Equality using (Π) | |
| 17 | 14 open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) |
| 15 open import Data.Nat.Properties -- using (<-trans) | |
| 16 | 16 open import Relation.Binary.PropositionalEquality |
| 80 | 17 open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev ) |
| 16 | 18 open import nat |
| 0 | 19 |
| 48 | 20 open import Symmetric |
| 0 | 21 |
| 22 | |
| 16 | 23 open import Relation.Nullary |
| 24 open import Data.Empty | |
| 17 | 25 open import Relation.Binary.Core |
| 80 | 26 open import Relation.Binary.Definitions |
| 17 | 27 open import fin |
| 16 | 28 |
| 38 | 29 -- An inductive construction of permutation |
| 34 | 30 |
| 59 | 31 -- Todo |
| 32 -- | |
| 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 | |
| 48 | 38 -- we already have refl and trans in the Symmetric Group |
| 41 | 39 |
| 34 | 40 pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) |
| 41 pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
| 33 | 42 p→ : Fin (suc n) → Fin (suc n) |
| 34 | 43 p→ zero = zero |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
44 p→ (suc x) = suc ( perm ⟨$⟩ʳ x) |
| 33 | 45 |
| 34 | 46 p← : Fin (suc n) → Fin (suc n) |
| 47 p← zero = zero | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
48 p← (suc x) = suc ( perm ⟨$⟩ˡ x) |
| 34 | 49 |
| 50 piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x | |
| 51 piso← zero = refl | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
52 piso← (suc x) = cong (λ k → suc k ) (inverseʳ perm) |
| 33 | 53 |
| 34 | 54 piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x |
| 55 piso→ zero = refl | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
56 piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) |
| 33 | 57 |
| 34 | 58 pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) |
| 59 pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
| 60 p→ : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 61 p→ zero = suc zero | |
| 62 p→ (suc zero) = zero | |
| 62 | 63 p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) |
| 18 | 64 |
| 34 | 65 p← : Fin (suc (suc n)) → Fin (suc (suc n)) |
| 66 p← zero = suc zero | |
| 67 p← (suc zero) = zero | |
| 62 | 68 p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) |
| 34 | 69 |
| 70 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x | |
| 71 piso← zero = refl | |
| 72 piso← (suc zero) = refl | |
| 62 | 73 piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) |
| 16 | 74 |
| 34 | 75 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x |
| 76 piso→ zero = refl | |
| 77 piso→ (suc zero) = refl | |
| 62 | 78 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) |
| 34 | 79 |
| 80 -- enumeration | |
| 81 | |
| 44 | 82 psawpn : {n : ℕ} → 1 < n → Permutation n n |
| 83 psawpn {suc zero} (s≤s ()) | |
| 84 psawpn {suc n} (s≤s (s≤s x)) = pswap pid | |
| 34 | 85 |
| 35 | 86 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n |
| 87 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 | |
| 88 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n | |
| 89 pfill1 0 _ perm = perm | |
| 90 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 | 91 |
| 48 | 92 -- |
| 93 -- psawpim (inseert swap at position m ) | |
| 94 -- | |
| 45 | 95 psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n |
| 96 psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) ) | |
| 97 | |
| 98 n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j | |
| 99 n≤ (zero) {j} = z≤n | |
| 100 n≤ (suc i) {j} = s≤s ( n≤ i ) | |
| 101 | |
| 102 lem0 : {n : ℕ } → n ≤ n | |
| 103 lem0 {zero} = z≤n | |
| 104 lem0 {suc n} = s≤s lem0 | |
| 105 | |
| 106 lem00 : {n m : ℕ } → n ≡ m → n ≤ m | |
| 107 lem00 refl = lem0 | |
| 44 | 108 |
| 80 | 109 plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ |
| 110 plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] | |
| 111 plist1 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 perm i (<-trans lt a<sa) | |
| 112 | |
| 37 | 113 plist : {n : ℕ} → Permutation n n → List ℕ |
| 114 plist {0} perm = [] | |
| 80 | 115 plist {suc n} perm = rev (plist1 perm n a<sa) |
| 116 | |
| 89 | 117 -- pconcat : {n m : ℕ } → Permutation m m → Permutation n n → Permutation (m + n) (m + n) |
| 118 -- pconcat {n} {m} p q = pfill {n + m} {m} ? p ∘ₚ ? | |
| 119 | |
| 120 -- inductivley enmumerate permutations | |
| 121 -- from n-1 length create n length inserting new element at position m | |
| 122 | |
| 123 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] | |
| 124 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] | |
| 125 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] plist ( pins {3} (n≤ 2) ) 2 ∷ 0 ∷ 1 ∷ 3 ∷ [] | |
| 126 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] plist ( pins {3} (n≤ 3) ) 3 ∷ 0 ∷ 1 ∷ 2 ∷ [] | |
| 127 pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) | |
| 128 pins {_} {zero} _ = pid | |
| 129 pins {suc _} {suc zero} _ = pswap pid | |
| 130 pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where | |
| 131 pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) | |
| 132 pins1 _ zero _ = pid | |
| 133 pins1 zero _ _ = pid | |
| 91 | 134 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 a≤sa ) |
| 89 | 135 |
| 90 | 136 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 91 | 137 open ≡-Reasoning |
| 90 | 138 |
| 89 | 139 pins' : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) |
| 140 pins' {_} {zero} _ = pid | |
| 141 pins' {suc n} {suc m} (s≤s m≤n) = permutation p← p→ record { left-inverse-of = piso← ; right-inverse-of = piso→ } where | |
| 142 | |
| 143 next : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 144 next zero = suc zero | |
| 91 | 145 next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) a≤sa ) |
| 89 | 146 |
| 147 p→ : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 148 p→ x with <-cmp (toℕ x) (suc m) | |
| 90 | 149 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) |
| 89 | 150 ... | tri≈ ¬a b ¬c = zero |
| 151 ... | tri> ¬a ¬b c = x | |
| 152 | |
| 153 p← : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 154 p← zero = fromℕ< (s≤s (s≤s m≤n)) | |
| 155 p← (suc x) with <-cmp (toℕ x) (suc m) | |
| 91 | 156 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) |
| 89 | 157 ... | tri≈ ¬a b ¬c = suc x |
| 158 ... | tri> ¬a ¬b c = suc x | |
| 90 | 159 |
| 160 mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m | |
| 161 mm = toℕ-fromℕ< (s≤s (s≤s m≤n)) | |
| 162 | |
| 91 | 163 mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) ) ≤ m |
| 164 mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n a≤sa ) )) x<sm | |
| 89 | 165 |
| 91 | 166 p3 : (x : Fin (suc n) ) → toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) ≡ suc (toℕ x) |
| 167 p3 x = begin | |
| 168 toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) | |
| 169 ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n a≤sa ) ) ⟩ | |
| 170 suc (toℕ x) | |
| 171 ∎ | |
| 89 | 172 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x |
| 90 | 173 piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm |
| 174 ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t ) | |
| 175 ... | tri≈ ¬a b ¬c | t = refl | |
| 176 ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t ) | |
| 177 piso← (suc x) with <-cmp (toℕ x) (suc m) | |
| 91 | 178 ... | tri> ¬a ¬b c with <-cmp (toℕ (suc x)) (suc m) |
| 179 ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-<> a (<-trans c a<sa ) ) | |
| 180 ... | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym b) (<-trans c a<sa )) | |
| 181 ... | tri> ¬a₁ ¬b₁ c₁ = refl | |
| 182 piso← (suc x) | tri≈ ¬a b ¬c with <-cmp (toℕ (suc x)) (suc m) | |
| 183 ... | tri< a ¬b ¬c₁ = ⊥-elim ( nat-≡< b (<-trans a<sa a) ) | |
| 184 ... | tri≈ ¬a₁ refl ¬c₁ = ⊥-elim ( nat-≡< b a<sa ) | |
| 185 ... | tri> ¬a₁ ¬b c = refl | |
| 186 piso← (suc x) | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) )) (suc m) | |
| 90 | 187 ... | tri≈ ¬a b ¬c₁ = ⊥-elim ( ¬a (s≤s (mma x a))) |
| 188 ... | tri> ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a))) | |
| 189 ... | tri< a₁ ¬b₁ ¬c₁ = p0 where | |
| 190 p2 : suc (suc (toℕ x)) ≤ suc (suc n) | |
| 191 p2 = s≤s (fin<n {suc n} {x}) | |
| 91 | 192 p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s a≤sa)))) ≤ suc (suc n) |
| 90 | 193 p6 = s≤s (≤-trans a₁ (s≤s m≤n)) |
| 194 p0 : fromℕ< (≤-trans (s≤s a₁) (s≤s (s≤s m≤n) )) ≡ suc x | |
| 195 p0 = begin | |
| 196 fromℕ< (≤-trans (s≤s a₁) (s≤s (s≤s m≤n) )) | |
| 197 ≡⟨⟩ | |
| 198 fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) | |
| 91 | 199 ≡⟨ lemma10 (p3 x) {p6} {p2} ⟩ |
| 90 | 200 fromℕ< ( s≤s (fin<n {suc n} {x}) ) |
| 91 | 201 ≡⟨⟩ |
| 90 | 202 suc (fromℕ< (fin<n {suc n} {x} )) |
| 91 | 203 ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩ |
| 90 | 204 suc x |
| 91 | 205 ∎ |
| 90 | 206 |
| 89 | 207 |
| 208 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x | |
| 209 piso→ = {!!} | |
| 210 | |
| 211 t7 = plist (pins' {3} (n≤ 3)) ∷ plist (flip ( pins' {3} (n≤ 3) )) ∷ plist ( pins' {3} (n≤ 3) ∘ₚ flip ( pins' {3} (n≤ 3))) ∷ [] | |
| 212 t8 = {!!} | |
| 213 | |
| 214 | |
| 80 | 215 plist2 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ |
| 216 plist2 {n} perm zero _ = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ [] | |
| 217 plist2 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ʳ (fromℕ< (s≤s lt))) ∷ plist2 perm i (<-trans lt a<sa) | |
| 218 | |
| 219 plist0 : {n : ℕ} → Permutation n n → List ℕ | |
| 220 plist0 {0} perm = [] | |
| 221 plist0 {suc n} perm = plist2 perm n a<sa | |
| 222 | |
| 85 | 223 open _=p=_ |
| 224 | |
|
86
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
225 -- |
|
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
226 -- plist cong |
|
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
227 -- |
| 85 | 228 ←pleq : {n : ℕ} → (x y : Permutation n n ) → x =p= y → plist0 x ≡ plist0 y |
| 229 ←pleq {zero} x y eq = refl | |
| 230 ←pleq {suc n} x y eq = ←pleq1 n a<sa where | |
| 231 ←pleq1 : (i : ℕ ) → (i<sn : i < suc n ) → plist2 x i i<sn ≡ plist2 y i i<sn | |
| 232 ←pleq1 zero _ = cong ( λ k → toℕ k ∷ [] ) ( peq eq (fromℕ< {zero} (s≤s z≤n))) | |
| 233 ←pleq1 (suc i) (s≤s lt) = cong₂ ( λ j k → toℕ j ∷ k ) ( peq eq (fromℕ< (s≤s lt))) ( ←pleq1 i (<-trans lt a<sa) ) | |
| 80 | 234 |
| 235 headeq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → x ≡ y | |
| 236 headeq refl = refl | |
| 237 | |
| 238 taileq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → xt ≡ yt | |
| 239 taileq refl = refl | |
| 240 | |
|
86
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
241 -- |
|
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
242 -- plist equalizer |
|
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
243 -- |
| 80 | 244 pleq : {n : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y |
| 245 pleq {0} x y refl = record { peq = λ q → pleq0 q } where | |
| 246 pleq0 : (q : Fin 0 ) → (x ⟨$⟩ʳ q) ≡ (y ⟨$⟩ʳ q) | |
| 247 pleq0 () | |
| 248 pleq {suc n} x y eq = record { peq = λ q → pleq1 n a<sa eq q fin<n } where | |
| 249 pleq1 : (i : ℕ ) → (i<sn : i < suc n ) → plist2 x i i<sn ≡ plist2 y i i<sn → (q : Fin (suc n)) → toℕ q < suc i → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q | |
| 81 | 250 pleq1 zero i<sn eq q q<i with <-cmp (toℕ q) zero |
| 251 ... | tri< () ¬b ¬c | |
| 252 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i ) | |
| 253 ... | tri≈ ¬a b ¬c = begin | |
| 254 x ⟨$⟩ʳ q | |
| 255 ≡⟨ cong ( λ k → x ⟨$⟩ʳ k ) (toℕ-injective b )⟩ | |
| 256 x ⟨$⟩ʳ zero | |
| 257 ≡⟨ toℕ-injective (headeq eq) ⟩ | |
| 258 y ⟨$⟩ʳ zero | |
| 259 ≡⟨ cong ( λ k → y ⟨$⟩ʳ k ) (sym (toℕ-injective b )) ⟩ | |
| 260 y ⟨$⟩ʳ q | |
| 91 | 261 ∎ |
| 80 | 262 pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i) |
| 263 ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a | |
| 81 | 264 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i ) |
| 80 | 265 ... | tri≈ ¬a b ¬c = begin |
| 266 x ⟨$⟩ʳ q | |
| 267 ≡⟨ cong (λ k → x ⟨$⟩ʳ k) (pleq3 b) ⟩ | |
| 268 x ⟨$⟩ʳ (suc (fromℕ< i<sn)) | |
| 269 ≡⟨ toℕ-injective pleq2 ⟩ | |
| 270 y ⟨$⟩ʳ (suc (fromℕ< i<sn)) | |
| 271 ≡⟨ cong (λ k → y ⟨$⟩ʳ k) (sym (pleq3 b)) ⟩ | |
| 272 y ⟨$⟩ʳ q | |
| 273 ∎ where | |
| 274 pleq3 : toℕ q ≡ suc i → q ≡ suc (fromℕ< i<sn) | |
| 275 pleq3 tq=si = toℕ-injective ( begin | |
| 276 toℕ q | |
| 277 ≡⟨ b ⟩ | |
| 278 suc i | |
| 279 ≡⟨ sym (toℕ-fromℕ< (s≤s i<sn)) ⟩ | |
| 280 toℕ (fromℕ< (s≤s i<sn)) | |
| 281 ≡⟨⟩ | |
| 282 toℕ (suc (fromℕ< i<sn)) | |
| 91 | 283 ∎ ) |
| 80 | 284 pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) |
| 285 pleq2 = headeq eq | |
| 37 | 286 |
| 87 | 287 pprep-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y |
| 288 pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where | |
| 289 pprep-cong1 : (q : Fin (suc n)) → (pprep x ⟨$⟩ʳ q) ≡ (pprep y ⟨$⟩ʳ q) | |
| 290 pprep-cong1 zero = refl | |
| 291 pprep-cong1 (suc q) = begin | |
| 292 pprep x ⟨$⟩ʳ suc q | |
| 293 ≡⟨⟩ | |
| 294 suc ( x ⟨$⟩ʳ q ) | |
| 295 ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩ | |
| 296 suc ( y ⟨$⟩ʳ q ) | |
| 297 ≡⟨⟩ | |
| 298 pprep y ⟨$⟩ʳ suc q | |
| 91 | 299 ∎ |
| 87 | 300 |
| 301 pprep-dist : {n : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y) | |
| 302 pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where | |
| 303 pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q) | |
| 304 pprep-dist1 zero = refl | |
| 305 pprep-dist1 (suc q) = cong ( λ k → suc k ) refl | |
| 306 | |
| 307 pswap-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pswap x =p= pswap y | |
| 308 pswap-cong {n} {x} {y} x=y = record { peq = pswap-cong1 } where | |
| 309 pswap-cong1 : (q : Fin (suc (suc n))) → (pswap x ⟨$⟩ʳ q) ≡ (pswap y ⟨$⟩ʳ q) | |
| 310 pswap-cong1 zero = refl | |
| 311 pswap-cong1 (suc zero) = refl | |
| 312 pswap-cong1 (suc (suc q)) = begin | |
| 313 pswap x ⟨$⟩ʳ suc (suc q) | |
| 314 ≡⟨⟩ | |
| 315 suc (suc (x ⟨$⟩ʳ q)) | |
| 316 ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩ | |
| 317 suc (suc (y ⟨$⟩ʳ q)) | |
| 318 ≡⟨⟩ | |
| 319 pswap y ⟨$⟩ʳ suc (suc q) | |
| 91 | 320 ∎ |
| 87 | 321 |
| 322 pswap-dist : {n : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y) | |
| 323 pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where | |
| 324 pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q) | |
| 325 pswap-dist1 zero = refl | |
| 326 pswap-dist1 (suc zero) = refl | |
| 327 pswap-dist1 (suc (suc q)) = cong ( λ k → suc (suc k) ) refl | |
|
86
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
328 |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
329 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
|
330 f0 : FL 0 |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
331 _::_ : { 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
|
332 |
| 50 | 333 open import logic |
| 334 | |
| 88 | 335 shlem→ : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) → perm ⟨$⟩ˡ x ≡ zero → x ≡ zero |
| 336 shlem→ perm p0=0 x px=0 = begin | |
| 61 | 337 x ≡⟨ sym ( inverseʳ perm ) ⟩ |
| 338 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x) ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) px=0 ⟩ | |
| 339 perm ⟨$⟩ʳ zero ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) (sym p0=0) ⟩ | |
| 340 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero) ≡⟨ inverseʳ perm ⟩ | |
| 341 zero | |
| 342 ∎ where open ≡-Reasoning | |
| 54 | 343 |
| 88 | 344 shlem← : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero |
| 345 shlem← perm p0=0 x px=0 = begin | |
| 61 | 346 x ≡⟨ sym (inverseˡ perm ) ⟩ |
| 347 perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x ) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) px=0 ⟩ | |
| 348 perm ⟨$⟩ˡ zero ≡⟨ p0=0 ⟩ | |
| 349 zero | |
| 350 ∎ where open ≡-Reasoning | |
| 54 | 351 |
| 88 | 352 sh2 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero |
| 353 sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq | |
| 354 sh2 perm p0=0 {x} eq | () | |
| 355 | |
| 356 sh1 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero | |
| 357 sh1 perm p0=0 {x} eq with shlem← perm p0=0 (suc x) eq | |
| 358 sh1 perm p0=0 {x} eq | () | |
| 359 | |
| 360 | |
| 361 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] | |
| 362 shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n | |
| 363 shrink {n} perm p0=0 = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
| 57 | 364 |
| 61 | 365 p→ : Fin n → Fin n |
| 88 | 366 p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) |
| 367 p→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) | |
| 61 | 368 p→ x | suc t | _ = t |
| 50 | 369 |
| 370 p← : Fin n → Fin n | |
| 88 | 371 p← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) |
| 372 p← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) | |
| 61 | 373 p← x | suc t | _ = t |
| 50 | 374 |
| 375 piso← : (x : Fin n ) → p→ ( p← x ) ≡ x | |
| 88 | 376 piso← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) |
| 377 piso← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) | |
| 378 piso← x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t) | |
| 379 piso← x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 e ) | |
| 61 | 380 piso← x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin |
| 381 t1 | |
| 382 ≡⟨ plem0 plem1 ⟩ | |
| 52 | 383 x |
| 61 | 384 ∎ where |
| 385 open ≡-Reasoning | |
| 386 plem0 : suc t1 ≡ suc x → t1 ≡ x | |
| 387 plem0 refl = refl | |
| 388 plem1 : suc t1 ≡ suc x | |
| 389 plem1 = begin | |
| 390 suc t1 | |
| 391 ≡⟨ sym e1 ⟩ | |
| 88 | 392 Inverse.to perm Π.⟨$⟩ suc t |
| 393 ≡⟨ cong (λ k → Inverse.to perm Π.⟨$⟩ k ) (sym e0) ⟩ | |
| 394 Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x ) | |
| 395 ≡⟨ inverseʳ perm ⟩ | |
| 61 | 396 suc x |
| 397 ∎ | |
| 50 | 398 |
| 399 piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x | |
| 88 | 400 piso→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) |
| 401 piso→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) | |
| 402 piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) | |
| 403 piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 e ) | |
| 61 | 404 piso→ x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin |
| 405 t1 | |
| 406 ≡⟨ plem2 plem3 ⟩ | |
| 53 | 407 x |
| 61 | 408 ∎ where |
| 409 open ≡-Reasoning | |
| 410 plem2 : suc t1 ≡ suc x → t1 ≡ x | |
| 411 plem2 refl = refl | |
| 412 plem3 : suc t1 ≡ suc x | |
| 413 plem3 = begin | |
| 414 suc t1 | |
| 415 ≡⟨ sym e1 ⟩ | |
| 88 | 416 Inverse.from perm Π.⟨$⟩ suc t |
| 417 ≡⟨ cong (λ k → Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩ | |
| 418 Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x ) | |
| 419 ≡⟨ inverseˡ perm ⟩ | |
| 61 | 420 suc x |
| 421 ∎ | |
| 57 | 422 |
| 88 | 423 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm |
| 424 shrink-iso {n} {perm} = record { peq = λ q → refl } | |
| 425 | |
| 57 | 426 FL→perm : {n : ℕ } → FL n → Permutation n n |
| 427 FL→perm f0 = pid | |
| 428 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) | |
| 429 | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
430 t40 = (# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
431 t4 = FL→perm ((# 2) :: t40 ) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
432 |
| 61 | 433 -- 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
|
434 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
|
435 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
|
436 -- ∷ 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
|
437 -- ∷ 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
|
438 -- ∷ 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
|
439 -- ∷ 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
|
440 ∷ 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
|
441 ∷ 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
|
442 ∷ 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
|
443 ∷ 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
|
444 -- ∷ 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
|
445 -- ∷ 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
|
446 -- ∷ 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
|
447 -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) )) |
| 57 | 448 ∷ [] |
| 50 | 449 |
| 58 | 450 |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
451 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
|
452 perm→FL {zero} perm = f0 |
| 89 | 453 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) |
| 454 -- 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
|
455 |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
456 -- 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
|
457 t5 = plist (t4) ∷ plist (flip t4) |
| 74 | 458 ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ< a<sa) ∷ [] ) |
| 61 | 459 ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] ) |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
460 -- ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 1 ) )) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
461 ∷ plist (remove (# 0) t4 ) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
462 ∷ plist ( FL→perm t40 ) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
463 ∷ [] |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
464 |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
465 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
|
466 |
| 63 | 467 postulate |
| 468 FL→iso : {n : ℕ } → (fl : FL n ) → perm→FL ( FL→perm fl ) ≡ fl | |
| 469 -- FL→iso f0 = refl | |
| 470 -- FL→iso (x :: fl) = {!!} -- with FL→iso fl | |
| 61 | 471 -- ... | t = {!!} |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
472 |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
473 open _=p=_ |
| 63 | 474 postulate |
| 475 FL←iso : {n : ℕ } → (perm : Permutation n n ) → FL→perm ( perm→FL perm ) =p= perm | |
| 476 -- FL←iso {0} perm = record { peq = λ () } | |
| 477 -- 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
|
478 |
| 66 | 479 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n |
| 91 | 480 lem2 i≤n = ≤-trans i≤n ( a≤sa ) |
| 66 | 481 |
|
67
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
482 ∀-FL : (n : ℕ ) → List (FL (suc n)) |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
483 ∀-FL x = fls6 x where |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
484 fls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → FL n → List (FL (suc n)) → List (FL (suc n)) |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
485 fls4 zero n i≤n perm x = (zero :: perm ) ∷ x |
| 91 | 486 fls4 (suc i) n i≤n perm x = fls4 i n (≤-trans a≤sa i≤n ) perm ((fromℕ< (s≤s i≤n) :: perm ) ∷ x) |
|
67
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
487 fls5 : ( n : ℕ ) → List (FL n) → List (FL (suc n)) → List (FL (suc n)) |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
488 fls5 n [] x = x |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
489 fls5 n (h ∷ x) y = fls5 n x (fls4 n n lem0 h y) |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
490 fls6 : ( n : ℕ ) → List (FL (suc n)) |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
491 fls6 zero = (zero :: f0) ∷ [] |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
492 fls6 (suc n) = fls5 (suc n) (fls6 n) [] |
| 65 | 493 |
| 48 | 494 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) ) |
| 495 all-perm n = pls6 n where | |
| 38 | 496 lem1 : {i n : ℕ } → i ≤ n → i < suc n |
| 497 lem1 z≤n = s≤s z≤n | |
| 498 lem1 (s≤s lt) = s≤s (lem1 lt) | |
| 40 | 499 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
| 48 | 500 pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x |
| 91 | 501 pls4 (suc i) n i≤n perm x = pls4 i n (≤-trans a≤sa i≤n ) perm (pprep perm ∘ₚ pins {n} {suc i} i≤n ∷ x) |
| 40 | 502 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
| 503 pls5 n [] x = x | |
| 504 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) | |
| 505 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) | |
| 506 pls6 zero = pid ∷ [] | |
| 48 | 507 pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first |
| 508 | |
| 509 pls : (n : ℕ ) → List (List ℕ ) | |
| 75 | 510 pls n = Data.List.map plist (all-perm n) |