Mercurial > hg > Members > kono > Proof > galois
annotate Putil.agda @ 135:4e2d272b4bcc
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Tue, 08 Sep 2020 12:29:58 +0900 |
| parents | d6ae92b8b5bc |
| children | d880595eae30 |
| 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 | |
| 112 | 7 open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) |
| 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 |
| 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 |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
35 p→ (suc x) = suc ( perm ⟨$⟩ʳ x) |
| 33 | 36 |
| 34 | 37 p← : Fin (suc n) → Fin (suc n) |
| 38 p← zero = zero | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
39 p← (suc x) = suc ( perm ⟨$⟩ˡ x) |
| 34 | 40 |
| 41 piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x | |
| 42 piso← zero = refl | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
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 | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
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 | |
| 62 | 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 | |
| 62 | 59 p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) |
| 34 | 60 |
| 61 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x | |
| 62 piso← zero = refl | |
| 63 piso← (suc zero) = refl | |
| 62 | 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 | |
| 62 | 69 piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) |
| 34 | 70 |
| 44 | 71 psawpn : {n : ℕ} → 1 < n → Permutation n n |
| 72 psawpn {suc zero} (s≤s ()) | |
| 73 psawpn {suc n} (s≤s (s≤s x)) = pswap pid | |
| 34 | 74 |
| 35 | 75 pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n |
| 76 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 | |
| 77 pfill1 : (i : ℕ ) → i ≤ n → Permutation (n - i) (n - i) → Permutation n n | |
| 78 pfill1 0 _ perm = perm | |
| 79 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 | 80 |
| 48 | 81 -- |
| 82 -- psawpim (inseert swap at position m ) | |
| 83 -- | |
| 45 | 84 psawpim : {n m : ℕ} → suc (suc m) ≤ n → Permutation n n |
| 85 psawpim {n} {m} m≤n = pfill m≤n ( psawpn (s≤s (s≤s z≤n)) ) | |
| 86 | |
| 87 n≤ : (i : ℕ ) → {j : ℕ } → i ≤ i + j | |
| 88 n≤ (zero) {j} = z≤n | |
| 89 n≤ (suc i) {j} = s≤s ( n≤ i ) | |
| 90 | |
| 91 lem0 : {n : ℕ } → n ≤ n | |
| 92 lem0 {zero} = z≤n | |
| 93 lem0 {suc n} = s≤s lem0 | |
| 94 | |
| 95 lem00 : {n m : ℕ } → n ≡ m → n ≤ m | |
| 96 lem00 refl = lem0 | |
| 44 | 97 |
| 80 | 98 plist1 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ |
| 99 plist1 {n} perm zero _ = toℕ ( perm ⟨$⟩ˡ (fromℕ< {zero} (s≤s z≤n))) ∷ [] | |
| 100 plist1 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ˡ (fromℕ< (s≤s lt))) ∷ plist1 perm i (<-trans lt a<sa) | |
| 101 | |
| 37 | 102 plist : {n : ℕ} → Permutation n n → List ℕ |
| 103 plist {0} perm = [] | |
| 80 | 104 plist {suc n} perm = rev (plist1 perm n a<sa) |
| 105 | |
| 129 | 106 -- |
| 89 | 107 -- from n-1 length create n length inserting new element at position m |
| 129 | 108 -- |
| 89 | 109 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] |
| 110 -- 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] plist ( pins {3} (n≤ 1) ) 1 ∷ 0 ∷ 2 ∷ 3 ∷ [] | |
| 111 -- 1 ∷ 2 ∷ 0 ∷ 3 ∷ [] plist ( pins {3} (n≤ 2) ) 2 ∷ 0 ∷ 1 ∷ 3 ∷ [] | |
| 112 -- 1 ∷ 2 ∷ 3 ∷ 0 ∷ [] plist ( pins {3} (n≤ 3) ) 3 ∷ 0 ∷ 1 ∷ 2 ∷ [] | |
| 129 | 113 -- |
| 114 -- defined by pprep and pswap | |
| 115 -- | |
| 94 | 116 -- pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) |
| 117 -- pins {_} {zero} _ = pid | |
| 118 -- pins {suc _} {suc zero} _ = pswap pid | |
| 119 -- pins {suc (suc n)} {suc m} (s≤s m<n) = pins1 (suc m) (suc (suc n)) lem0 where | |
| 120 -- pins1 : (i j : ℕ ) → j ≤ suc (suc n) → Permutation (suc (suc (suc n ))) (suc (suc (suc n))) | |
| 121 -- pins1 _ zero _ = pid | |
| 122 -- pins1 zero _ _ = pid | |
| 123 -- 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 | 124 |
| 90 | 125 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) |
| 91 | 126 open ≡-Reasoning |
| 90 | 127 |
| 94 | 128 pins : {n m : ℕ} → m ≤ n → Permutation (suc n) (suc n) |
| 129 pins {_} {zero} _ = pid | |
| 130 pins {suc n} {suc m} (s≤s m≤n) = permutation p← p→ record { left-inverse-of = piso← ; right-inverse-of = piso→ } where | |
| 89 | 131 |
| 132 next : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 133 next zero = suc zero | |
| 91 | 134 next (suc x) = fromℕ< (≤-trans (fin<n {_} {x} ) a≤sa ) |
| 89 | 135 |
| 136 p→ : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 137 p→ x with <-cmp (toℕ x) (suc m) | |
| 90 | 138 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) |
| 89 | 139 ... | tri≈ ¬a b ¬c = zero |
| 140 ... | tri> ¬a ¬b c = x | |
| 141 | |
| 142 p← : Fin (suc (suc n)) → Fin (suc (suc n)) | |
| 143 p← zero = fromℕ< (s≤s (s≤s m≤n)) | |
| 144 p← (suc x) with <-cmp (toℕ x) (suc m) | |
| 91 | 145 ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) |
| 89 | 146 ... | tri≈ ¬a b ¬c = suc x |
| 147 ... | tri> ¬a ¬b c = suc x | |
| 90 | 148 |
| 149 mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m | |
| 150 mm = toℕ-fromℕ< (s≤s (s≤s m≤n)) | |
| 151 | |
| 91 | 152 mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) ) ≤ m |
| 153 mma x (s≤s x<sm) = subst (λ k → k ≤ m) (sym (toℕ-fromℕ< (≤-trans fin<n a≤sa ) )) x<sm | |
| 89 | 154 |
| 91 | 155 p3 : (x : Fin (suc n) ) → toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) ≡ suc (toℕ x) |
| 156 p3 x = begin | |
| 157 toℕ (fromℕ< (≤-trans (fin<n {_} {suc x} ) (s≤s a≤sa))) | |
| 158 ≡⟨ toℕ-fromℕ< ( s≤s ( ≤-trans fin<n a≤sa ) ) ⟩ | |
| 159 suc (toℕ x) | |
| 160 ∎ | |
| 92 | 161 |
| 162 piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x | |
| 163 piso→ zero with <-cmp (toℕ (fromℕ< (≤-trans (s≤s z≤n) (s≤s (s≤s m≤n) )))) (suc m) | |
| 164 ... | tri< a ¬b ¬c = refl | |
| 165 piso→ (suc x) with <-cmp (toℕ (suc x)) (suc m) | |
| 94 | 166 ... | tri≈ ¬a refl ¬c = p13 where |
| 167 p13 : fromℕ< (s≤s (s≤s m≤n)) ≡ suc x | |
| 168 p13 = cong (λ k → suc k ) (fromℕ<-toℕ _ (s≤s m≤n) ) | |
| 95 | 169 ... | tri> ¬a ¬b c = p16 (suc x) refl where |
| 170 p16 : (y : Fin (suc (suc n))) → y ≡ suc x → p← y ≡ suc x | |
| 171 p16 zero eq = ⊥-elim ( nat-≡< (cong (λ k → suc (toℕ k) ) eq) (s≤s (s≤s (z≤n)))) | |
| 172 p16 (suc y) eq with <-cmp (toℕ y) (suc m) -- suc (suc m) < toℕ (suc x) | |
| 96 | 173 ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< refl ( ≤-trans c (subst (λ k → k < suc m) p17 a )) ) where |
| 174 -- x = suc m case, c : suc (suc m) ≤ suc (toℕ x), a : suc (toℕ y) ≤ suc m, suc y ≡ suc x | |
| 175 p17 : toℕ y ≡ toℕ x | |
| 176 p17 with <-cmp (toℕ y) (toℕ x) | cong toℕ eq | |
| 177 ... | tri< a ¬b ¬c | seq = ⊥-elim ( nat-≡< seq (s≤s a) ) | |
| 178 ... | tri≈ ¬a b ¬c | seq = b | |
| 179 ... | tri> ¬a ¬b c | seq = ⊥-elim ( nat-≡< (sym seq) (s≤s c)) | |
| 95 | 180 ... | tri≈ ¬a b ¬c = eq |
| 181 ... | tri> ¬a ¬b c₁ = eq | |
| 92 | 182 ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) ))) refl where |
| 183 p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) → p← y ≡ suc x | |
| 184 p10 zero () | |
| 93 | 185 p10 (suc y) eq = p15 where |
| 186 p12 : toℕ y ≡ suc (toℕ x) | |
| 187 p12 = begin | |
| 188 toℕ y | |
| 189 ≡⟨ cong (λ k → Data.Nat.pred (toℕ k)) eq ⟩ | |
| 190 toℕ (fromℕ< (≤-trans a (s≤s m≤n))) | |
| 191 ≡⟨ toℕ-fromℕ< {suc (toℕ x)} {suc n} (≤-trans a (s≤s m≤n)) ⟩ | |
| 192 suc (toℕ x) | |
| 92 | 193 ∎ |
| 93 | 194 p15 : p← (suc y) ≡ suc x |
| 195 p15 with <-cmp (toℕ y) (suc m) -- eq : suc y ≡ suc (suc (fromℕ< (≤-pred (≤-trans a (s≤s m≤n))))) , a : suc x < suc m | |
| 196 ... | tri< a₁ ¬b ¬c = p11 where | |
| 197 p11 : fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) ≡ suc x | |
| 198 p11 = begin | |
| 199 fromℕ< (≤-trans (fin<n {_} {y}) a≤sa ) | |
| 200 ≡⟨ fromℕ<-irrelevant _ _ p12 _ (s≤s (fin<n {suc n})) ⟩ | |
| 201 suc (fromℕ< (fin<n {suc n} {x} )) | |
| 202 ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩ | |
| 203 suc x | |
| 204 ∎ | |
| 205 ... | tri≈ ¬a b ¬c = ⊥-elim ( nat-≡< b (subst (λ k → k < suc m) (sym p12) a )) -- suc x < suc m -> y = suc x → toℕ y < suc m | |
| 206 ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (subst (λ k → k < suc m) (sym p12) a )) | |
| 92 | 207 |
| 89 | 208 piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x |
| 90 | 209 piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm |
| 210 ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t ) | |
| 211 ... | tri≈ ¬a b ¬c | t = refl | |
| 212 ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t ) | |
| 213 piso← (suc x) with <-cmp (toℕ x) (suc m) | |
| 91 | 214 ... | tri> ¬a ¬b c with <-cmp (toℕ (suc x)) (suc m) |
| 215 ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-<> a (<-trans c a<sa ) ) | |
| 216 ... | tri≈ ¬a₁ b ¬c = ⊥-elim ( nat-≡< (sym b) (<-trans c a<sa )) | |
| 217 ... | tri> ¬a₁ ¬b₁ c₁ = refl | |
| 218 piso← (suc x) | tri≈ ¬a b ¬c with <-cmp (toℕ (suc x)) (suc m) | |
| 219 ... | tri< a ¬b ¬c₁ = ⊥-elim ( nat-≡< b (<-trans a<sa a) ) | |
| 220 ... | tri≈ ¬a₁ refl ¬c₁ = ⊥-elim ( nat-≡< b a<sa ) | |
| 221 ... | tri> ¬a₁ ¬b c = refl | |
| 222 piso← (suc x) | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin<n {_} {x}) a≤sa ) )) (suc m) | |
| 90 | 223 ... | tri≈ ¬a b ¬c₁ = ⊥-elim ( ¬a (s≤s (mma x a))) |
| 224 ... | tri> ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a))) | |
| 225 ... | tri< a₁ ¬b₁ ¬c₁ = p0 where | |
| 226 p2 : suc (suc (toℕ x)) ≤ suc (suc n) | |
| 227 p2 = s≤s (fin<n {suc n} {x}) | |
| 91 | 228 p6 : suc (toℕ (fromℕ< (≤-trans (fin<n {_} {suc x}) (s≤s a≤sa)))) ≤ suc (suc n) |
| 90 | 229 p6 = s≤s (≤-trans a₁ (s≤s m≤n)) |
| 230 p0 : fromℕ< (≤-trans (s≤s a₁) (s≤s (s≤s m≤n) )) ≡ suc x | |
| 231 p0 = begin | |
| 232 fromℕ< (≤-trans (s≤s a₁) (s≤s (s≤s m≤n) )) | |
| 233 ≡⟨⟩ | |
| 234 fromℕ< (s≤s (≤-trans a₁ (s≤s m≤n))) | |
| 91 | 235 ≡⟨ lemma10 (p3 x) {p6} {p2} ⟩ |
| 90 | 236 fromℕ< ( s≤s (fin<n {suc n} {x}) ) |
| 91 | 237 ≡⟨⟩ |
| 90 | 238 suc (fromℕ< (fin<n {suc n} {x} )) |
| 91 | 239 ≡⟨ cong suc (fromℕ<-toℕ x _ ) ⟩ |
| 90 | 240 suc x |
| 91 | 241 ∎ |
| 90 | 242 |
| 94 | 243 t7 = plist (pins {3} (n≤ 3)) ∷ plist (flip ( pins {3} (n≤ 3) )) ∷ plist ( pins {3} (n≤ 3) ∘ₚ flip ( pins {3} (n≤ 3))) ∷ [] |
| 244 -- t8 = {!!} | |
| 89 | 245 |
| 97 | 246 open import logic |
| 247 | |
| 248 open _∧_ | |
| 249 | |
| 250 perm1 : {perm : Permutation 1 1 } {q : Fin 1} → (perm ⟨$⟩ʳ q ≡ # 0) ∧ ((perm ⟨$⟩ˡ q ≡ # 0)) | |
| 251 perm1 {p} {q} = ⟪ perm01 _ _ , perm00 _ _ ⟫ where | |
| 252 perm01 : (x y : Fin 1) → (p ⟨$⟩ʳ x) ≡ y | |
| 253 perm01 x y with p ⟨$⟩ʳ x | |
| 254 perm01 zero zero | zero = refl | |
| 255 perm00 : (x y : Fin 1) → (p ⟨$⟩ˡ x) ≡ y | |
| 256 perm00 x y with p ⟨$⟩ˡ x | |
| 257 perm00 zero zero | zero = refl | |
| 258 | |
| 259 | |
| 129 | 260 ---- |
| 261 -- find insertion point of pins | |
| 262 ---- | |
| 97 | 263 p=0 : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) ≡ # 0 |
| 264 p=0 {zero} perm with ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) | |
| 265 ... | zero = refl | |
| 266 p=0 {suc n} perm with perm ⟨$⟩ʳ (# 0) | inspect (_⟨$⟩ʳ_ perm ) (# 0)| toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) | inspect toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) | |
| 267 ... | zero | record { eq = e} | m<n | _ = p001 where | |
| 268 p001 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero | |
| 269 p001 = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) e (inverseˡ perm) | |
| 270 ... | suc t | record { eq = e } | m<n | record { eq = e1 } = p002 where -- m<n : suc (toℕ t) ≤ suc n | |
| 271 p002 : perm ⟨$⟩ˡ ( pins m<n ⟨$⟩ʳ zero) ≡ zero | |
| 272 p002 = p005 zero (toℕ t) refl m<n refl where -- suc (toℕ t) ≤ suc n | |
| 273 p003 : (s : Fin (suc (suc n))) → s ≡ (perm ⟨$⟩ʳ (# 0)) → perm ⟨$⟩ˡ s ≡ # 0 | |
| 274 p003 s eq = subst (λ k → perm ⟨$⟩ˡ k ≡ zero ) (sym eq) (inverseˡ perm) | |
| 275 p005 : (x : Fin (suc (suc n))) → (m : ℕ ) → x ≡ zero → (m≤n : suc m ≤ suc n ) → m ≡ toℕ t → perm ⟨$⟩ˡ ( pins m≤n ⟨$⟩ʳ zero) ≡ zero | |
| 276 p005 zero m eq (s≤s m≤n) meq = p004 where | |
| 277 p004 : perm ⟨$⟩ˡ (fromℕ< (s≤s (s≤s m≤n))) ≡ zero | |
| 278 p004 = p003 (fromℕ< (s≤s (s≤s m≤n))) ( | |
| 279 begin | |
| 280 fromℕ< (s≤s (s≤s m≤n)) | |
| 281 ≡⟨ fromℕ<-irrelevant _ _ (cong suc meq) (s≤s (s≤s m≤n)) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩ | |
| 282 fromℕ< (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) | |
| 283 ≡⟨ fromℕ<-toℕ {suc (suc n)} (suc t) (subst (λ k → suc k < suc (suc n)) meq (s≤s (s≤s m≤n)) ) ⟩ | |
| 284 suc t | |
| 285 ≡⟨ sym e ⟩ | |
| 286 (perm ⟨$⟩ʳ (# 0)) | |
| 287 ∎ ) | |
| 288 | |
| 129 | 289 ---- |
| 290 -- other elements are preserved in pins | |
| 291 ---- | |
| 101 | 292 px=x : {n : ℕ } → (x : Fin (suc n)) → pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) ≡ x |
| 293 px=x {n} zero = refl | |
| 103 | 294 px=x {suc n} (suc x) = p001 where |
| 295 p002 : fromℕ< (s≤s (toℕ≤pred[n] x)) ≡ x | |
| 296 p002 = fromℕ<-toℕ x (s≤s (toℕ≤pred[n] x)) | |
| 297 p001 : (pins (toℕ≤pred[n] (suc x)) ⟨$⟩ʳ (# 0)) ≡ suc x | |
| 298 p001 with <-cmp 0 ((toℕ x)) | |
| 299 ... | tri< a ¬b ¬c = cong suc p002 | |
| 300 ... | tri≈ ¬a b ¬c = cong suc p002 | |
| 97 | 301 |
| 302 -- pp : {n : ℕ } → (perm : Permutation (suc n) (suc n) ) → Fin (suc n) | |
| 303 -- pp perm → (( perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ˡ (# 0)) | |
| 304 | |
| 80 | 305 plist2 : {n : ℕ} → Permutation (suc n) (suc n) → (i : ℕ ) → i < suc n → List ℕ |
| 306 plist2 {n} perm zero _ = toℕ ( perm ⟨$⟩ʳ (fromℕ< {zero} (s≤s z≤n))) ∷ [] | |
| 307 plist2 {n} perm (suc i) (s≤s lt) = toℕ ( perm ⟨$⟩ʳ (fromℕ< (s≤s lt))) ∷ plist2 perm i (<-trans lt a<sa) | |
| 308 | |
| 309 plist0 : {n : ℕ} → Permutation n n → List ℕ | |
| 310 plist0 {0} perm = [] | |
| 311 plist0 {suc n} perm = plist2 perm n a<sa | |
| 312 | |
| 85 | 313 open _=p=_ |
| 314 | |
|
86
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
315 -- |
|
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
316 -- plist cong |
|
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
317 -- |
| 85 | 318 ←pleq : {n : ℕ} → (x y : Permutation n n ) → x =p= y → plist0 x ≡ plist0 y |
| 319 ←pleq {zero} x y eq = refl | |
| 320 ←pleq {suc n} x y eq = ←pleq1 n a<sa where | |
| 321 ←pleq1 : (i : ℕ ) → (i<sn : i < suc n ) → plist2 x i i<sn ≡ plist2 y i i<sn | |
| 322 ←pleq1 zero _ = cong ( λ k → toℕ k ∷ [] ) ( peq eq (fromℕ< {zero} (s≤s z≤n))) | |
| 323 ←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 | 324 |
| 325 headeq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → x ≡ y | |
| 326 headeq refl = refl | |
| 327 | |
| 328 taileq : {A : Set } → {x y : A } → {xt yt : List A } → (x ∷ xt) ≡ (y ∷ yt) → xt ≡ yt | |
| 329 taileq refl = refl | |
| 330 | |
|
86
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
331 -- |
| 129 | 332 -- plist injection / equalizer |
| 333 -- | |
| 334 -- if plist0 of two perm looks the same, the permutations are the same | |
|
86
c5329963c583
(x : Permutation 1 1 ) → x =p= pid
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
85
diff
changeset
|
335 -- |
| 80 | 336 pleq : {n : ℕ} → (x y : Permutation n n ) → plist0 x ≡ plist0 y → x =p= y |
| 337 pleq {0} x y refl = record { peq = λ q → pleq0 q } where | |
| 338 pleq0 : (q : Fin 0 ) → (x ⟨$⟩ʳ q) ≡ (y ⟨$⟩ʳ q) | |
| 339 pleq0 () | |
| 340 pleq {suc n} x y eq = record { peq = λ q → pleq1 n a<sa eq q fin<n } where | |
| 341 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 | 342 pleq1 zero i<sn eq q q<i with <-cmp (toℕ q) zero |
| 343 ... | tri< () ¬b ¬c | |
| 344 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i ) | |
| 345 ... | tri≈ ¬a b ¬c = begin | |
| 346 x ⟨$⟩ʳ q | |
| 347 ≡⟨ cong ( λ k → x ⟨$⟩ʳ k ) (toℕ-injective b )⟩ | |
| 348 x ⟨$⟩ʳ zero | |
| 349 ≡⟨ toℕ-injective (headeq eq) ⟩ | |
| 350 y ⟨$⟩ʳ zero | |
| 351 ≡⟨ cong ( λ k → y ⟨$⟩ʳ k ) (sym (toℕ-injective b )) ⟩ | |
| 352 y ⟨$⟩ʳ q | |
| 91 | 353 ∎ |
| 80 | 354 pleq1 (suc i) (s≤s i<sn) eq q q<i with <-cmp (toℕ q) (suc i) |
| 355 ... | tri< a ¬b ¬c = pleq1 i (<-trans i<sn a<sa ) (taileq eq) q a | |
| 81 | 356 ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> c q<i ) |
| 80 | 357 ... | tri≈ ¬a b ¬c = begin |
| 358 x ⟨$⟩ʳ q | |
| 359 ≡⟨ cong (λ k → x ⟨$⟩ʳ k) (pleq3 b) ⟩ | |
| 360 x ⟨$⟩ʳ (suc (fromℕ< i<sn)) | |
| 361 ≡⟨ toℕ-injective pleq2 ⟩ | |
| 362 y ⟨$⟩ʳ (suc (fromℕ< i<sn)) | |
| 363 ≡⟨ cong (λ k → y ⟨$⟩ʳ k) (sym (pleq3 b)) ⟩ | |
| 364 y ⟨$⟩ʳ q | |
| 365 ∎ where | |
| 366 pleq3 : toℕ q ≡ suc i → q ≡ suc (fromℕ< i<sn) | |
| 367 pleq3 tq=si = toℕ-injective ( begin | |
| 368 toℕ q | |
| 369 ≡⟨ b ⟩ | |
| 370 suc i | |
| 371 ≡⟨ sym (toℕ-fromℕ< (s≤s i<sn)) ⟩ | |
| 372 toℕ (fromℕ< (s≤s i<sn)) | |
| 373 ≡⟨⟩ | |
| 374 toℕ (suc (fromℕ< i<sn)) | |
| 91 | 375 ∎ ) |
| 80 | 376 pleq2 : toℕ ( x ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) ≡ toℕ ( y ⟨$⟩ʳ (suc (fromℕ< i<sn)) ) |
| 377 pleq2 = headeq eq | |
| 37 | 378 |
| 112 | 379 is-=p= : {n : ℕ} → (x y : Permutation n n ) → Dec (x =p= y ) |
| 380 is-=p= {zero} x y = yes record { peq = λ () } | |
| 381 is-=p= {suc n} x y with ℕL-eq? (plist0 x ) ( plist0 y ) | |
| 382 ... | yes t = yes (pleq x y t) | |
| 383 ... | no t = no ( contra-position (←pleq x y) t ) | |
| 384 | |
| 87 | 385 pprep-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pprep x =p= pprep y |
| 386 pprep-cong {n} {x} {y} x=y = record { peq = pprep-cong1 } where | |
| 387 pprep-cong1 : (q : Fin (suc n)) → (pprep x ⟨$⟩ʳ q) ≡ (pprep y ⟨$⟩ʳ q) | |
| 388 pprep-cong1 zero = refl | |
| 389 pprep-cong1 (suc q) = begin | |
| 390 pprep x ⟨$⟩ʳ suc q | |
| 391 ≡⟨⟩ | |
| 392 suc ( x ⟨$⟩ʳ q ) | |
| 393 ≡⟨ cong ( λ k → suc k ) ( peq x=y q ) ⟩ | |
| 394 suc ( y ⟨$⟩ʳ q ) | |
| 395 ≡⟨⟩ | |
| 396 pprep y ⟨$⟩ʳ suc q | |
| 91 | 397 ∎ |
| 87 | 398 |
| 399 pprep-dist : {n : ℕ} → {x y : Permutation n n } → pprep (x ∘ₚ y) =p= (pprep x ∘ₚ pprep y) | |
| 400 pprep-dist {n} {x} {y} = record { peq = pprep-dist1 } where | |
| 401 pprep-dist1 : (q : Fin (suc n)) → (pprep (x ∘ₚ y) ⟨$⟩ʳ q) ≡ ((pprep x ∘ₚ pprep y) ⟨$⟩ʳ q) | |
| 402 pprep-dist1 zero = refl | |
| 403 pprep-dist1 (suc q) = cong ( λ k → suc k ) refl | |
| 404 | |
| 405 pswap-cong : {n : ℕ} → {x y : Permutation n n } → x =p= y → pswap x =p= pswap y | |
| 406 pswap-cong {n} {x} {y} x=y = record { peq = pswap-cong1 } where | |
| 407 pswap-cong1 : (q : Fin (suc (suc n))) → (pswap x ⟨$⟩ʳ q) ≡ (pswap y ⟨$⟩ʳ q) | |
| 408 pswap-cong1 zero = refl | |
| 409 pswap-cong1 (suc zero) = refl | |
| 410 pswap-cong1 (suc (suc q)) = begin | |
| 411 pswap x ⟨$⟩ʳ suc (suc q) | |
| 412 ≡⟨⟩ | |
| 413 suc (suc (x ⟨$⟩ʳ q)) | |
| 414 ≡⟨ cong ( λ k → suc (suc k) ) ( peq x=y q ) ⟩ | |
| 415 suc (suc (y ⟨$⟩ʳ q)) | |
| 416 ≡⟨⟩ | |
| 417 pswap y ⟨$⟩ʳ suc (suc q) | |
| 91 | 418 ∎ |
| 87 | 419 |
| 420 pswap-dist : {n : ℕ} → {x y : Permutation n n } → pprep (pprep (x ∘ₚ y)) =p= (pswap x ∘ₚ pswap y) | |
| 421 pswap-dist {n} {x} {y} = record { peq = pswap-dist1 } where | |
| 422 pswap-dist1 : (q : Fin (suc (suc n))) → ((pprep (pprep (x ∘ₚ y))) ⟨$⟩ʳ q) ≡ ((pswap x ∘ₚ pswap y) ⟨$⟩ʳ q) | |
| 423 pswap-dist1 zero = refl | |
| 424 pswap-dist1 (suc zero) = refl | |
| 425 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
|
426 |
| 121 | 427 infixr 100 _::_ |
| 428 | |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
429 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
|
430 f0 : FL 0 |
|
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
431 _::_ : { 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
|
432 |
| 130 | 433 data _f<_ : {n : ℕ } (x : FL n ) (y : FL n) → Set where |
| 434 f<n : {m : ℕ } {xn yn : Fin (suc m) } {xt yt : FL m} → xn Data.Fin.< yn → (xn :: xt) f< ( yn :: yt ) | |
| 435 f<t : {m : ℕ } {xn : Fin (suc m) } {xt yt : FL m} → xt f< yt → (xn :: xt) f< ( xn :: yt ) | |
| 436 | |
| 131 | 437 _f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set |
| 438 _f≤_ x y = (x ≡ y ) ∨ (x f< y ) | |
| 439 | |
| 130 | 440 FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n} → xn :: x ≡ yn :: y → ( xn ≡ yn ) ∧ (x ≡ y ) |
| 441 FLeq refl = record { proj1 = refl ; proj2 = refl } | |
| 442 | |
| 443 f<> : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥ | |
| 444 f<> (f<n x) (f<n x₁) = nat-<> x x₁ | |
| 445 f<> (f<n x) (f<t lt2) = nat-≡< refl x | |
| 446 f<> (f<t lt) (f<n x) = nat-≡< refl x | |
| 447 f<> (f<t lt) (f<t lt2) = f<> lt lt2 | |
| 448 | |
| 449 f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥ | |
| 450 f-≡< refl (f<n x) = nat-≡< refl x | |
| 451 f-≡< refl (f<t lt) = f-≡< refl lt | |
| 452 | |
| 453 FLcmp : {n : ℕ } → Trichotomous {Level.zero} {FL n} _≡_ _f<_ | |
| 454 FLcmp f0 f0 = tri≈ (λ ()) refl (λ ()) | |
| 455 FLcmp (xn :: xt) (yn :: yt) with <-fcmp xn yn | |
| 456 ... | tri< a ¬b ¬c = tri< (f<n a) (λ eq → nat-≡< (cong toℕ (proj1 (FLeq eq)) ) a) (λ lt → f<> lt (f<n a) ) | |
| 457 ... | tri> ¬a ¬b c = tri> (λ lt → f<> lt (f<n c) ) (λ eq → nat-≡< (cong toℕ (sym (proj1 (FLeq eq)) )) c) (f<n c) | |
| 458 ... | tri≈ ¬a refl ¬c with FLcmp xt yt | |
| 459 ... | tri< a ¬b ¬c₁ = tri< (f<t a) (λ eq → ¬b (proj2 (FLeq eq) )) (λ lt → f<> lt (f<t a) ) | |
| 460 ... | tri≈ ¬a₁ refl ¬c₁ = tri≈ (λ lt → f-≡< refl lt ) refl (λ lt → f-≡< refl lt ) | |
| 461 ... | tri> ¬a₁ ¬b c = tri> (λ lt → f<> lt (f<t c) ) (λ eq → ¬b (proj2 (FLeq eq) )) (f<t c) | |
| 462 | |
| 463 infixr 250 _f<?_ | |
| 464 | |
| 465 _f<?_ : {n : ℕ} → (x y : FL n ) → Dec (x f< y ) | |
| 466 x f<? y with FLcmp x y | |
| 467 ... | tri< a ¬b ¬c = yes a | |
| 468 ... | tri≈ ¬a refl ¬c = no ( ¬a ) | |
| 469 ... | tri> ¬a ¬b c = no ( ¬a ) | |
| 129 | 470 |
| 88 | 471 shlem→ : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n) ) → perm ⟨$⟩ˡ x ≡ zero → x ≡ zero |
| 472 shlem→ perm p0=0 x px=0 = begin | |
| 61 | 473 x ≡⟨ sym ( inverseʳ perm ) ⟩ |
| 474 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ x) ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) px=0 ⟩ | |
| 475 perm ⟨$⟩ʳ zero ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) (sym p0=0) ⟩ | |
| 476 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero) ≡⟨ inverseʳ perm ⟩ | |
| 477 zero | |
| 130 | 478 ∎ |
| 54 | 479 |
| 88 | 480 shlem← : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → (x : Fin (suc n)) → perm ⟨$⟩ʳ x ≡ zero → x ≡ zero |
| 481 shlem← perm p0=0 x px=0 = begin | |
| 61 | 482 x ≡⟨ sym (inverseˡ perm ) ⟩ |
| 483 perm ⟨$⟩ˡ ( perm ⟨$⟩ʳ x ) ≡⟨ cong (λ k → perm ⟨$⟩ˡ k ) px=0 ⟩ | |
| 484 perm ⟨$⟩ˡ zero ≡⟨ p0=0 ⟩ | |
| 485 zero | |
| 130 | 486 ∎ |
| 54 | 487 |
| 88 | 488 sh2 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ˡ (suc x) ≡ zero |
| 489 sh2 perm p0=0 {x} eq with shlem→ perm p0=0 (suc x) eq | |
| 490 sh2 perm p0=0 {x} eq | () | |
| 491 | |
| 492 sh1 : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → (p0=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0 ) → {x : Fin n} → ¬ perm ⟨$⟩ʳ (suc x) ≡ zero | |
| 493 sh1 perm p0=0 {x} eq with shlem← perm p0=0 (suc x) eq | |
| 494 sh1 perm p0=0 {x} eq | () | |
| 495 | |
| 496 | |
| 497 -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] → 0 ∷ 1 ∷ 2 ∷ [] | |
| 498 shrink : {n : ℕ} → (perm : Permutation (suc n) (suc n) ) → perm ⟨$⟩ˡ (# 0) ≡ # 0 → Permutation n n | |
| 499 shrink {n} perm p0=0 = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where | |
| 57 | 500 |
| 61 | 501 p→ : Fin n → Fin n |
| 88 | 502 p→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) |
| 503 p→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) | |
| 61 | 504 p→ x | suc t | _ = t |
| 50 | 505 |
| 506 p← : Fin n → Fin n | |
| 88 | 507 p← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) |
| 508 p← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) | |
| 61 | 509 p← x | suc t | _ = t |
| 50 | 510 |
| 511 piso← : (x : Fin n ) → p→ ( p← x ) ≡ x | |
| 88 | 512 piso← x with perm ⟨$⟩ˡ (suc x) | inspect (_⟨$⟩ˡ_ perm ) (suc x) |
| 513 piso← x | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 {x} e ) | |
| 514 piso← x | suc t | _ with perm ⟨$⟩ʳ (suc t) | inspect (_⟨$⟩ʳ_ perm ) (suc t) | |
| 515 piso← x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 e ) | |
| 61 | 516 piso← x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin |
| 517 t1 | |
| 518 ≡⟨ plem0 plem1 ⟩ | |
| 52 | 519 x |
| 61 | 520 ∎ where |
| 521 open ≡-Reasoning | |
| 522 plem0 : suc t1 ≡ suc x → t1 ≡ x | |
| 523 plem0 refl = refl | |
| 524 plem1 : suc t1 ≡ suc x | |
| 525 plem1 = begin | |
| 526 suc t1 | |
| 527 ≡⟨ sym e1 ⟩ | |
| 88 | 528 Inverse.to perm Π.⟨$⟩ suc t |
| 529 ≡⟨ cong (λ k → Inverse.to perm Π.⟨$⟩ k ) (sym e0) ⟩ | |
| 530 Inverse.to perm Π.⟨$⟩ ( Inverse.from perm Π.⟨$⟩ suc x ) | |
| 531 ≡⟨ inverseʳ perm ⟩ | |
| 61 | 532 suc x |
| 533 ∎ | |
| 50 | 534 |
| 535 piso→ : (x : Fin n ) → p← ( p→ x ) ≡ x | |
| 88 | 536 piso→ x with perm ⟨$⟩ʳ (suc x) | inspect (_⟨$⟩ʳ_ perm ) (suc x) |
| 537 piso→ x | zero | record { eq = e } = ⊥-elim ( sh1 perm p0=0 {x} e ) | |
| 538 piso→ x | suc t | _ with perm ⟨$⟩ˡ (suc t) | inspect (_⟨$⟩ˡ_ perm ) (suc t) | |
| 539 piso→ x | suc t | _ | zero | record { eq = e } = ⊥-elim ( sh2 perm p0=0 e ) | |
| 61 | 540 piso→ x | suc t | record { eq = e0 } | suc t1 | record { eq = e1 } = begin |
| 541 t1 | |
| 542 ≡⟨ plem2 plem3 ⟩ | |
| 53 | 543 x |
| 61 | 544 ∎ where |
| 545 plem2 : suc t1 ≡ suc x → t1 ≡ x | |
| 546 plem2 refl = refl | |
| 547 plem3 : suc t1 ≡ suc x | |
| 548 plem3 = begin | |
| 549 suc t1 | |
| 550 ≡⟨ sym e1 ⟩ | |
| 88 | 551 Inverse.from perm Π.⟨$⟩ suc t |
| 552 ≡⟨ cong (λ k → Inverse.from perm Π.⟨$⟩ k ) (sym e0 ) ⟩ | |
| 553 Inverse.from perm Π.⟨$⟩ ( Inverse.to perm Π.⟨$⟩ suc x ) | |
| 554 ≡⟨ inverseˡ perm ⟩ | |
| 61 | 555 suc x |
| 556 ∎ | |
| 57 | 557 |
| 88 | 558 shrink-iso : { n : ℕ } → {perm : Permutation n n} → shrink (pprep perm) refl =p= perm |
| 559 shrink-iso {n} {perm} = record { peq = λ q → refl } | |
| 560 | |
| 107 | 561 shrink-iso2 : { n : ℕ } → {perm : Permutation (suc n) (suc n)} |
| 108 | 562 → (p=0 : perm ⟨$⟩ˡ (# 0) ≡ # 0) → pprep (shrink perm p=0) =p= perm |
| 563 shrink-iso2 {n} {perm} p=0 = record { peq = s001 } where | |
| 109 | 564 s001 : (q : Fin (suc n)) → (pprep (shrink perm p=0) ⟨$⟩ʳ q) ≡ perm ⟨$⟩ʳ q |
| 565 s001 zero = begin | |
| 566 zero | |
| 567 ≡⟨ sym ( inverseʳ perm ) ⟩ | |
| 568 perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ zero ) | |
| 569 ≡⟨ cong (λ k → perm ⟨$⟩ʳ k ) p=0 ⟩ | |
| 570 perm ⟨$⟩ʳ zero | |
| 571 ∎ | |
| 572 s001 (suc q) with perm ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ perm ) (suc q) | |
| 573 ... | zero | record {eq = e} = ⊥-elim (sh1 perm p=0 {q} e) | |
| 574 ... | suc t | e = refl | |
| 108 | 575 |
| 107 | 576 |
| 98 | 577 shrink-cong : { n : ℕ } → {x y : Permutation (suc n) (suc n)} |
| 578 → x =p= y | |
| 579 → (x=0 : x ⟨$⟩ˡ (# 0) ≡ # 0 ) → (y=0 : y ⟨$⟩ˡ (# 0) ≡ # 0 ) → shrink x x=0 =p= shrink y y=0 | |
| 99 | 580 shrink-cong {n} {x} {y} x=y x=0 y=0 = record { peq = p002 } where |
| 581 p002 : (q : Fin n) → (shrink x x=0 ⟨$⟩ʳ q) ≡ (shrink y y=0 ⟨$⟩ʳ q) | |
| 582 p002 q with x ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ x ) (suc q) | y ⟨$⟩ʳ (suc q) | inspect (_⟨$⟩ʳ_ y ) (suc q) | |
| 583 p002 q | zero | record { eq = ex } | zero | ey = ⊥-elim ( sh1 x x=0 ex ) | |
| 584 p002 q | zero | record { eq = ex } | suc py | ey = ⊥-elim ( sh1 x x=0 ex ) | |
| 585 p002 q | suc px | ex | zero | record { eq = ey } = ⊥-elim ( sh1 y y=0 ey ) | |
| 586 p002 q | suc px | record { eq = ex } | suc py | record { eq = ey } = p003 ( begin | |
| 587 suc px | |
| 588 ≡⟨ sym ex ⟩ | |
| 589 x ⟨$⟩ʳ (suc q) | |
| 590 ≡⟨ peq x=y (suc q) ⟩ | |
| 591 y ⟨$⟩ʳ (suc q) | |
| 592 ≡⟨ ey ⟩ | |
| 593 suc py | |
| 594 ∎ ) where | |
| 595 p003 : suc px ≡ suc py → px ≡ py | |
| 596 p003 refl = refl | |
| 98 | 597 |
| 57 | 598 FL→perm : {n : ℕ } → FL n → Permutation n n |
| 599 FL→perm f0 = pid | |
| 600 FL→perm (x :: fl) = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) | |
| 601 | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
602 t40 = (# 2) :: ( (# 1) :: (( # 0 ) :: f0 )) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
603 t4 = FL→perm ((# 2) :: t40 ) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
604 |
| 61 | 605 -- 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
|
606 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
|
607 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
|
608 -- ∷ 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
|
609 -- ∷ 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
|
610 -- ∷ 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
|
611 -- ∷ 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
|
612 ∷ 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
|
613 ∷ 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
|
614 ∷ 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
|
615 ∷ 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
|
616 -- ∷ 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
|
617 -- ∷ 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
|
618 -- ∷ 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
|
619 -- ∷ plist ( (flip (FL→perm ((# 3) :: ((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) ))) ∘ₚ (FL→perm ((# 3) :: (((# 1) :: ( (# 0) :: (( # 0 ) :: f0 )) )))) )) |
| 57 | 620 ∷ [] |
| 50 | 621 |
| 58 | 622 |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
623 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
|
624 perm→FL {zero} perm = f0 |
| 98 | 625 perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) |
| 626 -- perm→FL {suc n} perm = (perm ⟨$⟩ʳ (# 0)) :: perm→FL (remove (# 0) perm) | |
| 627 | |
| 130 | 628 _p<_ : {n : ℕ } ( x y : Permutation n n ) → Set |
| 629 x p< y = perm→FL x f< perm→FL y | |
| 630 | |
| 98 | 631 pcong-pF : {n : ℕ } → {x y : Permutation n n} → x =p= y → perm→FL x ≡ perm→FL y |
| 99 | 632 pcong-pF {zero} eq = refl |
| 100 | 633 pcong-pF {suc n} {x} {y} eq = cong₂ (λ j k → j :: k ) ( peq eq (# 0)) (pcong-pF (shrink-cong (presp eq p001 ) (p=0 x) (p=0 y))) where |
| 634 p002 : x ⟨$⟩ʳ (# 0) ≡ y ⟨$⟩ʳ (# 0) | |
| 635 p002 = peq eq (# 0) | |
| 636 p001 : flip (pins (toℕ≤pred[n] (x ⟨$⟩ʳ (# 0)))) =p= flip (pins (toℕ≤pred[n] (y ⟨$⟩ʳ (# 0)))) | |
| 637 p001 = subst ( λ k → flip (pins (toℕ≤pred[n] (x ⟨$⟩ʳ (# 0)))) =p= flip (pins (toℕ≤pred[n] k ))) p002 prefl | |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
638 |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
639 -- 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
|
640 t5 = plist (t4) ∷ plist (flip t4) |
| 74 | 641 ∷ ( toℕ (t4 ⟨$⟩ˡ fromℕ< a<sa) ∷ [] ) |
| 61 | 642 ∷ ( toℕ (t4 ⟨$⟩ʳ (# 0)) ∷ [] ) |
|
60
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
643 -- ∷ plist ( t4 ∘ₚ flip (pins ( n≤ 1 ) )) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
644 ∷ plist (remove (# 0) t4 ) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
645 ∷ plist ( FL→perm t40 ) |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
646 ∷ [] |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
647 |
|
48926e810f5f
perm→FL done. pprep fix.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
59
diff
changeset
|
648 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
|
649 |
| 98 | 650 FL→iso : {n : ℕ } → (fl : FL n ) → perm→FL ( FL→perm fl ) ≡ fl |
| 651 FL→iso f0 = refl | |
| 100 | 652 FL→iso {suc n} (x :: fl) = cong₂ ( λ j k → j :: k ) f001 f002 where |
| 98 | 653 perm = pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x ) |
| 654 f001 : perm ⟨$⟩ʳ (# 0) ≡ x | |
| 100 | 655 f001 = begin |
| 656 (pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x )) ⟨$⟩ʳ (# 0) | |
| 101 | 657 ≡⟨⟩ |
| 658 pins ( toℕ≤pred[n] x ) ⟨$⟩ʳ (# 0) | |
| 659 ≡⟨ px=x x ⟩ | |
| 100 | 660 x |
| 661 ∎ | |
| 98 | 662 x=0 : (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ˡ (# 0) ≡ # 0 |
| 100 | 663 x=0 = subst ( λ k → (perm ∘ₚ flip (pins (toℕ≤pred[n] k))) ⟨$⟩ˡ (# 0) ≡ # 0 ) f001 (p=0 perm) |
| 98 | 664 x=0' : (pprep (FL→perm fl) ∘ₚ pid) ⟨$⟩ˡ (# 0) ≡ # 0 |
| 100 | 665 x=0' = refl |
| 103 | 666 f003 : (q : Fin (suc n)) → |
| 667 ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ⟨$⟩ʳ q) ≡ | |
| 668 ((perm ∘ₚ flip (pins (toℕ≤pred[n] x))) ⟨$⟩ʳ q) | |
| 669 f003 q = cong (λ k → (perm ∘ₚ flip (pins (toℕ≤pred[n] k))) ⟨$⟩ʳ q ) f001 | |
| 98 | 670 f002 : perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) ≡ fl |
| 671 f002 = begin | |
| 672 perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ) | |
| 103 | 673 ≡⟨ pcong-pF (shrink-cong {n} {perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))} {perm ∘ₚ flip (pins (toℕ≤pred[n] x))} record {peq = f003 } (p=0 perm) x=0) ⟩ |
| 98 | 674 perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] x))) x=0 ) |
| 675 ≡⟨⟩ | |
| 676 perm→FL (shrink ((pprep (FL→perm fl) ∘ₚ pins ( toℕ≤pred[n] x )) ∘ₚ flip (pins (toℕ≤pred[n] x))) x=0 ) | |
| 103 | 677 ≡⟨ pcong-pF (shrink-cong (passoc (pprep (FL→perm fl)) (pins ( toℕ≤pred[n] x )) (flip (pins (toℕ≤pred[n] x))) ) x=0 x=0) ⟩ |
| 98 | 678 perm→FL (shrink (pprep (FL→perm fl) ∘ₚ (pins ( toℕ≤pred[n] x ) ∘ₚ flip (pins (toℕ≤pred[n] x)))) x=0 ) |
| 103 | 679 ≡⟨ pcong-pF (shrink-cong {n} {pprep (FL→perm fl) ∘ₚ (pins ( toℕ≤pred[n] x ) ∘ₚ flip (pins (toℕ≤pred[n] x)))} {pprep (FL→perm fl) ∘ₚ pid} |
| 680 ( presp {suc n} {pprep (FL→perm fl) } {_} {(pins ( toℕ≤pred[n] x ) ∘ₚ flip (pins (toℕ≤pred[n] x)))} {pid} prefl | |
| 681 record { peq = λ q → inverseˡ (pins ( toℕ≤pred[n] x )) } ) x=0 x=0') ⟩ | |
| 98 | 682 perm→FL (shrink (pprep (FL→perm fl) ∘ₚ pid) x=0' ) |
| 103 | 683 ≡⟨ pcong-pF (shrink-cong {n} {pprep (FL→perm fl) ∘ₚ pid} {pprep (FL→perm fl)} record {peq = λ q → refl } x=0' x=0') ⟩ -- prefl won't work |
| 98 | 684 perm→FL (shrink (pprep (FL→perm fl)) x=0' ) |
| 685 ≡⟨ pcong-pF shrink-iso ⟩ | |
| 686 perm→FL ( FL→perm fl ) | |
| 687 ≡⟨ FL→iso fl ⟩ | |
| 688 fl | |
| 689 ∎ | |
| 690 | |
| 104 | 691 pcong-Fp : {n : ℕ } → {x y : FL n} → x ≡ y → FL→perm x =p= FL→perm y |
| 692 pcong-Fp {n} {x} {x} refl = prefl | |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
693 |
| 104 | 694 FL←iso : {n : ℕ } → (perm : Permutation n n ) → FL→perm ( perm→FL perm ) =p= perm |
| 695 FL←iso {0} perm = record { peq = λ () } | |
| 106 | 696 FL←iso {suc n} perm = record { peq = λ q → ( begin |
| 697 FL→perm ( perm→FL perm ) ⟨$⟩ʳ q | |
| 698 ≡⟨⟩ | |
| 107 | 699 (pprep (FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) ) ) ⟨$⟩ʳ q |
| 110 | 700 ≡⟨ peq (presp {suc n} {_} {_} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))} (pprep-cong {n} {FL→perm (perm→FL (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm) ))} (FL←iso _ ) ) prefl ) q ⟩ |
| 107 | 701 (pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm)) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )) ⟨$⟩ʳ q |
| 110 | 702 ≡⟨ peq (presp {suc n} {pprep (shrink (perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) (p=0 perm))} {perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))} {pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )} (shrink-iso2 (p=0 perm)) prefl) q ⟩ |
| 107 | 703 ((perm ∘ₚ flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0))))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)) )) ⟨$⟩ʳ q |
| 110 | 704 ≡⟨ peq (presp {suc n} {perm} {_} {flip (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) ∘ₚ pins ( toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))} {pid} prefl record { peq = λ q → inverseʳ (pins (toℕ≤pred[n] (perm ⟨$⟩ʳ (# 0)))) }) q ⟩ |
| 107 | 705 ( perm ∘ₚ pid ) ⟨$⟩ʳ q |
| 110 | 706 ≡⟨⟩ |
| 104 | 707 perm ⟨$⟩ʳ q |
| 107 | 708 ∎ ) } |
|
49
8b3b95362ca9
remove (fromℕ≤ a<sa) perm is no good
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
48
diff
changeset
|
709 |
| 111 | 710 FL-inject : {n : ℕ } → {g h : Permutation n n } → perm→FL g ≡ perm→FL h → g =p= h |
| 711 FL-inject {n} {g} {h} g=h = record { peq = λ q → ( begin | |
| 712 g ⟨$⟩ʳ q | |
| 713 ≡⟨ peq (psym (FL←iso g )) q ⟩ | |
| 714 ( FL→perm (perm→FL g) ) ⟨$⟩ʳ q | |
| 715 ≡⟨ cong ( λ k → FL→perm k ⟨$⟩ʳ q ) g=h ⟩ | |
| 716 ( FL→perm (perm→FL h) ) ⟨$⟩ʳ q | |
| 717 ≡⟨ peq (FL←iso h) q ⟩ | |
| 718 h ⟨$⟩ʳ q | |
| 719 ∎ ) } | |
| 720 | |
| 721 | |
| 66 | 722 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n |
| 91 | 723 lem2 i≤n = ≤-trans i≤n ( a≤sa ) |
| 66 | 724 |
|
67
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
725 ∀-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
|
726 ∀-FL x = fls6 x where |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
727 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
|
728 fls4 zero n i≤n perm x = (zero :: perm ) ∷ x |
| 91 | 729 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
|
730 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
|
731 fls5 n [] x = x |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
732 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
|
733 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
|
734 fls6 zero = (zero :: f0) ∷ [] |
|
3825082ebdbd
∀-FL : (n : ℕ ) → List (FL (suc n))
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
66
diff
changeset
|
735 fls6 (suc n) = fls5 (suc n) (fls6 n) [] |
| 65 | 736 |
| 97 | 737 tf1 = ∀-FL 4 |
| 738 tf2 = Data.List.map (λ k → ⟪ plist (FL→perm k ) , k ⟫ ) tf1 | |
| 739 | |
| 48 | 740 all-perm : (n : ℕ ) → List (Permutation (suc n) (suc n) ) |
| 741 all-perm n = pls6 n where | |
| 38 | 742 lem1 : {i n : ℕ } → i ≤ n → i < suc n |
| 743 lem1 z≤n = s≤s z≤n | |
| 744 lem1 (s≤s lt) = s≤s (lem1 lt) | |
| 40 | 745 pls4 : ( i n : ℕ ) → (i<n : i ≤ n ) → Permutation n n → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
| 48 | 746 pls4 zero n i≤n perm x = (pprep perm ∘ₚ pins i≤n ) ∷ x |
| 91 | 747 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 | 748 pls5 : ( n : ℕ ) → List (Permutation n n) → List (Permutation (suc n) (suc n)) → List (Permutation (suc n) (suc n)) |
| 749 pls5 n [] x = x | |
| 750 pls5 n (h ∷ x) y = pls5 n x (pls4 n n lem0 h y) | |
| 751 pls6 : ( n : ℕ ) → List (Permutation (suc n) (suc n)) | |
| 752 pls6 zero = pid ∷ [] | |
| 48 | 753 pls6 (suc n) = pls5 (suc n) (rev (pls6 n) ) [] -- rev to put id first |
| 754 | |
| 755 pls : (n : ℕ ) → List (List ℕ ) | |
| 75 | 756 pls n = Data.List.map plist (all-perm n) |