Mercurial > hg > Members > kono > Proof > galois

changeset 237:3aafd76f21c1

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 Wed, 09 Dec 2020 14:40:31 +0900
parents f8bfda8d0669
children c3a67bb7cbc0
files FLComm.agda
diffstat 1 files changed, 15 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Wed Dec 09 11:33:43 2020 +0900
+++ b/FLComm.agda	Wed Dec 09 14:40:31 2020 +0900
@@ -77,16 +77,26 @@
     allListF (s≤s z≤n) z = allListFL zero (allFL (anyFL0 n)) z
     allListF (s≤s (s≤s i<n)) z = allListFL (suc (fromℕ< (s≤s i<n ))) (allFL (anyFL0 n)) (allListF (<-trans (s≤s i<n) a<sa) z)
     anyFL3 :  {i : ℕ} → (i<n : i < suc (suc n)) (x : FL (suc (suc n))) → (toℕ (FLpos x ) ≤ i) → (z : FList (suc (suc n))) → Any (_≡_ x) (allListF i<n z)
-    anyFL3 {zero} (s≤s z≤n) (x :: y) x<i z = {!!} where
+    anyFL3 {zero} (s≤s z≤n) (x :: y) x<i z = anyFL6 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) (anyFL5 x<i) where
         anyFL5 : toℕ x ≤ zero → x ≡ zero
         anyFL5 lt with <-fcmp x zero
         ... | tri≈ ¬a b ¬c = b
         ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
-    anyFL3 {suc i} (s≤s i<n) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
-    ... | tri< a ¬b ¬c = anyFL1 i<n where
+        anyFL6 : (L : FList (suc n)) → Any (_≡_ y) L → x ≡ zero → Any (_≡_ (x :: y)) (allListFL zero L z)
+        anyFL6 (cons _ xs _) (here refl) refl = x∈FLins (x :: y)  (allListFL zero xs z)
+        anyFL6 (cons _ xs  _) (there any) refl = insAny _ (anyFL6 xs any refl )
+    anyFL3 {suc i} (s≤s (s≤s i<n)) (x :: y) x<i z with <-cmp (toℕ x) (suc i)
+    ... | tri< a ¬b ¬c = anyFL1 (s≤s i<n) where
         anyFL1 : {i : ℕ } → (i<n : i < suc n) →  Any (_≡_ (x :: y)) (allListF (s≤s i<n) z)
-        anyFL1 L = {!!}
-    ... | tri≈ ¬a b ¬c = {!!}
+        anyFL1 i<n = {!!}
+    ... | tri≈ ¬a b ¬c = anyFL7 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) where
+        anyFL8 : (L : FList (suc n)) → Any (_≡_ y) L →  Any (_≡_ (x :: y)) (allListFL x L
+                (allListF {!!} z)) -- b : toℕ x ≡ suc i
+        anyFL8 (cons _ xs _) (here refl) = x∈FLins (x :: y)  (allListFL x xs (allListF {!!} z))
+        anyFL8 (cons _ xs _) (there any) = insAny _ (anyFL8 xs any)
+        anyFL7 : (L : FList (suc n)) → Any (_≡_ y) L → Any (_≡_ (x :: y)) (allListF (s≤s (s≤s i<n)) z)
+        anyFL7 (cons _ xs _) (there any) = anyFL7 xs any
+        anyFL7 (cons _ xs _) (here refl) = subst (λ k →  Any (_≡_ (x :: y)) k) {!!} ( anyFL8 (allFL (anyFL0 n)) (anyP (anyFL0 n) y) )
     ... | tri> ¬a ¬b c = ⊥-elim (nat-≤> x<i c)
 
 anyFL :  (n : ℕ) → AnyFL n fmax