Mercurial > hg > Members > kono > Proof > galois

changeset 191:03d40f6e98b1

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 Sun, 29 Nov 2020 02:57:57 +0900
parents 2056fc69974c
children a670644d5624
files FLComm.agda FLutil.agda
diffstat 2 files changed, 11 insertions(+), 9 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Sun Nov 29 00:28:19 2020 +0900
+++ b/FLComm.agda	Sun Nov 29 02:57:57 2020 +0900
@@ -58,9 +58,7 @@
    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 (H ∷# cons a L1 x) (here refl) L3 = comm3 (cons a L1 x) {!!} {!!} where
-       L3' : FList n
-       L3' = tl3 G L1 (FLinsert (perm→FL [ FL→perm G , FL→perm a ]) (FLinsert (perm→FL [ FL→perm G , FL→perm H ]) L3))
+   comm3 (cons H (cons a L1 x) x₁) (here refl) L3 = {!!}
    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
@@ -68,7 +66,6 @@
        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) L4 L3 a = {!!}
-       -- subst (λ k → Any (_≡_ (perm→FL [ g , h ])) k) {!!} (comm8 L5 L4 (cons a L3 {!!}) a₁ ) 
        comm7 [] L3 = comm3 L1 b L3  
        comm7 (cons a L4 x) L3 = comm8 L1 L4 L3 a
    comm2 (cons x L xr) L1 (there a) b L3 = comm2 L L1 a b {!!}
--- a/FLutil.agda	Sun Nov 29 00:28:19 2020 +0900
+++ b/FLutil.agda	Sun Nov 29 02:57:57 2020 +0900
@@ -304,13 +304,18 @@
 nextAny (here x₁) = there (here x₁)
 nextAny (there any) = there (there any)
 
-
 AnyFList : {n : ℕ }  → (x : FL n ) →  Any (x ≡_ ) (∀Flist fmax)
 AnyFList {zero} f0 = here refl
-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 = {!!} 
+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)) 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 (((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 a L xr) L1 x<n (s≤s z≤n) (here refl) = x∈FLins (zero :: a) (Flist 0 i<n L L1)
+   AnyFList1 zero zero i<n (cons a L xr) L1 x<n (s≤s z≤n) (there wh) with AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh
+   ... | t = {!!}
+   AnyFList1 (suc i) x i<n L L1 x<n x<i wh = {!!}
 
 -- FLinsert membership