annotate Putil.agda @ 61:c16749815259

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