# HG changeset patch # User Shinji KONO # Date 1610155088 -32400 # Node ID 6d1619d9f880673daf35beb5d483b79ea2bbe0bc # Parent a5b3061f15eed2446f6520bc6210d567db1d5881 library diff -r a5b3061f15ee -r 6d1619d9f880 FLComm.agda --- a/FLComm.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,174 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) -module FLComm (n : ℕ) where - -open import Level renaming ( suc to Suc ; zero to Zero ) hiding (lift) -open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) -open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) -open import Data.Fin.Permutation -open import Data.Nat.Properties -open import Relation.Binary.PropositionalEquality hiding ( [_] ) renaming ( sym to ≡-sym ) -open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev ) -open import Data.Product hiding (_,_ ) -open import Relation.Nullary -open import Data.Unit hiding (_≤_) -open import Data.Empty -open import Relation.Binary.Core -open import Relation.Binary.Definitions hiding (Symmetric ) -open import logic -open import nat - -open import FLutil -open import Putil -import Solvable -open import Symmetric - --- infixr 100 _::_ - -open import Relation.Nary using (⌊_⌋) -open import Data.List.Fresh hiding ([_]) -open import Data.List.Fresh.Relation.Unary.Any - -open import Algebra -open Group (Symmetric n) hiding (refl) -open Solvable (Symmetric n) -open _∧_ --- open import Relation.Nary using (⌊_⌋) -open import Relation.Nullary.Decidable hiding (⌊_⌋) - -open import fin - --- all cobmbination in P and Q (could be more general) -record AnyComm {n m l : ℕ} (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where - field - commList : FList l - commAny : (p : FL n) (q : FL m) - → Any ( p ≡_ ) P → Any ( q ≡_ ) Q - → Any (fpq p q ≡_) commList - -------------- --- (p,q) (p,qn) .... (p,q0) --- pn,q --- : AnyComm FL0 FL0 P Q --- p0,q - -open AnyComm -anyComm : {n m l : ℕ } → (P : FList n) (Q : FList m) → (fpq : (p : FL n) (q : FL m) → FL l) → AnyComm P Q fpq -anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () } -anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () } -anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () } -anyComm {n} {m} {l} (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q) ; commAny = anyc0n } where - commListP : (P1 : FList n) → FList l - commListP [] = commList (anyComm P Q fpq) - commListP (cons p₁ P1 x) = FLinsert (fpq p₁ q) (commListP P1) - commListQ : (Q1 : FList m) → FList l - commListQ [] = commListP P - commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1) - anyc0n : (p₁ : FL n) (q₁ : FL m) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) - → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q)) - anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q ) - anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where - anyc01 : (Q1 : FList m) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) - anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _ - anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any) - anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where - anyc03 : (P1 : FList n) → Any (_≡_ p₁) P1 → Any (_≡_ (fpq p₁ q₁)) (commListP P1) - anyc03 (cons a P1 x) (here refl) = x∈FLins _ _ - anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any) - anyc02 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) - anyc02 [] = anyc03 P anyp - anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1) - anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where - anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1) - anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq - anyc05 (cons a P1 x) = insAny _ (anyc05 P1) - anyc04 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) - anyc04 [] = anyc05 P - anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1) - -------------- --- # 0 :: # 0 :: # 0 : # 0 :: f0 --- # 0 :: # 0 :: # 1 : # 0 :: f0 --- # 0 :: # 1 :: # 0 : # 0 :: f0 --- # 0 :: # 1 :: # 1 : # 0 :: f0 --- # 0 :: # 2 :: # 0 : # 0 :: f0 --- ... --- # 3 :: # 2 :: # 0 : # 0 :: f0 --- # 3 :: # 2 :: # 1 : # 0 :: f0 - --- all FL -record AnyFL (n : ℕ) : Set where - field - allFL : FList n - anyP : (x : FL n) → Any (x ≡_ ) allFL - -open AnyFL - --- all FL as all combination --- anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n) - -anyFL01 : (n : ℕ) → AnyFL (suc n) -anyFL01 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } where - anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y - anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl -anyFL01 (suc n) = record { allFL = commList anyC ; anyP = anyFL02 } where - anyFL05 : {n i : ℕ} → (i < suc n) → FList (suc n) - anyFL05 {_} {0} (s≤s z≤n) = zero :: FL0 ∷# [] - anyFL05 {n} {suc i} (s≤s i ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) ) - anyC = anyComm (anyFL05 a : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥ -f-<> (f x x₁ -f-<> (f (f (f lt lt2 - -f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥ -f-≡< refl (f lt (f ¬a ¬b c = tri> (λ lt → f-<> lt (f lt (f ¬a₁ ¬b c = tri> (λ lt → f-<> lt (f ¬a ¬b c = no ( ¬a ) - -_f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set -_f≤_ x y = (x ≡ y ) ∨ (x f< y ) - -FL0 : {n : ℕ } → FL n -FL0 {zero} = f0 -FL0 {suc n} = zero :: FL0 - -fmax : { n : ℕ } → FL n -fmax {zero} = f0 -fmax {suc n} = fromℕ< a (fmax1 x) lt where - fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a ¬a ¬b c = ⊥-elim (fmax< c) - -x≤fmax : {n : ℕ } → {x : FL n} → x f≤ fmax -x≤fmax {n} {x} with FLcmp x fmax -... | tri< a ¬b ¬c = case2 a -... | tri≈ ¬a b ¬c = case1 b -... | tri> ¬a ¬b c = ⊥-elim ( fmax< c ) - -open import Data.Nat.Properties using ( ≤-trans ; <-trans ) -fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n -fsuc {n} (x :: y) (f ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) -FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a ¬a ¬b b ¬a ¬b b ¬a ¬b b ¬a ¬b a ¬a ¬b a ¬a ¬b c = here refl -insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl -insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any) - --- FLinsert membership - -module FLMB { n : ℕ } where - - FL-Setoid : Setoid Level.zero Level.zero - FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }} - - open import Data.List.Fresh.Membership.Setoid FL-Setoid - - FLinsert-mb : (x : FL n ) → (xs : FList n) → x ∈ FLinsert x xs - FLinsert-mb x xs = x∈FLins {n} x xs - - diff -r a5b3061f15ee -r 6d1619d9f880 Galois.agda-lib --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Galois.agda-lib Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,2 @@ +name: Galois +depend: standard-library include: src diff -r a5b3061f15ee -r 6d1619d9f880 Galois.agda-pkg --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/Galois.agda-pkg Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,12 @@ +name: Galois +version: v0.0.1 + + +homepage: https://ie.u-ryukyu.ac.jp/~kono +license: MIT +license-file: LICENSE.md +source-repository: https://github.com/shinji-kono/Galois +tested-with: 2.6.2-102d9c8 +description: Solvability on Symmetry + +# End diff -r a5b3061f15ee -r 6d1619d9f880 Gutil.agda --- a/Gutil.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,130 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module Gutil {n m : Level} (G : Group n m ) where - -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - - -open Group G - -import Relation.Binary.Reasoning.Setoid as EqReasoning - -gsym = Algebra.Group.sym G -grefl = Algebra.Group.refl G -gtrans = Algebra.Group.trans G - -lemma3 : ε ≈ ε ⁻¹ -lemma3 = begin - ε ≈⟨ gsym (proj₁ inverse _) ⟩ - ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ - ε ⁻¹ - ∎ where open EqReasoning (Algebra.Group.setoid G) - -lemma6 : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f -lemma6 {f} = begin - ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩ - ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩ - (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩ - f ∙ ( f ⁻¹ ∙ ( f ⁻¹ ) ⁻¹ ) ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩ - f ∙ ε ≈⟨ proj₂ identity _ ⟩ - f - ∎ where open EqReasoning (Algebra.Group.setoid G) - -≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g -≡→≈ refl = grefl - ---- --- to avoid assoc storm, flatten multiplication according to the template --- - -data MP : Carrier → Set (Level.suc n) where - am : (x : Carrier ) → MP x - _o_ : {x y : Carrier } → MP x → MP y → MP ( x ∙ y ) - -mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier -mpf (am x) y = x ∙ y -mpf (m o m₁) y = mpf m ( mpf m₁ y ) - -mp-flatten : {x : Carrier } → (m : MP x ) → Carrier -mp-flatten m = mpf m ε - -mpl1 : Carrier → {x : Carrier } → MP x → Carrier -mpl1 x (am y) = x ∙ y -mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1 - -mpl : {x z : Carrier } → MP x → MP z → Carrier -mpl (am x) m = mpl1 x m -mpl (m o m1) m2 = mpl m (m1 o m2) - -mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier -mp-flattenl m = mpl m (am ε) - -test1 : ( f g : Carrier ) → Carrier -test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) - -test2 : ( f g : Carrier ) → test1 f g ≡ g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙ (f ∙ g) ⁻¹ ∙ ε -test2 f g = _≡_.refl - -test3 : ( f g : Carrier ) → Carrier -test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) - -test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) -test4 f g = _≡_.refl - - -∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m -∙-flatten {x} (am x) = gsym (proj₂ identity _) -∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q ) -∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where - mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r - mp-cong (am x) q=r = ∙-cong grefl q=r - mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r ) - mp-assoc : {p q r : Carrier} → (P : MP p) → mpf P q ∙ r ≈ mpf P (q ∙ r ) - mp-assoc (am x) = assoc _ _ _ - mp-assoc {p} {q} {r} (P o P₁) = begin - mpf P (mpf P₁ q) ∙ r ≈⟨ mp-assoc P ⟩ - mpf P (mpf P₁ q ∙ r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q ∙ r)) - ∎ where open EqReasoning (Algebra.Group.setoid G) - lemma9 : (x y z : Carrier) → x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε → x ∙ y ∙ z ≈ mp-flatten ((p o q) o r) - lemma9 x y z t s = begin - x ∙ y ∙ z ≈⟨ ∙-cong t grefl ⟩ - mpf p (mpf q ε) ∙ z ≈⟨ mp-assoc p ⟩ - mpf p (mpf q ε ∙ z) ≈⟨ mp-cong p (mp-assoc q ) ⟩ - mpf p (mpf q (ε ∙ z)) ≈⟨ mp-cong p (mp-cong q (proj₁ identity _ )) ⟩ - mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩ - mpf p (mpf q (mpf r ε)) - ∎ where open EqReasoning (Algebra.Group.setoid G) - -grepl : { x y0 y1 z : Carrier } → x ∙ y0 ≈ y1 → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z -grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl ) - -grm : { x y0 y1 z : Carrier } → x ∙ y0 ≈ ε → x ∙ ( y0 ∙ z ) ≈ z -grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ ) - --- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m --- ∙-flattenl (am x) = gsym (proj₂ identity _) --- ∙-flattenl (q o am x) with ∙-flattenl q -- x₁ ∙ x ≈ mpl q (am x o am ε) , t : x₁ ≈ mpl q (am ε) --- ... | t = {!!} --- ∙-flattenl (q o (x o y )) with ∙-flattenl q --- ... | t = gtrans (gsym (assoc _ _ _ )) {!!} - -lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ -lemma5 f g = begin - g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ - g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ - g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) ⟩ - g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩ - g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩ - g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ gsym (assoc _ _ _) ⟩ - (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩ - (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ - (f ∙ g) ⁻¹ - ∎ where open EqReasoning (Algebra.Group.setoid G) - diff -r a5b3061f15ee -r 6d1619d9f880 LICENSE.md --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/LICENSE.md Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,19 @@ +Copyright (c) 2020 + +Permission is hereby granted, free of charge, to any person obtaining a copy +of this software and associated documentation files (the "Software"), to deal +in the Software without restriction, including without limitation the rights +to use, copy, modify, merge, publish, distribute, sublicense, and/or sell +copies of the Software, and to permit persons to whom the Software is +furnished to do so, subject to the following conditions: + +The above copyright notice and this permission notice shall be included in all +copies or substantial portions of the Software. + +THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR +IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, +FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE +AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER +LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM, +OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE +SOFTWARE. diff -r a5b3061f15ee -r 6d1619d9f880 Putil.agda --- a/Putil.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,703 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -module Putil where - -open import Level hiding ( suc ; zero ) -open import Algebra -open import Algebra.Structures -open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) -open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) -open import Data.Fin.Permutation -open import Function hiding (id ; flip) -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function.LeftInverse using ( _LeftInverseOf_ ) -open import Function.Equality using (Π) -open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) -open import Data.Nat.Properties -- using (<-trans) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) -open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev ) -open import nat - -open import Symmetric - - -open import Relation.Nullary -open import Data.Empty -open import Relation.Binary.Core -open import Relation.Binary.Definitions -open import fin - --- An inductive construction of permutation - -pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) -pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where - p→ : Fin (suc n) → Fin (suc n) - p→ zero = zero - p→ (suc x) = suc ( perm ⟨$⟩ʳ x) - - p← : Fin (suc n) → Fin (suc n) - p← zero = zero - p← (suc x) = suc ( perm ⟨$⟩ˡ x) - - piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x - piso← zero = refl - piso← (suc x) = cong (λ k → suc k ) (inverseʳ perm) - - piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x - piso→ zero = refl - piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) - -pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) -pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where - p→ : Fin (suc (suc n)) → Fin (suc (suc n)) - p→ zero = suc zero - p→ (suc zero) = zero - p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) - - p← : Fin (suc (suc n)) → Fin (suc (suc n)) - p← zero = suc zero - p← (suc zero) = zero - p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) - - piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x - piso← zero = refl - piso← (suc zero) = refl - piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) - - piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x - piso→ zero = refl - piso→ (suc zero) = refl - piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) - -psawpn : {n : ℕ} → 1 < n → Permutation n n -psawpn {suc zero} (s≤s ()) -psawpn {suc n} (s≤s (s≤s x)) = pswap pid - -pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n -pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m ¬a ¬b c = x - - p← : Fin (suc (suc n)) → Fin (suc (suc n)) - p← zero = fromℕ< (s≤s (s≤s m≤n)) - p← (suc x) with <-cmp (toℕ x) (suc m) - ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin ¬a ¬b c = suc x - - mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m - mm = toℕ-fromℕ< (s≤s (s≤s m≤n)) - - mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin ¬a ¬b c = p16 (suc x) refl where - p16 : (y : Fin (suc (suc n))) → y ≡ suc x → p← y ≡ suc x - p16 zero eq = ⊥-elim ( nat-≡< (cong (λ k → suc (toℕ k) ) eq) (s≤s (s≤s (z≤n)))) - p16 (suc y) eq with <-cmp (toℕ y) (suc m) -- suc (suc m) < toℕ (suc x) - ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< refl ( ≤-trans c (subst (λ k → k < suc m) p17 a )) ) where - -- x = suc m case, c : suc (suc m) ≤ suc (toℕ x), a : suc (toℕ y) ≤ suc m, suc y ≡ suc x - p17 : toℕ y ≡ toℕ x - p17 with <-cmp (toℕ y) (toℕ x) | cong toℕ eq - ... | tri< a ¬b ¬c | seq = ⊥-elim ( nat-≡< seq (s≤s a) ) - ... | tri≈ ¬a b ¬c | seq = b - ... | tri> ¬a ¬b c | seq = ⊥-elim ( nat-≡< (sym seq) (s≤s c)) - ... | tri≈ ¬a b ¬c = eq - ... | tri> ¬a ¬b c₁ = eq - ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) ))) refl where - p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) → p← y ≡ suc x - p10 zero () - p10 (suc y) eq = p15 where - p12 : toℕ y ≡ suc (toℕ x) - p12 = begin - toℕ y - ≡⟨ cong (λ k → Data.Nat.pred (toℕ k)) eq ⟩ - toℕ (fromℕ< (≤-trans a (s≤s m≤n))) - ≡⟨ toℕ-fromℕ< {suc (toℕ x)} {suc n} (≤-trans a (s≤s m≤n)) ⟩ - suc (toℕ x) - ∎ - p15 : p← (suc y) ≡ suc x - 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 - ... | tri< a₁ ¬b ¬c = p11 where - p11 : fromℕ< (≤-trans (fin y = suc x → toℕ y < suc m - ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (subst (λ k → k < suc m) (sym p12) a )) - - piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x - piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm - ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t ) - ... | tri≈ ¬a b ¬c | t = refl - ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t ) - piso← (suc x) with <-cmp (toℕ x) (suc m) - ... | tri> ¬a ¬b c with <-cmp (toℕ (suc x)) (suc m) - ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-<> a (<-trans c a ¬a₁ ¬b₁ c₁ = refl - piso← (suc x) | tri≈ ¬a b ¬c with <-cmp (toℕ (suc x)) (suc m) - ... | tri< a ¬b ¬c₁ = ⊥-elim ( nat-≡< b (<-trans a ¬a₁ ¬b c = refl - piso← (suc x) | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a))) - ... | tri< a₁ ¬b₁ ¬c₁ = p0 where - p2 : suc (suc (toℕ x)) ≤ suc (suc n) - p2 = s≤s (fin ¬a ¬b c = ⊥-elim (nat-≤> c q ¬a ¬b c = ⊥-elim (nat-≤> c q 0 → Data.Nat.pred (toℕ f) < n -pred_ : Bool → Bool → Bool -true <=> true = true -false <=> false = true -_ <=> _ = false - -infixr 130 _\/_ -infixr 140 _/\_ - -open import Relation.Binary.PropositionalEquality - -≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B -≡-Bool-func {true} {true} a→b b→a = refl -≡-Bool-func {false} {true} a→b b→a with b→a refl -... | () -≡-Bool-func {true} {false} a→b b→a with a→b refl -... | () -≡-Bool-func {false} {false} a→b b→a = refl - -bool-≡-? : (a b : Bool) → Dec ( a ≡ b ) -bool-≡-? true true = yes refl -bool-≡-? true false = no (λ ()) -bool-≡-? false true = no (λ ()) -bool-≡-? false false = yes refl - -¬-bool-t : {a : Bool} → ¬ ( a ≡ true ) → a ≡ false -¬-bool-t {true} ne = ⊥-elim ( ne refl ) -¬-bool-t {false} ne = refl - -¬-bool-f : {a : Bool} → ¬ ( a ≡ false ) → a ≡ true -¬-bool-f {true} ne = refl -¬-bool-f {false} ne = ⊥-elim ( ne refl ) - -¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥ -¬-bool refl () - -lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ -lemma-∧-0 {true} {true} refl () -lemma-∧-0 {true} {false} () -lemma-∧-0 {false} {true} () -lemma-∧-0 {false} {false} () - -lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥ -lemma-∧-1 {true} {true} refl () -lemma-∧-1 {true} {false} () -lemma-∧-1 {false} {true} () -lemma-∧-1 {false} {false} () - -bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true -bool-and-tt refl refl = refl - -bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true -bool-∧→tt-0 {true} {true} refl = refl -bool-∧→tt-0 {false} {_} () - -bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true -bool-∧→tt-1 {true} {true} refl = refl -bool-∧→tt-1 {true} {false} () -bool-∧→tt-1 {false} {false} () - -bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b -bool-or-1 {false} {true} refl = refl -bool-or-1 {false} {false} refl = refl -bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a -bool-or-2 {true} {false} refl = refl -bool-or-2 {false} {false} refl = refl - -bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true -bool-or-3 {true} = refl -bool-or-3 {false} = refl - -bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true -bool-or-31 {true} {true} refl = refl -bool-or-31 {false} {true} refl = refl - -bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true -bool-or-4 {true} = refl -bool-or-4 {false} = refl - -bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true -bool-or-41 {true} {b} refl = refl - -bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false -bool-and-1 {false} {b} refl = refl -bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false -bool-and-2 {true} {false} refl = refl -bool-and-2 {false} {false} refl = refl - - diff -r a5b3061f15ee -r 6d1619d9f880 nat.agda --- a/nat.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,340 +0,0 @@ -{-# OPTIONS --allow-unsolved-metas #-} -module nat where - -open import Data.Nat -open import Data.Nat.Properties -open import Data.Empty -open import Relation.Nullary -open import Relation.Binary.PropositionalEquality -open import Relation.Binary.Core -open import Relation.Binary.Definitions -open import logic - - -nat-<> : { x y : ℕ } → x < y → y < x → ⊥ -nat-<> (s≤s x x : { x y : ℕ } → x ≤ y → y < x → ⊥ -nat-≤> (s≤s x x→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) ->→¬< (s≤s x→¬< x y → minus x y + y ≡ x -minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl -minus+n {zero} {suc y} (s≤s ()) -minus+n {suc x} {suc y} (s≤s lt) = begin - minus (suc x) (suc y) + suc y - ≡⟨ +-comm _ (suc y) ⟩ - suc y + minus x y - ≡⟨ cong ( λ k → suc k ) ( - begin - y + minus x y - ≡⟨ +-comm y _ ⟩ - minus x y + y - ≡⟨ minus+n {x} {y} lt ⟩ - x - ∎ - ) ⟩ - suc x - ∎ where open ≡-Reasoning - -sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m ) -sn-m=sn-m {0} {n} z≤n = refl -sn-m=sn-m {suc m} {suc n} (s≤s m0 : {x y : ℕ } → x < y → 0 < minus y x -minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n -minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt - -distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) -distr-minus-* {x} {zero} {z} = refl -distr-minus-* {x} {suc y} {z} with <-cmp x y -distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin - minus x (suc y) * z - ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin - minus x (suc y) * z + suc y * z - ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩ - ( minus x (suc y) + suc y ) * z - ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩ - x * z - ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩ - minus (x * z) (suc y * z) + suc y * z - ∎ ) where - open ≡-Reasoning - lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z - lt {x} {y} {z} le = *≤ le - -minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) -minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin - minus (minus x y) z + z - ≡⟨ minus+n {_} {z} lemma ⟩ - minus x y - ≡⟨ +m= {_} {_} {y} ( begin - minus x y + y - ≡⟨ minus+n {_} {y} lemma1 ⟩ - x - ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ - minus x (z + y) + (z + y) - ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ - minus x (z + y) + z + y - ∎ ) ⟩ - minus x (z + y) + z - ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ - minus x (y + z) + z - ∎ ) where - open ≡-Reasoning - lemma1 : suc x > y - lemma1 = x+y z - lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) - -minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M -minus-* {zero} {k} {n} lt = begin - minus k (suc n) * zero - ≡⟨ *-comm (minus k (suc n)) zero ⟩ - zero * minus k (suc n) - ≡⟨⟩ - 0 * minus k n - ≡⟨ *-comm 0 (minus k n) ⟩ - minus (minus k n * 0 ) 0 - ∎ where - open ≡-Reasoning -minus-* {suc m} {k} {n} lt with <-cmp k 1 -minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl -minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl -minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl -minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt -minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c -minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin - minus k (suc n) * M - ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ - minus (k * M ) ((suc n) * M) - ≡⟨⟩ - minus (k * M ) (M + n * M ) - ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ - minus (k * M ) ((n * M) + M ) - ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩ - minus (minus (k * M ) (n * M)) M - ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ - minus (minus k n * M ) M - ∎ where - M = suc m - lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m - lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y )) - lemma {suc n} {suc k} {m} lt = begin - suc (suc m + suc n * suc m) - ≡⟨⟩ - suc ( suc (suc n) * suc m) - ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ - suc (suc k * suc m) - ∎ where open ≤-Reasoning - open ≡-Reasoning - -open import Data.List - -ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1 -ℕL-inject refl = refl - -ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y -ℕL-inject-t refl = refl - -ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y ) -ℕL-eq? [] [] = yes refl -ℕL-eq? [] (x ∷ y) = no (λ ()) -ℕL-eq? (x ∷ x₁) [] = no (λ ()) -ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y -... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 ) -... | yes y1 | no n = no (λ e → n (ℕL-inject-t e)) -... | no n | t = no (λ e → n (ℕL-inject e)) - diff -r a5b3061f15ee -r 6d1619d9f880 src/FLComm.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/FLComm.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,174 @@ +{-# OPTIONS --allow-unsolved-metas #-} +open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) +module FLComm (n : ℕ) where + +open import Level renaming ( suc to Suc ; zero to Zero ) hiding (lift) +open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) +open import Data.Fin.Properties hiding ( <-trans ; ≤-refl ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin.Permutation +open import Data.Nat.Properties +open import Relation.Binary.PropositionalEquality hiding ( [_] ) renaming ( sym to ≡-sym ) +open import Data.List using (List; []; _∷_ ; length ; _++_ ; tail ) renaming (reverse to rev ) +open import Data.Product hiding (_,_ ) +open import Relation.Nullary +open import Data.Unit hiding (_≤_) +open import Data.Empty +open import Relation.Binary.Core +open import Relation.Binary.Definitions hiding (Symmetric ) +open import logic +open import nat + +open import FLutil +open import Putil +import Solvable +open import Symmetric + +-- infixr 100 _::_ + +open import Relation.Nary using (⌊_⌋) +open import Data.List.Fresh hiding ([_]) +open import Data.List.Fresh.Relation.Unary.Any + +open import Algebra +open Group (Symmetric n) hiding (refl) +open Solvable (Symmetric n) +open _∧_ +-- open import Relation.Nary using (⌊_⌋) +open import Relation.Nullary.Decidable hiding (⌊_⌋) + +open import fin + +-- all cobmbination in P and Q (could be more general) +record AnyComm {n m l : ℕ} (P : FList n) (Q : FList m) (fpq : (p : FL n) (q : FL m) → FL l) : Set where + field + commList : FList l + commAny : (p : FL n) (q : FL m) + → Any ( p ≡_ ) P → Any ( q ≡_ ) Q + → Any (fpq p q ≡_) commList + +------------- +-- (p,q) (p,qn) .... (p,q0) +-- pn,q +-- : AnyComm FL0 FL0 P Q +-- p0,q + +open AnyComm +anyComm : {n m l : ℕ } → (P : FList n) (Q : FList m) → (fpq : (p : FL n) (q : FL m) → FL l) → AnyComm P Q fpq +anyComm [] [] _ = record { commList = [] ; commAny = λ _ _ () } +anyComm [] (cons q Q qr) _ = record { commList = [] ; commAny = λ _ _ () } +anyComm (cons p P pr) [] _ = record { commList = [] ; commAny = λ _ _ _ () } +anyComm {n} {m} {l} (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q) ; commAny = anyc0n } where + commListP : (P1 : FList n) → FList l + commListP [] = commList (anyComm P Q fpq) + commListP (cons p₁ P1 x) = FLinsert (fpq p₁ q) (commListP P1) + commListQ : (Q1 : FList m) → FList l + commListQ [] = commListP P + commListQ (cons q₁ Q1 qr₁) = FLinsert (fpq p q₁) (commListQ Q1) + anyc0n : (p₁ : FL n) (q₁ : FL m) → Any (_≡_ p₁) (cons p P pr) → Any (_≡_ q₁) (cons q Q qr) + → Any (_≡_ (fpq p₁ q₁)) (FLinsert (fpq p q) (commListQ Q)) + anyc0n p₁ q₁ (here refl) (here refl) = x∈FLins _ (commListQ Q ) + anyc0n p₁ q₁ (here refl) (there anyq) = insAny (commListQ Q) (anyc01 Q anyq) where + anyc01 : (Q1 : FList m) → Any (_≡_ q₁) Q1 → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) + anyc01 (cons q Q1 qr₂) (here refl) = x∈FLins _ _ + anyc01 (cons q₂ Q1 qr₂) (there any) = insAny _ (anyc01 Q1 any) + anyc0n p₁ q₁ (there anyp) (here refl) = insAny _ (anyc02 Q) where + anyc03 : (P1 : FList n) → Any (_≡_ p₁) P1 → Any (_≡_ (fpq p₁ q₁)) (commListP P1) + anyc03 (cons a P1 x) (here refl) = x∈FLins _ _ + anyc03 (cons a P1 x) (there any) = insAny _ ( anyc03 P1 any) + anyc02 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) + anyc02 [] = anyc03 P anyp + anyc02 (cons a Q1 x) = insAny _ (anyc02 Q1) + anyc0n p₁ q₁ (there anyp) (there anyq) = insAny (commListQ Q) (anyc04 Q) where + anyc05 : (P1 : FList n) → Any (_≡_ (fpq p₁ q₁)) (commListP P1) + anyc05 [] = commAny (anyComm P Q fpq) p₁ q₁ anyp anyq + anyc05 (cons a P1 x) = insAny _ (anyc05 P1) + anyc04 : (Q1 : FList m) → Any (_≡_ (fpq p₁ q₁)) (commListQ Q1) + anyc04 [] = anyc05 P + anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1) + +------------- +-- # 0 :: # 0 :: # 0 : # 0 :: f0 +-- # 0 :: # 0 :: # 1 : # 0 :: f0 +-- # 0 :: # 1 :: # 0 : # 0 :: f0 +-- # 0 :: # 1 :: # 1 : # 0 :: f0 +-- # 0 :: # 2 :: # 0 : # 0 :: f0 +-- ... +-- # 3 :: # 2 :: # 0 : # 0 :: f0 +-- # 3 :: # 2 :: # 1 : # 0 :: f0 + +-- all FL +record AnyFL (n : ℕ) : Set where + field + allFL : FList n + anyP : (x : FL n) → Any (x ≡_ ) allFL + +open AnyFL + +-- all FL as all combination +-- anyComm ( #0 :: FL0 ... # n :: FL0 ) (all n) (λ p q → FLpos p :: q ) = all (suc n) + +anyFL01 : (n : ℕ) → AnyFL (suc n) +anyFL01 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } where + anyFL2 : (x : FL 1) → (y : FList 1) → y ≡ ((zero :: f0) ∷# []) → Any (_≡_ x) y + anyFL2 (zero :: f0) .(cons (zero :: f0) [] (Level.lift tt)) refl = here refl +anyFL01 (suc n) = record { allFL = commList anyC ; anyP = anyFL02 } where + anyFL05 : {n i : ℕ} → (i < suc n) → FList (suc n) + anyFL05 {_} {0} (s≤s z≤n) = zero :: FL0 ∷# [] + anyFL05 {n} {suc i} (s≤s i ¬a ¬b c = ⊥-elim ( nat-≤> c (s≤s lt) ) + anyC = anyComm (anyFL05 a : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥ +f-<> (f x x₁ +f-<> (f (f (f lt lt2 + +f-≡< : {n : ℕ } {x : FL n } {y : FL n} → x ≡ y → y f< x → ⊥ +f-≡< refl (f lt (f ¬a ¬b c = tri> (λ lt → f-<> lt (f lt (f ¬a₁ ¬b c = tri> (λ lt → f-<> lt (f ¬a ¬b c = no ( ¬a ) + +_f≤_ : {n : ℕ } (x : FL n ) (y : FL n) → Set +_f≤_ x y = (x ≡ y ) ∨ (x f< y ) + +FL0 : {n : ℕ } → FL n +FL0 {zero} = f0 +FL0 {suc n} = zero :: FL0 + +fmax : { n : ℕ } → FL n +fmax {zero} = f0 +fmax {suc n} = fromℕ< a (fmax1 x) lt where + fmax1 : {n : ℕ } → (x : Fin (suc n)) → toℕ x ≤ toℕ (fromℕ< {n} a ¬a ¬b c = ⊥-elim (fmax< c) + +x≤fmax : {n : ℕ } → {x : FL n} → x f≤ fmax +x≤fmax {n} {x} with FLcmp x fmax +... | tri< a ¬b ¬c = case2 a +... | tri≈ ¬a b ¬c = case1 b +... | tri> ¬a ¬b c = ⊥-elim ( fmax< c ) + +open import Data.Nat.Properties using ( ≤-trans ; <-trans ) +fsuc : { n : ℕ } → (x : FL n ) → x f< fmax → FL n +fsuc {n} (x :: y) (f ¬a ¬b lt = cons a ( x ∷# [] ) ( Level.lift (fromWitness lt) , Level.lift tt ) +FLinsert {suc n} x (cons a y yr) | tri> ¬a ¬b a ¬a ¬b b ¬a ¬b b ¬a ¬b b ¬a ¬b a ¬a ¬b a ¬a ¬b c = here refl +insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (here refl) | tri> ¬a ¬b c = here refl +insAny {suc n} {x} {h} (cons a (cons a₁ L x₁) xr) (there any) | tri> ¬a ¬b c = there (insAny (cons a₁ L x₁) any) + +-- FLinsert membership + +module FLMB { n : ℕ } where + + FL-Setoid : Setoid Level.zero Level.zero + FL-Setoid = record { Carrier = FL n ; _≈_ = _≡_ ; isEquivalence = record { sym = sym ; refl = refl ; trans = trans }} + + open import Data.List.Fresh.Membership.Setoid FL-Setoid + + FLinsert-mb : (x : FL n ) → (xs : FList n) → x ∈ FLinsert x xs + FLinsert-mb x xs = x∈FLins {n} x xs + + diff -r a5b3061f15ee -r 6d1619d9f880 src/Gutil.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Gutil.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,130 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module Gutil {n m : Level} (G : Group n m ) where + +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + + +open Group G + +import Relation.Binary.Reasoning.Setoid as EqReasoning + +gsym = Algebra.Group.sym G +grefl = Algebra.Group.refl G +gtrans = Algebra.Group.trans G + +lemma3 : ε ≈ ε ⁻¹ +lemma3 = begin + ε ≈⟨ gsym (proj₁ inverse _) ⟩ + ε ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ + ε ⁻¹ + ∎ where open EqReasoning (Algebra.Group.setoid G) + +lemma6 : {f : Carrier } → ( f ⁻¹ ) ⁻¹ ≈ f +lemma6 {f} = begin + ( f ⁻¹ ) ⁻¹ ≈⟨ gsym ( proj₁ identity _) ⟩ + ε ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ ∙-cong (gsym ( proj₂ inverse _ )) grefl ⟩ + (f ∙ f ⁻¹ ) ∙ ( f ⁻¹ ) ⁻¹ ≈⟨ assoc _ _ _ ⟩ + f ∙ ( f ⁻¹ ∙ ( f ⁻¹ ) ⁻¹ ) ≈⟨ ∙-cong grefl (proj₂ inverse _) ⟩ + f ∙ ε ≈⟨ proj₂ identity _ ⟩ + f + ∎ where open EqReasoning (Algebra.Group.setoid G) + +≡→≈ : {f g : Carrier } → f ≡ g → f ≈ g +≡→≈ refl = grefl + +--- +-- to avoid assoc storm, flatten multiplication according to the template +-- + +data MP : Carrier → Set (Level.suc n) where + am : (x : Carrier ) → MP x + _o_ : {x y : Carrier } → MP x → MP y → MP ( x ∙ y ) + +mpf : {x : Carrier } → (m : MP x ) → Carrier → Carrier +mpf (am x) y = x ∙ y +mpf (m o m₁) y = mpf m ( mpf m₁ y ) + +mp-flatten : {x : Carrier } → (m : MP x ) → Carrier +mp-flatten m = mpf m ε + +mpl1 : Carrier → {x : Carrier } → MP x → Carrier +mpl1 x (am y) = x ∙ y +mpl1 x (y o y1) = mpl1 ( mpl1 x y ) y1 + +mpl : {x z : Carrier } → MP x → MP z → Carrier +mpl (am x) m = mpl1 x m +mpl (m o m1) m2 = mpl m (m1 o m2) + +mp-flattenl : {x : Carrier } → (m : MP x ) → Carrier +mp-flattenl m = mpl m (am ε) + +test1 : ( f g : Carrier ) → Carrier +test1 f g = mp-flattenl ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) + +test2 : ( f g : Carrier ) → test1 f g ≡ g ⁻¹ ∙ f ⁻¹ ∙ f ∙ g ∙ (f ∙ g) ⁻¹ ∙ ε +test2 f g = _≡_.refl + +test3 : ( f g : Carrier ) → Carrier +test3 f g = mp-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) + +test4 : ( f g : Carrier ) → test3 f g ≡ g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) +test4 f g = _≡_.refl + + +∙-flatten : {x : Carrier } → (m : MP x ) → x ≈ mp-flatten m +∙-flatten {x} (am x) = gsym (proj₂ identity _) +∙-flatten {_} (am x o q) = ∙-cong grefl ( ∙-flatten q ) +∙-flatten (_o_ {_} {z} (_o_ {x} {y} p q) r) = lemma9 _ _ _ ( ∙-flatten {x ∙ y } (p o q )) ( ∙-flatten {z} r ) where + mp-cong : {p q r : Carrier} → (P : MP p) → q ≈ r → mpf P q ≈ mpf P r + mp-cong (am x) q=r = ∙-cong grefl q=r + mp-cong (P o P₁) q=r = mp-cong P ( mp-cong P₁ q=r ) + mp-assoc : {p q r : Carrier} → (P : MP p) → mpf P q ∙ r ≈ mpf P (q ∙ r ) + mp-assoc (am x) = assoc _ _ _ + mp-assoc {p} {q} {r} (P o P₁) = begin + mpf P (mpf P₁ q) ∙ r ≈⟨ mp-assoc P ⟩ + mpf P (mpf P₁ q ∙ r) ≈⟨ mp-cong P (mp-assoc P₁) ⟩ mpf P ((mpf P₁) (q ∙ r)) + ∎ where open EqReasoning (Algebra.Group.setoid G) + lemma9 : (x y z : Carrier) → x ∙ y ≈ mpf p (mpf q ε) → z ≈ mpf r ε → x ∙ y ∙ z ≈ mp-flatten ((p o q) o r) + lemma9 x y z t s = begin + x ∙ y ∙ z ≈⟨ ∙-cong t grefl ⟩ + mpf p (mpf q ε) ∙ z ≈⟨ mp-assoc p ⟩ + mpf p (mpf q ε ∙ z) ≈⟨ mp-cong p (mp-assoc q ) ⟩ + mpf p (mpf q (ε ∙ z)) ≈⟨ mp-cong p (mp-cong q (proj₁ identity _ )) ⟩ + mpf p (mpf q z) ≈⟨ mp-cong p (mp-cong q s) ⟩ + mpf p (mpf q (mpf r ε)) + ∎ where open EqReasoning (Algebra.Group.setoid G) + +grepl : { x y0 y1 z : Carrier } → x ∙ y0 ≈ y1 → x ∙ ( y0 ∙ z ) ≈ y1 ∙ z +grepl eq = gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl ) + +grm : { x y0 y1 z : Carrier } → x ∙ y0 ≈ ε → x ∙ ( y0 ∙ z ) ≈ z +grm eq = gtrans ( gtrans (gsym (assoc _ _ _ )) (∙-cong eq grefl )) ( proj₁ identity _ ) + +-- ∙-flattenl : {x : Carrier } → (m : MP x ) → x ≈ mp-flattenl m +-- ∙-flattenl (am x) = gsym (proj₂ identity _) +-- ∙-flattenl (q o am x) with ∙-flattenl q -- x₁ ∙ x ≈ mpl q (am x o am ε) , t : x₁ ≈ mpl q (am ε) +-- ... | t = {!!} +-- ∙-flattenl (q o (x o y )) with ∙-flattenl q +-- ... | t = gtrans (gsym (assoc _ _ _ )) {!!} + +lemma5 : (f g : Carrier ) → g ⁻¹ ∙ f ⁻¹ ≈ (f ∙ g) ⁻¹ +lemma5 f g = begin + g ⁻¹ ∙ f ⁻¹ ≈⟨ gsym (proj₂ identity _) ⟩ + g ⁻¹ ∙ f ⁻¹ ∙ ε ≈⟨ gsym (∙-cong grefl (proj₂ inverse _ )) ⟩ + g ⁻¹ ∙ f ⁻¹ ∙ ( (f ∙ g) ∙ (f ∙ g) ⁻¹ ) ≈⟨ ∙-flatten ((am (g ⁻¹) o am (f ⁻¹) ) o ( (am f o am g) o am ((f ∙ g) ⁻¹ ))) ⟩ + g ⁻¹ ∙ (f ⁻¹ ∙ (f ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)))) ≈⟨ ∙-cong grefl (gsym (assoc _ _ _ )) ⟩ + g ⁻¹ ∙ ((f ⁻¹ ∙ f) ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε))) ≈⟨ ∙-cong grefl (gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _)) ⟩ + g ⁻¹ ∙ (g ∙ ((f ∙ g) ⁻¹ ∙ ε)) ≈⟨ gsym (assoc _ _ _) ⟩ + (g ⁻¹ ∙ g ) ∙ ((f ∙ g) ⁻¹ ∙ ε) ≈⟨ gtrans (∙-cong (proj₁ inverse _ ) grefl) (proj₁ identity _) ⟩ + (f ∙ g) ⁻¹ ∙ ε ≈⟨ proj₂ identity _ ⟩ + (f ∙ g) ⁻¹ + ∎ where open EqReasoning (Algebra.Group.setoid G) + diff -r a5b3061f15ee -r 6d1619d9f880 src/Putil.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/Putil.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,703 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module Putil where + +open import Level hiding ( suc ; zero ) +open import Algebra +open import Algebra.Structures +open import Data.Fin hiding ( _<_ ; _≤_ ; _-_ ; _+_ ; _≟_) +open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-irrelevant ; _≟_ ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin.Permutation +open import Function hiding (id ; flip) +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function.LeftInverse using ( _LeftInverseOf_ ) +open import Function.Equality using (Π) +open import Data.Nat -- using (ℕ; suc; zero; s≤s ; z≤n ) +open import Data.Nat.Properties -- using (<-trans) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Data.List using (List; []; _∷_ ; length ; _++_ ; head ; tail ) renaming (reverse to rev ) +open import nat + +open import Symmetric + + +open import Relation.Nullary +open import Data.Empty +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import fin + +-- An inductive construction of permutation + +pprep : {n : ℕ } → Permutation n n → Permutation (suc n) (suc n) +pprep {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where + p→ : Fin (suc n) → Fin (suc n) + p→ zero = zero + p→ (suc x) = suc ( perm ⟨$⟩ʳ x) + + p← : Fin (suc n) → Fin (suc n) + p← zero = zero + p← (suc x) = suc ( perm ⟨$⟩ˡ x) + + piso← : (x : Fin (suc n)) → p→ ( p← x ) ≡ x + piso← zero = refl + piso← (suc x) = cong (λ k → suc k ) (inverseʳ perm) + + piso→ : (x : Fin (suc n)) → p← ( p→ x ) ≡ x + piso→ zero = refl + piso→ (suc x) = cong (λ k → suc k ) (inverseˡ perm) + +pswap : {n : ℕ } → Permutation n n → Permutation (suc (suc n)) (suc (suc n )) +pswap {n} perm = permutation p→ p← record { left-inverse-of = piso→ ; right-inverse-of = piso← } where + p→ : Fin (suc (suc n)) → Fin (suc (suc n)) + p→ zero = suc zero + p→ (suc zero) = zero + p→ (suc (suc x)) = suc ( suc ( perm ⟨$⟩ʳ x) ) + + p← : Fin (suc (suc n)) → Fin (suc (suc n)) + p← zero = suc zero + p← (suc zero) = zero + p← (suc (suc x)) = suc ( suc ( perm ⟨$⟩ˡ x) ) + + piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x + piso← zero = refl + piso← (suc zero) = refl + piso← (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseʳ perm) + + piso→ : (x : Fin (suc (suc n)) ) → p← ( p→ x ) ≡ x + piso→ zero = refl + piso→ (suc zero) = refl + piso→ (suc (suc x)) = cong (λ k → suc (suc k) ) (inverseˡ perm) + +psawpn : {n : ℕ} → 1 < n → Permutation n n +psawpn {suc zero} (s≤s ()) +psawpn {suc n} (s≤s (s≤s x)) = pswap pid + +pfill : { n m : ℕ } → m ≤ n → Permutation m m → Permutation n n +pfill {n} {m} m≤n perm = pfill1 (n - m) (n-m ¬a ¬b c = x + + p← : Fin (suc (suc n)) → Fin (suc (suc n)) + p← zero = fromℕ< (s≤s (s≤s m≤n)) + p← (suc x) with <-cmp (toℕ x) (suc m) + ... | tri< a ¬b ¬c = fromℕ< (≤-trans (fin ¬a ¬b c = suc x + + mm : toℕ (fromℕ< {suc m} {suc (suc n)} (s≤s (s≤s m≤n))) ≡ suc m + mm = toℕ-fromℕ< (s≤s (s≤s m≤n)) + + mma : (x : Fin (suc n) ) → suc (toℕ x) ≤ suc m → toℕ ( fromℕ< (≤-trans (fin ¬a ¬b c = p16 (suc x) refl where + p16 : (y : Fin (suc (suc n))) → y ≡ suc x → p← y ≡ suc x + p16 zero eq = ⊥-elim ( nat-≡< (cong (λ k → suc (toℕ k) ) eq) (s≤s (s≤s (z≤n)))) + p16 (suc y) eq with <-cmp (toℕ y) (suc m) -- suc (suc m) < toℕ (suc x) + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< refl ( ≤-trans c (subst (λ k → k < suc m) p17 a )) ) where + -- x = suc m case, c : suc (suc m) ≤ suc (toℕ x), a : suc (toℕ y) ≤ suc m, suc y ≡ suc x + p17 : toℕ y ≡ toℕ x + p17 with <-cmp (toℕ y) (toℕ x) | cong toℕ eq + ... | tri< a ¬b ¬c | seq = ⊥-elim ( nat-≡< seq (s≤s a) ) + ... | tri≈ ¬a b ¬c | seq = b + ... | tri> ¬a ¬b c | seq = ⊥-elim ( nat-≡< (sym seq) (s≤s c)) + ... | tri≈ ¬a b ¬c = eq + ... | tri> ¬a ¬b c₁ = eq + ... | tri< a ¬b ¬c = p10 (fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) ))) refl where + p10 : (y : Fin (suc (suc n)) ) → y ≡ fromℕ< (≤-trans (s≤s a) (s≤s (s≤s m≤n) )) → p← y ≡ suc x + p10 zero () + p10 (suc y) eq = p15 where + p12 : toℕ y ≡ suc (toℕ x) + p12 = begin + toℕ y + ≡⟨ cong (λ k → Data.Nat.pred (toℕ k)) eq ⟩ + toℕ (fromℕ< (≤-trans a (s≤s m≤n))) + ≡⟨ toℕ-fromℕ< {suc (toℕ x)} {suc n} (≤-trans a (s≤s m≤n)) ⟩ + suc (toℕ x) + ∎ + p15 : p← (suc y) ≡ suc x + 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 + ... | tri< a₁ ¬b ¬c = p11 where + p11 : fromℕ< (≤-trans (fin y = suc x → toℕ y < suc m + ... | tri> ¬a ¬b c = ⊥-elim ( nat-<> c (subst (λ k → k < suc m) (sym p12) a )) + + piso← : (x : Fin (suc (suc n)) ) → p→ ( p← x ) ≡ x + piso← zero with <-cmp (toℕ (fromℕ< (s≤s (s≤s m≤n)))) (suc m) | mm + ... | tri< a ¬b ¬c | t = ⊥-elim ( ¬b t ) + ... | tri≈ ¬a b ¬c | t = refl + ... | tri> ¬a ¬b c | t = ⊥-elim ( ¬b t ) + piso← (suc x) with <-cmp (toℕ x) (suc m) + ... | tri> ¬a ¬b c with <-cmp (toℕ (suc x)) (suc m) + ... | tri< a ¬b₁ ¬c = ⊥-elim ( nat-<> a (<-trans c a ¬a₁ ¬b₁ c₁ = refl + piso← (suc x) | tri≈ ¬a b ¬c with <-cmp (toℕ (suc x)) (suc m) + ... | tri< a ¬b ¬c₁ = ⊥-elim ( nat-≡< b (<-trans a ¬a₁ ¬b c = refl + piso← (suc x) | tri< a ¬b ¬c with <-cmp (toℕ ( fromℕ< (≤-trans (fin ¬a ¬b₁ c = ⊥-elim ( ¬a (s≤s (mma x a))) + ... | tri< a₁ ¬b₁ ¬c₁ = p0 where + p2 : suc (suc (toℕ x)) ≤ suc (suc n) + p2 = s≤s (fin ¬a ¬b c = ⊥-elim (nat-≤> c q ¬a ¬b c = ⊥-elim (nat-≤> c q 0 → Data.Nat.pred (toℕ f) < n +pred_ : Bool → Bool → Bool +true <=> true = true +false <=> false = true +_ <=> _ = false + +infixr 130 _\/_ +infixr 140 _/\_ + +open import Relation.Binary.PropositionalEquality + +≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B +≡-Bool-func {true} {true} a→b b→a = refl +≡-Bool-func {false} {true} a→b b→a with b→a refl +... | () +≡-Bool-func {true} {false} a→b b→a with a→b refl +... | () +≡-Bool-func {false} {false} a→b b→a = refl + +bool-≡-? : (a b : Bool) → Dec ( a ≡ b ) +bool-≡-? true true = yes refl +bool-≡-? true false = no (λ ()) +bool-≡-? false true = no (λ ()) +bool-≡-? false false = yes refl + +¬-bool-t : {a : Bool} → ¬ ( a ≡ true ) → a ≡ false +¬-bool-t {true} ne = ⊥-elim ( ne refl ) +¬-bool-t {false} ne = refl + +¬-bool-f : {a : Bool} → ¬ ( a ≡ false ) → a ≡ true +¬-bool-f {true} ne = refl +¬-bool-f {false} ne = ⊥-elim ( ne refl ) + +¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥ +¬-bool refl () + +lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ +lemma-∧-0 {true} {true} refl () +lemma-∧-0 {true} {false} () +lemma-∧-0 {false} {true} () +lemma-∧-0 {false} {false} () + +lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥ +lemma-∧-1 {true} {true} refl () +lemma-∧-1 {true} {false} () +lemma-∧-1 {false} {true} () +lemma-∧-1 {false} {false} () + +bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true +bool-and-tt refl refl = refl + +bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true +bool-∧→tt-0 {true} {true} refl = refl +bool-∧→tt-0 {false} {_} () + +bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true +bool-∧→tt-1 {true} {true} refl = refl +bool-∧→tt-1 {true} {false} () +bool-∧→tt-1 {false} {false} () + +bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b +bool-or-1 {false} {true} refl = refl +bool-or-1 {false} {false} refl = refl +bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a +bool-or-2 {true} {false} refl = refl +bool-or-2 {false} {false} refl = refl + +bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true +bool-or-3 {true} = refl +bool-or-3 {false} = refl + +bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true +bool-or-31 {true} {true} refl = refl +bool-or-31 {false} {true} refl = refl + +bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true +bool-or-4 {true} = refl +bool-or-4 {false} = refl + +bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true +bool-or-41 {true} {b} refl = refl + +bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false +bool-and-1 {false} {b} refl = refl +bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false +bool-and-2 {true} {false} refl = refl +bool-and-2 {false} {false} refl = refl + + diff -r a5b3061f15ee -r 6d1619d9f880 src/nat.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/nat.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,340 @@ +{-# OPTIONS --allow-unsolved-metas #-} +module nat where + +open import Data.Nat +open import Data.Nat.Properties +open import Data.Empty +open import Relation.Nullary +open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Core +open import Relation.Binary.Definitions +open import logic + + +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ +nat-<> (s≤s x x : { x y : ℕ } → x ≤ y → y < x → ⊥ +nat-≤> (s≤s x x→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) +>→¬< (s≤s x→¬< x y → minus x y + y ≡ x +minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl +minus+n {zero} {suc y} (s≤s ()) +minus+n {suc x} {suc y} (s≤s lt) = begin + minus (suc x) (suc y) + suc y + ≡⟨ +-comm _ (suc y) ⟩ + suc y + minus x y + ≡⟨ cong ( λ k → suc k ) ( + begin + y + minus x y + ≡⟨ +-comm y _ ⟩ + minus x y + y + ≡⟨ minus+n {x} {y} lt ⟩ + x + ∎ + ) ⟩ + suc x + ∎ where open ≡-Reasoning + +sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m ) +sn-m=sn-m {0} {n} z≤n = refl +sn-m=sn-m {suc m} {suc n} (s≤s m0 : {x y : ℕ } → x < y → 0 < minus y x +minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n +minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt + +distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) +distr-minus-* {x} {zero} {z} = refl +distr-minus-* {x} {suc y} {z} with <-cmp x y +distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin + minus x (suc y) * z + suc y * z + ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩ + ( minus x (suc y) + suc y ) * z + ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩ + x * z + ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩ + minus (x * z) (suc y * z) + suc y * z + ∎ ) where + open ≡-Reasoning + lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z + lt {x} {y} {z} le = *≤ le + +minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) +minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin + minus (minus x y) z + z + ≡⟨ minus+n {_} {z} lemma ⟩ + minus x y + ≡⟨ +m= {_} {_} {y} ( begin + minus x y + y + ≡⟨ minus+n {_} {y} lemma1 ⟩ + x + ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ + minus x (z + y) + (z + y) + ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ + minus x (z + y) + z + y + ∎ ) ⟩ + minus x (z + y) + z + ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ + minus x (y + z) + z + ∎ ) where + open ≡-Reasoning + lemma1 : suc x > y + lemma1 = x+y z + lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) + +minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M +minus-* {zero} {k} {n} lt = begin + minus k (suc n) * zero + ≡⟨ *-comm (minus k (suc n)) zero ⟩ + zero * minus k (suc n) + ≡⟨⟩ + 0 * minus k n + ≡⟨ *-comm 0 (minus k n) ⟩ + minus (minus k n * 0 ) 0 + ∎ where + open ≡-Reasoning +minus-* {suc m} {k} {n} lt with <-cmp k 1 +minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl +minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl +minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl +minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt +minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c +minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin + minus k (suc n) * M + ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ + minus (k * M ) ((suc n) * M) + ≡⟨⟩ + minus (k * M ) (M + n * M ) + ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ + minus (k * M ) ((n * M) + M ) + ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩ + minus (minus (k * M ) (n * M)) M + ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ + minus (minus k n * M ) M + ∎ where + M = suc m + lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m + lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y )) + lemma {suc n} {suc k} {m} lt = begin + suc (suc m + suc n * suc m) + ≡⟨⟩ + suc ( suc (suc n) * suc m) + ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ + suc (suc k * suc m) + ∎ where open ≤-Reasoning + open ≡-Reasoning + +open import Data.List + +ℕL-inject : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → h ≡ h1 +ℕL-inject refl = refl + +ℕL-inject-t : {h h1 : ℕ } {x y : List ℕ } → h ∷ x ≡ h1 ∷ y → x ≡ y +ℕL-inject-t refl = refl + +ℕL-eq? : (x y : List ℕ ) → Dec (x ≡ y ) +ℕL-eq? [] [] = yes refl +ℕL-eq? [] (x ∷ y) = no (λ ()) +ℕL-eq? (x ∷ x₁) [] = no (λ ()) +ℕL-eq? (h ∷ x) (h1 ∷ y) with h ≟ h1 | ℕL-eq? x y +... | yes y1 | yes y2 = yes ( cong₂ (λ j k → j ∷ k ) y1 y2 ) +... | yes y1 | no n = no (λ e → n (ℕL-inject-t e)) +... | no n | t = no (λ e → n (ℕL-inject e)) + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym2.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym2.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,114 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym2 where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import FLutil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation + +sym2solvable : solvable (Symmetric 2) +solvable.dervied-length sym2solvable = 1 +solvable.end sym2solvable x d = solved x d where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 2) + -- open Group (Symmetric 2) using (_⁻¹) + + + p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid + p0 = pleq _ _ refl + + p0r : perm→FL pid ≡ ((# 0) :: ((# 0 ) :: f0)) + p0r = refl + + p1 : FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid + p1 = pleq _ _ refl + + p1r : perm→FL (pswap pid) ≡ ((# 1) :: ((# 0 ) :: f0)) + p1r = refl + + -- FL→iso : (fl : FL 2 ) → perm→FL ( FL→perm fl ) ≡ fl + -- FL→iso (zero :: (zero :: f0)) = refl + -- FL→iso ((suc zero) :: (zero :: f0)) = refl + + open _=p=_ + open ≡-Reasoning + + sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) + sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h + sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} | record { eq = h=00} = begin + [ g , h ] ⟨$⟩ʳ q + ≡⟨⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩ + h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) + ≡⟨⟩ + [ pid , h ] ⟨$⟩ʳ q + ≡⟨ peq (idcomtl h) q ⟩ + q + ∎ where + sym2lem1 : g =p= pid + sym2lem1 = FL-inject g=00 + sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00} = begin + [ g , h ] ⟨$⟩ʳ q + ≡⟨⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ peq sym2lem2 _ ⟩ + pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩ + pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨⟩ + [ g , pid ] ⟨$⟩ʳ q + ≡⟨ peq (idcomtr g) q ⟩ + q + ∎ where + sym2lem2 : h =p= pid + sym2lem2 = FL-inject h=00 + sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00}= begin + [ g , h ] ⟨$⟩ʳ q + ≡⟨⟩ + h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ peq (psym g=h ) _ ⟩ + g ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → g ⟨$⟩ʳ (g ⟨$⟩ʳ k) ) (peqˡ (psym g=h) _) ⟩ + g ⟨$⟩ʳ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) + ≡⟨ cong (λ k → g ⟨$⟩ʳ k) ( inverseʳ g ) ⟩ + g ⟨$⟩ʳ ( g ⟨$⟩ˡ q ) + ≡⟨ inverseʳ g ⟩ + q + ∎ where + g=h : g =p= h + g=h = FL-inject (trans g=00 (sym h=00)) + solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid + solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h } + solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d + ... | record { peq = f=e } = record { peq = λ q → cc q } where + cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q + cc q = begin + x ⟨$⟩ʳ q + ≡⟨ sym (f=g q) ⟩ + f ⟨$⟩ʳ q + ≡⟨ f=e q ⟩ + q + ∎ where open ≡-Reasoning + + + + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym2n.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym2n.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,51 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym2n where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + + +sym2solvable : solvable (Symmetric 2) +solvable.dervied-length sym2solvable = 1 +solvable.end sym2solvable x d = solved1 x d where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 2) + open import FLutil + open import Data.List.Fresh hiding ([_]) + open import Relation.Nary using (⌊_⌋) + + p0id : FL→perm ((# 0) :: ((# 0) :: f0)) =p= pid + p0id = pleq _ _ refl + + open import Data.List.Fresh.Relation.Unary.Any + open import FLComm + + stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt) + stage2FList = refl + + solved1 : (x : Permutation 2 2) → deriving 1 x → x =p= pid + solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where + solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 ) + solved0 = CommStage→ 2 1 x dr + + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym3.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym3.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,185 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym3 where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import FLutil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + + +sym3solvable : solvable (Symmetric 3) +solvable.dervied-length sym3solvable = 2 +solvable.end sym3solvable x d = solved1 x d where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 3) + + p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid + p0id = pleq _ _ refl + + p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) + p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) + p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) + p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) + p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) + p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) + t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ [] + + t1 = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷ plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷ plist [ p5 , p1 ] ∷ + plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷ plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷ plist [ p5 , p1 ] ∷ + plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷ plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷ plist [ p5 , p2 ] ∷ + plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷ plist [ p5 , p3 ] ∷ + plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p4 ] ∷ + plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p5 ] ∷ + [] + + open _=p=_ + + stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero) + stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x + + open import logic + + p33=4 : ( p3 ∘ₚ p3 ) =p= p4 + p33=4 = pleq _ _ refl + + p44=3 : ( p4 ∘ₚ p4 ) =p= p3 + p44=3 = pleq _ _ refl + + p34=0 : ( p3 ∘ₚ p4 ) =p= pid + p34=0 = pleq _ _ refl + + p43=0 : ( p4 ∘ₚ p3 ) =p= pid + p43=0 = pleq _ _ refl + + com33 : [ p3 , p3 ] =p= pid + com33 = pleq _ _ refl + + com44 : [ p4 , p4 ] =p= pid + com44 = pleq _ _ refl + + com34 : [ p3 , p4 ] =p= pid + com34 = pleq _ _ refl + + com43 : [ p4 , p3 ] =p= pid + com43 = pleq _ _ refl + + + pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x + pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl ) + + open ≡-Reasoning + +-- st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4 +-- st01 x y s t = record { peq = λ q → ( begin +-- (x ∘ₚ y) ⟨$⟩ʳ q +-- ≡⟨ peq ( presp s t ) q ⟩ +-- ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q +-- ≡⟨ peq p33=4 q ⟩ +-- p4 ⟨$⟩ʳ q +-- ∎ ) } + + st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) ] + + st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) + st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h + ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) ) + ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) ) + ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + + ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 ))| record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) + ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = + case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = + case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) + + stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 ) + stage12 x (comm {g} {h} x1 y1 ) = st02 g h + stage12 _ (ccong {y} x=y sx) with stage12 y sx + ... | case1 id = case1 ( ptrans (psym x=y ) id ) + ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ )) + ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ )) + + + solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid + solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d + ... | record { peq = f=e } = record { peq = λ q → cc q } where + cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q + cc q = begin + x ⟨$⟩ʳ q + ≡⟨ sym (f=g q) ⟩ + f ⟨$⟩ʳ q + ≡⟨ f=e q ⟩ + q + ∎ + solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y + ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl) + ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h) + ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g) + ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com33 q) } + ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com44 q) } + ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com34 q) } + ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com43 q) } + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym3n.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym3n.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,51 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym3n where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + + +sym3solvable : solvable (Symmetric 3) +solvable.dervied-length sym3solvable = 2 +solvable.end sym3solvable x d = solved1 x d where + + open import Data.List using ( List ; [] ; _∷_ ) + + open Solvable (Symmetric 3) + open import FLutil + open import Data.List.Fresh hiding ([_]) + open import Relation.Nary using (⌊_⌋) + + p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid + p0id = pleq _ _ refl + + open import Data.List.Fresh.Relation.Unary.Any + open import FLComm + + stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt) + stage3FList = refl + + solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid + solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where + solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 ) + solved2 = CommStage→ 3 2 x dr + + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym4.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym4.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,65 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym4 where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + +sym4solvable : solvable (Symmetric 4) +solvable.dervied-length sym4solvable = 3 +solvable.end sym4solvable x d = solved1 x d where + + open import Data.List using ( List ; [] ; _∷_ ) + open Solvable (Symmetric 4) + + -- Klien + -- + -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3) + -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] , + + a0 = pid {4} + a1 = pswap (pswap (pid {0})) + a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) + a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}) + + k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ [] + + open import FLutil + open import Data.List.Fresh hiding ([_]) + open import Relation.Nary using (⌊_⌋) + + p0id : FL→perm ((# 0) :: (# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid + p0id = pleq _ _ refl + + + open import Data.List.Fresh.Relation.Unary.Any + open import FLComm + + stage3FList : CommFListN 4 3 ≡ cons (zero :: zero :: zero :: zero :: f0) [] (Level.lift tt) + stage3FList = refl + + st3 = proj₁ (toList ( CommFListN 4 2 )) + -- st4 = {!!} + + solved1 : (x : Permutation 4 4) → deriving 3 x → x =p= pid + solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where + -- p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid + solved2 : Any (perm→FL x ≡_) ( CommFListN 4 3 ) + solved2 = CommStage→ 4 3 x dr diff -r a5b3061f15ee -r 6d1619d9f880 src/sym5.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym5.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,220 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym5 where + +open import Symmetric +open import Data.Unit using (⊤ ; tt ) +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function hiding (flip) +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Data.Nat.Properties +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin hiding (_<_ ; _≤_ ; lift ) +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + +open import Data.List hiding ( [_] ) +open import nat +open import fin +open import logic + +open _∧_ + +¬sym5solvable : ¬ ( solvable (Symmetric 5) ) +¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where +-- +-- dba 1320 d → b → a → d +-- (dba)⁻¹ 3021 a → b → d → a +-- aec 21430 +-- (aec)⁻¹ 41032 +-- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc +-- so commutator always contains abc, dba and aec + + open ≡-Reasoning + + open solvable + open Solvable ( Symmetric 5) + end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid + end5 x der = end sol x der + + 0<4 : 0 < 4 + 0<4 = s≤s z≤n + + 0<3 : 0 < 3 + 0<3 = s≤s z≤n + + --- 1 ∷ 2 ∷ 0 ∷ [] abc + 3rot : Permutation 3 3 + 3rot = pid {3} ∘ₚ pins (n≤ 2) + + save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) + + ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) + + ins2cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → ins2 x i<3 j<4 =p= ins2 y i<3 j<4 + ins2cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )} + (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl + + open _=p=_ + + abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + abc i<3 j<4 = ins2 3rot i<3 j<4 + dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4 + + counter-example : ¬ (abc 0<3 0<4 =p= pid ) + counter-example eq with ←pleq _ _ eq + ... | () + + record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where + field + dba0<3 : Fin 4 + dba1<4 : Fin 5 + aec0<3 : Fin 4 + aec1<4 : Fin 5 + abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] + + open Triple + triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot + triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = + record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + + _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n + _⁻¹ = pinv + + -- tt5 : (i : Fin 4) (j : Fin 5) → (z : Fin 4) → (w : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) → List (List ℕ) + -- tt5 i j z w x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j)) + -- [ ins2 (rot ∘ₚ rot) (fin≤n z) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n w) ] + -- ... | yes _ = ( toℕ i ∷ toℕ j ∷ 9 ∷ toℕ z ∷ toℕ x ∷ toℕ y ∷ toℕ w ∷ [] ) ∷ t + -- ... | no _ = t + + -- open import Relation.Binary.Definitions + + -- tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ) + -- tt2 i j rot = tt3 (# 4) (# 3) (# 3) (# 4) [] where + -- tt3 : (w : Fin 5) (z : Fin 4) (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ) + -- tt3 zero zero zero zero t = ( tt5 i j zero zero zero zero rot [] ) ++ t + -- tt3 (suc w) zero zero zero t = tt3 (fin+1 w) (# 3) (# 3) (# 4) ((tt5 i j zero (suc w) zero zero rot [] ) ++ t) + -- tt3 w z zero (suc y) t = tt3 w z (# 3) (fin+1 y) ((tt5 i j z w (suc y) zero rot [] ) ++ t) + -- tt3 w z (suc x) y t = tt3 w z (fin+1 x) y ((tt5 i j z w y (suc x) rot [] ) ++ t) + -- tt3 w (suc z) zero zero t = tt3 w (fin+1 z) (# 3) (# 4) ((tt5 i j (suc z) w zero zero rot [] ) ++ t) + + -- tt4 : List (List (List ℕ)) + -- tt4 = tt2 (# 0) (# 0) (pinv 3rot) ∷ + -- tt2 (# 1) (# 0) (pinv 3rot) ∷ + -- tt2 (# 2) (# 0) (pinv 3rot) ∷ + -- tt2 (# 3) (# 0) (pinv 3rot) ∷ + -- tt2 (# 0) (# 1) (pinv 3rot) ∷ + -- tt2 (# 1) (# 1) (pinv 3rot) ∷ + -- tt2 (# 2) (# 1) (pinv 3rot) ∷ + -- tt2 (# 3) (# 1) (pinv 3rot) ∷ + -- tt2 (# 0) (# 2) (pinv 3rot) ∷ + -- tt2 (# 1) (# 2) (pinv 3rot) ∷ + -- tt2 (# 2) (# 2) (pinv 3rot) ∷ + -- tt2 (# 3) (# 2) (pinv 3rot) ∷ + -- tt2 (# 0) (# 3) (pinv 3rot) ∷ + -- tt2 (# 1) (# 3) (pinv 3rot) ∷ + -- tt2 (# 2) (# 3) (pinv 3rot) ∷ + -- tt2 (# 3) (# 3) (pinv 3rot) ∷ + -- tt2 (# 0) (# 4) (pinv 3rot) ∷ + -- tt2 (# 1) (# 4) (pinv 3rot) ∷ + -- tt2 (# 2) (# 4) (pinv 3rot) ∷ + -- tt2 (# 3) (# 4) (pinv 3rot) ∷ + -- [] + + open Triple + dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) + dba-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + dba-triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + dba-triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + dba-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + dba-triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } + dba-triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } + dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = + record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } + + -3=33 : pinv 3rot =p= (3rot ∘ₚ 3rot ) + -3=33 = pleq _ _ refl + + 4=1 : (3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot ) =p= 3rot + 4=1 = pleq _ _ refl + + dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) + → deriving n (abc i<3 j<4 ) + dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) + → deriving n (dba i<3 j<4 ) + + commd : {n : ℕ } → (f g : Permutation 5 5) + → deriving n f + → deriving n g + → Commutator (deriving n) [ f , g ] + commd {n} f g df dg = comm {deriving n} {f} {g} df dg + + dervie-any-3rot0 0 i<3 j<4 = lift tt + dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where + tc = triple i<3 j<4 + dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) + aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) + ceq : abc i<3 j<4 =p= [ dba0 , aec0 ] + ceq = record { peq = peq (abc= tc) } + df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) + dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) + + dervie-any-3rot1 0 i<3 j<4 = lift tt + dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq ) (commd aec0 abc0 df dg ) where + tdba = dba-triple i<3 j<4 + aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)) + abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)) + ceq : dba i<3 j<4 =p= [ aec0 , abc0 ] + ceq = record { peq = peq (abc= tdba) } + df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) + df = deriving-subst (psym (ins2cong {toℕ (dba0<3 (dba-triple i<3 j<4))} {toℕ (dba1<4 (dba-triple i<3 j<4))} 4=1 )) + (dervie-any-3rot0 n (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) + dg : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) + dg = deriving-subst (psym (ins2cong {toℕ (aec0<3 (dba-triple i<3 j<4))} {toℕ (aec1<4 (dba-triple i<3 j<4))} 4=1 )) + (dervie-any-3rot0 n (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym5a.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym5a.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,94 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym5a where + +open import Symmetric +open import Data.Unit using (⊤ ; tt ) +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function hiding (flip) +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Data.Nat.Properties +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin hiding (_<_ ; _≤_ ; lift ) +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + +open import Data.List hiding ( [_] ) +open import nat +open import fin +open import logic + +open _∧_ + +¬sym5solvable : ¬ ( solvable (Symmetric 5) ) +¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where +-- +-- dba 1320 d → b → a → d +-- (dba)⁻¹ 3021 a → b → d → a +-- aec 21430 +-- (aec)⁻¹ 41032 +-- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc +-- so commutator always contains abc, dba and aec + + open ≡-Reasoning + + open solvable + open Solvable ( Symmetric 5) + end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid + end5 x der = end sol x der + + 0<4 : 0 < 4 + 0<4 = s≤s z≤n + + 0<3 : 0 < 3 + 0<3 = s≤s z≤n + + --- 1 ∷ 2 ∷ 0 ∷ [] abc + 3rot : Permutation 3 3 + 3rot = pid {3} ∘ₚ pins (n≤ 2) + + save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) + + -- Permutation 5 5 include any Permutation 3 3 + any3 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) + + any3cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → any3 x i<3 j<4 =p= any3 y i<3 j<4 + any3cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )} + (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl + + open _=p=_ + + -- derving n includes any Permutation 3 3, + any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (any3 abc i<3 j<4) + any3de {i} {j} zero abc i<3 j<4 = Level.lift tt + any3de {i} {j} (suc n) abc i<3 j<4 = ccong abc-from-comm (comm (any3de n (abc ∘ₚ abc) i<3 j0<4 ) (any3de n (abc ∘ₚ abc) i0<3 j<4 )) where + i0 : ℕ + i0 = ? + j0 : ℕ + j0 = ? + i0<3 : i0 ≤ 3 + i0<3 = {!!} + j0<4 : j0 ≤ 4 + j0<4 = {!!} + abc-from-comm : [ any3 (abc ∘ₚ abc) i<3 j0<4 , any3 (abc ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4 + abc-from-comm = {!!} + + abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 + abc i<3 j<4 = any3 3rot i<3 j<4 + + counter-example : ¬ (abc 0<3 0<4 =p= pid ) + counter-example eq with ←pleq _ _ eq + ... | () + diff -r a5b3061f15ee -r 6d1619d9f880 src/sym5n.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/sym5n.agda Sat Jan 09 10:18:08 2021 +0900 @@ -0,0 +1,103 @@ +open import Level hiding ( suc ; zero ) +open import Algebra +module sym5n where + +open import Symmetric +open import Data.Unit +open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) +open import Function +open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) +open import Relation.Nullary +open import Data.Empty +open import Data.Product + +open import Gutil +open import Putil +open import Solvable using (solvable) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) + +open import Data.Fin +open import Data.Fin.Permutation hiding (_∘ₚ_) + +infixr 200 _∘ₚ_ +_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ + +-- open import IO +open import Data.String hiding (toList) +open import Data.Unit +open import Agda.Builtin.String + +sym5solvable : (n : ℕ) → String -- ¬ solvable (Symmetric 5) +sym5solvable n = FListtoStr (CommFListN 5 n) where + + open import Data.List using ( List ; [] ; _∷_ ) + open Solvable (Symmetric 5) + + open import FLutil + open import Data.List.Fresh hiding ([_]) + open import Relation.Nary using (⌊_⌋) + + p0id : FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid + p0id = pleq _ _ refl + + open import Data.List.Fresh.Relation.Unary.Any + open import FLComm + + + stage4FList = CommFListN 5 0 + stage6FList = CommFListN 5 3 + + -- stage5FList = {!!} + -- s2=s3 : CommFListN 5 2 ≡ CommFListN 5 3 + -- s2=s3 = refl + + FLtoStr : {n : ℕ} → (x : FL n) → String + FLtoStr f0 = "f0" + FLtoStr (x :: y) = primStringAppend ( primStringAppend (primShowNat (toℕ x)) " :: " ) (FLtoStr y) + + FListtoStr : {n : ℕ} → (x : FList n) → String + FListtoStr [] = "" + FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x)) + +open import Codata.Musical.Notation +open import Data.Maybe hiding (_>>=_) +open import Data.List +open import Data.Char +open import IO.Primitive +open import Codata.Musical.Costring + +postulate + getArgs : IO (List (List Char)) +{-# FOREIGN GHC import qualified System.Environment #-} +{-# COMPILE GHC getArgs = System.Environment.getArgs #-} + +charToDigit : Char → Maybe ℕ +charToDigit '0' = just ( 0) +charToDigit '1' = just ( 1) +charToDigit '2' = just ( 2) +charToDigit '3' = just ( 3) +charToDigit '4' = just ( 4) +charToDigit '5' = just ( 5) +charToDigit '6' = just ( 6) +charToDigit '7' = just ( 7) +charToDigit '8' = just ( 8) +charToDigit '9' = just ( 9) +charToDigit _ = nothing + +getNumArg1 : (List (List Char)) → ℕ +getNumArg1 [] = 0 +getNumArg1 ([] ∷ y) = 0 +getNumArg1 ((x ∷ _) ∷ y) with charToDigit x +... | just n = n +... | nothing = 0 + + +-- +-- CommFListN 5 x is too slow use compiler +-- agda --compile sym5n.agda +-- + +main : IO ⊤ +main = getArgs >>= (λ x → putStrLn $ toCostring $ sym5solvable $ getNumArg1 x ) + + diff -r a5b3061f15ee -r 6d1619d9f880 sym2.agda --- a/sym2.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,125 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym2 where - -open import Symmetric -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import FLutil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin -open import Data.Fin.Permutation - -sym2solvable : solvable (Symmetric 2) -solvable.dervied-length sym2solvable = 1 -solvable.end sym2solvable x d = solved x d where - - open import Data.List using ( List ; [] ; _∷_ ) - - open Solvable (Symmetric 2) - -- open Group (Symmetric 2) using (_⁻¹) - - - p0 : FL→perm ((# 0) :: ((# 0 ) :: f0)) =p= pid - p0 = pleq _ _ refl - - p0r : perm→FL pid ≡ ((# 0) :: ((# 0 ) :: f0)) - p0r = refl - - p1 : FL→perm ((# 1) :: ((# 0 ) :: f0)) =p= pswap pid - p1 = pleq _ _ refl - - p1r : perm→FL (pswap pid) ≡ ((# 1) :: ((# 0 ) :: f0)) - p1r = refl - - -- FL→iso : (fl : FL 2 ) → perm→FL ( FL→perm fl ) ≡ fl - -- FL→iso (zero :: (zero :: f0)) = refl - -- FL→iso ((suc zero) :: (zero :: f0)) = refl - - open _=p=_ - open ≡-Reasoning - - sym2lem0 : ( g h : Permutation 2 2 ) → (q : Fin 2) → ([ g , h ] ⟨$⟩ʳ q) ≡ (pid ⟨$⟩ʳ q) - sym2lem0 g h q with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h - sym2lem0 g h q | zero :: (zero :: f0) | _ | record { eq = g=00} | record { eq = h=00} = begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ k))) ((peqˡ sym2lem1 _ )) ⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → h ⟨$⟩ʳ k ) (peq sym2lem1 _ ) ⟩ - h ⟨$⟩ʳ (pid ⟨$⟩ʳ ( h ⟨$⟩ˡ ( pid ⟨$⟩ˡ q ))) - ≡⟨⟩ - [ pid , h ] ⟨$⟩ʳ q - ≡⟨ peq (idcomtl h) q ⟩ - q - ∎ where - sym2lem1 : g =p= pid - sym2lem1 = FL-inject g=00 - sym2lem0 g h q | _ | zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00} = begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ peq sym2lem2 _ ⟩ - pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → pid ⟨$⟩ʳ (g ⟨$⟩ʳ k)) (peqˡ sym2lem2 _ ) ⟩ - pid ⟨$⟩ʳ (g ⟨$⟩ʳ ( pid ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨⟩ - [ g , pid ] ⟨$⟩ʳ q - ≡⟨ peq (idcomtr g) q ⟩ - q - ∎ where - sym2lem2 : h =p= pid - sym2lem2 = FL-inject h=00 - sym2lem0 g h q | suc zero :: (zero :: f0) | suc zero :: (zero :: f0) | record { eq = g=00} | record { eq = h=00}= begin - [ g , h ] ⟨$⟩ʳ q - ≡⟨⟩ - h ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ peq (psym g=h ) _ ⟩ - g ⟨$⟩ʳ (g ⟨$⟩ʳ ( h ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → g ⟨$⟩ʳ (g ⟨$⟩ʳ k) ) (peqˡ (psym g=h) _) ⟩ - g ⟨$⟩ʳ (g ⟨$⟩ʳ ( g ⟨$⟩ˡ ( g ⟨$⟩ˡ q ))) - ≡⟨ cong (λ k → g ⟨$⟩ʳ k) ( inverseʳ g ) ⟩ - g ⟨$⟩ʳ ( g ⟨$⟩ˡ q ) - ≡⟨ inverseʳ g ⟩ - q - ∎ where - g=h : g =p= h - g=h = FL-inject (trans g=00 (sym h=00)) - solved : (x : Permutation 2 2) → Commutator (λ x₁ → Lift (Level.suc Level.zero) ⊤) x → x =p= pid - solved x uni = prefl - solved x (comm {g} {h} _ _) = record { peq = sym2lem0 g h } - solved x (gen {f} {g} d d₁) with solved f d | solved g d₁ - ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where - genlem : ( q : Fin 2 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q - genlem q = begin - g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) - ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ where open ≡-Reasoning - solved x (ccong {f} {g} (record {peq = f=g}) d) with solved f d - ... | record { peq = f=e } = record { peq = λ q → cc q } where - cc : ( q : Fin 2 ) → x ⟨$⟩ʳ q ≡ q - cc q = begin - x ⟨$⟩ʳ q - ≡⟨ sym (f=g q) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ where open ≡-Reasoning - - - - diff -r a5b3061f15ee -r 6d1619d9f880 sym2n.agda --- a/sym2n.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym2n where - -open import Symmetric -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - - -sym2solvable : solvable (Symmetric 2) -solvable.dervied-length sym2solvable = 1 -solvable.end sym2solvable x d = solved1 x d where - - open import Data.List using ( List ; [] ; _∷_ ) - - open Solvable (Symmetric 2) - open import FLutil - open import Data.List.Fresh hiding ([_]) - open import Relation.Nary using (⌊_⌋) - - p0id : FL→perm ((# 0) :: ((# 0) :: f0)) =p= pid - p0id = pleq _ _ refl - - open import Data.List.Fresh.Relation.Unary.Any - open import FLComm - - stage2FList : CommFListN 2 1 ≡ cons (zero :: zero :: f0) [] (Level.lift tt) - stage2FList = refl - - solved1 : (x : Permutation 2 2) → deriving 1 x → x =p= pid - solved1 x dr = CommSolved 2 x ( CommFListN 2 1 ) stage2FList p0id solved0 where - solved0 : Any (perm→FL x ≡_) ( CommFListN 2 1 ) - solved0 = CommStage→ 2 1 x dr - - diff -r a5b3061f15ee -r 6d1619d9f880 sym3.agda --- a/sym3.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,185 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym3 where - -open import Symmetric -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import FLutil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - - -sym3solvable : solvable (Symmetric 3) -solvable.dervied-length sym3solvable = 2 -solvable.end sym3solvable x d = solved1 x d where - - open import Data.List using ( List ; [] ; _∷_ ) - - open Solvable (Symmetric 3) - - p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid - p0id = pleq _ _ refl - - p0 = FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) - p1 = FL→perm ((# 0) :: ((# 1) :: ((# 0 ) :: f0))) - p2 = FL→perm ((# 1) :: ((# 0) :: ((# 0 ) :: f0))) - p3 = FL→perm ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) - p4 = FL→perm ((# 2) :: ((# 0) :: ((# 0 ) :: f0))) - p5 = FL→perm ((# 2) :: ((# 1) :: ((# 0 ) :: f0))) - t0 = plist p0 ∷ plist p1 ∷ plist p2 ∷ plist p3 ∷ plist p4 ∷ plist p5 ∷ [] - - t1 = plist [ p0 , p0 ] ∷ plist [ p1 , p0 ] ∷ plist [ p2 , p0 ] ∷ plist [ p3 , p0 ] ∷ plist [ p4 , p0 ] ∷ plist [ p5 , p1 ] ∷ - plist [ p0 , p1 ] ∷ plist [ p1 , p1 ] ∷ plist [ p2 , p1 ] ∷ plist [ p3 , p1 ] ∷ plist [ p4 , p1 ] ∷ plist [ p5 , p1 ] ∷ - plist [ p0 , p2 ] ∷ plist [ p1 , p2 ] ∷ plist [ p2 , p2 ] ∷ plist [ p3 , p2 ] ∷ plist [ p4 , p2 ] ∷ plist [ p5 , p2 ] ∷ - plist [ p0 , p3 ] ∷ plist [ p1 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p3 , p3 ] ∷ plist [ p4 , p3 ] ∷ plist [ p5 , p3 ] ∷ - plist [ p0 , p4 ] ∷ plist [ p1 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p3 , p4 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p4 ] ∷ - plist [ p0 , p5 ] ∷ plist [ p1 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p3 , p5 ] ∷ plist [ p4 , p4 ] ∷ plist [ p5 , p5 ] ∷ - [] - - open _=p=_ - - stage1 : (x : Permutation 3 3) → Set (Level.suc Level.zero) - stage1 x = Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x - - open import logic - - p33=4 : ( p3 ∘ₚ p3 ) =p= p4 - p33=4 = pleq _ _ refl - - p44=3 : ( p4 ∘ₚ p4 ) =p= p3 - p44=3 = pleq _ _ refl - - p34=0 : ( p3 ∘ₚ p4 ) =p= pid - p34=0 = pleq _ _ refl - - p43=0 : ( p4 ∘ₚ p3 ) =p= pid - p43=0 = pleq _ _ refl - - com33 : [ p3 , p3 ] =p= pid - com33 = pleq _ _ refl - - com44 : [ p4 , p4 ] =p= pid - com44 = pleq _ _ refl - - com34 : [ p3 , p4 ] =p= pid - com34 = pleq _ _ refl - - com43 : [ p4 , p3 ] =p= pid - com43 = pleq _ _ refl - - - pFL : ( g : Permutation 3 3) → { x : FL 3 } → perm→FL g ≡ x → g =p= FL→perm x - pFL g {x} refl = ptrans (psym (FL←iso g)) ( FL-inject refl ) - - open ≡-Reasoning - --- st01 : ( x y : Permutation 3 3) → x =p= p3 → y =p= p3 → x ∘ₚ y =p= p4 --- st01 x y s t = record { peq = λ q → ( begin --- (x ∘ₚ y) ⟨$⟩ʳ q --- ≡⟨ peq ( presp s t ) q ⟩ --- ( p3 ∘ₚ p3 ) ⟨$⟩ʳ q --- ≡⟨ peq p33=4 q ⟩ --- p4 ⟨$⟩ʳ q --- ∎ ) } - - st00 = perm→FL [ FL→perm ((suc zero) :: (suc zero :: (zero :: f0 ))) , FL→perm ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) ] - - st02 : ( g h : Permutation 3 3) → ([ g , h ] =p= pid) ∨ ([ g , h ] =p= p3) ∨ ([ g , h ] =p= p4) - st02 g h with perm→FL g | perm→FL h | inspect perm→FL g | inspect perm→FL h - ... | (zero :: (zero :: (zero :: f0))) | t | record { eq = ge } | te = case1 (ptrans (comm-resp {g} {h} {pid} (FL-inject ge ) prefl ) (idcomtl h) ) - ... | s | (zero :: (zero :: (zero :: f0))) | se | record { eq = he } = case1 (ptrans (comm-resp {g} {h} {_} {pid} prefl (FL-inject he ))(idcomtr g) ) - ... | (zero :: (suc zero) :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - ... | (suc zero) :: (zero :: (zero :: f0 )) | (suc zero) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - ... | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - - ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (zero :: (suc zero) :: (zero :: f0 )) | (suc (suc zero)) :: (zero :: (zero :: f0 ))| record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (zero :: (suc zero) :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0))| record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc zero) :: (suc zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc zero) :: (zero :: (zero :: f0 ))) | ((suc (suc zero)) :: (zero :: (zero :: f0 )))| record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc zero) :: (zero :: (zero :: f0 ))) | (suc (suc zero)) :: (suc zero) :: (zero :: f0) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (suc zero) :: (suc zero :: (zero :: f0 )) | (zero :: (suc zero) :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - ... | (suc zero) :: (suc zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) ) - ... | (suc (suc zero)) :: (zero :: (zero :: f0 )) | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((zero :: (suc zero) :: (zero :: f0 )) ) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | ((suc zero) :: (suc zero :: (zero :: f0 ))) | record { eq = ge } | record { eq = he } = - case2 (case2 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - ... | ((suc (suc zero)) :: (suc zero) :: (zero :: f0)) | (suc (suc zero)) :: (zero :: (zero :: f0 )) | record { eq = ge } | record { eq = he } = - case2 (case1 (ptrans (comm-resp (pFL g ge) (pFL h he)) (FL-inject refl) )) - - stage12 : (x : Permutation 3 3) → stage1 x → ( x =p= pid ) ∨ ( x =p= p3 ) ∨ ( x =p= p4 ) - stage12 x (comm {g} {h} x1 y1 ) = st02 g h - stage12 _ (ccong {y} x=y sx) with stage12 y sx - ... | case1 id = case1 ( ptrans (psym x=y ) id ) - ... | case2 (case1 x₁) = case2 (case1 ( ptrans (psym x=y ) x₁ )) - ... | case2 (case2 x₁) = case2 (case2 ( ptrans (psym x=y ) x₁ )) - - - solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid - solved1 x (ccong {f} {g} (record {peq = f=g}) d) with solved1 f d - ... | record { peq = f=e } = record { peq = λ q → cc q } where - cc : ( q : Fin 3 ) → x ⟨$⟩ʳ q ≡ q - cc q = begin - x ⟨$⟩ʳ q - ≡⟨ sym (f=g q) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ - solved1 _ (comm {g} {h} x y) with stage12 g x | stage12 h y - ... | case1 t | case1 s = ptrans (comm-resp t s) (comm-refl {pid} prefl) - ... | case1 t | case2 s = ptrans (comm-resp {g} {h} {pid} t prefl) (idcomtl h) - ... | case2 t | case1 s = ptrans (comm-resp {g} {h} {_} {pid} prefl s) (idcomtr g) - ... | case2 (case1 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com33 q) } - ... | case2 (case2 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com44 q) } - ... | case2 (case1 t) | case2 (case2 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com34 q) } - ... | case2 (case2 t) | case2 (case1 s) = record { peq = λ q → trans ( peq ( comm-resp {g} {h} t s ) q ) (peq com43 q) } - diff -r a5b3061f15ee -r 6d1619d9f880 sym3n.agda --- a/sym3n.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,51 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym3n where - -open import Symmetric -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - - -sym3solvable : solvable (Symmetric 3) -solvable.dervied-length sym3solvable = 2 -solvable.end sym3solvable x d = solved1 x d where - - open import Data.List using ( List ; [] ; _∷_ ) - - open Solvable (Symmetric 3) - open import FLutil - open import Data.List.Fresh hiding ([_]) - open import Relation.Nary using (⌊_⌋) - - p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid - p0id = pleq _ _ refl - - open import Data.List.Fresh.Relation.Unary.Any - open import FLComm - - stage3FList : CommFListN 3 2 ≡ cons (zero :: zero :: zero :: f0) [] (Level.lift tt) - stage3FList = refl - - solved1 : (x : Permutation 3 3) → deriving 2 x → x =p= pid - solved1 x dr = CommSolved 3 x ( CommFListN 3 2 ) stage3FList p0id solved2 where - solved2 : Any (perm→FL x ≡_) ( CommFListN 3 2 ) - solved2 = CommStage→ 3 2 x dr - - diff -r a5b3061f15ee -r 6d1619d9f880 sym4.agda --- a/sym4.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,65 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym4 where - -open import Symmetric -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - -sym4solvable : solvable (Symmetric 4) -solvable.dervied-length sym4solvable = 3 -solvable.end sym4solvable x d = solved1 x d where - - open import Data.List using ( List ; [] ; _∷_ ) - open Solvable (Symmetric 4) - - -- Klien - -- - -- 1 (1,2),(3,4) (1,3),(2,4) (1,4),(2,3) - -- 0 ∷ 1 ∷ 2 ∷ 3 ∷ [] , 1 ∷ 0 ∷ 3 ∷ 2 ∷ [] , 2 ∷ 3 ∷ 0 ∷ 1 ∷ [] , 3 ∷ 2 ∷ 1 ∷ 0 ∷ [] , - - a0 = pid {4} - a1 = pswap (pswap (pid {0})) - a2 = pid {4} ∘ₚ pins (n≤ 3) ∘ₚ pins (n≤ 3 ) - a3 = pins (n≤ 3) ∘ₚ pins (n≤ 2) ∘ₚ pswap (pid {2}) - - k3 = plist (a1 ∘ₚ a2 ) ∷ plist (a1 ∘ₚ a3) ∷ plist (a2 ∘ₚ a1 ) ∷ [] - - open import FLutil - open import Data.List.Fresh hiding ([_]) - open import Relation.Nary using (⌊_⌋) - - p0id : FL→perm ((# 0) :: (# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid - p0id = pleq _ _ refl - - - open import Data.List.Fresh.Relation.Unary.Any - open import FLComm - - stage3FList : CommFListN 4 3 ≡ cons (zero :: zero :: zero :: zero :: f0) [] (Level.lift tt) - stage3FList = refl - - st3 = proj₁ (toList ( CommFListN 4 2 )) - -- st4 = {!!} - - solved1 : (x : Permutation 4 4) → deriving 3 x → x =p= pid - solved1 x dr = CommSolved 4 x ( CommFListN 4 3 ) stage3FList p0id solved2 where - -- p0id : FL→perm ((# 0) :: ((# 0) :: ((# 0 ) :: f0))) =p= pid - solved2 : Any (perm→FL x ≡_) ( CommFListN 4 3 ) - solved2 = CommStage→ 4 3 x dr diff -r a5b3061f15ee -r 6d1619d9f880 sym5.agda --- a/sym5.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,220 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym5 where - -open import Symmetric -open import Data.Unit using (⊤ ; tt ) -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function hiding (flip) -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Data.Nat.Properties -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin hiding (_<_ ; _≤_ ; lift ) -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - -open import Data.List hiding ( [_] ) -open import nat -open import fin -open import logic - -open _∧_ - -¬sym5solvable : ¬ ( solvable (Symmetric 5) ) -¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (dervie-any-3rot0 (dervied-length sol) 0<3 0<4 ) ) where --- --- dba 1320 d → b → a → d --- (dba)⁻¹ 3021 a → b → d → a --- aec 21430 --- (aec)⁻¹ 41032 --- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc --- so commutator always contains abc, dba and aec - - open ≡-Reasoning - - open solvable - open Solvable ( Symmetric 5) - end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid - end5 x der = end sol x der - - 0<4 : 0 < 4 - 0<4 = s≤s z≤n - - 0<3 : 0 < 3 - 0<3 = s≤s z≤n - - --- 1 ∷ 2 ∷ 0 ∷ [] abc - 3rot : Permutation 3 3 - 3rot = pid {3} ∘ₚ pins (n≤ 2) - - save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) - - ins2 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - ins2 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) - - ins2cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → ins2 x i<3 j<4 =p= ins2 y i<3 j<4 - ins2cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )} - (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl - - open _=p=_ - - abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - abc i<3 j<4 = ins2 3rot i<3 j<4 - dba : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - dba i<3 j<4 = ins2 (3rot ∘ₚ 3rot) i<3 j<4 - - counter-example : ¬ (abc 0<3 0<4 =p= pid ) - counter-example eq with ←pleq _ _ eq - ... | () - - record Triple {i j : ℕ } (i<3 : i ≤ 3) (j<4 : j ≤ 4) (rot : Permutation 3 3) : Set where - field - dba0<3 : Fin 4 - dba1<4 : Fin 5 - aec0<3 : Fin 4 - aec1<4 : Fin 5 - abc= : ins2 rot i<3 j<4 =p= [ ins2 (rot ∘ₚ rot) (fin≤n {3} dba0<3) (fin≤n {4} dba1<4) , ins2 (rot ∘ₚ rot) (fin≤n {3} aec0<3) (fin≤n {4} aec1<4) ] - - open Triple - triple : {i j : ℕ } → (i<3 : i ≤ 3) (j<4 : j ≤ 4) → Triple i<3 j<4 3rot - triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } - triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } - triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 3 ; aec1<4 = # 1 ; abc= = pleq _ _ refl } - triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 3 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = - record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - - _⁻¹ : {n : ℕ } ( x : Permutation n n) → Permutation n n - _⁻¹ = pinv - - -- tt5 : (i : Fin 4) (j : Fin 5) → (z : Fin 4) → (w : Fin 5) → (x : Fin 5) (y : Fin 4) → (rot : Permutation 3 3 ) → List (List ℕ) → List (List ℕ) - -- tt5 i j z w x y rot t with is-=p= (ins2 rot (fin≤n i) (fin≤n j)) - -- [ ins2 (rot ∘ₚ rot) (fin≤n z) (fin≤n x) , ins2 (pinv rot) (fin≤n y) (fin≤n w) ] - -- ... | yes _ = ( toℕ i ∷ toℕ j ∷ 9 ∷ toℕ z ∷ toℕ x ∷ toℕ y ∷ toℕ w ∷ [] ) ∷ t - -- ... | no _ = t - - -- open import Relation.Binary.Definitions - - -- tt2 : (i : Fin 4) (j : Fin 5) → (rot : Permutation 3 3 ) → List (List ℕ) - -- tt2 i j rot = tt3 (# 4) (# 3) (# 3) (# 4) [] where - -- tt3 : (w : Fin 5) (z : Fin 4) (x : Fin 4) (y : Fin 5) → List (List ℕ) → List (List ℕ) - -- tt3 zero zero zero zero t = ( tt5 i j zero zero zero zero rot [] ) ++ t - -- tt3 (suc w) zero zero zero t = tt3 (fin+1 w) (# 3) (# 3) (# 4) ((tt5 i j zero (suc w) zero zero rot [] ) ++ t) - -- tt3 w z zero (suc y) t = tt3 w z (# 3) (fin+1 y) ((tt5 i j z w (suc y) zero rot [] ) ++ t) - -- tt3 w z (suc x) y t = tt3 w z (fin+1 x) y ((tt5 i j z w y (suc x) rot [] ) ++ t) - -- tt3 w (suc z) zero zero t = tt3 w (fin+1 z) (# 3) (# 4) ((tt5 i j (suc z) w zero zero rot [] ) ++ t) - - -- tt4 : List (List (List ℕ)) - -- tt4 = tt2 (# 0) (# 0) (pinv 3rot) ∷ - -- tt2 (# 1) (# 0) (pinv 3rot) ∷ - -- tt2 (# 2) (# 0) (pinv 3rot) ∷ - -- tt2 (# 3) (# 0) (pinv 3rot) ∷ - -- tt2 (# 0) (# 1) (pinv 3rot) ∷ - -- tt2 (# 1) (# 1) (pinv 3rot) ∷ - -- tt2 (# 2) (# 1) (pinv 3rot) ∷ - -- tt2 (# 3) (# 1) (pinv 3rot) ∷ - -- tt2 (# 0) (# 2) (pinv 3rot) ∷ - -- tt2 (# 1) (# 2) (pinv 3rot) ∷ - -- tt2 (# 2) (# 2) (pinv 3rot) ∷ - -- tt2 (# 3) (# 2) (pinv 3rot) ∷ - -- tt2 (# 0) (# 3) (pinv 3rot) ∷ - -- tt2 (# 1) (# 3) (pinv 3rot) ∷ - -- tt2 (# 2) (# 3) (pinv 3rot) ∷ - -- tt2 (# 3) (# 3) (pinv 3rot) ∷ - -- tt2 (# 0) (# 4) (pinv 3rot) ∷ - -- tt2 (# 1) (# 4) (pinv 3rot) ∷ - -- tt2 (# 2) (# 4) (pinv 3rot) ∷ - -- tt2 (# 3) (# 4) (pinv 3rot) ∷ - -- [] - - open Triple - dba-triple : {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → Triple i<3 j<4 (3rot ∘ₚ 3rot ) - dba-triple z≤n z≤n = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple z≤n (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple z≤n (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - dba-triple z≤n (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } - dba-triple z≤n (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - dba-triple (s≤s z≤n) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - dba-triple (s≤s z≤n) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 0 ; aec0<3 = # 1 ; aec1<4 = # 3 ; abc= = pleq _ _ refl } - dba-triple (s≤s z≤n) (s≤s (s≤s z≤n)) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s z≤n) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s z≤n)) z≤n = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s z≤n)) (s≤s z≤n) = record { dba0<3 = # 2 ; dba1<4 = # 4 ; aec0<3 = # 0 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s z≤n)) = record { dba0<3 = # 0 ; dba1<4 = # 2 ; aec0<3 = # 2 ; aec1<4 = # 4 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 4 ; aec0<3 = # 2 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s z≤n)) (s≤s (s≤s (s≤s (s≤s z≤n)))) = record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s (s≤s z≤n))) z≤n = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s z≤n) = record { dba0<3 = # 0 ; dba1<4 = # 4 ; aec0<3 = # 1 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s z≤n)) = record { dba0<3 = # 3 ; dba1<4 = # 0 ; aec0<3 = # 0 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s z≤n))) = record { dba0<3 = # 1 ; dba1<4 = # 3 ; aec0<3 = # 3 ; aec1<4 = # 0 ; abc= = pleq _ _ refl } - dba-triple (s≤s (s≤s (s≤s z≤n))) (s≤s (s≤s (s≤s (s≤s z≤n)))) = - record { dba0<3 = # 2 ; dba1<4 = # 0 ; aec0<3 = # 3 ; aec1<4 = # 2 ; abc= = pleq _ _ refl } - - -3=33 : pinv 3rot =p= (3rot ∘ₚ 3rot ) - -3=33 = pleq _ _ refl - - 4=1 : (3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot ) =p= 3rot - 4=1 = pleq _ _ refl - - dervie-any-3rot0 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) - → deriving n (abc i<3 j<4 ) - dervie-any-3rot1 : (n : ℕ ) → {i j : ℕ } → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) - → deriving n (dba i<3 j<4 ) - - commd : {n : ℕ } → (f g : Permutation 5 5) - → deriving n f - → deriving n g - → Commutator (deriving n) [ f , g ] - commd {n} f g df dg = comm {deriving n} {f} {g} df dg - - dervie-any-3rot0 0 i<3 j<4 = lift tt - dervie-any-3rot0 (suc i) i<3 j<4 = ccong {deriving i} (psym ceq) (commd dba0 aec0 df dg )where - tc = triple i<3 j<4 - dba0 = dba (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) - aec0 = dba (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) - ceq : abc i<3 j<4 =p= [ dba0 , aec0 ] - ceq = record { peq = peq (abc= tc) } - df = dervie-any-3rot1 i (fin≤n {3} (dba0<3 tc)) (fin≤n {4} (dba1<4 tc)) - dg = dervie-any-3rot1 i (fin≤n {3} (aec0<3 tc)) (fin≤n {4} (aec1<4 tc)) - - dervie-any-3rot1 0 i<3 j<4 = lift tt - dervie-any-3rot1 (suc n) {i} {j} i<3 j<4 = ccong {deriving n} ( psym ceq ) (commd aec0 abc0 df dg ) where - tdba = dba-triple i<3 j<4 - aec0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba)) - abc0 = ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba)) - ceq : dba i<3 j<4 =p= [ aec0 , abc0 ] - ceq = record { peq = peq (abc= tdba) } - df : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) - df = deriving-subst (psym (ins2cong {toℕ (dba0<3 (dba-triple i<3 j<4))} {toℕ (dba1<4 (dba-triple i<3 j<4))} 4=1 )) - (dervie-any-3rot0 n (fin≤n {3} (dba0<3 tdba)) (fin≤n {4} (dba1<4 tdba))) - dg : deriving n (ins2 ((3rot ∘ₚ 3rot) ∘ₚ (3rot ∘ₚ 3rot )) (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) - dg = deriving-subst (psym (ins2cong {toℕ (aec0<3 (dba-triple i<3 j<4))} {toℕ (aec1<4 (dba-triple i<3 j<4))} 4=1 )) - (dervie-any-3rot0 n (fin≤n {3} (aec0<3 tdba)) (fin≤n {4} (aec1<4 tdba))) - diff -r a5b3061f15ee -r 6d1619d9f880 sym5a.agda --- a/sym5a.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,94 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym5a where - -open import Symmetric -open import Data.Unit using (⊤ ; tt ) -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function hiding (flip) -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Data.Nat.Properties -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin hiding (_<_ ; _≤_ ; lift ) -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - -open import Data.List hiding ( [_] ) -open import nat -open import fin -open import logic - -open _∧_ - -¬sym5solvable : ¬ ( solvable (Symmetric 5) ) -¬sym5solvable sol = counter-example (end5 (abc 0<3 0<4 ) (any3de (dervied-length sol) 3rot 0<3 0<4 ) ) where --- --- dba 1320 d → b → a → d --- (dba)⁻¹ 3021 a → b → d → a --- aec 21430 --- (aec)⁻¹ 41032 --- [ dba , aec ] = (abd)(cea)(dba)(aec) = abc --- so commutator always contains abc, dba and aec - - open ≡-Reasoning - - open solvable - open Solvable ( Symmetric 5) - end5 : (x : Permutation 5 5) → deriving (dervied-length sol) x → x =p= pid - end5 x der = end sol x der - - 0<4 : 0 < 4 - 0<4 = s≤s z≤n - - 0<3 : 0 < 3 - 0<3 = s≤s z≤n - - --- 1 ∷ 2 ∷ 0 ∷ [] abc - 3rot : Permutation 3 3 - 3rot = pid {3} ∘ₚ pins (n≤ 2) - - save2 : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - save2 i<3 j<4 = flip (pins (s≤s i<3)) ∘ₚ flip (pins j<4) - - -- Permutation 5 5 include any Permutation 3 3 - any3 : {i j : ℕ } → Permutation 3 3 → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - any3 abc i<3 j<4 = (save2 i<3 j<4 ∘ₚ (pprep (pprep abc))) ∘ₚ flip (save2 i<3 j<4 ) - - any3cong : {i j : ℕ } → {x y : Permutation 3 3 } → {i<3 : i ≤ 3 } → {j<4 : j ≤ 4 } → x =p= y → any3 x i<3 j<4 =p= any3 y i<3 j<4 - any3cong {i} {j} {x} {y} {i<3} {j<4} x=y = presp {5} {save2 i<3 j<4 ∘ₚ (pprep (pprep x))} {_} {flip (save2 i<3 j<4 )} - (presp {5} {save2 i<3 j<4} prefl (pprep-cong (pprep-cong x=y)) ) prefl - - open _=p=_ - - -- derving n includes any Permutation 3 3, - any3de : {i j : ℕ } → (n : ℕ) → (abc : Permutation 3 3) → (i<3 : i ≤ 3 ) → (j<4 : j ≤ 4 ) → deriving n (any3 abc i<3 j<4) - any3de {i} {j} zero abc i<3 j<4 = Level.lift tt - any3de {i} {j} (suc n) abc i<3 j<4 = ccong abc-from-comm (comm (any3de n (abc ∘ₚ abc) i<3 j0<4 ) (any3de n (abc ∘ₚ abc) i0<3 j<4 )) where - i0 : ℕ - i0 = ? - j0 : ℕ - j0 = ? - i0<3 : i0 ≤ 3 - i0<3 = {!!} - j0<4 : j0 ≤ 4 - j0<4 = {!!} - abc-from-comm : [ any3 (abc ∘ₚ abc) i<3 j0<4 , any3 (abc ∘ₚ abc) i0<3 j<4 ] =p= any3 abc i<3 j<4 - abc-from-comm = {!!} - - abc : {i j : ℕ } → (i ≤ 3 ) → ( j ≤ 4 ) → Permutation 5 5 - abc i<3 j<4 = any3 3rot i<3 j<4 - - counter-example : ¬ (abc 0<3 0<4 =p= pid ) - counter-example eq with ←pleq _ _ eq - ... | () - diff -r a5b3061f15ee -r 6d1619d9f880 sym5n.agda --- a/sym5n.agda Tue Dec 15 08:50:32 2020 +0900 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,103 +0,0 @@ -open import Level hiding ( suc ; zero ) -open import Algebra -module sym5n where - -open import Symmetric -open import Data.Unit -open import Function.Inverse as Inverse using (_↔_; Inverse; _InverseOf_) -open import Function -open import Data.Nat hiding (_⊔_) -- using (ℕ; suc; zero) -open import Relation.Nullary -open import Data.Empty -open import Data.Product - -open import Gutil -open import Putil -open import Solvable using (solvable) -open import Relation.Binary.PropositionalEquality hiding ( [_] ) - -open import Data.Fin -open import Data.Fin.Permutation hiding (_∘ₚ_) - -infixr 200 _∘ₚ_ -_∘ₚ_ = Data.Fin.Permutation._∘ₚ_ - --- open import IO -open import Data.String hiding (toList) -open import Data.Unit -open import Agda.Builtin.String - -sym5solvable : (n : ℕ) → String -- ¬ solvable (Symmetric 5) -sym5solvable n = FListtoStr (CommFListN 5 n) where - - open import Data.List using ( List ; [] ; _∷_ ) - open Solvable (Symmetric 5) - - open import FLutil - open import Data.List.Fresh hiding ([_]) - open import Relation.Nary using (⌊_⌋) - - p0id : FL→perm (zero :: zero :: zero :: (zero :: (zero :: f0))) =p= pid - p0id = pleq _ _ refl - - open import Data.List.Fresh.Relation.Unary.Any - open import FLComm - - - stage4FList = CommFListN 5 0 - stage6FList = CommFListN 5 3 - - -- stage5FList = {!!} - -- s2=s3 : CommFListN 5 2 ≡ CommFListN 5 3 - -- s2=s3 = refl - - FLtoStr : {n : ℕ} → (x : FL n) → String - FLtoStr f0 = "f0" - FLtoStr (x :: y) = primStringAppend ( primStringAppend (primShowNat (toℕ x)) " :: " ) (FLtoStr y) - - FListtoStr : {n : ℕ} → (x : FList n) → String - FListtoStr [] = "" - FListtoStr (cons a x x₁) = primStringAppend (FLtoStr a) (primStringAppend "\n" (FListtoStr x)) - -open import Codata.Musical.Notation -open import Data.Maybe hiding (_>>=_) -open import Data.List -open import Data.Char -open import IO.Primitive -open import Codata.Musical.Costring - -postulate - getArgs : IO (List (List Char)) -{-# FOREIGN GHC import qualified System.Environment #-} -{-# COMPILE GHC getArgs = System.Environment.getArgs #-} - -charToDigit : Char → Maybe ℕ -charToDigit '0' = just ( 0) -charToDigit '1' = just ( 1) -charToDigit '2' = just ( 2) -charToDigit '3' = just ( 3) -charToDigit '4' = just ( 4) -charToDigit '5' = just ( 5) -charToDigit '6' = just ( 6) -charToDigit '7' = just ( 7) -charToDigit '8' = just ( 8) -charToDigit '9' = just ( 9) -charToDigit _ = nothing - -getNumArg1 : (List (List Char)) → ℕ -getNumArg1 [] = 0 -getNumArg1 ([] ∷ y) = 0 -getNumArg1 ((x ∷ _) ∷ y) with charToDigit x -... | just n = n -... | nothing = 0 - - --- --- CommFListN 5 x is too slow use compiler --- agda --compile sym5n.agda --- - -main : IO ⊤ -main = getArgs >>= (λ x → putStrLn $ toCostring $ sym5solvable $ getNumArg1 x ) - -