Mercurial > hg > Members > kono > Proof > galois

changeset 246:d8f6d04edbbc

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
AnyFL from AnyFin and anyComm
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Thu, 10 Dec 2020 19:15:25 +0900
parents ee27673aa3fe
children 80b9fb5f80ab
files FLComm.agda
diffstat 1 files changed, 3 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/FLComm.agda	Thu Dec 10 19:09:50 2020 +0900
+++ b/FLComm.agda	Thu Dec 10 19:15:25 2020 +0900
@@ -189,6 +189,9 @@
 anyFL01 (suc n) = record { allFL = commList anyC ;  anyP =  anyFL02 } where
      anyFL04 :  (n : ℕ) → AnyFin n
      anyFL04 n = record { allFin = anyFL05 a<sa ; anyF = λ {j} j<n → anyFL06 {n} {j} a<sa j<n (anyFL07 j<n) } where 
+         anyFL08 : {i n : ℕ } (i<n : suc i ≤ n) (j<n : suc (suc i) ≤ suc n) → fromℕ< (≤-pred j<n) ≡ fromℕ< i<n
+         anyFL08 {zero} {.(suc _)} (s≤s z≤n) (s≤s (s≤s j<n)) = refl
+         anyFL08 {suc i} {.(suc _)} (s≤s i<n) (s≤s j<n) = cong (λ k → suc k ) (anyFL08 (i<n) (j<n) )
          anyFL07 : {j : ℕ } → j < suc n → j ≤ n
          anyFL07 (s≤s j<n) = j<n
          anyFL05 : {i : ℕ} → (i < suc n) → FList (suc n)
@@ -202,9 +205,6 @@
          ... | 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