Skip to content

Commit cf1451b

Browse files
TanebTaneb
committed
WIP parity theorem
1 parent 0ab3191 commit cf1451b

File tree

3 files changed

+187
-4
lines changed

3 files changed

+187
-4
lines changed

‎src/Data/Fin/Permutation/Components.agda

+34-1
Original file line numberDiff line numberDiff line change
@@ -8,7 +8,7 @@
88

99
module Data.Fin.Permutation.Components where
1010

11-
open import Data.Bool.Base using (Bool; true; false)
11+
open import Data.Bool.Base using (Bool; true; false; if_then_else_)
1212
open import Data.Fin.Base
1313
open import Data.Fin.Properties
1414
open import Data.Nat.Base as ℕ using (zero; suc; _∸_)
@@ -28,16 +28,32 @@ open ≡-Reasoning
2828

2929
-- 'tranpose i j' swaps the places of 'i' and 'j'.
3030

31+
{-
3132
transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
3233
transpose i j k with does (k ≟ i) | does (k ≟ j)
3334
... | true | _ = j
3435
... | false | true = i
3536
... | false | false = k
37+
-}
38+
39+
transpose : ∀ {n} → Fin n → Fin n → Fin n → Fin n
40+
transpose i j k = if does (k ≟ i)
41+
then j
42+
else if does (k ≟ j)
43+
then i
44+
else k
3645

3746
--------------------------------------------------------------------------------
3847
-- Properties
3948
--------------------------------------------------------------------------------
4049

50+
transpose-comm : ∀ {n} (i j : Fin n) → transpose i j ≗ transpose j i
51+
transpose-comm i j k with k ≟ i | k ≟ j
52+
... | no _ | no _ = refl
53+
... | no _ | yes _ = refl
54+
... | yes _ | no _ = refl
55+
... | yes k≡i | yes k≡j = trans (sym k≡j) k≡i
56+
4157
transpose-inverse : ∀ {n} (i j : Fin n) {k} →
4258
transpose i j (transpose j i k) ≡ k
4359
transpose-inverse i j {k} with k ≟ j
@@ -50,6 +66,23 @@ transpose-inverse i j {k} with k ≟ j
5066
... | false because [k≢i] rewrite dec-false (k ≟ i) (invert [k≢i])
5167
| dec-false (k ≟ j) (invert [k≢j]) = refl
5268

69+
transpose-inverse′ : ∀ {n} (i j : Fin n) {k} → transpose i j (transpose i j k) ≡ k
70+
transpose-inverse′ i j {k} with k ≟ i
71+
transpose-inverse′ i j {k} | yes k≡i with j ≟ i
72+
... | yes j≡i = trans j≡i (sym k≡i)
73+
... | no j≢i rewrite dec-true (j ≟ j) refl = sym k≡i
74+
transpose-inverse′ i j {k} | no k≢i with k ≟ j
75+
... | yes k≡j rewrite dec-true (i ≟ i) refl = sym k≡j
76+
... | no k≢j rewrite dec-false (k ≟ i) k≢i rewrite dec-false (k ≟ j) k≢j = refl
77+
78+
transpose-matchˡ : ∀ {n} (i j : Fin n) → transpose i j i ≡ j
79+
transpose-matchˡ i j rewrite dec-true (i ≟ i) refl = refl
80+
81+
transpose-matchʳ : ∀ {n} (i j : Fin n) → transpose i j j ≡ i
82+
transpose-matchʳ i j with j ≟ i
83+
... | yes j≡i = j≡i
84+
... | no j≢i rewrite dec-true (j ≟ j) refl = refl
85+
5386
------------------------------------------------------------------------
5487
-- DEPRECATED NAMES
5588
------------------------------------------------------------------------

‎src/Data/Fin/Permutation/Transposition/List.agda

+150-3
Original file line numberDiff line numberDiff line change
@@ -8,16 +8,23 @@
88

99
module Data.Fin.Permutation.Transposition.List where
1010

11+
open import Data.Bool.Base
1112
open import Data.Fin.Base
1213
open import Data.Fin.Patterns using (0F)
1314
open import Data.Fin.Permutation as P hiding (lift₀)
1415
open import Data.Fin.Properties using (_≟_; suc-injective)
1516
import Data.Fin.Permutation.Components as PC
1617
open import Data.List as L using (List; []; _∷_; _++_; map)
18+
import Data.List.Membership.DecPropositional as L∈
1719
import Data.List.Properties as L
18-
open import Data.Nat.Base using (ℕ; suc; zero)
19-
open import Data.Product using (∃₂; _×_; _,_)
20-
open import Function using (_∘_)
20+
open import Data.List.Relation.Unary.Any using (here; there)
21+
open import Data.Nat.Base as ℕ using (ℕ; suc; zero; parity)
22+
import Data.Nat.Properties as ℕ
23+
open import Data.Parity.Base as ℙ using (Parity; 0ℙ; 1ℙ)
24+
open import Data.Product using (Σ-syntax; ∃₂; _×_; _,_; proj₁; proj₂)
25+
open import Function.Base hiding (id; flip)-- using (_∘_)
26+
open import Relation.Nullary.Negation using (contradiction)
27+
open import Relation.Nullary.Decidable hiding (map)
2128
open import Relation.Binary.PropositionalEquality
2229
using (_≡_; _≢_; refl; sym; trans; cong; module ≡-Reasoning)
2330
open ≡-Reasoning
@@ -96,3 +103,143 @@ eval-reverse (x@(a , b , _) ∷ xs) i = begin
96103
flip (eval xs) ∘ₚ transpose a b ⟨$⟩ʳ i ≡⟨ transpose-comm a b (flip (eval xs) ⟨$⟩ʳ i) ⟩
97104
flip (eval xs) ∘ₚ transpose b a ⟨$⟩ʳ i ∎
98105

106+
-- Properties of transposition lists that evaluate to the identity
107+
108+
eval[xs]≈id⇒length[xs]≢1 : ∀ (xs : TranspositionList n) → eval xs ≈ id → L.length xs ≢ 1
109+
eval[xs]≈id⇒length[xs]≢1 [] _ = λ ()
110+
eval[xs]≈id⇒length[xs]≢1 ((i , j , i≢j) ∷ []) p with j≡i ← p i rewrite dec-true (i ≟ i) refl = contradiction (sym j≡i) i≢j
111+
eval[xs]≈id⇒length[xs]≢1 (_ ∷ _ ∷ _) _ = λ ()
112+
113+
-- this is the workhorse of the parity theorem!
114+
-- If we have a representation of the identity permutations in 2 + k transpositions we can find one in k transpositions
115+
p₂ : ∀ (xs : TranspositionList n) → eval xs ≈ id → ∀ {k} → L.length xs ≡ 2 ℕ.+ k → Σ[ ys ∈ TranspositionList n ] (eval ys ≈ id × L.length ys ≡ k)
116+
p₂ {n = n} ((i₀ , j , i₀≢j) ∷ xs₀) p q = let (ys , r , s) = machine i₀ i₀≢j xs₀ xs₀[i₀]≡j xs₀[j]≡i₀ (ℕ.suc-injective q) in ys , (λ k → trans (sym (r k)) (p k)) , s
117+
where
118+
xs₀[i₀]≡j : eval xs₀ ⟨$⟩ʳ i₀ ≡ j
119+
xs₀[i₀]≡j = begin
120+
eval xs₀ ⟨$⟩ʳ i₀ ≡˘⟨ cong (eval xs₀ ⟨$⟩ʳ_) (PC.transpose-matchʳ i₀ j) ⟩
121+
transpose i₀ j ∘ₚ eval xs₀ ⟨$⟩ʳ j ≡⟨ p j ⟩
122+
j ∎
123+
124+
xs₀[j]≡i₀ : eval xs₀ ⟨$⟩ʳ j ≡ i₀
125+
xs₀[j]≡i₀ = begin
126+
eval xs₀ ⟨$⟩ʳ j ≡˘⟨ cong (eval xs₀ ⟨$⟩ʳ_) (PC.transpose-matchˡ i₀ j) ⟩
127+
transpose i₀ j ∘ₚ eval xs₀ ⟨$⟩ʳ i₀ ≡⟨ p i₀ ⟩
128+
i₀ ∎
129+
130+
open L∈ _≟_
131+
132+
machine : ∀ (i : Fin n) (i≢j : i ≢ j) (xs : TranspositionList n) → eval xs ⟨$⟩ʳ i ≡ j → eval xs ⟨$⟩ʳ j ≡ i → ∀ {k} → L.length xs ≡ 1 ℕ.+ k → Σ[ ys ∈ TranspositionList n ] transpose i j ∘ₚ eval xs ≈ eval ys × L.length ys ≡ k
133+
machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j xs[j]≡i {k} 1+∣xs∣≡1+k with iₕ ∈? i ∷ j ∷ []
134+
machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j xs[j]≡i {k} 1+∣xs∣≡1+k | no ¬p with jₕ ∈? i ∷ j ∷ []
135+
... | no ¬q
136+
rewrite dec-false (i ≟ iₕ) λ i≡iₕ → ¬p (here (sym i≡iₕ))
137+
rewrite dec-false (i ≟ jₕ) λ i≡jₕ → ¬q (here (sym i≡jₕ))
138+
rewrite dec-false (j ≟ iₕ) λ j≡iₕ → ¬p (there (here (sym j≡iₕ)))
139+
rewrite dec-false (j ≟ jₕ) λ j≡jₕ → ¬q (there (here (sym j≡jₕ)))
140+
= (iₕ , jₕ , iₕ≢jₕ) ∷ ys , ys′-eval , trans (cong suc (proj₂ (proj₂ rec))) (ℕ.suc-pred k {{ℕ.≢-nonZero k≢0}})
141+
where
142+
xs≢[] : xs ≢ []
143+
xs≢[] refl = i≢j xs[i]≡j
144+
145+
k≢0 : k ≢ 0
146+
k≢0 k≡0 = xs≢[] (L.length[xs]≡0⇒xs≡[] (trans (ℕ.suc-injective 1+∣xs∣≡1+k) k≡0))
147+
148+
k′ : ℕ
149+
k′ = ℕ.pred k
150+
151+
rec = machine i i≢j xs xs[i]≡j xs[j]≡i {k′} (trans (ℕ.suc-injective 1+∣xs∣≡1+k) (sym (ℕ.suc-pred k {{ℕ.≢-nonZero k≢0}})))
152+
153+
ys : TranspositionList n
154+
ys = proj₁ rec
155+
156+
ys-eval : transpose i j ∘ₚ eval xs ≈ eval ys
157+
ys-eval = proj₁ (proj₂ rec)
158+
159+
ys′-eval : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ transpose iₕ jₕ ∘ₚ eval ys
160+
ys′-eval k with k ∈? i ∷ j ∷ iₕ ∷ jₕ ∷ []
161+
... | no ¬r
162+
with ys[k] ← ys-eval k
163+
rewrite dec-false (k ≟ i) λ k≡i → ¬r (here k≡i)
164+
rewrite dec-false (k ≟ j) λ k≡j → ¬r (there (here k≡j))
165+
rewrite dec-false (k ≟ iₕ) λ k≡iₕ → ¬r (there (there (here k≡iₕ)))
166+
rewrite dec-false (k ≟ jₕ) λ k≡jₕ → ¬r (there (there (there (here k≡jₕ))))
167+
= ys[k]
168+
... | yes (here k≡i)
169+
with ys[k] ← ys-eval k
170+
rewrite dec-true (k ≟ i) k≡i
171+
rewrite dec-false (k ≟ iₕ) λ k≡iₕ → ¬p (here (trans (sym k≡iₕ) k≡i))
172+
rewrite dec-false (k ≟ jₕ) λ k≡jₕ → ¬q (here (trans (sym k≡jₕ) k≡i))
173+
rewrite dec-false (j ≟ iₕ) λ j≡iₕ → ¬p (there (here (sym j≡iₕ)))
174+
rewrite dec-false (j ≟ jₕ) λ j≡jₕ → ¬q (there (here (sym j≡jₕ)))
175+
= ys[k]
176+
... | yes (there (here k≡j))
177+
with ys[k] ← ys-eval k
178+
rewrite dec-false (k ≟ i) λ k≡i → i≢j (trans (sym k≡i) k≡j)
179+
rewrite dec-true (k ≟ j) k≡j
180+
rewrite dec-false (k ≟ iₕ) λ k≡iₕ → ¬p (there (here (trans (sym k≡iₕ) k≡j)))
181+
rewrite dec-false (k ≟ jₕ) λ k≡jₕ → ¬q (there (here (trans (sym k≡jₕ) k≡j)))
182+
rewrite dec-false (i ≟ iₕ) λ i≡iₕ → ¬p (here (sym i≡iₕ))
183+
rewrite dec-false (i ≟ jₕ) λ i≡jₕ → ¬q (here (sym i≡jₕ))
184+
= ys[k]
185+
... | yes (there (there (here k≡iₕ)))
186+
with ys[jₕ] ← ys-eval jₕ
187+
rewrite dec-false (k ≟ i) λ k≡i → ¬p (here (trans (sym k≡iₕ) k≡i))
188+
rewrite dec-false (k ≟ j) λ k≡j → ¬p (there (here (trans (sym k≡iₕ) k≡j)))
189+
rewrite dec-true (k ≟ iₕ) k≡iₕ
190+
rewrite dec-false (jₕ ≟ i) λ jₕ≡i → ¬q (here jₕ≡i)
191+
rewrite dec-false (jₕ ≟ j) λ jₕ≡j → ¬q (there (here jₕ≡j))
192+
= ys[jₕ]
193+
... | yes (there (there (there (here k≡jₕ))))
194+
with ys[iₕ] ← ys-eval iₕ
195+
rewrite dec-false (k ≟ i) λ k≡i → ¬q (here (trans (sym k≡jₕ) k≡i))
196+
rewrite dec-false (k ≟ j) λ k≡j → ¬q (there (here (trans (sym k≡jₕ) k≡j)))
197+
rewrite dec-false (k ≟ iₕ) λ k≡iₕ → iₕ≢jₕ (trans (sym k≡iₕ) k≡jₕ)
198+
rewrite dec-true (k ≟ jₕ) k≡jₕ
199+
rewrite dec-false (iₕ ≟ i) λ iₕ≡i → ¬p (here iₕ≡i)
200+
rewrite dec-false (iₕ ≟ j) λ iₕ≡j → ¬p (there (here iₕ≡j))
201+
= ys[iₕ]
202+
... | yes (here jₕ≡i)
203+
rewrite dec-false (i ≟ iₕ) λ i≡iₕ → iₕ≢jₕ (sym (trans jₕ≡i i≡iₕ))
204+
rewrite dec-true (i ≟ jₕ) (sym jₕ≡i)
205+
rewrite dec-false (j ≟ iₕ) λ j≡iₕ → ¬p (there (here (sym j≡iₕ)))
206+
rewrite dec-false (j ≟ jₕ) λ j≡jₕ → i≢j (sym (trans j≡jₕ jₕ≡i))
207+
= {!!}
208+
where
209+
xs≢[] : xs ≢ []
210+
xs≢[] refl = i≢j (sym xs[j]≡i)
211+
212+
k≢0 : k ≢ 0
213+
k≢0 k≡0 = xs≢[] (L.length[xs]≡0⇒xs≡[] (trans (ℕ.suc-injective 1+∣xs∣≡1+k) k≡0))
214+
215+
k′ : ℕ
216+
k′ = ℕ.pred k
217+
218+
rec = machine iₕ (λ iₕ≡j → ¬p (there (here iₕ≡j))) xs xs[i]≡j {!xs[j]≡i!} {k′} {!!}
219+
220+
221+
... | yes (there (here jₕ≡j)) = {!!}
222+
machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j {k} 1+∣xs∣≡1+k | yes (here iₕ≡i) with jₕ ≟ j
223+
... | no jₕ≢j = {!!}
224+
... | yes jₕ≡j = xs , prop , ℕ.suc-injective 1+∣xs∣≡1+k
225+
where
226+
prop : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ eval xs
227+
prop k rewrite iₕ≡i rewrite jₕ≡j = cong (eval xs ⟨$⟩ʳ_) (PC.transpose-inverse′ i j)
228+
machine i i≢j ((iₕ , jₕ , iₕ≢jₕ) ∷ xs) xs[i]≡j {k} 1+∣xs∣≡1+k | yes (there (here iₕ≡j)) with jₕ ≟ i
229+
... | no jₕ≢i = {!!}
230+
... | yes jₕ≡i = xs , prop , ℕ.suc-injective 1+∣xs∣≡1+k
231+
where
232+
prop : transpose i j ∘ₚ transpose iₕ jₕ ∘ₚ eval xs ≈ eval xs
233+
prop k rewrite iₕ≡j rewrite jₕ≡i = cong (eval xs ⟨$⟩ʳ_) (PC.transpose-inverse j i)
234+
235+
{-
236+
237+
p₃ : ∀ (xs : TranspositionList n) → eval xs ≈ id → parity (L.length xs) ≡ 0ℙ
238+
p₃ [] p = refl
239+
p₃ xs@(_ ∷ []) p = contradiction refl (eval[xs]≈id⇒length[xs]≢1 xs p)
240+
p₃ xs@(_ ∷ _ ∷ _) p with p₂ xs p refl
241+
... | ys , p′ , ys-shorter = {!parity (L.length ys)!}
242+
243+
p₄ : ∀ (xs ys : TranspositionList n) → eval xs ≈ eval ys → parity (L.length xs) ≡ parity (L.length ys)
244+
p₄ = {!!}
245+
-}

‎src/Data/List/Properties.agda

+3
Original file line numberDiff line numberDiff line change
@@ -75,6 +75,9 @@ module _ {x y : A} {xs ys : List A} where
7575
≡-dec _≟_ [] (y ∷ ys) = no λ()
7676
≡-dec _≟_ (x ∷ xs) (y ∷ ys) = ∷-dec (x ≟ y) (≡-dec _≟_ xs ys)
7777

78+
length[xs]≡0⇒xs≡[] : {xs : List A} → length xs ≡ 0 → xs ≡ []
79+
length[xs]≡0⇒xs≡[] {xs = []} _ = refl
80+
7881
------------------------------------------------------------------------
7982
-- map
8083

0 commit comments

Comments
 (0)