Mercurial > hg > Members > kono > Proof > automaton

changeset 363:21aa222b11c9

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
finiteSet from fin injection done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 19 Jul 2023 07:58:18 +0900
parents 6d5344d3be9c
children 00f5076ef2de
files automaton-in-agda/src/finiteSetUtil.agda
diffstat 1 files changed, 30 insertions(+), 14 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Wed Jul 19 07:08:43 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Wed Jul 19 07:58:18 2023 +0900
@@ -704,8 +704,8 @@
             →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i ≡ count-B j → i ≡ j
         lem06 i j i<fa j<fa bi bj eq = lem08 where
             lem20 : (i j : ℕ) → i < j → (i<fa : i < finite fa) (j<fa : j < finite fa) 
-                →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B j ≡ count-B i → ⊥
-            lem20 zero (suc j) i<j i<fa j<fa bi bj le with <-cmp (finite fa) (suc j) 
+                →  Is B A f (Q←F fa (fromℕ< i<fa)) → Is B A f (Q←F fa (fromℕ< j<fa)) → count-B i < count-B j
+            lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc j) 
             ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
             ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
             ... | tri> ¬a ¬b c with  is-B (Q←F fa ( fromℕ< 0<fa )) | inspect count-B 0 | is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
@@ -715,23 +715,39 @@
             ... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where
                  lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
                  lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
-            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where
-                 lem24 : count-B j ≡ 0
-                 lem24 = cong pred le
-                 lem25 : 1 ≤ 0
+            ... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = lem25 where
+                 lem25 : 2 ≤ suc (count-B j)
                  lem25 = begin
-                    1 ≡⟨ sym eq1 ⟩
-                    count-B 0 ≤⟨ count-B-mono {0} {j} z≤n ⟩
-                    count-B j ≡⟨ lem24 ⟩
-                    0 ∎ where open ≤-Reasoning
-            lem20 (suc i) zero () bi bj le
-            lem20 (suc i) (suc j) (s≤s i<j) bi bj le = ?
+                    2 ≡⟨ cong suc (sym eq1) ⟩
+                    suc (count-B 0) ≤⟨ s≤s (count-B-mono {0} {j} z≤n) ⟩
+                    suc (count-B j)  ∎ where open ≤-Reasoning
+            lem20 (suc i) zero () i<fa j<fa bi bj 
+            lem20 (suc i) (suc j) (s≤s i<j) i<fa j<fa bi bj = lem21 where
+                 --
+                 --                    i  <     suc i  ≤    j
+                 --    cb i <  suc (cb i) < cb (suc i) ≤ cb j
+                 --
+                 lem23 : suc (count-B j) ≡ count-B (suc j)
+                 lem23 with <-cmp (finite fa) (suc j)
+                 ... | tri< a ¬b ¬c = ⊥-elim (¬c j<fa)
+                 ... | tri≈ ¬a b ¬c = ⊥-elim (¬c j<fa)
+                 ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | inspect count-B (suc j)
+                 ... | yes _ | record { eq = eq1 } = refl
+                 ... | no nisa | _ = ⊥-elim ( nisa record { a = Is.a bj ; fa=c = lem26 } ) where
+                     lem26 : f (Is.a bj) ≡ Q←F fa (fromℕ< c)
+                     lem26 = trans (Is.fa=c bj) (cong (Q←F fa) (fromℕ<-cong _ _ refl j<fa c) )
+                 lem21 : count-B (suc i) < count-B (suc j)
+                 lem21 = sx≤py→x≤y ( begin
+                     suc (suc (count-B (suc i))) ≤⟨ s≤s ( s≤s ( count-B-mono i<j )) ⟩
+                     suc (suc (count-B j)) ≡⟨ cong suc lem23 ⟩
+                     suc (count-B (suc j))   ∎ ) where
+                        open ≤-Reasoning
 
             lem08 : i ≡ j
             lem08 with <-cmp i j
-            ... | tri< a ¬b ¬c = ⊥-elim ? -- ( lem20 i j a i<fa j<fa bi bj (sym eq) )
+            ... | tri< a ¬b ¬c = ⊥-elim (nat-≡< eq ( lem20 i j a i<fa j<fa bi bj  ))
             ... | tri≈ ¬a b ¬c = b
-            ... | tri> ¬a ¬b c₁ = ⊥-elim ? -- ( lem20 j i c₁ j<fa i<fa bj bi eq )
+            ... | tri> ¬a ¬b c₁ = ⊥-elim (nat-≡< (sym eq) ( lem20 j i c₁ j<fa i<fa bj bi ))
 
         lem09 : (i j : ℕ) →  suc n ≤ j → j ≡ count-B i →  CountB n
         lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) | inspect count-B 0