Mercurial > hg > Members > kono > Proof > automaton

changeset 347:5b985fea126e

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 Mon, 17 Jul 2023 21:02:46 +0900
parents bcf3ca6ba87b
children 8cd5bea05150
files automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/nat.agda
diffstat 2 files changed, 84 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 08:14:57 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 17 21:02:46 2023 +0900
@@ -3,8 +3,8 @@
 module finiteSetUtil  where
 
 open import Data.Nat hiding ( _≟_ )
-open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
-open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred )
+open import Data.Fin.Properties hiding ( <-trans ; ≤-trans ; ≤-refl ; <-irrelevant ) renaming ( <-cmp to <-fcmp )
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Definitions
@@ -572,44 +572,92 @@
 
 open import bijection using ( InjectiveF ; Is )
 
-record countB (B : Set) : Set where
-   field
-      cb : ℕ
-      ib : {i : ℕ} → i < cb → B
-      ib-inject : {i j : ℕ} → (i<cb : i < cb) → (j<cb : j < cb) → ib i<cb ≡ ib j<cb  → i ≡ j
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 inject-fin : {A B : Set}  (fa : FiniteSet A ) 
    → (fi : InjectiveF B A) 
    → (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a)  )
    → FiniteSet B
-inject-fin {A} {B} fa fi is-B = record {
-       finite = countB.cb (cb00 (finite fa) NP.≤-refl )
-       ; Q←F = λ fb → countB.ib (cb00 (finite fa) NP.≤-refl ) (fin<n {_} {fb})
-       ; F←Q =  λ b → fromℕ< (cb<cb (fin<n {_} {F←Q fa (InjectiveF.f fi b)} ))
+inject-fin {A} {B} fa fi is-B with finite fa | inspect finite fa
+... | zero | record { eq = eq1 } = ?
+... | suc pfa | record { eq = eq1 } = record {
+       finite = maxb
+       ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} {fb}))
+       ; F←Q = λ b → fromℕ< (cb<mb b)
        ; finiso→ = ?
        ; finiso← = ?
        } where
-   f = InjectiveF.f fi
-   cb00 : (i : ℕ) → i ≤ finite fa → countB B
-   cb00 0 i<fa = record { cb = 0 ; ib = λ () ; ib-inject = λ () }
-   cb00 (suc i) i<fa with is-B (Q←F fa (fromℕ< i<fa))
-   ... | yes y = record { cb = suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) ; ib = cb01 ; ib-inject = cb02 } where
-        pcb : countB B
-        pcb = cb00 i (NP.≤-trans a≤sa i<fa)
-        cb01 :  {j : ℕ} → j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) → B
-        cb01 {j} j<c with <-∨ j<c
-        ... | case1 eq = Is.a y
-        ... | case2 lt = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) lt
-        cb02 : {i1 : ℕ} {j : ℕ}
-            (i<cb : i1 < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))))
-            (j<cb : j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)))) →
-            cb01 i<cb ≡ cb01 j<cb → i1 ≡ j
-        cb02 = ?
-   ... | no n  = record { cb = countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))       ; ib = cb01 
-     ; ib-inject = countB.ib-inject (cb00 i (NP.≤-trans a≤sa i<fa))} where
-        cb01 :  {j : ℕ} → j < countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)) → B
-        cb01 {j} j<c = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) j<c
+    f = InjectiveF.f fi
+    pfa<fa : pfa < finite fa
+    pfa<fa = subst (λ k → pfa < k ) (sym eq1) a<sa
+    0<fa : 0 < finite fa
+    0<fa = <-transˡ (s≤s z≤n) pfa<fa  
+
+    count-B : ℕ → ℕ
+    count-B zero with is-B (Q←F fa ( fromℕ< {0} 0<fa ))
+    ... | yes isb = 1
+    ... | no nisb = 0
+    count-B (suc n) with <-cmp (finite fa) n
+    ... | tri< a ¬b ¬c = count-B n
+    ... | tri≈ ¬a b ¬c = count-B n
+    ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))
+    ... | yes isb = suc (count-B n)
+    ... | no nisb = count-B n
+
+    record CountB (n : ℕ)  : Set where
+       field
+          b : B
+          cb : ℕ
+          b=cn : cb ≡ toℕ (F←Q fa (f b))
+          cb=n : count-B cb ≡ suc n
+          cb-inject : (cb1 : ℕ) → (c1<a : cb1 < finite fa)  → Is B A f (Q←F fa (fromℕ< c1<a)) → count-B cb ≡ count-B cb1 → cb ≡ cb1
+
+    maxb : ℕ
+    maxb = count-B (finite fa)
+
+    cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb
+    cb<mb = ?
+
+    cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n
+    cb00 n n<cb = ? where
 
-   cb<cb : {i : ℕ} → (i<fa : i ≤ finite fa) → countB.cb (cb00 _ i<fa) < countB.cb (cb00 _ NP.≤-refl)  
-   cb<cb = ?
+        lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
+        lem07 n 0 eq with is-B (Q←F fa (fromℕ< ? )) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym ? ; cb=n = trans eq1 eq 
+                ; cb-inject = λ cb1 iscb1 cb1eq → ? } 
+        ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq ? )
+        lem07 n (suc i) eq with <-cmp (finite fa) i
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))| inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym ? ; cb=n = trans eq1 ?
+                 ; cb-inject = λ cb1 iscb1 cb1eq → ? } 
+        ... | no nisb | record { eq = eq1 } = lem07 n i ?
 
+        lem09 : (i j : ℕ) →  suc n ≤ j → j ≡ count-B i →  CountB n
+        lem09 0 (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n 0 (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with is-B (Q←F fa (fromℕ< ? )) | inspect count-B 0
+        ... | yes isb | record { eq = eq1 } = ⊥-elim ?
+        ... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) ?)
+        lem09 (suc i) (suc j) (s≤s le) eq with ≤-∨ (s≤s le)
+        ... | case1 eq1 = lem07 n (suc i) (sym (trans eq1 eq ))
+        ... | case2 (s≤s lt) with <-cmp (finite fa) i
+        ... | tri< a ¬b ¬c = ?
+        ... | tri≈ ¬a b ¬c = ?
+        ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c))| inspect count-B (suc i)
+        ... | yes isb | record { eq = eq1 } = ? -- lem09 i j lt ?
+        ... | no nisb | record { eq = eq1 } = ? -- lem09 i (suc j) (≤-trans lt a≤sa) ?
+
+        -- cb01 : (i j : ℕ) → suc n ≤ j  → j ≡ count-B j → CountB n
+        -- cb01 0 (suc j) (s≤s le) eq with
+        -- cb01 (suc i) (suc j) (s≤s le) eq = ?
+        -- cb01 (suc i) (suc j) j<fa i<cb with is-B (Q←F fa (fromℕ< j<fa ))
+        -- ... | yes y = record { b = Is.a y ; cb = suc (CountB.cb pcb)  ; b=cn = ? ; cb=n = ? ; cb-inject = ? }  where
+        --     pcb : CountB j
+        --     pcb = cb00 (suc
+        -- ... | no nb  = record { b = CountB.b pcb ; cb = CountB.cb pcb ; b=cn = CountB.b=cn pcb ; cb=n = ? ; cb-inject = ? } where
+        --     pcb : CountB j
+        --     pcb = cb00 i j (<-trans a<sa j<fa)
+
+-- end
--- a/automaton-in-agda/src/nat.agda	Mon Jul 17 08:14:57 2023 +0900
+++ b/automaton-in-agda/src/nat.agda	Mon Jul 17 21:02:46 2023 +0900
@@ -287,6 +287,9 @@
 x≤y→x<sy {.zero} {y} z≤n = ≤-trans a<sa (s≤s z≤n)
 x≤y→x<sy {.(suc _)} {.(suc _)} (s≤s le) = s≤s ( x≤y→x<sy le) 
 
+sx≤y→x<y : {x y : ℕ } → suc x ≤ y → x < y 
+sx≤y→x<y {zero} {suc y} (s≤s le) = s≤s z≤n
+sx≤y→x<y {suc x} {suc y} (s≤s le) = s≤s ( sx≤y→x<y {x} {y} le )
 
 open import Data.Product