Mercurial > hg > Members > kono > Proof > galois

changeset 201:a626ab1dbbcd

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
comm8
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Nov 2020 18:02:06 +0900
parents b5b4ee29cbe4
children d9f610c9a4f1
files FLComm.agda
diffstat 1 files changed, 11 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Mon Nov 30 12:27:07 2020 +0900
+++ b/FLComm.agda	Mon Nov 30 18:02:06 2020 +0900
@@ -68,13 +68,19 @@
    comm3 (cons a L  _) (there b) L3 = comm3 L b (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) L3)
    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 : (L5 L4 L3 : FList n) → (a : FL n)
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1           (tl3 G L1 L3))
+            → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L5 (tl3 G L1 L3)))
+       comm8 L5 [] L3 a any = {!!}
+       comm8 L5 (cons a₁ L4 x) L3 a any with comm8 L5 L4 L3 a₁ {!!}
+       ... | t = {!!}
+       -- 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))
-       comm8 : (L5 L4 L3 : FList n) → (a : FL n) → Any (_≡_ (perm→FL [ g , h ])) (tl2 L4 L1 (tl3 a L5 (tl3 (perm→FL g) L1 L3)))
-       comm8 [] L4 L3 a = comm7 L4 L3
-       comm8 (cons a₁ L5 x) [] L3 a = {!!}
-       comm8 (cons a₁ L5 x) (cons a₂ L4 x₁) L3 a = subst (λ k →  Any (_≡_ (perm→FL [ g , h ])) k) {!!} (comm8 L5 (cons a₂ L4 x₁) L3 a₂)
+       -- at the end, find h
        comm7 [] L3 = comm3 L1 b L3  
-       comm7 (cons a L4 x) L3 = comm8 L1 L4 L3 a
+       -- add n path
+       comm7 (cons a L4 x) L3 = comm8 L1 L4 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
    comm4 : f =p= x →  perm→FL f ≡ perm→FL x