Mercurial > hg > Members > kono > Proof > galois

changeset 200:b5b4ee29cbe4

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
TERMINATING AnyFList
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 30 Nov 2020 12:27:07 +0900
parents 6c81c3d535d1
children a626ab1dbbcd
files FLComm.agda FLutil.agda
diffstat 2 files changed, 19 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Mon Nov 30 10:13:22 2020 +0900
+++ b/FLComm.agda	Mon Nov 30 12:27:07 2020 +0900
@@ -48,7 +48,7 @@
 open import Algebra 
 open Group (Symmetric n) hiding (refl)
 
-{-# TERMINATING #-}
+-- {-# 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
@@ -71,10 +71,11 @@
        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) L4 L3 a = {!!}
+       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₂)
        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 {!!}
+   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
    comm4 = pcong-pF
--- a/FLutil.agda	Mon Nov 30 10:13:22 2020 +0900
+++ b/FLutil.agda	Mon Nov 30 12:27:07 2020 +0900
@@ -314,24 +314,29 @@
 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)) 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
+         (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) = 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) = insAny _ (AnyFList1 zero zero i<n L L1 x<n (s≤s z≤n) wh)
-   AnyFList1 (suc i) x (s≤s i<n) (cons y L x₁) L1 x<n (s≤s x<i) (here refl) with <-fcmp (fromℕ< x<n) (fromℕ< (s≤s i<n))
-   ... | tri< a ¬b ¬c = insAny _ af1 where
-        af1 : Any (_≡_ (fromℕ< x<n :: y)) (Flist (suc i) (s≤s i<n) L L1)
-        af1 = AnyFList1 (suc i) x (s≤s i<n) L L1 x<n (s≤s x<i) {!!}
+   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 i<n (cons a L x₁) L1 x<n (s≤s x<i) (there wh) = {!!}
+   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