Mercurial > hg > Members > kono > Proof > galois

changeset 223:9da456c2bfe3

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 Mon, 07 Dec 2020 20:29:13 +0900
parents 9f86424a09b1
children 71e08656273b
files FLComm.agda
diffstat 1 files changed, 18 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Mon Dec 07 06:59:38 2020 +0900
+++ b/FLComm.agda	Mon Dec 07 20:29:13 2020 +0900
@@ -111,38 +111,25 @@
 anyComm [] [] = record { commList = [] ; commAny = λ _ _ () }
 anyComm [] (cons q Q qr) = record { commList = [] ; commAny = λ _ _ () }
 anyComm (cons p P pr) [] = record { commList = [] ; commAny = λ _ _ _ () }
-anyComm (cons p P pr) (cons q Q qr) = anyc0n Q where
-  insAnyComm : {p₁ q₁ h : FL n } → (xs : FList n)  → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) xs
-        → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert h xs)
-  insAnyComm xs any = insAny _ any
-  anyc04 : (x b : FL n) → (L : FList n) → Any (x ≡_)  L → Any (x ≡_)  (FLinsert b L)
-  anyc04 a b L any = insAny L any
-
+anyComm (cons p P pr) (cons q Q qr) = anyc0n (cons q Q qr) where
   anyc0n : (Q1 : FList n) → AnyComm (cons p P pr) (cons q Q qr)
-  anyc01 :  (Q1 : FList n)  (q₁ : FL n) → (qr₁ : fresh (FL n) ⌊ _f<?_ ⌋ q₁ Q1 ) → (p₁ q₂ : FL n) → Any (p₁ ≡_) (cons p P pr) → Any (q₂ ≡_) (cons q Q qr) →
-    Any (perm→FL [ FL→perm p₁ , FL→perm q₂ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ])  (commList (anyc0n Q1)) ) 
-  anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (here refl) = {!!}
-  anyc01 [] q₁ qr₁ p₁ q₂ (here refl) (there anyq) with anyc04 (perm→FL [ FL→perm p , FL→perm q₁ ]) (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n [])) {!!}
-  ... | t = {!!}
-  anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (here refl) =  {!!} 
-  anyc01 [] q₁ qr₁ p₁ q₂ (there anyp) (there anyq) = {!!} --  insAny (commList (anyc0n [])) {!!}  -- (commAny (anyc0n [])  p₁  q₂ (here refl) (there anyq) )
-  anyc01 (cons q₃ Q1 qr₃) q₁ qr₁ p₁ q₂ anyp anyq = {!!}
-  anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = {!!} } where
-    anyc03 :  (P Q : FList n) → (p₁ q₁ : FL n) 
-        → Any (p₁ ≡_) P → Any (q₁ ≡_) Q
-        → Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P Q))) 
-    anyc03 = {!!} where
-       anyc05 :  (P Q : FList n) → (p₁ q₁ : FL n) 
-           → Any (p₁ ≡_) P → Any (q₁ ≡_) Q → (x y : FL n) → ( z : FList n )
-           → Any (x ≡_) z 
-           → Any (x ≡_) (FLinsert y z) 
-       anyc05 P Q p₁ q₁ anyp anyq x y z anyz = {!!}
-       anyc07 : (x b : FL n) → (L : FList n) → Any (x ≡_)  L → Any (x ≡_)  (FLinsert b L)
-       anyc07 a b L any = insAny L any
-       anyc06 : (x y : FL n) → ( z : FList n ) → Any (x ≡_) z → Any (x ≡_) (FLinsert y z) 
-       anyc06 x y z anyz = insAny  z anyz
-  anyc0n (cons q₁ Q1 qr₁ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₁ ]) (commList (anyc0n Q1)) 
-                                 ; commAny = {!!}  }
+  anyc0n [] = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))) ; commAny = anyc03 } where
+    anyc03 :  (p₁ q₁ : FL n) →
+        Any ( p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr)
+        → Any ((perm→FL [ FL→perm p₁ , FL→perm q₁ ]) ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q ]) (commList (anyComm P (cons q Q qr))))
+    anyc03 p₁ q₁ (there anyp) (here x)     = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (here x))
+    anyc03 p₁ q₁ (there anyp) (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ anyp (there anyq))
+    anyc03 p₁ q₁ (here refl)  (there anyq) = insAny _ (commAny (anyComm P (cons q Q qr)) p₁ q₁ (here refl) (there anyq))
+    anyc03 p₁ q₁ (here refl)  (here x) = {!!}
+  anyc0n (cons q₂ Q1 qr₂ ) = record { commList = FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ]) (commList (anyc0n Q1)) 
+                                 ; commAny = anyc01 Q1 q₂ qr₂ } where
+    anyc01 :  (Q1 : FList n)  (q₂ : FL n) → (qr₂ : fresh (FL n) ⌊ _f<?_ ⌋ q₂ Q1 ) → (p₁ q₁ : FL n) → Any (p₁ ≡_) (cons p P pr) → Any (q₁ ≡_) (cons q Q qr) →
+      Any (perm→FL [ FL→perm p₁ , FL→perm q₁ ] ≡_) (FLinsert (perm→FL [ FL→perm p , FL→perm q₂ ])  (commList (anyc0n Q1)) ) 
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (there anyq)  = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (here refl)  (there anyq))
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (here refl)  = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (there anyp) (here refl))
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (there anyp) (there anyq) = insAny _ (commAny (anyc0n Q1)  p₁ q₁ (there anyp) (there anyq) )
+    anyc01 Q1 q₂ qr₂ p₁ q₁ (here refl) (here refl) with  x∈FLins (perm→FL [ FL→perm p , FL→perm q₂ ])  (commList (anyc0n Q1)) 
+    ... | t = {!!}    -- t : p₁ q₂ → p₁ q₁  
 
 -- {-# TERMINATING #-}
 CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) ( CommFListN i )