Mercurial > hg > Members > kono > Proof > galois
changeset 208:47df9343efa9
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Fri, 04 Dec 2020 22:47:01 +0900 |
| parents | a180e6d4bfd6 |
| children | 40695d752dd0 |
| files | FLComm.agda FLutil.agda sym3.agda |
| diffstat | 3 files changed, 46 insertions(+), 27 deletions(-) [+] |
line wrap: on
line diff
--- a/FLComm.agda Thu Dec 03 07:11:22 2020 +0900 +++ b/FLComm.agda Fri Dec 04 22:47:01 2020 +0900 @@ -29,7 +29,50 @@ 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 _∧_ + +-- Flist : {n : ℕ } (i : ℕ) → i < suc n → FList n → FList n → FList (suc n) +-- Flist zero i<n [] _ = [] +-- Flist zero i<n (a ∷# x ) z = FLinsert ( zero :: a ) (Flist zero i<n x z ) +-- Flist (suc i) (s≤s i<n) [] z = Flist i (<-trans i<n a<sa) z z +-- Flist (suc i) i<n (a ∷# x ) z = FLinsert ((fromℕ< i<n ) :: a ) (Flist (suc i) i<n x z ) +-- +-- ∀Flist : {n : ℕ } → FL n → FList n +-- ∀Flist {zero} f0 = f0 ∷# [] +-- Flist {suc n} (x :: y) = Flist n a<sa (∀Flist y) (∀Flist y) + +-- all FL +record AnyFL (n : ℕ) (p : FL n) : Set where + field + anyList : FList n + anyP : (x : FL n) → p f≤ x → Any ( _≡ x ) anyList + +open AnyFL +anyFL : (n : ℕ ) → AnyFL n FL0 +anyFL zero = record { anyList = f0 ∷# [] ; anyP = any00 } where + any00 : (p : FL zero) → FL0 f≤ p → Any (_≡ p) (f0 ∷# []) + any00 f0 (case1 refl) = here refl +anyFL (suc n) = any01 n (anyList (anyFL n)) (anyP (anyFL n) FL0 (case1 refl) ) {!!} where + any02 : (i : ℕ ) → (i<n : i < suc n ) → (a : FL n) → AnyFL (suc n) (fromℕ< i<n :: a) → AnyFL (suc n) (zero :: a) + any02 zero (s≤s z≤n) a any = any + any02 (suc i) i<n a any = {!!} + any01 : (i : ℕ ) → (L : FList n) → Any (_≡ FL0) L → AnyFL (suc n) fmax → AnyFL (suc n) FL0 + any01 zero [] () + any01 (suc i) [] () + any01 zero (cons a L x) _ any = any03 any where + any03 : AnyFL (suc n) (fromℕ< a<sa :: fmax) → AnyFL (suc n) FL0 + any03 any = any02 n a<sa FL0 {!!} + any01 (suc i) (cons .FL0 L x) (here refl) any = any01 i L {!!} {!!} -- can't happen + any01 (suc i) (cons a L x) (there b) any = any01 i L b any + +-- all comm cobmbibation in P and Q +record AnyComm (P Q : FList n) : Set where + field + commList : FList n + commAny : (p q : FL n) → Any (p ≡_) P → Any (q ≡_) Q → Any ( _≡ perm→FL [ FL→perm p , FL→perm q ] ) commList tl3 : (FL n) → ( z : FList n) → FList n → FList n tl3 h [] w = w @@ -45,11 +88,6 @@ CommFListN 0 = ∀Flist fmax CommFListN (suc i) = CommFList (CommFListN i) -open import Algebra -open Group (Symmetric n) hiding (refl) - -open _∧_ - -- {-# TERMINATING #-} CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i ) CommStage→ zero x (Level.lift tt) = AnyFList (perm→FL x)
--- a/FLutil.agda Thu Dec 03 07:11:22 2020 +0900 +++ b/FLutil.agda Fri Dec 04 22:47:01 2020 +0900 @@ -30,6 +30,9 @@ FLeq : {n : ℕ } {xn yn : Fin (suc n)} {x : FL n } {y : FL n} → xn :: x ≡ yn :: y → ( xn ≡ yn ) × (x ≡ y ) FLeq refl = refl , refl +FLpos : {n : ℕ} → FL (suc n) → Fin (suc n) +FLpos (x :: _) = x + f-<> : {n : ℕ } {x : FL n } {y : FL n} → x f< y → y f< x → ⊥ f-<> (f<n x) (f<n x₁) = nat-<> x x₁ f-<> (f<n x) (f<t lt2) = nat-≡< refl x
--- a/sym3.agda Thu Dec 03 07:11:22 2020 +0900 +++ b/sym3.agda Fri Dec 04 22:47:01 2020 +0900 @@ -156,18 +156,7 @@ 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 uni = case1 prefl stage12 x (comm {g} {h} x1 y1 ) = st02 g h - stage12 _ (gen {x} {y} sx sy) with stage12 x sx | stage12 y sy - ... | case1 t | case1 s = case1 ( record { peq = λ q → peq (presp t s) q} ) - ... | case1 t | case2 (case1 s) = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } )) - ... | case1 t | case2 (case2 s) = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } )) - ... | case2 (case1 t) | case1 s = case2 (case1 ( record { peq = λ q → peq (presp t s ) q } )) - ... | case2 (case2 t) | case1 s = case2 (case2 ( record { peq = λ q → peq (presp t s ) q } )) - ... | case2 (case1 s) | case2 (case1 t) = case2 (case2 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p33=4 q) } ) - ... | case2 (case1 s) | case2 (case2 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p34=0 q) } - ... | case2 (case2 s) | case2 (case1 t) = case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p43=0 q) } - ... | case2 (case2 s) | case2 (case2 t) = case2 (case1 record { peq = λ q → trans (peq ( presp s t ) q) ( peq p44=3 q) } ) 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₁ )) @@ -175,17 +164,6 @@ solved1 : (x : Permutation 3 3) → Commutator (λ x₁ → Commutator (λ x₂ → Lift (Level.suc Level.zero) ⊤) x₁) x → x =p= pid - solved1 _ uni = prefl - solved1 x (gen {f} {g} d d₁) with solved1 f d | solved1 g d₁ - ... | record { peq = f=e } | record { peq = g=e } = record { peq = λ q → genlem q } where - genlem : ( q : Fin 3 ) → g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) ≡ q - genlem q = begin - g ⟨$⟩ʳ ( f ⟨$⟩ʳ q ) - ≡⟨ g=e ( f ⟨$⟩ʳ q ) ⟩ - f ⟨$⟩ʳ q - ≡⟨ f=e q ⟩ - q - ∎ 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