Mercurial > hg > Members > kono > Proof > galois

changeset 186:3c7e8855996f

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 27 Nov 2020 20:54:55 +0900
parents b99927719b8e
children c22ef5bc695a
files FLComm.agda FLutil.agda Putil.agda Solvable.agda
diffstat 4 files changed, 40 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Fri Nov 27 08:55:59 2020 +0900
+++ b/FLComm.agda	Fri Nov 27 20:54:55 2020 +0900
@@ -7,7 +7,7 @@
 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 ( [_] )
+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 
@@ -28,16 +28,17 @@
 open import Data.List.Fresh hiding ([_])
 open import Data.List.Fresh.Relation.Unary.Any
 
-open Solvable (Symmetric n)
+open Solvable (Symmetric n) 
+
+tl3 : (FL n) → ( z : FList n) → FList n → FList n
+tl3 h [] w = w
+tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
+tl2 : ( x z : FList n) → FList n →  FList n
+tl2 [] _ x = x
+tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
 
 CommFList  :  FList n →  FList n
-CommFList x =  tl2 x x [] where
-   tl3 : (FL n) → ( z : FList n) → FList n → FList n
-   tl3 h [] w = w
-   tl3 h (x ∷# z) w = tl3 h z (FLinsert ( perm→FL [ FL→perm h , FL→perm x ] ) w )
-   tl2 : ( x z : FList n) → FList n →  FList n
-   tl2 [] _ x = x
-   tl2 (h ∷# x) z w = tl2 x z (tl3 h z w)
+CommFList x =  tl2 x x [] 
 
 CommFListN  : ℕ  →  FList n
 CommFListN  0 = ∀Flist fmax
@@ -48,10 +49,22 @@
 
 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)
-CommStage→ (suc i) x uni = {!!}
-CommStage→ (suc i) x (comm {g} {h} p q) = {!!}
-CommStage→ (suc i) x (gen {f} {g} p q) = {!!}
-CommStage→ (suc i) x (ccong {f} {g} eq p) = {!!}
+CommStage→ (suc i) ε uni = comm0  (CommFListN i) (CommStage→ i ε deriving-ε) where
+   comm0 :  (L : FList n) → Any (_≡_ (perm→FL ε)) L →  Any (_≡_ (perm→FL ε)) (tl2 L L [])
+   comm0 = {!!}
+CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) where
+   G = perm→FL g
+   H = perm→FL h
+   comm2 : (L : FList n) → Any (G ≡_) L → Any (H ≡_) L → Any (perm→FL [ g , h ]  ≡_) (tl2 L L [])
+   comm2 L a b = {!!}
+CommStage→ (suc i) .(f ∘ₚ g) (gen {f} {g} p q) = comm3 (CommFListN i) (CommStage→ i f {!!}) (CommStage→ i g {!!}) where
+   G = perm→FL f
+   H = perm→FL g
+   comm3 : (L : FList n) → Any (G ≡_) L → Any (H ≡_) L → Any (perm→FL (f ∘ₚ g)  ≡_) (tl2 L L [])
+   comm3 L a b = {!!}
+CommStage→ (suc i) x (ccong {f} {x} eq p) = subst (λ k → Any (k ≡_) (tl2 (CommFListN i) (CommFListN i) [])) (comm4 eq) (CommStage→ (suc i) f p ) where
+   comm4 : f =p= x →  perm→FL f ≡ perm→FL x
+   comm4 = {!!} 
 
 CommSolved : (x : Permutation n n) → (y : FList n) → y ≡ FL0 ∷# [] → (FL→perm (FL0 {n}) =p= pid ) → Any (perm→FL x ≡_) y → x =p= pid
 CommSolved x .(cons FL0 [] (Level.lift tt)) refl eq0 (here eq) = FLpid _ eq eq0
--- a/FLutil.agda	Fri Nov 27 08:55:59 2020 +0900
+++ b/FLutil.agda	Fri Nov 27 20:54:55 2020 +0900
@@ -307,7 +307,7 @@
 
 AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 AnyFList {zero} f0 = here refl
-AnyFList {suc zero} (x :: f0) = ?
+AnyFList {suc zero} (x :: f0) = {!!}
 AnyFList {suc (suc n)} (x :: y) = AnyFList1 (suc n) a<sa (∀Flist fmax) (∀Flist fmax) fin<n (AnyFList y) where
    AnyFList1 :  (i : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → toℕ x < suc i → Any (y ≡_ ) L1 → Any ((x :: y) ≡_ ) (Flist i i<n L L1)
    AnyFList1 = {!!} 
--- a/Putil.agda	Fri Nov 27 08:55:59 2020 +0900
+++ b/Putil.agda	Fri Nov 27 20:54:55 2020 +0900
@@ -685,6 +685,15 @@
    pf0 : FL→perm (perm→FL x) =p= FL→perm FL0
    pf0 = pcong-Fp eq
 
+pFL0 : {n : ℕ } → FL0 {n} ≡ perm→FL pid
+pFL0 {zero} = refl
+pFL0 {suc n} = sym ( begin
+        perm→FL pid
+     ≡⟨⟩
+        {!!}
+     ≡⟨ {!!} ⟩
+        FL0
+     ∎  )
 
 lem2 : {i n : ℕ } → i ≤ n → i ≤ suc n
 lem2 i≤n = ≤-trans i≤n ( a≤sa )
--- a/Solvable.agda	Fri Nov 27 08:55:59 2020 +0900
+++ b/Solvable.agda	Fri Nov 27 20:54:55 2020 +0900
@@ -87,6 +87,10 @@
        ε
      ∎ 
 
+deriving-ε : { i : ℕ } → deriving i ε
+deriving-ε {zero} = lift tt
+deriving-ε {suc i} = ccong (idcomtr ε) (comm deriving-ε deriving-ε) 
+
 comm-refl : {f g : Carrier } → f ≈ g  → [ f ,  g ] ≈ ε 
 comm-refl {f} {g} f=g = begin
        f ⁻¹ ∙ g ⁻¹ ∙   f ∙ g