|
7
|
1 module Symmetric where
|
|
0
|
2
|
|
|
3 open import Level hiding ( suc ; zero )
|
|
|
4 open import Algebra
|
|
|
5 open import Algebra.Structures
|
|
17
|
6 open import Data.Fin hiding ( _<_ )
|
|
29
|
7 open import Data.Fin.Properties hiding ( <-cmp ; <-trans )
|
|
3
|
8 open import Data.Product
|
|
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
|
|
|
17 open import Data.List using (List; []; _∷_ ; length)
|
|
|
18 open import nat
|
|
0
|
19
|
|
|
20 fid : {p : ℕ } → Fin p → Fin p
|
|
|
21 fid x = x
|
|
|
22
|
|
|
23 -- Data.Fin.Permutation.id
|
|
|
24 pid : {p : ℕ } → Permutation p p
|
|
|
25 pid = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
|
|
|
26
|
|
|
27 -- Data.Fin.Permutation.flip
|
|
|
28 pinv : {p : ℕ } → Permutation p p → Permutation p p
|
|
|
29 pinv {p} P = permutation (_⟨$⟩ˡ_ P) (_⟨$⟩ʳ_ P ) record { left-inverse-of = λ x → inverseʳ P ; right-inverse-of = λ x → inverseˡ P }
|
|
|
30
|
|
3
|
31 record _=p=_ {p : ℕ } ( x y : Permutation p p ) : Set where
|
|
|
32 field
|
|
|
33 peq : ( q : Fin p ) → x ⟨$⟩ʳ q ≡ y ⟨$⟩ʳ q
|
|
0
|
34
|
|
3
|
35 open _=p=_
|
|
0
|
36
|
|
3
|
37 prefl : {p : ℕ } { x : Permutation p p } → x =p= x
|
|
|
38 peq (prefl {p} {x}) q = refl
|
|
1
|
39
|
|
3
|
40 psym : {p : ℕ } { x y : Permutation p p } → x =p= y → y =p= x
|
|
|
41 peq (psym {p} {x} {y} eq ) q = sym (peq eq q)
|
|
1
|
42
|
|
3
|
43 ptrans : {p : ℕ } { x y z : Permutation p p } → x =p= y → y =p= z → x =p= z
|
|
|
44 peq (ptrans {p} {x} {y} x=y y=z ) q = trans (peq x=y q) (peq y=z q)
|
|
0
|
45
|
|
7
|
46 Symmetric : ℕ → Group Level.zero Level.zero
|
|
|
47 Symmetric p = record {
|
|
0
|
48 Carrier = Permutation p p
|
|
3
|
49 ; _≈_ = _=p=_
|
|
0
|
50 ; _∙_ = _∘ₚ_
|
|
|
51 ; ε = pid
|
|
|
52 ; _⁻¹ = pinv
|
|
3
|
53 ; isGroup = record { isMonoid = record { isSemigroup = record { isMagma = record {
|
|
|
54 isEquivalence = record {refl = prefl ; trans = ptrans ; sym = psym }
|
|
0
|
55 ; ∙-cong = presp }
|
|
|
56 ; assoc = passoc }
|
|
3
|
57 ; identity = ( (λ q → record { peq = λ q → refl } ) , (λ q → record { peq = λ q → refl } )) }
|
|
|
58 ; inverse = ( (λ x → record { peq = λ q → inverseʳ x} ) , (λ x → record { peq = λ q → inverseˡ x} ))
|
|
|
59 ; ⁻¹-cong = λ i=j → record { peq = λ q → p-inv i=j q }
|
|
0
|
60 }
|
|
|
61 } where
|
|
3
|
62 presp : {x y u v : Permutation p p } → x =p= y → u =p= v → (x ∘ₚ u) =p= (y ∘ₚ v)
|
|
|
63 presp {x} {y} {u} {v} x=y u=v = record { peq = λ q → lemma4 q } where
|
|
|
64 lemma4 : (q : Fin p) → ((x ∘ₚ u) ⟨$⟩ʳ q) ≡ ((y ∘ₚ v) ⟨$⟩ʳ q)
|
|
|
65 lemma4 q = trans (cong (λ k → Inverse.to u Π.⟨$⟩ k) (peq x=y q) ) (peq u=v _ )
|
|
|
66 passoc : (x y z : Permutation p p) → ((x ∘ₚ y) ∘ₚ z) =p= (x ∘ₚ (y ∘ₚ z))
|
|
|
67 passoc x y z = record { peq = λ q → refl }
|
|
|
68 p-inv : {i j : Permutation p p} → i =p= j → (q : Fin p) → pinv i ⟨$⟩ʳ q ≡ pinv j ⟨$⟩ʳ q
|
|
|
69 p-inv {i} {j} i=j q = begin
|
|
4
|
70 i ⟨$⟩ˡ q ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (inverseʳ j) ) ⟩
|
|
|
71 i ⟨$⟩ˡ ( j ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ cong (λ k → i ⟨$⟩ˡ k) (sym (peq i=j _ )) ⟩
|
|
|
72 i ⟨$⟩ˡ ( i ⟨$⟩ʳ ( j ⟨$⟩ˡ q )) ≡⟨ inverseˡ i ⟩
|
|
|
73 j ⟨$⟩ˡ q
|
|
3
|
74 ∎ where open ≡-Reasoning
|
|
0
|
75
|
|
33
|
76 perm0 : {n : ℕ } → Permutation n n
|
|
16
|
77 perm0 = permutation fid fid record { left-inverse-of = λ x → refl ; right-inverse-of = λ x → refl }
|
|
0
|
78
|
|
16
|
79 open import Relation.Nullary
|
|
|
80 open import Data.Empty
|
|
17
|
81 open import Relation.Binary.Core
|
|
|
82 open import fin
|
|
16
|
83
|
|
33
|
84 fperm0 : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n)
|
|
|
85 fperm0 {n} perm = permutation p→ p← record { left-inverse-of = piso← ; right-inverse-of = {!!} } where
|
|
|
86 p→ : Fin (suc n) → Fin (suc n)
|
|
|
87 p→ x with <-cmp (toℕ x) n
|
|
|
88 p→ x | tri< a ¬b ¬c = fin+1 ( perm ⟨$⟩ˡ ( fromℕ≤ a ))
|
|
|
89 p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
|
|
|
90 p→ x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
|
|
|
91
|
|
|
92 p← : Fin (suc n) → Fin (suc n)
|
|
|
93 p← x with <-cmp (toℕ x) n
|
|
|
94 p← x | tri< a ¬b ¬c = fin+1 ( perm ⟨$⟩ʳ ( fromℕ≤ a ))
|
|
|
95 p← x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
|
|
|
96 p← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
|
|
|
97
|
|
|
98 piso← : (x : Fin (suc n)) → p← ( p→ x ) ≡ x
|
|
|
99 piso← x with <-cmp (toℕ x) n
|
|
|
100 piso← x | tri< a ¬b ¬c = begin
|
|
|
101 p← ( fin+1 (perm ⟨$⟩ˡ (fromℕ≤ a)) )
|
|
|
102 ≡⟨ {!!} ⟩
|
|
|
103 fin+1 ( perm ⟨$⟩ʳ ( perm ⟨$⟩ˡ ( fromℕ≤ a )) )
|
|
|
104 ≡⟨ cong (λ k → fin+1 k ) ( inverseʳ perm ) ⟩
|
|
|
105 fin+1 (fromℕ≤ a)
|
|
|
106 ≡⟨ {!!} ⟩
|
|
|
107 x
|
|
|
108 ∎ where
|
|
|
109 open ≡-Reasoning
|
|
|
110 piso← x | tri≈ ¬a b ¬c = begin
|
|
|
111 p← ( fromℕ≤ a<sa )
|
|
|
112 ≡⟨ {!!} ⟩
|
|
|
113 x
|
|
|
114 ∎ where open ≡-Reasoning
|
|
|
115 piso← x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
|
|
|
116
|
|
|
117 fswap : {n m : ℕ } → suc m < n → Permutation n n
|
|
|
118 fswap {n} {m} n<m = permutation p→ p→ record { left-inverse-of = piso← ; right-inverse-of = piso←} where
|
|
|
119 p→ : Fin n → Fin (n)
|
|
|
120 p→ x with <-cmp (toℕ x) m
|
|
|
121 p→ x | tri< a ¬b ¬c = x
|
|
|
122 p→ x | tri≈ ¬a b ¬c = fromℕ≤ {suc m} {n} n<m
|
|
|
123 p→ x | tri> ¬a ¬b c with <-cmp (toℕ x) (suc m)
|
|
|
124 p→ x | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = x
|
|
|
125 p→ x | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = fromℕ≤ {m} {n} (<-trans a<sa n<m)
|
|
|
126 p→ x | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = x
|
|
|
127
|
|
|
128 piso← : (x : Fin (n)) → p→ ( p→ x ) ≡ x
|
|
|
129 piso← x with <-cmp (toℕ x) m
|
|
|
130 piso← x | tri< a ¬b ¬c = {!!}
|
|
|
131 piso← x | tri≈ ¬a b ¬c = {!!}
|
|
|
132 piso← x | tri> ¬a ¬b c with <-cmp (toℕ x) (suc m)
|
|
|
133 piso← x | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = {!!}
|
|
|
134 piso← x | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = {!!}
|
|
|
135 piso← x | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ = {!!}
|
|
|
136
|
|
|
137
|
|
17
|
138 fperm : {n m : ℕ} → m < n → Permutation n n → Permutation (suc n) (suc n)
|
|
|
139 fperm {zero} ()
|
|
|
140 fperm {suc n} {m} (s≤s m<n) perm = permutation p→ p← record { left-inverse-of = piso← ; right-inverse-of = piso→ } where
|
|
|
141 p→ : Fin (suc (suc n)) → Fin (suc (suc n))
|
|
|
142 p→ x with <-cmp (toℕ x) m
|
|
|
143 p→ x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn)) where
|
|
|
144 x<sn : toℕ x < suc n
|
|
|
145 x<sn = <-trans a (s≤s m<n)
|
|
|
146 p→ x | tri≈ ¬a b ¬c = fromℕ≤ a<sa
|
|
|
147 p→ x | tri> ¬a ¬b c = fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s )))
|
|
18
|
148
|
|
17
|
149 p← : Fin (suc (suc n)) → Fin (suc (suc n))
|
|
19
|
150 p← x = lemma (suc n) refl x where
|
|
|
151 lemma : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → Fin (suc (suc n))
|
|
|
152 lemma i refl x with <-cmp (toℕ x) i
|
|
|
153 lemma i refl x | tri< a ¬b ¬c = fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn)) where
|
|
17
|
154 x<sn : toℕ x < suc n
|
|
18
|
155 x<sn = a
|
|
30
|
156 lemma i refl x | tri≈ ¬a b ¬c = fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
|
|
19
|
157 lemma i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
|
|
30
|
158 lem8 : {x : Fin (suc (suc n)) } → toℕ ( fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )) ≡ m
|
|
|
159 lem8 {x} = toℕ-fromℕ≤ (<-trans (s≤s m<n ) a<sa )
|
|
17
|
160 piso← : (x : Fin (suc (suc n))) → p← ( p→ x ) ≡ x
|
|
|
161 piso← x with <-cmp (toℕ x) m
|
|
31
|
162 piso← x | tri< a ¬b ¬c = begin
|
|
|
163 p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ x<sn)) )
|
|
|
164 ≡⟨ {!!} ⟩
|
|
32
|
165 fin+1 (perm ⟨$⟩ˡ (perm ⟨$⟩ʳ fromℕ≤ (<-trans a (s≤s m<n))))
|
|
|
166 ≡⟨ cong (λ k → fin+1 k ) (inverseˡ perm) ⟩
|
|
|
167 fin+1 (fromℕ≤ x<sn)
|
|
|
168 ≡⟨ {!!} ⟩
|
|
31
|
169 x
|
|
|
170 ∎ where
|
|
|
171 open ≡-Reasoning
|
|
32
|
172 k = inverseˡ perm
|
|
31
|
173 x<sn : toℕ x < suc n
|
|
|
174 x<sn = <-trans a (s≤s m<n)
|
|
|
175 piso← x | tri> ¬a ¬b c = begin
|
|
|
176 p← ( fin+1 (perm ⟨$⟩ʳ (fromℕ≤ (pred<n {_} {x} 0<s ))))
|
|
|
177 ≡⟨ {!!} ⟩
|
|
|
178 x
|
|
|
179 ∎ where
|
|
|
180 open ≡-Reasoning
|
|
18
|
181 piso← x | tri≈ ¬a refl ¬c = begin
|
|
|
182 p← ( fromℕ≤ a<sa )
|
|
19
|
183 ≡⟨ lem4 refl ⟩
|
|
30
|
184 fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
|
|
19
|
185 ≡⟨ {!!} ⟩
|
|
18
|
186 x
|
|
|
187 ∎ where
|
|
|
188 open ≡-Reasoning
|
|
30
|
189 lem4 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {suc n} a<sa → p← x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )
|
|
18
|
190 lem4 {x} refl with <-cmp (toℕ x) (suc n)
|
|
30
|
191 lem4 refl | tri< a ¬b ¬c = ⊥-elim ( ¬b {!!} )
|
|
19
|
192 lem4 refl | tri≈ ¬a b ¬c = refl
|
|
30
|
193 lem4 refl | tri> ¬a ¬b c = ⊥-elim ( ¬b {!!} )
|
|
17
|
194 piso→ : (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
|
|
19
|
195 piso→ x = lemma2 (suc n) refl x where
|
|
|
196 lemma2 : (i : ℕ ) → i ≡ suc n → (x : Fin (suc (suc n))) → p→ ( p← x ) ≡ x
|
|
|
197 lemma2 i refl x with <-cmp (toℕ x) i
|
|
31
|
198 lemma2 i refl x | tri< a ¬b ¬c = begin
|
|
|
199 p→ ( fin+1 (perm ⟨$⟩ˡ (fromℕ≤ x<sn)))
|
|
|
200 ≡⟨ {!!} ⟩
|
|
|
201 x
|
|
|
202 ∎ where
|
|
|
203 open ≡-Reasoning
|
|
|
204 x<sn : toℕ x < suc n
|
|
|
205 x<sn = a
|
|
|
206 lemma2 i refl x | tri> ¬a ¬b c = ⊥-elim ( nat-≤> c fin<n )
|
|
19
|
207 lemma2 i refl x | tri≈ ¬a b ¬c = begin
|
|
30
|
208 p→ (fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ))
|
|
|
209 ≡⟨ lem5 (fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa )) {!!} ⟩
|
|
19
|
210 fromℕ≤ a<sa
|
|
30
|
211 ≡⟨ {!!} ⟩
|
|
18
|
212 x
|
|
|
213 ∎ where
|
|
|
214 open ≡-Reasoning
|
|
30
|
215 lem7 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ m
|
|
|
216 lem7 refl = trans (toℕ-fromℕ≤ _) {!!}
|
|
29
|
217 lem6 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ (s≤s (s≤s m<n)) → toℕ x ≡ (suc m)
|
|
|
218 lem6 refl = toℕ-fromℕ≤ _
|
|
30
|
219 -- lem5 : {x : Fin (suc (suc n)) } → x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) → p→ x ≡ fromℕ≤ a<sa
|
|
|
220 lem5 : (x : Fin (suc (suc n)) ) → x ≡ fromℕ≤ {m} {suc (suc n)} (<-trans (s≤s m<n ) a<sa ) → p→ x ≡ fromℕ≤ a<sa
|
|
|
221 lem5 x eq with <-cmp (toℕ x) m
|
|
|
222 lem5 x eq | tri< a ¬b ¬c = {!!}
|
|
|
223 lem5 x eq | tri≈ ¬a refl ¬c = refl
|
|
|
224 lem5 x eq | tri> ¬a ¬b c = {!!}
|
|
16
|
225
|
