Members/kono/Proof/automaton: automaton-in-agda/src/finiteSetUtil.agda comparison

comparison automaton-in-agda/src/finiteSetUtil.agda @ 346:4456eebbd1bc

copying countable bijection may not easy

author	Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date	Mon, 17 Jul 2023 11:00:19 +0900
parents	bcf3ca6ba87b
children

comparison

equal deleted inserted replaced

-:bcf3ca6ba87b
+:4456eebbd1bc
 {-# OPTIONS --allow-unsolved-metas #-}
 module finiteSetUtil  where
 open import Data.Nat hiding ( _≟_ )
-open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ )
+open import Data.Fin renaming ( _<_ to _<<_ ; _>_ to _f>_ ; _≟_ to _f≟_ ) hiding (_≤_ ; pred )
-open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp )
+open import Data.Fin.Properties hiding ( <-trans ) renaming ( <-cmp to <-fcmp ) hiding (≤-refl ; ≤-trans )
 open import Data.Empty
 open import Relation.Nullary
 open import Relation.Binary.Definitions
 open import Relation.Binary.PropositionalEquality
 open import logic
 dl01 = subst (λ k →  fin-dup-in-list k (map (F←Q finq) qs) ≡ true )
 (sym (finiso← finq _)) ( FDup-in-list.is-dup dl )
 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
 inject-fin : {A B : Set}  (fa : FiniteSet A )
-→ (fi : InjectiveF B A)
+→ (gi : InjectiveF B A)
-→ (is-B : (a : A ) → Dec (Is B A (InjectiveF.f fi) a)  )
+→ (is-B : (a : A ) → Dec (Is B A (InjectiveF.f gi) a)  )
 → FiniteSet B
-inject-fin {A} {B} fa fi is-B = record {
+inject-fin {A} {B} fa gi is-B with finite fa | inspect finite fa
-finite = countB.cb (cb00 (finite fa) NP.≤-refl )
+inject-fin {A} {B} fa gi is-B | zero | record { eq = eq1 } = ?
-; Q←F = λ fb → countB.ib (cb00 (finite fa) NP.≤-refl ) (fin<n {_} {fb})
+inject-fin {A} {B} fa gi is-B | suc pfa | record { eq = eq1 } = record {
-; F←Q =  λ b → fromℕ< (cb<cb (fin<n {_} {F←Q fa (InjectiveF.f fi b)} ))
+finite = maxb
+; Q←F = λ fb → ntob (toℕ fb) fin<n
+; F←Q =  λ b → fromℕ< (bton<maxb b)
 ; finiso→ = ?
 ; finiso← = ?
 } where
-f = InjectiveF.f fi
+g = InjectiveF.f gi
-cb00 : (i : ℕ) → i ≤ finite fa → countB B
+pfa<fa : pfa < finite fa
-cb00 0 i<fa = record { cb = 0 ; ib = λ () ; ib-inject = λ () }
+pfa<fa = subst (λ k → pfa < k ) (sym eq1) a<sa
-cb00 (suc i) i<fa with is-B (Q←F fa (fromℕ< i<fa))
+h : ℕ → A
-... | yes y = record { cb = suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) ; ib = cb01 ; ib-inject = cb02 } where
+h i with <-cmp i (finite fa)
-pcb : countB B
+... | tri< a ¬b ¬c = Q←F fa (fromℕ< a )
-pcb = cb00 i (NP.≤-trans a≤sa i<fa)
+... | tri≈ ¬a b ¬c = Q←F fa (fromℕ< pfa<fa )
-cb01 :  {j : ℕ} → j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))) → B
+... | tri> ¬a ¬b c = Q←F fa (fromℕ< pfa<fa )
-cb01 {j} j<c with <-∨ j<c
+C = A
-... | case1 eq = Is.a y
+h⁻¹ : A → ℕ
-... | case2 lt = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) lt
+h⁻¹ a = toℕ (F←Q fa a)
-cb02 : {i1 : ℕ} {j : ℕ}
-(i<cb : i1 < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))))
+h-iso : (i : ℕ) → i < finite fa → h⁻¹ (h i) ≡ i
-(j<cb : j < suc (countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)))) →
+h-iso = ?
-cb01 i<cb ≡ cb01 j<cb → i1 ≡ j
-cb02 = ?
+count-B : ℕ → ℕ
-... | no n  = record { cb = countB.cb (cb00 i (NP.≤-trans a≤sa i<fa))       ; ib = cb01
+count-B zero with is-B (h zero)
-; ib-inject = countB.ib-inject (cb00 i (NP.≤-trans a≤sa i<fa))} where
+... | yes isb = 1
-cb01 :  {j : ℕ} → j < countB.cb (cb00 i (NP.≤-trans a≤sa i<fa)) → B
+... | no nisb = 0
-cb01 {j} j<c = countB.ib (cb00 i (NP.≤-trans a≤sa i<fa)) j<c
+count-B (suc n) with is-B (h (suc n))
+... | yes isb = suc (count-B n)
-cb<cb : {i : ℕ} → (i<fa : i ≤ finite fa) → countB.cb (cb00 _ i<fa) < countB.cb (cb00 _ NP.≤-refl)
+... | no nisb = count-B n
-cb<cb = ?
+maxb : ℕ
+maxb = count-B (finite fa)
+--
+-- countB record create ℕ → B and its injection
+--
+record CountB (n : ℕ) : Set where
+field
+b : B
+cb : ℕ
+b=cn : h cb ≡ g b
+cb=n : count-B cb ≡ suc n
+cb-inject : (cb1 : ℕ) → Is B C g (h cb1) → count-B cb ≡ count-B cb1 → cb ≡ cb1
+count-B-mono : {i j : ℕ} → i ≤ j → count-B i ≤ count-B j
+count-B-mono {i} {j} i≤j with ≤-∨ i≤j
+... | case1 refl = ≤-refl
+... | case2 i<j = lem00 _ _ i<j where
+lem00 : (i j : ℕ) → i < j → count-B i ≤ count-B j
+lem00 i (suc j) (s≤s i<j) = ≤-trans (count-B-mono i<j) (lem01 j) where
+lem01 : (j : ℕ) → count-B j ≤ count-B (suc j)
+lem01 zero with is-B (h (suc zero))
+... | yes isb = refl-≤s
+... | no nisb = ≤-refl
+lem01 (suc n) with is-B (h (suc (suc n)))
+... | yes isb = refl-≤s
+... | no nisb = ≤-refl
+lem01 : (n i : ℕ) → suc n ≤ count-B i → CountB n
+lem01 n i le = lem09 i (count-B i) le refl where
+-- injection of count-B
+---
+lem06 : (i j : ℕ ) → Is B C g (h i) → Is B C g (h j) → count-B i ≡ count-B j → i ≡ j
+lem06 i j bi bj eq = lem08  where
+lem20 : (i j : ℕ) → i < j →  Is B C g (h i) → Is B C g (h j) → count-B j ≡ count-B i → ⊥
+lem20 zero (suc j) i<j bi bj le with  is-B (h 0) | inspect count-B 0 | is-B (h (suc j)) | inspect count-B (suc j)
+... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
+... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
+... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = ⊥-elim ( nat-≤> lem25 a<sa) where
+lem22 : 1 ≡ count-B 0
+lem22 with is-B (h 0) | inspect count-B 0
+... | yes _ | record { eq = eq1 } = refl
+... | no nisa | _ = ⊥-elim ( nisa bi )
+lem24 : count-B j ≡ 0
+lem24 = cong pred le
+lem25 : 1 ≤ 0
+lem25 = begin
+1 ≡⟨ lem22 ⟩
+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 = ⊥-elim ( nat-≡< lem24 lem21 ) where
+--
+--                    i  <     suc i  ≤    j
+--    cb i <  suc (cb i) < cb (suc i) ≤ cb j
+--    suc (cb i) ≡ suc (cb j) → cb i ≡ cb j
+lem22 : suc (count-B i) ≡ count-B (suc i)
+lem22 with is-B (h (suc i)) | inspect count-B (suc i)
+... | yes _ | record { eq = eq1 } = refl
+... | no nisa | _ = ⊥-elim ( nisa bi )
+lem23 : suc (count-B j) ≡ count-B (suc j)
+lem23 with is-B (h (suc j)) | inspect count-B (suc j)
+... | yes _ | record { eq = eq1 } = refl
+... | no nisa | _ = ⊥-elim ( nisa bj )
+lem24 : count-B i ≡ count-B j
+lem24 with  is-B (h (suc i)) | inspect count-B (suc i) | is-B (h (suc j)) | inspect count-B (suc j)
+... | no nisc  | _ | _ | _ = ⊥-elim (nisc bi)
+... |  yes _ | _ | no nisc | _  = ⊥-elim (nisc bj)
+... | yes _ | record { eq = eq1 } | yes _ | record { eq = eq2 } = sym (cong pred le)
+lem21 : suc (count-B i) ≤ count-B j
+lem21 = begin
+suc (count-B i) ≡⟨ lem22 ⟩
+count-B (suc i) ≤⟨ count-B-mono i<j ⟩
+count-B j ∎ where
+open ≤-Reasoning
+lem08 : i ≡ j
+lem08 with <-cmp i j
+... | tri< a ¬b ¬c = ⊥-elim ( lem20 i j a bi bj (sym eq) )
+... | tri≈ ¬a b ¬c = b
+... | tri> ¬a ¬b c₁ = ⊥-elim ( lem20 j i c₁ bj bi eq )
+lem07 : (n i : ℕ) → count-B i ≡ suc n → CountB n
+lem07 n 0 eq with is-B (h 0) | inspect count-B 0
+... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
+; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+lem12 : (cb1 : ℕ) →  Is B C g (h cb1)  → 1 ≡ count-B cb1 → 0 ≡ cb1
+lem12 cb1 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans eq1 cbeq)
+... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< eq (s≤s z≤n ) )
+lem07 n (suc i) eq with is-B (h (suc i)) | inspect count-B (suc i)
+... | yes isb | record { eq = eq1 } = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans eq1 eq
+; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) eq1 cb1eq)   } where
+lem12 : (cb1 : ℕ) → Is B C g (h cb1) → suc (count-B i)  ≡ count-B cb1 → suc i ≡ cb1
+lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans eq1 cbeq)
+... | no nisb | record { eq = eq1 } = lem07 n i  eq
+-- starting from 0, if count B i ≡ suc n, this is it
+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 (h 0) | inspect count-B 0
+... | yes isb | record { eq = eq1 } = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) )
+... | no nisb | record { eq = eq1 } = ⊥-elim (nat-≡< (sym eq) (s≤s z≤n))
+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 is-B (h (suc i)) | inspect count-B (suc i)
+... | yes isb | record { eq = eq1 } = lem09 i j lt (cong pred eq)
+... | no nisb | record { eq = eq1 } = lem09 i (suc j) (≤-trans lt a≤sa) eq
+bton : B → ℕ
+bton b = pred (count-B (h⁻¹ (g b)))
+lem22 : {n : ℕ } →  n < maxb → suc n ≤ count-B n
+lem22 {n} n<mb = ?
+lem23 : (b : B) →  0 < count-B (h⁻¹ (g b))
+lem23 = ?
+bton<maxb : (b : B) →  bton b < maxb
+bton<maxb b = begin
+suc (bton b) ≡⟨ sucprd (lem23 b)  ⟩
+count-B (h⁻¹ (g b)) ≤⟨ count-B-mono {h⁻¹ (g b)} {finite fa} (<to≤ fin<n) ⟩
+count-B (finite fa) ≡⟨ refl ⟩
+maxb ∎ where
+open ≤-Reasoning
+ntob : (n : ℕ) → n < maxb  → B
+ntob n n<mb = CountB.b (lem01 n n (lem22 n<mb))
+biso : (n : ℕ) → (n<mb : n < maxb) → bton (ntob n n<mb ) ≡ n
+biso n n<mb = begin
+bton (ntob n n<mb ) ≡⟨ refl ⟩
+pred (count-B (h⁻¹ (g (CountB.b CB)))) ≡⟨ sym ( cong (λ k → pred (count-B (h⁻¹ k))) ( CountB.b=cn CB)) ⟩
+pred (count-B (h⁻¹ (h (CountB.cb CB)))) ≡⟨ cong (λ k → pred (count-B k)) (h-iso _ cb<fa) ⟩
+pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩
+pred (suc n) ≡⟨ refl ⟩
+n ∎ where
+open ≡-Reasoning
+CB  : CountB n
+CB  = lem01 n n (lem22 n<mb)
+cb<fa : CountB.cb CB < finite fa
+cb<fa = ?
+--
+-- uniqueness of ntob is proved by injection
+--
+biso1 : (b : B) → ntob (bton b) (bton<maxb b) ≡ b
+biso1 b = ?

Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/finiteSetUtil.agda @ 346:4456eebbd1bc