Mercurial > hg > Members > kono > Proof > galois

changeset 240:2b7b343616af

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
all done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 09 Dec 2020 18:59:14 +0900
parents f45298e34491
children 2a7d092e1240
files FLComm.agda FLutil.agda
diffstat 2 files changed, 41 insertions(+), 149 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Wed Dec 09 17:33:55 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 18:59:14 2020 +0900
@@ -36,24 +36,13 @@
 -- open import Relation.Nary using (⌊_⌋)
 open import Relation.Nullary.Decidable hiding (⌊_⌋)
 
--- 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)   
-
 -------------
---    # 0 : # 0 : .... # 0 : # 0 :: f0
---    # 0 : # 0 : .... # 1 : # 0 :: f0
---   
---    # sn: # 0 : .... # 0 : # 0 :: f0
---   
---    # sn: # n : .... # 1 : # 0 :: f0
---  
+--    # 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
+--       ...
 
 -- all FL
 record AnyFL (n : ℕ) (y : FL n) : Set where
@@ -64,7 +53,6 @@
 open import fin
 open AnyFL
 
--- {-# TERMINATING #-}
 anyFL0 :  (n : ℕ) → AnyFL (suc n) fmax
 anyFL0 zero = record { allFL = (zero :: f0) ∷# [] ; anyP = anyFL2 } where 
     anyFL2 : (x : FL 1) → Any (_≡_ x) (cons (zero :: f0) [] (Level.lift tt))
@@ -90,7 +78,7 @@
         anyFL1  : {i : ℕ} → (i<n : i < suc n) → (x<i : suc (toℕ x) ≤ suc i )  →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
         anyFL10 : {i : ℕ} → (i<n : i < suc n ) → (x<i : suc (toℕ x) ≤ suc i) → (L : FList (suc n))  
             → Any (_≡_ (x :: y))  (allListFL (suc (fromℕ< i<n)) L (allListF (<-trans i<n a<sa) z) )
-        anyFL10 {i} (s≤s j<n) (s≤s x<i) [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) x<i z  --  where suc (toℕ x) ≤ suc i → toℕ x ≤ i
+        anyFL10 {i} (s≤s j<n) (s≤s x<i) [] = anyFL3 (<-trans (s≤s j<n) a<sa) (x :: y) x<i z  
         anyFL10 {i} i<n x<i (cons _ xs _)  = insAny _ (anyFL10 {i} i<n x<i xs )
         anyFL1 {i} (s≤s i<n) x<i = anyFL10 (s≤s i<n ) x<i (allFL (anyFL0 n)) 
     ... | tri≈ ¬a b ¬c = anyFL7 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) where
@@ -116,26 +104,13 @@
     anyFL4 f0 = here refl
 anyFL (suc n) = anyFL0 n
 
-at1 = allFL (anyFL 1)
-at2 = allFL (anyFL 2)
-at3 = allFL (anyFL 3)
-
-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 [] 
-
-CommFListN  : ℕ  →  FList n
-CommFListN  0 = ∀Flist fmax
-CommFListN  (suc i) = CommFList (CommFListN i)
+at1 = toList (allFL (anyFL 1))
+at2 = toList (allFL (anyFL 2))
+at3 = toList (allFL (anyFL 3))
+at4 = toList (allFL (anyFL 4))
 
 -- all cobmbination in P and Q
-record AnyComm  (P Q : FList n) (fpq : (p q : FL n) → FL n) : Set where
+record AnyComm {n : ℕ}  (P Q : FList n) (fpq : (p q : FL n) → FL n) : Set where
    field
      commList : FList n
      commAny : (p q : FL n)
@@ -148,25 +123,25 @@
 --     :        AnyComm FL0 FL0 P  Q
 --    p0,q       
 
-p<anyL : {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → p f≤ p₁
-p<anyL {p} {p₁} {P} {pr} (here refl) = case1 refl
-p<anyL {p} {p₁} {cons a P x} { Data.Product._,_ (Level.lift p<a) snd} (there any) with p<anyL any
+p<anyL : {n : ℕ } {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → p f≤ p₁
+p<anyL {n} {p} {p₁} {P} {pr} (here refl) = case1 refl
+p<anyL {n} {p} {p₁} {cons a P x} { Data.Product._,_ (Level.lift p<a) snd} (there any) with p<anyL any
 ... | case1 refl = case2 (toWitness p<a)
 ... | case2 a<p₁ = case2 (f<-trans (toWitness p<a) a<p₁)
 
-p<anyL1 : {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → ¬ (p ≡ p₁)  → p f< p₁
-p<anyL1 {p} {p₁} {P} {pr} any neq with p<anyL any
+p<anyL1 : {n : ℕ } {p p₁ : FL n} {P : FList n} → {pr : fresh (FL n) ⌊ _f<?_ ⌋ p P } → Any (_≡_ p₁) (cons p P pr) → ¬ (p ≡ p₁)  → p f< p₁
+p<anyL1 {n} {p} {p₁} {P} {pr} any neq with p<anyL any
 ... | case1 eq = ⊥-elim ( neq eq )
 ... | case2 x = x
 
 open AnyComm 
-anyComm : (P Q : FList n) → (fpq : (p q : FL n) → FL n)  → AnyComm P Q fpq
+anyComm : {n : ℕ } → (P Q : FList n) → (fpq : (p q : FL n) → FL n)  → 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 (cons p P pr) (cons q Q qr) fpq = record { commList = FLinsert (fpq p q) (commListQ Q)  ; commAny = anyc0n } where 
+anyComm {n} (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 n
-  commListP [] = commList (anyComm P Q fpq)
+  commListP [] = commList (anyComm {n} P Q fpq)
   commListP (cons p₁ P1 x) =  FLinsert (fpq p₁ q) (commListP P1)
   commListQ : (Q1 : FList n) → FList n
   commListQ [] = commListP P
@@ -193,68 +168,28 @@
      anyc04 [] = anyc05 P 
      anyc04 (cons a Q1 x) = insAny _ (anyc04 Q1)
 
--- {-# 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)
-CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 (CommFListN i) (CommFListN i) (CommStage→ i g p) (CommStage→ i h q) [] where
-   G = perm→FL g
-   H = perm→FL h
-
-   -- tl3 case
-   commc :  (L3 L1 : FList n) →  Any ((perm→FL [  FL→perm G , FL→perm H ]) ≡_) L3 
-           →  Any ((perm→FL [ FL→perm G , FL→perm H ]) ≡_) (tl3 G L1 L3)
-   commc L3 [] any = any
-   commc L3 (cons a L1 _) any = commc (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3) L1 (insAny _ any)
-   comm6 : perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
-   comm6 = pcong-pF (comm-resp (FL←iso _) (FL←iso _))  
-   comm3 : (L1 : FList n) → Any (H ≡_) L1 → (L3 : FList n) → Any ((perm→FL [ g , h ]) ≡_) (tl3 G L1 L3)
-   comm3 (H ∷# []) (here refl) L3 = subst (λ k → Any (k ≡_) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) )
-       comm6 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3 )
-   comm3 (cons H L1 x₁) (here refl) L3 = subst (λ k → Any (k ≡_) (tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))) comm6
-       (commc (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3 ) L1 (x∈FLins ( perm→FL [ FL→perm G , FL→perm H ] ) L3))
-   comm3 (cons a L  _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3)
+CommFListN  : ℕ →  FList n
+CommFListN  zero = allFL (anyFL n)
+CommFListN (suc i ) = commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))
 
-   -- tl2 case
-   comm2 : (L L1 : FList n) → Any (G ≡_) L → Any (H ≡_) L1 → (L3 : FList n) → Any (perm→FL [ g , h ] ≡_ ) (tl2 L L1 L3)
-   comm2 (cons G L xr) L1 (here refl) b L3 = comm7 L L3 where
-       comm8 : (L L4 L2 : FList n) → (a : FL n) 
-            → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2)
-            → Any ((perm→FL [ g , h ]) ≡_ ) (tl2 L4 L1 (tl3 a L L2))
-       comm8← : (L L4 L2 : FList n) → (a : FL n)  → ¬ ( a ≡ perm→FL g )
-           →  Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (tl3 a L L2))
-           →  Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2)
-       comm9← : (L4 L2 : FList n) → (a a₁ : FL n) → ¬ ( a ≡ perm→FL g )
-           → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
-           → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) 
-       --  Any (_≡ (perm→FL [ g , h ])) (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) → Any ((perm→FL [ g , h ]) ≡_) L2
-       comm9← [] L2 a a₁ not any = {!!}
-       comm9← (cons a₂ L4 x) L2 a a₁ not any = comm8 L1 L4 L2 a₂
-           (comm9← L4 L2 a a₁ not
-           (comm8← L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2 ) a₂ {!!} any)) 
-       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) →
-       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
-       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 L2)
-       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a₂ L1 L2))
-       comm8← [] L4 L2 a _ any = any 
-       comm8← (cons a₁ L x) L4 L2 a not any  = comm8← L  L4 L2 a not
-            (comm9← L4 (tl3 a L L2 ) a a₁ not (subst (λ k →  Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1  k )) {!!} any ))
-       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))) →
-       -- Any (_≡ (perm→FL [ g , h ])) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) (tl3 a L L2)))
-       comm9 : (L4 L2 : FList n) → (a a₁ : FL n) → Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 L2) →
-                                                   Any ((perm→FL [ g , h ]) ≡_) (tl2 L4 L1 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2))
-       comm8 [] L4 L2 a any = any
-       comm8 (cons a₁ L x) L4 L2 a any =  comm8 L  L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a  (comm9 L4 L2 a a₁ any)
-       comm9 [] L2 a a₁ any = insAny _ any
-       comm9 (cons a₂ L4 x) L2 a a₁ any = comm8 L1 L4 (FLinsert (perm→FL [ FL→perm a , FL→perm a₁ ]) L2) a₂ (comm9 L4 L2 a a₁ (comm8← L1 L4 L2 a₂ {!!} any))
-       -- found g, we have to walk thru till the end
-       comm7 : (L L3 : FList n) → Any ((perm→FL [ g , h ]) ≡_) (tl2 L L1 (tl3 G L1 L3))
-       -- at the end, find h
-       comm7 [] L3 = comm3 L1 b L3  
-       -- add n path
-       comm7 (cons a L4 xr) L3 = comm8 L1 L4 (tl3 G L1 L3) a (comm7 L4 L3)
-   -- accumerate tl3
-   comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b (tl3 x L1 L3)
-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
+CommStage→ : (i : ℕ) → (x : Permutation n n ) → deriving i x → Any (perm→FL x ≡_) (CommFListN i)
+CommStage→ zero x (Level.lift tt) = anyP (anyFL n) (perm→FL x)
+CommStage→ (suc i) .( [ g , h ] ) (comm {g} {h} p q) = comm2 where
+  G = perm→FL g
+  H = perm→FL h
+  comm3 :  perm→FL [ FL→perm G , FL→perm H ] ≡ perm→FL [ g , h ]
+  comm3 = begin
+              perm→FL [ FL→perm G , FL→perm H ] 
+           ≡⟨ pcong-pF (comm-resp (FL←iso _) (FL←iso _)) ⟩
+              perm→FL [ g , h ]
+          ∎  where open ≡-Reasoning
+  comm2 : Any (_≡_ (perm→FL [ g , h ])) (CommFListN (suc i))
+  comm2 = subst (λ k → Any (_≡_ k) (CommFListN (suc i)) ) comm3
+     ( commAny ( anyComm (CommFListN i) (CommFListN i) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] )) G H (CommStage→ i g p) (CommStage→ i h q) )
+
+CommStage→ (suc i) x (ccong {f} {x} eq p) =
+      subst (λ k → Any (k ≡_) (commList (anyComm ( CommFListN i ) ( CommFListN i ) (λ p q →  perm→FL [ FL→perm p , FL→perm q ] ))))
+          (comm4 eq) (CommStage→ (suc i) f p ) where
    comm4 : f =p= x →  perm→FL f ≡ perm→FL x
    comm4 = pcong-pF
 
--- a/FLutil.agda	Wed Dec 09 17:33:55 2020 +0900
+++ b/FLutil.agda	Wed Dec 09 18:59:14 2020 +0900
@@ -265,28 +265,9 @@
 
 fr6 = FLinsert ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) fr1 
 
--- open import Data.List.Fresh.Relation.Unary.All
--- fr7 = append ( ((# 1) :: ((# 1) :: ((# 0 ) :: f0))) ∷# [] ) fr1 ( ({!!} , {!!} ) ∷ [] )
-
-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)   
-
 ¬x<FL0 : {n : ℕ} {x : FL n} → ¬ ( x f< FL0 )
 ¬x<FL0 {suc n} {zero :: y} (f<t not) = ¬x<FL0 {n} {y} not
 
-fr8 : FList 4
-fr8 = ∀Flist fmax 
-
-fr9 : FList 3
-fr9 = ∀Flist fmax 
-
 open import Data.List.Fresh.Relation.Unary.Any 
 open import Data.List.Fresh.Relation.Unary.All 
 
@@ -314,30 +295,6 @@
 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)
 
-{-# TERMINATING #-}
-AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_) (∀Flist fmax)
-AnyFList {zero} f0 = here refl
-AnyFList {suc zero} (zero :: f0) = here refl
-AnyFList {suc (suc n)} (x :: y) = subst (λ k → Any ((k :: y) ≡_) (Flist (suc n) a<sa (∀Flist fmax) (∀Flist fmax) ))
-         (fromℕ<-toℕ _ _) ( AnyFList1 (suc n) (toℕ x) a<sa (∀Flist fmax) (∀Flist fmax) fin<n fin<n (AnyFList y) (AnyFList y)) where
-   AnyFList1 :  (i x : ℕ) → (i<n : i < suc (suc n) ) → (L L1 : FList (suc n) ) → (x<n : x < suc (suc n) ) → x < suc i
-        → Any (y ≡_) L → Any (y  ≡_) L1
-        → Any (((fromℕ< x<n) :: y) ≡_) (Flist i i<n L L1)
-   AnyFList1 zero x i<n [] L1 (s≤s x<i) _ () _
-   AnyFList1 zero zero i<n (cons y L xr) L1 x<n (s≤s z≤n) (here refl) any = x∈FLins (zero :: y) (Flist 0 i<n L L1)
-   AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) any = insAny _ (AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh any)
-   AnyFList1 (suc i) x (s≤s i<n) (cons y L x₁) L1 x<n (s≤s x<i) (here refl) any with <-fcmp (fromℕ< x<n) (fromℕ< (s≤s i<n))
-   ... | tri< a ¬b ¬c = insAny  (Flist (suc i) (s≤s i<n) L L1) (af1 L ) where
-        af1 : (L : FList (suc n)) → Any ((fromℕ< x<n :: y) ≡_) (Flist (suc i) (s≤s i<n) L L1)
-        af1 [] = AnyFList1 i x (<-trans i<n a<sa) L1 L1 x<n (subst₂ (λ j k → j < k )  (toℕ-fromℕ< _) (cong suc  (toℕ-fromℕ< _)) a )  any any
-        af1 (cons a L x) = insAny (Flist (suc i) (s≤s i<n) L L1) (af1 L )
-   ... | tri≈ ¬a b ¬c = subst (λ k → Any ((fromℕ< x<n :: y) ≡_) (FLinsert k  (Flist (suc i) (s≤s i<n) L L1) )) (cong (λ k → k :: y) b)
-        (x∈FLins (fromℕ< x<n :: y) (Flist (suc i) (s≤s i<n) L L1))
-   ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> x<i (subst₂ (λ j k → suc (suc k) ≤ j ) (toℕ-fromℕ< _) (toℕ-fromℕ< _) c) )
-   AnyFList1 (suc i) x (s≤s i<n) (cons a (cons a₁ L x₂) x₁) L1 x<n (s≤s x<i) (there wh) any with FLcmp a a₁
-   ... | tri< a₂ ¬b ¬c = insAny _ (AnyFList1 (suc i) x (s≤s i<n) (cons a₁ L x₂) L1 x<n (s≤s x<i) wh any )
-   AnyFList1 (suc i) x (s≤s i<n) (cons a (cons .a L x₂) (Level.lift () , snd)) L1 x<n (s≤s x<i) (there wh) any | tri≈ ¬a refl ¬c
-
 -- FLinsert membership
 
 module FLMB { n : ℕ } where