Mercurial > hg > Members > kono > Proof > galois

changeset 245:ee27673aa3fe

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
irr
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 10 Dec 2020 19:09:50 +0900
parents f1f76eed9335
children d8f6d04edbbc
files FLComm.agda
diffstat 1 files changed, 14 insertions(+), 4 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Thu Dec 10 17:15:54 2020 +0900
+++ b/FLComm.agda	Thu Dec 10 19:09:50 2020 +0900
@@ -188,13 +188,23 @@
 anyFL01 zero    = record { allFL = (zero :: f0) ∷# [] ; anyP = λ x → anyFL2 x ((zero :: f0) ∷# []) refl } 
 anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
      anyFL04 :  (n : ℕ) → AnyFin n
-     anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = anyFL06 a<sa} where
+     anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = λ {j} j<n → anyFL06 {n} {j} a<sa j<n (anyFL07 j<n) } where 
+         anyFL07 : {j : ℕ } → j < suc n → j ≤ n
+         anyFL07 (s≤s j<n) = j<n
          anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
          anyFL05 {0} (s≤s z≤n) = zero :: FL0 ∷# []
          anyFL05 {suc i} (s≤s i<n) = FLinsert (fromℕ< (s≤s i<n) :: FL0) (anyFL05 {i} (<-trans i<n a<sa))
-         anyFL06 : {i j : ℕ} (i<n : i < suc n) → (j<n : j < suc n) → Any (_≡_ (fromℕ< j<n :: FL0)) (anyFL05 i<n)
-         anyFL06 {0} (s≤s z≤n) = here refl
-         anyFL06 {i} i<n = {!!}
+         anyFL06 : {i j : ℕ} (i<n : i < suc n) → (j<n : j < suc n) → (j≤i : j ≤ i) → Any (_≡_ (fromℕ< j<n :: FL0)) (anyFL05 i<n)
+         anyFL06 {0} {zero} (s≤s z≤n) j<n j≤i = here refl
+         anyFL06 {suc i} {0} (s≤s i<n) j<n j≤i = insAny _ (anyFL06 {i} {0} (<-trans i<n a<sa) j<n z≤n)
+         anyFL06 {suc i} {j} (s≤s i<n) j<n (s≤s j≤i) with <-cmp j (suc i)
+         ... | tri> ¬a ¬b c = ⊥-elim ( nat-≤> (s≤s j≤i) c) 
+         ... | tri< (s≤s a) ¬b ¬c = insAny _ (anyFL06 {i} {j} (<-trans i<n a<sa) j<n a)
+         ... | tri≈ ¬a refl ¬c = subst (λ k →  Any (_≡_ _) (FLinsert (suc k :: FL0) (anyFL05 (<-trans i<n a<sa))) ) (anyFL08 i<n j<n)
+              (x∈FLins  (suc (fromℕ< (≤-pred j<n)) :: FL0) (anyFL05 (<-trans i<n a<sa)))
+          where
+             anyFL08 : {i n : ℕ } (i<n : suc i ≤ n) (j<n : suc (suc i) ≤ suc n) → fromℕ< (≤-pred j<n) ≡ fromℕ< i<n
+             anyFL08 {i} {n} i<n j<n = ?
      anyC = anyComm (allFin (anyFL04 (suc n))) (allFL (anyFL01 n)) (λ p q → FLpos p :: q )
      anyFL02 : (x : FL (suc (suc n))) → Any (_≡_ x) (commList anyC)
      anyFL02 (x :: y) = commAny anyC (x :: FL0) y