Mercurial > hg > Members > kono > Proof > automaton
changeset 403:c298981108c1
fix for std-lib 2.0
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 11:32:01 +0900 |
| parents | 093e386c10a2 |
| children | dfaf230f7b9a |
| files | automaton-in-agda/automaton-in-agda.agda-lib automaton-in-agda/src/automaton.agda automaton-in-agda/src/bijection.agda automaton-in-agda/src/derive.agda automaton-in-agda/src/fin.agda automaton-in-agda/src/finiteSet.agda automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/logic.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/non-regular.agda automaton-in-agda/src/pumping.agda automaton-in-agda/src/regular-star.agda |
| diffstat | 12 files changed, 313 insertions(+), 305 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton-in-agda/automaton-in-agda.agda-lib Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/automaton-in-agda.agda-lib Sun Sep 24 11:32:01 2023 +0900 @@ -1,6 +1,8 @@ -- File generated by Agda-Pkg name: automaton-in-agda -depend: standard-library +depend: standard-library-2.0 include: src +flags: + --warning=noUnsupportedIndexedMatch -- End
--- a/automaton-in-agda/src/automaton.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/automaton.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --cubical-compatible --safe #-} module automaton where open import Data.Nat
--- a/automaton-in-agda/src/bijection.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/bijection.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module bijection where @@ -217,8 +217,8 @@ -- nn zero = record { j = 0 ; k = 0 ; k1 = refl ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } - nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) - ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 + nn (suc i) with NN.k (nn i) in eq + ... | zero = record { k = suc (sum ) ; j = 0 ; k1 = nn02 ; nn-unique = nn04 } where --- --- increment the stage @@ -262,7 +262,7 @@ i ∎ where open ≡-Reasoning nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ nn06 = NN.nn-unique (nn i) - ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where + ... | suc k = record { k = k ; j = suc (NN.j (nn i)) ; k1 = nn11 ; nn-unique = nn13 } where --- --- increment in a stage --- @@ -438,8 +438,8 @@ lb zero = record { nlist = [] ; isBin = refl ; isUnique = lb05 } where lb05 : (x : List Bool) → lton x ≡ zero → [] ≡ x lb05 x eq = lb=b [] x (sym eq) - lb (suc n) with LB.nlist (lb n) | inspect LB.nlist (lb n) - ... | [] | record { eq = eq } = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where + lb (suc n) with LB.nlist (lb n) in eq + ... | [] = record { nlist = false ∷ [] ; isUnique = lb06 ; isBin = lb10 } where open ≡-Reasoning lb10 : lton1 (false ∷ []) ∸ 1 ≡ suc n lb10 = begin @@ -450,7 +450,7 @@ suc n ∎ lb06 : (x : List Bool) → pred (lton1 x ) ≡ suc n → false ∷ [] ≡ x lb06 x eq1 = lb=b (false ∷ []) x (trans lb10 (sym eq1)) -- lton (false ∷ []) ≡ lton x - ... | false ∷ t | record { eq = eq } = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where + ... | false ∷ t = record { nlist = true ∷ t ; isBin = lb01 ; isUnique = lb09 } where lb01 : lton (true ∷ t) ≡ suc n lb01 = begin lton (true ∷ t) ≡⟨ refl ⟩ @@ -461,7 +461,7 @@ suc n ∎ where open ≡-Reasoning lb09 : (x : List Bool) → lton1 x ∸ 1 ≡ suc n → true ∷ t ≡ x lb09 x eq1 = lb=b (true ∷ t) x (trans lb01 (sym eq1) ) -- lton (true ∷ t) ≡ lton x - ... | true ∷ t | record { eq = eq } = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where + ... | true ∷ t = record { nlist = lb+1 (true ∷ t) ; isBin = lb02 (true ∷ t) lb03 ; isUnique = lb07 } where lb03 : lton (true ∷ t) ≡ n lb03 = begin lton (true ∷ t) ≡⟨ cong (λ k → lton k ) (sym eq ) ⟩ @@ -757,14 +757,14 @@ lem06 : (i j : ℕ ) → Is B C g (fun← cn i) → Is B C g (fun← cn 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 (fun← cn i) → Is B C g (fun← cn j) → count-B j ≡ count-B i → ⊥ - lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) | inspect count-B 0 | is-B (fun← cn (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 + lem20 zero (suc j) i<j bi bj le with is-B (fun← cn 0) in eq1 | is-B (fun← cn (suc j)) in eq2 + ... | no nisc | _ = ⊥-elim (nisc bi) + ... | yes _ | no nisc = ⊥-elim (nisc bj) + ... | yes _ | yes _ = ⊥-elim ( nat-≤> lem25 a<sa) where lem22 : 1 ≡ count-B 0 - lem22 with is-B (fun← cn 0) | inspect count-B 0 - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem22 with is-B (fun← cn 0) in eq1 + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa bi ) lem24 : count-B j ≡ 0 lem24 = cong pred le lem25 : 1 ≤ 0 @@ -780,18 +780,18 @@ -- 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 (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa bi ) + lem22 with is-B (fun← cn (suc i)) in eq1 + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa bi ) lem23 : suc (count-B j) ≡ count-B (suc j) - lem23 with is-B (fun← cn (suc j)) | inspect count-B (suc j) - ... | yes _ | record { eq = eq1 } = refl - ... | no nisa | _ = ⊥-elim ( nisa bj ) + lem23 with is-B (fun← cn (suc j)) in eq1 + ... | yes _ = refl + ... | no nisa = ⊥-elim ( nisa bj ) lem24 : count-B i ≡ count-B j - lem24 with is-B (fun← cn (suc i)) | inspect count-B (suc i) | is-B (fun← cn (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) + lem24 with is-B (fun← cn (suc i)) in eq1 | is-B (fun← cn (suc j)) in eq2 + ... | no nisc | _ = ⊥-elim (nisc bi) + ... | yes _ | no nisc = ⊥-elim (nisc bj) + ... | yes _ | yes _ = sym (cong pred le) lem21 : suc (count-B i) ≤ count-B j lem21 = begin suc (count-B i) ≡⟨ lem22 ⟩ @@ -805,32 +805,44 @@ ... | 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 (fun← cn 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 + lem07 n 0 eq with is-B (fun← cn 0) + ... | yes isb = lem13 where + cb1 = count-B 0 + lem14 : count-B 0 ≡ 1 + lem14 with is-B (fun← cn 0) + ... | yes _ = refl + ... | no ne = ⊥-elim (ne isb) lem12 : (cb1 : ℕ) → Is B C g (fun← cn 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 (fun← cn (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 iscb1 cbeq = lem06 0 cb1 isb iscb1 (trans lem14 cbeq) + lem13 : CountB n + lem13 = record { b = Is.a isb ; cb = 0 ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } + ... | no nisb = ⊥-elim ( nat-≡< eq (s≤s z≤n ) ) + lem07 n (suc i) eq with is-B (fun← cn (suc i)) + ... | yes isb = record { b = Is.a isb ; cb = suc i ; b=cn = sym (Is.fa=c isb) ; cb=n = trans lem14 eq + ; cb-inject = λ cb1 iscb1 cb1eq → lem12 cb1 iscb1 (subst (λ k → k ≡ count-B cb1) lem14 cb1eq) } where + cbs = count-B (suc i) + lem14 : count-B (suc i) ≡ suc (count-B i) + lem14 with is-B (fun← cn (suc i)) + ... | yes _ = refl + ... | no ne = ⊥-elim (ne isb) lem12 : (cb1 : ℕ) → Is B C g (fun← cn 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 + lem12 cb1 iscb1 cbeq = lem06 (suc i) cb1 isb iscb1 (trans lem14 cbeq) + ... | no nisb = 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 (fun← cn 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)) + ... | case2 (s≤s lt) with is-B (fun← cn 0) in eq1 + ... | yes isb = ⊥-elim ( nat-≤> (≤-trans (s≤s lt) (refl-≤≡ eq) ) (s≤s (s≤s z≤n)) ) + ... | no nisb = ⊥-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 (fun← cn (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 + ... | case2 (s≤s lt) with is-B (fun← cn (suc i)) in eq1 + ... | yes isb = lem09 i j lt (cong pred eq) + ... | no nisb = lem09 i (suc j) (≤-trans lt a≤sa) eq bton : B → ℕ bton b = pred (count-B (fun→ cn (g b))) @@ -853,18 +865,18 @@ -- uniqueness of ntob is proved by injection -- biso1 : (b : B) → ntob (bton b) ≡ b - biso1 b with count-B (fun→ cn (g b)) | inspect count-B (fun→ cn (g b)) - ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where + biso1 b with count-B (fun→ cn (g b)) in eq1 + ... | zero = ⊥-elim ( nat-≡< (sym lem20) (lem21 _ refl) ) where lem20 : count-B (fun→ cn (InjectiveF.f gi b)) ≡ zero lem20 = eq1 lem21 : (i : ℕ) → i ≡ fun→ cn (InjectiveF.f gi b) → 0 < count-B i - lem21 0 eq with is-B (fun← cn 0) | inspect count-B 0 - ... | yes isb | record { eq = eq1 } = ≤-refl - ... | no nisb | record{ eq = eq1 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) - lem21 (suc i) eq with is-B (fun← cn (suc i)) | inspect count-B (suc i) - ... | yes isb | record{ eq = eq2 } = s≤s z≤n - ... | no nisb | record{ eq = eq2 } = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) - ... | suc n | record { eq = eq1 } = begin + lem21 0 eq with is-B (fun← cn 0) in eq1 + ... | yes isb = ≤-refl + ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) + lem21 (suc i) eq with is-B (fun← cn (suc i)) in eq2 + ... | yes isb = s≤s z≤n + ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = trans (sym (fiso← cn _)) (cong (fun← cn) (sym eq)) } ) + ... | suc n = begin CountB.b CB ≡⟨ InjectiveF.inject gi (bi-inject→ cn (begin fun→ cn (g (CountB.b CB)) ≡⟨ cong (fun→ cn) (sym (CountB.b=cn CB)) ⟩ fun→ cn (fun← cn (CountB.cb CB)) ≡⟨ fiso→ cn _ ⟩ @@ -991,27 +1003,27 @@ -- LMℕ A Ln = Countable-Bernstein (List A) (List (Maybe A)) (List A ∧ List Bool) Ln (LM1 A Ln) fi gi dec0 dec1 where -- someday ... -LBBℕ : Bijection (List (List Bool)) ℕ -LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ)) - ? ? ? ? where - - atob : List (List Bool) → List Bool ∧ List Bool - atob [] = ⟪ [] , [] ⟫ - atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫ - atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫ - - btoa : List Bool ∧ List Bool → List (List Bool) - btoa ⟪ [] , _ ⟫ = [] - btoa ⟪ _ ∷ _ , [] ⟫ = [] - btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ - btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫ - ... | [] = ( h ∷ [] ) ∷ [] - ... | x ∷ y = (h ∷ x ) ∷ y - -Lℕ=ℕ : Bijection (List ℕ) ℕ -Lℕ=ℕ = record { - fun→ = λ x → ? - ; fun← = λ n → ? - ; fiso→ = ? - ; fiso← = ? - } +-- LBBℕ : Bijection (List (List Bool)) ℕ +-- LBBℕ = Countable-Bernstein (List Bool ∧ List Bool) (List (List Bool)) (List Bool ∧ List Bool ) (LM1 Bool (bi-sym _ _ LBℕ)) (LM1 Bool (bi-sym _ _ LBℕ)) +-- ? ? ? ? where +-- +-- atob : List (List Bool) → List Bool ∧ List Bool +-- atob [] = ⟪ [] , [] ⟫ +-- atob ( [] ∷ t ) = ⟪ false ∷ proj1 ( atob t ) , false ∷ proj2 ( atob t ) ⟫ +-- atob ( (h ∷ t1) ∷ t ) = ⟪ h ∷ proj1 ( atob t ) , true ∷ proj2 ( atob t ) ⟫ +-- +-- btoa : List Bool ∧ List Bool → List (List Bool) +-- btoa ⟪ [] , _ ⟫ = [] +-- btoa ⟪ _ ∷ _ , [] ⟫ = [] +-- btoa ⟪ _ ∷ t0 , false ∷ t1 ⟫ = [] ∷ btoa ⟪ t0 , t1 ⟫ +-- btoa ⟪ h ∷ t0 , true ∷ t1 ⟫ with btoa ⟪ t0 , t1 ⟫ +-- ... | [] = ( h ∷ [] ) ∷ [] +-- ... | x ∷ y = (h ∷ x ) ∷ y +-- +-- Lℕ=ℕ : Bijection (List ℕ) ℕ +-- Lℕ=ℕ = record { +-- fun→ = λ x → ? +-- ; fun← = λ n → ? +-- ; fiso→ = ? +-- ; fiso← = ? +-- }
--- a/automaton-in-agda/src/derive.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/derive.agda Sun Sep 24 11:32:01 2023 +0900 @@ -238,6 +238,9 @@ fb00 record { s = s ; is-sub = (sub* is-sub) } = {!!} fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt } +d-ISB : (r : Regex Σ) → ISB r → (s : Σ) → ISB r → Bool +d-ISB r x s y = ? + toSB : (r : Regex Σ) → ISB r → Bool toSB r record { s = s ; is-sub = is-sub } with rg-eq? r s ... | yes _ = true @@ -274,24 +277,8 @@ sbderive : (r : Regex Σ) → (ISB r → Bool) → Σ → ISB r → Bool sbderive ε f s record { s = .ε ; is-sub = sε } = false sbderive φ f s record { s = t ; is-sub = sφ } = false -sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } with f record { s = t ; is-sub = sub* is-sub } -... | false = true -... | true with derivative r s -... | ε = true -... | φ = false -... | t₁ * = false -... | t₁ & t₂ = false -... | t₁ || t₂ = false -... | < x > = false -sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } with f record { s = (x & (r *)) ; is-sub = sub*& x r x₁ is-sub } -... | false = true -... | true with derivative r s -... | ε = false -... | φ = false -... | t₁ * = true -... | t₁ & t₂ = true -... | t₁ || t₂ = true -... | < s > = true +sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } = ? +sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } = ? sbderive (r & r₁) f s record { s = t ; is-sub = sub&1 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&1 r r₁ t is-sub } ... | false = true ... | true = false
--- a/automaton-in-agda/src/fin.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/fin.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,9 +1,9 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module fin where open import Data.Fin hiding (_<_ ; _≤_ ; _>_ ; _+_ ) -open import Data.Fin.Properties as DFP hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp ) +open import Data.Fin.Properties hiding (≤-trans ; <-trans ; ≤-refl ) renaming ( <-cmp to <-fcmp ) open import Data.Nat open import Data.Nat.Properties open import logic @@ -23,7 +23,7 @@ pred<n : {n : ℕ} {f : Fin (suc n)} → n > 0 → Data.Nat.pred (toℕ f) < n pred<n {suc n} {zero} (s≤s z≤n) = s≤s z≤n -pred<n {suc n} {suc f} (s≤s z≤n) = fin<n f +pred<n {suc n} {suc f} (s≤s z≤n) = fin<n _ fin<asa : {n : ℕ} → toℕ (fromℕ< {n} a<sa) ≡ n fin<asa = toℕ-fromℕ< nat.a<sa @@ -33,17 +33,20 @@ toℕ→from {0} {zero} refl = refl toℕ→from {suc n} {suc x} eq = cong (λ k → suc k ) ( toℕ→from {n} {x} (cong (λ k → Data.Nat.pred k ) eq )) -0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa -0≤fmax = subst (λ k → 0 ≤ k ) (sym (toℕ-fromℕ< a<sa)) z≤n +-- 0≤fmax : {n : ℕ } → (# 0) Data.Fin.≤ fromℕ< {n} a<sa +-- 0≤fmax {n} = ? -0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa -0<fmax = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< a<sa)) (s≤s z≤n) +-- 0<fmax : {n : ℕ } → (# 0) Data.Fin.< fromℕ< {suc n} a<sa +-- 0<fmax {n} = subst (λ k → 0 < k ) (sym (toℕ-fromℕ< {suc n} {suc (suc n)} a<sa)) (s≤s z≤n) -- toℕ-injective i=j : {n : ℕ} (i j : Fin n) → toℕ i ≡ toℕ j → i ≡ j i=j {suc n} zero zero refl = refl i=j {suc n} (suc i) (suc j) eq = cong ( λ k → suc k ) ( i=j i j (cong ( λ k → Data.Nat.pred k ) eq) ) +fin1≡0 : (f : Fin 1) → # 0 ≡ f +fin1≡0 zero = refl + -- raise 1 fin+1 : { n : ℕ } → Fin n → Fin (suc n) fin+1 zero = zero @@ -51,9 +54,6 @@ open import Data.Nat.Properties as NatP hiding ( _≟_ ) -fin1≡0 : (f : Fin 1) → # 0 ≡ f -fin1≡0 zero = refl - fin+1≤ : { i n : ℕ } → (a : i < n) → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa) fin+1≤ {0} {suc i} (s≤s z≤n) = refl fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) ) @@ -90,32 +90,39 @@ lemma12 {zero} {suc m} (s≤s z≤n) zero refl = refl lemma12 {suc n} {suc m} (s≤s n<m) (suc f) refl = cong suc ( lemma12 {n} {m} n<m f refl ) -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- this requires K +-- +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- <-irrelevant -<-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n -<-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl -<-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl ) +-- <-nat=irr : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n +-- <-nat=irr {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl +-- <-nat=irr {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( <-nat=irr {i} {i} {n} refl ) + +-- lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n +-- lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl +-- lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl ) -lemma8 : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n -lemma8 {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl -lemma8 {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8 {i} {i} {n} refl ) +lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n +lemma10 {.(suc _)} {zero} {zero} refl {s≤s z≤n} {s≤s z≤n} = refl +lemma10 {suc n} {suc i} {suc i} refl {s≤s i<n} {s≤s j<n} = cong suc (lemma10 {n} {i} {i} refl {i<n} {j<n}) --- fromℕ<-irrelevant -lemma10 : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n -lemma10 {n} refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8 refl )) +fpred-comm : {n : ℕ } → (x : Fin n) → toℕ (Data.Fin.pred x) ≡ toℕ x ∸ 1 +fpred-comm {suc n} zero = refl +fpred-comm {suc n} (suc x) = begin + toℕ (Data.Fin.pred (suc x)) ≡⟨ sym ( toℕ-fromℕ< _ ) ⟩ + toℕ (fromℕ< (fin<n _) ) ≡⟨ cong toℕ (lemma10 (toℕ-inject₁ _ ) ) ⟩ + toℕ (fromℕ< (<-trans (fin<n _) a<sa) ) ≡⟨ toℕ-fromℕ< _ ⟩ + toℕ (suc x) ∸ 1 ∎ where open ≡-Reasoning -lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c -lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) +-- lemma31 : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NatP.<-trans a<b b<c ≡ a<c +-- lemma31 {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8 refl) -- toℕ-fromℕ< lemma11 : {n m : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡ toℕ x lemma11 {n} {m} {x} n<m = begin - toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) - ≡⟨ toℕ-fromℕ< _ ⟩ - toℕ x - ∎ where - open ≡-Reasoning + toℕ (fromℕ< (NatP.<-trans (toℕ<n x) n<m)) ≡⟨ toℕ-fromℕ< _ ⟩ + toℕ x ∎ where open ≡-Reasoning x<y→fin-1 : {n : ℕ } → { x y : Fin (suc n)} → toℕ x < toℕ y → Fin n x<y→fin-1 {n} {x} {y} lt = fromℕ< (≤-trans lt (fin≤n _ )) @@ -140,12 +147,21 @@ -- find duplicate element in a List (Fin n) -- -- if the length is longer than n, we can find duplicate element as FDup-in-list +-- +-- How about do it in ℕ ? -list2func : (n : ℕ) → (x : List (Fin n)) → n < length x → Fin (length x) → Fin n -list2func n x n<l y = lf00 (toℕ y) x (fin<n y) where - lf00 : (i : ℕ) → (x : List (Fin n)) → i < length x → Fin n - lf00 zero (x ∷ t) lt = x - lf00 (suc i) (x ∷ t) (s≤s lt) = lf00 i t lt +-- fin-count : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → ℕ +-- fin-count q p[ = 0 +-- fin-count q (q0 ∷ qs ) with <-fcmp q q0 +-- ... | tri-e = suc (fin-count q qs) +-- ... | false = fin-count q qs + +-- fin-not-dup-in-list : { n : ℕ} (qs : List (Fin n) ) → Set +-- fin-not-dup-in-list {n} qs = (q : Fin n) → fin-count q ≤ 1 + +-- this is far easier +-- fin-not-dup-in-list→len<n : { n : ℕ} (qs : List (Fin n) ) → ( (q : Fin n) → fin-not-dup-in-list qs q) → length qs ≤ n +-- fin-not-dup-in-list→len<n = ? fin-phase2 : { n : ℕ } (q : Fin n) (qs : List (Fin n) ) → Bool -- find the dup fin-phase2 q [] = false @@ -175,6 +191,11 @@ ... | tri≈ ¬a b ¬c = list-less ls ... | tri> ¬a ¬b c = x<y→fin-1 c ∷ list-less ls +fin010 : {n m : ℕ } {x : Fin n} (c : suc (toℕ x) ≤ toℕ (fromℕ< {m} a<sa) ) → toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡ toℕ x +fin010 {_} {_} {x} c = begin + toℕ (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) ≡⟨ toℕ-fromℕ< _ ⟩ + toℕ x ∎ where open ≡-Reasoning + --- --- if List (Fin n) is longer than n, there is at most one duplication --- @@ -233,7 +254,7 @@ ... | tri< a ¬b ¬c₁ = f1-phase1 qs p (case2 q1) ... | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (fdup-10 b b₁) where fdup-10 : fromℕ< a<sa ≡ x → fin+1 i ≡ x → ⊥ - fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _)) + fdup-10 eq eq1 = nat-≡< (cong toℕ (trans eq1 (sym eq))) (subst₂ (λ j k → j < k ) (sym fin+1-toℕ) (sym fin<asa) (fin<n _) ) ... | tri> ¬a₁ ¬b c = f1-phase1 qs p (case2 q1) f1-phase1 (x ∷ qs) p (case1 q1) | tri> ¬a ¬b c with <-fcmp i (fromℕ< (≤-trans c (fin≤n (fromℕ< a<sa)))) | <-fcmp (fin+1 i) x ... | tri< a ¬b₁ ¬c | tri< a₁ ¬b₂ ¬c₁ = f1-phase1 qs p (case1 q1) @@ -259,9 +280,9 @@ ... | tri> ¬a₁ ¬b₁ c₁ | tri≈ ¬a₂ b ¬c = ⊥-elim ( ¬c (subst₂ (λ j k → j > k) (sym fin+1-toℕ) (toℕ-fromℕ< _) c₁ )) ... | tri> ¬a₁ ¬b₁ c₁ | tri> ¬a₂ ¬b₂ c₂ = f1-phase1 qs p (case2 q1) fdup-phase0 : FDup-in-list (suc n) qs - fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs | inspect (fin-dup-in-list (fromℕ< a<sa)) qs - ... | true | record { eq = eq } = record { dup = fromℕ< a<sa ; is-dup = eq } - ... | false | record { eq = ne } = fdup+1 qs (FDup-in-list.dup fdup) ne (FDup-in-list.is-dup fdup) where + fdup-phase0 with fin-dup-in-list (fromℕ< a<sa) qs in eq + ... | true = record { dup = fromℕ< a<sa ; is-dup = eq } + ... | false = fdup+1 qs (FDup-in-list.dup fdup) eq (FDup-in-list.is-dup fdup) where -- if no dup in the max element, the list without the element is only one length shorter fless : (qs : List (Fin (suc n))) → length qs > suc n → fin-dup-in-list (fromℕ< a<sa) qs ≡ false → n < length (list-less qs) fless qs lt p = fl-phase1 n qs lt p where @@ -283,6 +304,6 @@ ... | tri> ¬a ¬b c = s≤s ( fl-phase1 n1 qs lt p ) -- if the list without the max element is only one length shorter, we can recurse fdup : FDup-in-list n (list-less qs) - fdup = fin-dup-in-list>n (list-less qs) (fless qs lt ne) + fdup = fin-dup-in-list>n (list-less qs) (fless qs lt eq) --
--- a/automaton-in-agda/src/finiteSet.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/finiteSet.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module finiteSet where open import Data.Nat hiding ( _≟_ ) @@ -12,7 +12,7 @@ open import nat open import Data.Nat.Properties hiding ( _≟_ ) -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) record FiniteSet ( Q : Set ) : Set where field
--- a/automaton-in-agda/src/finiteSetUtil.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/finiteSetUtil.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,4 +1,4 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} module finiteSetUtil where @@ -14,7 +14,6 @@ open import finiteSet open import fin open import Data.Nat.Properties as NP hiding ( _≟_ ) -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) record Found ( Q : Set ) (p : Q → Bool ) : Set where field @@ -25,13 +24,12 @@ open import Axiom.Extensionality.Propositional open import Level hiding (suc ; zero) -postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n -- (Level.suc n) module _ {Q : Set } (F : FiniteSet Q) where open FiniteSet F equal?-refl : { x : Q } → equal? x x ≡ true equal?-refl {x} with F←Q x ≟ F←Q x - ... | yes refl = refl + ... | yes eq = refl ... | no ne = ⊥-elim (ne refl) equal→refl : { x y : Q } → equal? x y ≡ true → x ≡ y equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1 @@ -89,9 +87,9 @@ found← : { p : Q → Bool } → exists p ≡ true → Found Q p found← {p} exst = found2 finite NP.≤-refl (first-end p ) where found2 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → End m p → Found Q p - found2 0 m<n end = ⊥-elim ( ¬-bool (not-found (λ q → end (F←Q q) z≤n ) ) (subst (λ k → exists k ≡ true) (sym lemma) exst ) ) where - lemma : (λ z → p (Q←F (F←Q z))) ≡ p - lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl ) + found2 0 m<n end = ⊥-elim ( ¬-bool f01 exst ) where + f01 : exists p ≡ false + f01 = not-found (λ q → subst ( λ k → p k ≡ false ) (finiso→ _) (end (F←Q q) z≤n )) found2 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true found2 (suc m) m<n end | yes eq = record { found-q = Q←F (fromℕ< m<n) ; found-p = eq } found2 (suc m) m<n end | no np = @@ -289,7 +287,7 @@ open ≡-Reasoning open Data.Product -cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → cast eq ( cast (sym eq ) f) ≡ f +cast-iso : {n m : ℕ } → (eq : n ≡ m ) → (f : Fin m ) → Data.Fin.cast eq ( Data.Fin.cast (sym eq ) f) ≡ f cast-iso refl zero = refl cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) @@ -338,8 +336,6 @@ ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q open import Level renaming ( suc to Suc ; zero to Zero) -open import Axiom.Extensionality.Propositional --- postulate f-extensionality : { n : Level} → Axiom.Extensionality.Propositional.Extensionality n n F2L-iso : { Q : Set } → (fin : FiniteSet Q ) → (x : Vec Bool (FiniteSet.finite fin) ) → F2L fin a<sa (λ q _ → List2Func fin a<sa x q ) ≡ x F2L-iso {Q} fin x = f2l m a<sa x where @@ -363,9 +359,7 @@ lemma3f : F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) ≡ t lemma3f = begin F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (s≤s n<m) (h ∷ t) q ) - ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ( λ q q<n → k q q<n )) - (f-extensionality ( λ q → - (f-extensionality ( λ q<n → lemma4 q q<n )))) ⟩ + ≡⟨ cong (λ k → F2L fin (NP.<-trans n<m a<sa) ?) ? ⟩ F2L fin (NP.<-trans n<m a<sa) (λ q q<n → List2Func fin (NP.<-trans n<m a<sa) t q ) ≡⟨ f2l n (NP.<-trans n<m a<sa ) t ⟩ t @@ -410,9 +404,9 @@ fun← iso x = F2L fin a<sa ( λ q _ → x q ) fun→ iso x = List2Func fin a<sa x fiso← iso x = F2L-iso fin x - fiso→ iso x = lemma where - lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → x q)) ≡ x - lemma = f-extensionality ( λ q → L2F-iso fin x q ) + fiso→ iso f = lemma where + lemma : List2Func fin a<sa (F2L fin a<sa (λ q _ → f q)) ≡ f + lemma = ? Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) @@ -427,21 +421,10 @@ get-< : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa }→ (f : fin-less fa n<m ) → toℕ (FiniteSet.F←Q fa (get-elm f )) < n get-< (elm1 _ b ) = b -fin-less-cong : { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) - → (x y : fin-less fa n<m ) → get-elm {n} {A} {fa} x ≡ get-elm {n} {A} {fa} y → get-< x ≅ get-< y → x ≡ y -fin-less-cong fa n<m (elm1 elm x) (elm1 elm x) refl HE.refl = refl - fin-< : {A : Set} → { n : ℕ } → (fa : FiniteSet A ) → (n<m : n < FiniteSet.finite fa ) → FiniteSet (fin-less fa n<m ) fin-< {A} {n} fa n<m = iso-fin (Fin2Finite n) iso where m = FiniteSet.finite fa iso : Bijection (Fin n) (fin-less fa n<m ) - lemma8f : {i j n : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → i<n ≅ j<n - lemma8f {zero} {zero} {suc n} refl {s≤s z≤n} {s≤s z≤n} = HE.refl - lemma8f {suc i} {suc i} {suc n} refl {s≤s i<n} {s≤s j<n} = HE.cong (λ k → s≤s k ) ( lemma8f {i} {i} refl ) - lemma10f : {n i j : ℕ } → ( i ≡ j ) → {i<n : i < n } → {j<n : j < n } → fromℕ< i<n ≡ fromℕ< j<n - lemma10f refl = HE.≅-to-≡ (HE.cong (λ k → fromℕ< k ) (lemma8f refl )) - lemma3f : {a b c : ℕ } → { a<b : a < b } { b<c : b < c } { a<c : a < c } → NP.<-trans a<b b<c ≡ a<c - lemma3f {a} {b} {c} {a<b} {b<c} {a<c} = HE.≅-to-≡ (lemma8f refl) lemma11f : {n : ℕ } {x : Fin n } → (n<m : n < m ) → toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) ≡ toℕ x lemma11f {n} {x} n<m = begin toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) @@ -475,7 +458,7 @@ open ≡-Reasoning lemma6 : toℕ (fromℕ< (NP.<-trans (toℕ<n x) n<m)) < n lemma6 = subst ( λ k → k < n ) (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x ) - fiso→ iso (elm1 elm x) = fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where + fiso→ iso (elm1 elm x) = ? where -- fin-less-cong fa n<m _ _ lemma (lemma8 (cong (λ k → toℕ (FiniteSet.F←Q fa k) ) lemma ) ) where lemma13 : toℕ (fromℕ< x) ≡ toℕ (FiniteSet.F←Q fa elm) lemma13 = begin toℕ (fromℕ< x) @@ -489,7 +472,7 @@ FiniteSet.Q←F fa (fromℕ< ( NP.<-trans (toℕ<n ( fromℕ< x ) ) n<m)) ≡⟨ cong (λ k → FiniteSet.Q←F fa k) (lemma10 lemma13 ) ⟩ FiniteSet.Q←F fa (fromℕ< ( NP.<-trans x n<m)) - ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) (HE.≅-to-≡ (lemma8 refl)) ⟩ + ≡⟨ cong (λ k → FiniteSet.Q←F fa (fromℕ< k )) ? ⟩ FiniteSet.Q←F fa (fromℕ< ( toℕ<n (FiniteSet.F←Q fa elm))) ≡⟨ cong (λ k → FiniteSet.Q←F fa k ) ( fromℕ<-toℕ _ _ ) ⟩ FiniteSet.Q←F fa (FiniteSet.F←Q fa elm ) @@ -545,22 +528,22 @@ dup-in-list+fin {Q} finq q qs p = i-phase1 qs p where i-phase2 : (qs : List Q) → fin-phase2 (F←Q finq q) (map (F←Q finq) qs) ≡ true → phase2 finq q qs ≡ true - i-phase2 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) - ... | true | _ | t = refl - ... | false | _ | tri< a ¬b ¬c = i-phase2 qs p - ... | false | record { eq = eq } | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq + i-phase2 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x) + ... | true | t = refl + ... | false | tri< a ¬b ¬c = i-phase2 qs p + ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) - ... | false | _ | tri> ¬a ¬b c = i-phase2 qs p + ... | false | tri> ¬a ¬b c = i-phase2 qs p i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true → phase1 finq q qs ≡ true - i-phase1 (x ∷ qs) p with equal? finq q x | inspect (equal? finq q ) x | <-fcmp (F←Q finq q) (F←Q finq x) - ... | true | record { eq = eq } | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) - ... | true | _ | tri≈ ¬a b ¬c = i-phase2 qs p - ... | true | record { eq = eq} | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) - ... | false | _ | tri< a ¬b ¬c = i-phase1 qs p - ... | false | record {eq = eq} | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq + i-phase1 (x ∷ qs) p with equal? finq q x in eq | <-fcmp (F←Q finq q) (F←Q finq x) + ... | true | tri< a ¬b ¬c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) ( equal→refl finq eq )) a ) + ... | true | tri≈ ¬a b ¬c = i-phase2 qs p + ... | true | tri> ¬a ¬b c = ⊥-elim ( nat-≡< (cong (λ x → toℕ (F←Q finq x)) (sym ( equal→refl finq eq ))) c ) + ... | false | tri< a ¬b ¬c = i-phase1 qs p + ... | false | tri≈ ¬a b ¬c = ⊥-elim (¬-bool eq (subst₂ (λ j k → equal? finq j k ≡ true) (finiso→ finq q) (subst (λ k → Q←F finq k ≡ x) (sym b) (finiso→ finq x)) ( equal?-refl finq ))) - ... | false | _ | tri> ¬a ¬b c = i-phase1 qs p + ... | false | tri> ¬a ¬b c = i-phase1 qs p record Dup-in-list {Q : Set } (finq : FiniteSet Q) (qs : List Q) : Set where field @@ -587,8 +570,8 @@ → (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 with finite fa | inspect finite fa -... | zero | record { eq = eq1 } = record { +inject-fin {A} {B} fa fi is-B with finite fa in eq1 +... | zero = record { finite = 0 ; Q←F = λ () ; F←Q = λ b → ⊥-elim ( lem00 b) @@ -598,7 +581,7 @@ lem00 : ( b : B) → ⊥ lem00 b with subst (λ k → Fin k ) eq1 (F←Q fa (InjectiveF.f fi b)) ... | () -... | suc pfa | record { eq = eq1 } = record { +... | suc pfa = record { finite = maxb ; Q←F = λ fb → CountB.b (cb00 _ (fin<n {_} fb)) ; F←Q = λ b → fromℕ< (cb<mb b) @@ -643,28 +626,32 @@ lem01 zero with <-cmp (finite fa) 1 lem01 zero | tri< a ¬b ¬c = ≤-refl lem01 zero | tri≈ ¬a b ¬c = ≤-refl - lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) | inspect count-B 0 - ... | yes isb1 | yes isb0 | record { eq = eq0 } = s≤s z≤n - ... | yes isb1 | no nisb0 | record { eq = eq0 } = z≤n - ... | no nisb1 | yes isb0 | record { eq = eq0 } = refl-≤≡ (sym eq0) - ... | no nisb1 | no nisb0 | record { eq = eq0 } = z≤n - lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) | inspect count-B (suc i) | inspect count-B (suc (suc i)) - ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ | record { eq = eq0 } | record { eq = eq1 } = refl-≤≡ (sym eq0) - ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ | _ | _ = ⊥-elim (nat-≡< b (<-trans a a<sa)) - ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c | _ | _ = ⊥-elim (nat-<> a (<-trans a<sa c) ) - ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ | record { eq = eq0 } | _ = refl-≤≡ (sym eq0) - ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ | _ | _ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) ) - ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c | _ | _ = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c)) - ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c | _ | _ = ⊥-elim (nat-≤> a (<-transʳ c a<sa ) ) - ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c | record { eq = eq0 } | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) - ... | yes isb = refl-≤≡ (sym eq0) - ... | no nisb = refl-≤≡ (sym eq0) - lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ | record { eq = eq0 } | record { eq = eq1 } + lem01 zero | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa ( fromℕ< {0} 0<fa )) + ... | yes isb1 | yes isb0 = s≤s z≤n + ... | yes isb1 | no nisb0 = z≤n + ... | no nisb1 | yes isb0 = refl-≤≡ (sym lem14 ) where + lem14 : count-B 0 ≡ 1 + lem14 with is-B (Q←F fa ( fromℕ< {0} 0<fa )) + ... | yes isb = refl + ... | no ne = ⊥-elim (ne isb0) + ... | no nisb1 | no nisb0 = z≤n + lem01 (suc i) with <-cmp (finite fa) (suc i) | <-cmp (finite fa) (suc (suc i)) + ... | tri< a ¬b ¬c | tri< a₁ ¬b₁ ¬c₁ = refl-≤≡ (sym ? ) + ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< b (<-trans a a<sa)) + ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = ⊥-elim (nat-<> a (<-trans a<sa c) ) + ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = refl-≤≡ (sym ?) + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = ⊥-elim (nat-≡< (sym b) (subst (λ k → _ < k ) (sym b₁) a<sa) ) + ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< (sym b) (<-trans a<sa c)) + ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = ⊥-elim (nat-≤> a (<-transʳ c a<sa ) ) + ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c with is-B (Q←F fa (fromℕ< c)) + ... | yes isb = refl-≤≡ (sym ?) + ... | no nisb = refl-≤≡ (sym ?) + lem01 (suc i) | tri> ¬a ¬b c | tri> ¬a₁ ¬b₁ c₁ with is-B (Q←F fa (fromℕ< c)) | is-B (Q←F fa (fromℕ< c₁)) - ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa - ... | yes isb0 | no nisb1 = refl-≤≡ (sym eq0) - ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym eq0)) a≤sa - ... | no nisb0 | no nisb1 = refl-≤≡ (sym eq0) + ... | yes isb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa + ... | yes isb0 | no nisb1 = refl-≤≡ (sym ?) + ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa + ... | no nisb0 | no nisb1 = refl-≤≡ (sym ?) lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b))) lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where @@ -679,10 +666,10 @@ Q←F fa ( fromℕ< (fin<n _) ) ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) 0<fa) ⟩ Q←F fa ( fromℕ< {0} 0<fa ) ∎ where open ≡-Reasoning - lem32 (suc i) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) - ... | tri< a ¬b ¬c | _ = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) ) - ... | tri≈ ¬a eq1 ¬c | _ = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _))) - ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) + lem32 (suc i) eq with <-cmp (finite fa) (suc i) + ... | tri< a ¬b ¬c = ⊥-elim ( nat-≡< eq (<-trans (fin<n _) a) ) + ... | tri≈ ¬a eq1 ¬c = ⊥-elim ( nat-≡< eq (subst (λ k → toℕ (F←Q fa (f b)) < k ) eq1 (fin<n _))) + ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) ... | yes isb = s≤s z≤n ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where lem33 : f b ≡ Q←F fa ( fromℕ< c) @@ -713,17 +700,17 @@ 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) - ... | no nisc | _ | _ | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where + ... | tri> ¬a ¬b c with is-B (Q←F fa ( fromℕ< 0<fa )) | is-B (Q←F fa (fromℕ< c)) + ... | no nisc | _ = ⊥-elim (nisc record { a = Is.a bi ; fa=c = lem26 } ) where lem26 : f (Is.a bi) ≡ Q←F fa (fromℕ< 0<fa) lem26 = trans (Is.fa=c bi) (cong (Q←F fa) (fromℕ<-cong _ _ refl i<fa 0<fa) ) - ... | yes _ | _ | no nisc | _ = ⊥-elim (nisc record { a = Is.a bj ; fa=c = lem26 } ) where + ... | 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 } = lem25 where + ... | yes _ | yes _ = lem25 where lem25 : 2 ≤ suc (count-B j) lem25 = begin - 2 ≡⟨ cong suc (sym eq1) ⟩ + 2 ≡⟨ cong suc (sym ?) ⟩ 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 @@ -736,9 +723,9 @@ 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 + ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) + ... | yes _ = 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) @@ -755,10 +742,10 @@ ... | 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 - ... | no nisb | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) - ... | yes isb | record { eq = eq1 } with ≤-∨ (s≤s le) - ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans eq1 (sym (trans eq2 eq)) + lem09 0 (suc j) (s≤s le) eq with is-B (Q←F fa (fromℕ< {0} 0<fa )) + ... | no nisb = ⊥-elim ( nat-≡< (sym eq) (s≤s z≤n) ) + ... | yes isb with ≤-∨ (s≤s le) + ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans ? (sym (trans eq2 eq)) ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb))) lem10 = begin @@ -767,13 +754,13 @@ toℕ (F←Q fa (Q←F fa (fromℕ< {0} 0<fa ))) ≡⟨ cong (λ k → toℕ ((F←Q fa k))) (sym (Is.fa=c isb)) ⟩ toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning ... | case2 (s≤s lt) = ⊥-elim ( nat-≡< (sym eq) (s≤s (<-transʳ z≤n lt) )) - lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) | inspect count-B (suc i) - ... | tri< a ¬b ¬c | _ = lem09 i (suc j) (s≤s le) eq - ... | tri≈ ¬a b ¬c | _ = lem09 i (suc j) (s≤s le) eq - ... | tri> ¬a ¬b c | record { eq = eq1 } with is-B (Q←F fa (fromℕ< c)) + lem09 (suc i) (suc j) (s≤s le) eq with <-cmp (finite fa) (suc i) + ... | tri< a ¬b ¬c = lem09 i (suc j) (s≤s le) eq + ... | tri≈ ¬a b ¬c = lem09 i (suc j) (s≤s le) eq + ... | tri> ¬a ¬b c with is-B (Q←F fa (fromℕ< c)) ... | no nisb = lem09 i (suc j) (s≤s le) eq ... | yes isb with ≤-∨ (s≤s le) - ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans eq1 (sym (trans eq2 eq )) + ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans ? (sym (trans eq2 eq )) ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb))) lem11 = begin
--- a/automaton-in-agda/src/logic.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/logic.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module logic where open import Level @@ -10,10 +12,6 @@ true : Bool false : Bool -data Two : Set where - i0 : Two - i1 : Two - record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where constructor ⟪_,_⟫ field @@ -27,13 +25,6 @@ _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m) _⇔_ A B = ( A → B ) ∧ ( B → A ) -∧-exch : {n m : Level} {A : Set n} { B : Set m } → A ∧ B → B ∧ A -∧-exch p = ⟪ _∧_.proj2 p , _∧_.proj1 p ⟫ - -∨-exch : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → B ∨ A -∨-exch (case1 x) = case2 x -∨-exch (case2 x) = case1 x - contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) @@ -47,10 +38,6 @@ de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) -de-morgan∨ : {n : Level } {A B : Set n} → A ∨ B → ¬ ( (¬ A ) ∧ (¬ B ) ) -de-morgan∨ {n} {A} {B} (case1 a) and = ⊥-elim ( _∧_.proj1 and a ) -de-morgan∨ {n} {A} {B} (case2 b) and = ⊥-elim ( _∧_.proj2 and b ) - dont-or : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a ) dont-or {A} {B} (case2 b) ¬A = b @@ -71,7 +58,7 @@ false \/ false = false _ \/ _ = true -not : Bool → Bool +not_ : Bool → Bool not true = false not false = true @@ -80,11 +67,10 @@ false <=> false = true _ <=> _ = false -open import Relation.Binary.PropositionalEquality +infixr 130 _\/_ +infixr 140 _/\_ -not-not-bool : { b : Bool } → not (not b) ≡ b -not-not-bool {true} = refl -not-not-bool {false} = refl +open import Relation.Binary.PropositionalEquality record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where field @@ -97,13 +83,14 @@ injection R S f = (x y : R) → f x ≡ f y → x ≡ y +not-not-bool : { b : Bool } → not (not b) ≡ b +not-not-bool {true} = refl +not-not-bool {false} = refl + ¬t=f : (t : Bool ) → ¬ ( not t ≡ t) ¬t=f true () ¬t=f false () -infixr 130 _\/_ -infixr 140 _/\_ - ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B ≡-Bool-func {true} {true} a→b b→a = refl ≡-Bool-func {false} {true} a→b b→a with b→a refl @@ -130,89 +117,57 @@ ¬-bool refl () lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ -lemma-∧-0 {true} {true} refl () lemma-∧-0 {true} {false} () lemma-∧-0 {false} {true} () lemma-∧-0 {false} {false} () +lemma-∧-0 {true} {true} eq1 () lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥ -lemma-∧-1 {true} {true} refl () lemma-∧-1 {true} {false} () lemma-∧-1 {false} {true} () lemma-∧-1 {false} {false} () +lemma-∧-1 {true} {true} eq1 () bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true bool-and-tt refl refl = refl bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true -bool-∧→tt-0 {true} {true} refl = refl +bool-∧→tt-0 {true} {true} eq = refl bool-∧→tt-0 {false} {_} () bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true -bool-∧→tt-1 {true} {true} refl = refl +bool-∧→tt-1 {true} {true} eq = refl bool-∧→tt-1 {true} {false} () bool-∧→tt-1 {false} {false} () bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b -bool-or-1 {false} {true} refl = refl -bool-or-1 {false} {false} refl = refl +bool-or-1 {false} {true} eq = refl +bool-or-1 {false} {false} eq = refl bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a -bool-or-2 {true} {false} refl = refl -bool-or-2 {false} {false} refl = refl +bool-or-2 {true} {false} eq = refl +bool-or-2 {false} {false} eq = refl bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true bool-or-3 {true} = refl bool-or-3 {false} = refl bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true -bool-or-31 {true} {true} refl = refl -bool-or-31 {false} {true} refl = refl +bool-or-31 {true} {true} eq = refl +bool-or-31 {false} {true} eq = refl bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true bool-or-4 {true} = refl bool-or-4 {false} = refl bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true -bool-or-41 {true} {b} refl = refl +bool-or-41 {true} {b} eq = refl bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false -bool-and-1 {false} {b} refl = refl +bool-and-1 {false} {b} eq = refl bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false -bool-and-2 {true} {false} refl = refl -bool-and-2 {false} {false} refl = refl +bool-and-2 {true} {false} eq = refl +bool-and-2 {false} {false} eq = refl +bool-and-2 {true} {true} () +bool-and-2 {false} {true} () -open import Data.Nat -open import Data.Nat.Properties - -_≥b_ : ( x y : ℕ) → Bool -x ≥b y with <-cmp x y -... | tri< a ¬b ¬c = false -... | tri≈ ¬a b ¬c = true -... | tri> ¬a ¬b c = true - -_>b_ : ( x y : ℕ) → Bool -x >b y with <-cmp x y -... | tri< a ¬b ¬c = false -... | tri≈ ¬a b ¬c = false -... | tri> ¬a ¬b c = true - -_≤b_ : ( x y : ℕ) → Bool -x ≤b y = y ≥b x - -_<b_ : ( x y : ℕ) → Bool -x <b y = y >b x - -open import Relation.Binary.PropositionalEquality - -¬i0≡i1 : ¬ ( i0 ≡ i1 ) -¬i0≡i1 () - -¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1 -¬i0→i1 {i0} ne = ⊥-elim ( ne refl ) -¬i0→i1 {i1} ne = refl - -¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0 -¬i1→i0 {i0} ne = refl -¬i1→i0 {i1} ne = ⊥-elim ( ne refl ) -
--- a/automaton-in-agda/src/nat.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/nat.agda Sun Sep 24 11:32:01 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + module nat where open import Data.Nat @@ -104,15 +105,15 @@ div2-eq : (x : ℕ ) → div2-rev ( div2 x ) ≡ x div2-eq zero = refl div2-eq (suc zero) = refl -div2-eq (suc (suc x)) with div2 x | inspect div2 x -... | ⟪ x1 , true ⟫ | record { eq = eq1 } = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫ +div2-eq (suc (suc x)) with div2 x in eq1 +... | ⟪ x1 , true ⟫ = begin -- eq1 : div2 x ≡ ⟪ x1 , true ⟫ div2-rev ⟪ suc x1 , true ⟫ ≡⟨⟩ suc (suc (x1 + suc x1)) ≡⟨ cong (λ k → suc (suc k )) (+-comm x1 _ ) ⟩ suc (suc (suc (x1 + x1))) ≡⟨⟩ suc (suc (div2-rev ⟪ x1 , true ⟫)) ≡⟨ cong (λ k → suc (suc (div2-rev k ))) (sym eq1) ⟩ suc (suc (div2-rev (div2 x))) ≡⟨ cong (λ k → suc (suc k)) (div2-eq x) ⟩ suc (suc x) ∎ where open ≡-Reasoning -... | ⟪ x1 , false ⟫ | record { eq = eq1 } = begin +... | ⟪ x1 , false ⟫ = begin div2-rev ⟪ suc x1 , false ⟫ ≡⟨⟩ suc (x1 + suc x1) ≡⟨ cong (λ k → (suc k )) (+-comm x1 _ ) ⟩ suc (suc (x1 + x1)) ≡⟨⟩ @@ -138,6 +139,40 @@ _-_ = minus +sn-m=sn-m : {m n : ℕ } → m ≤ n → suc n - m ≡ suc ( n - m ) +sn-m=sn-m {0} {n} z≤n = refl +sn-m=sn-m {suc m} {suc n} (s≤s m<n) = sn-m=sn-m m<n + +si-sn=i-n : {i n : ℕ } → n < i → suc (i - suc n) ≡ (i - n) +si-sn=i-n {i} {n} n<i = begin + suc (i - suc n) ≡⟨ sym (sn-m=sn-m n<i ) ⟩ + suc i - suc n ≡⟨⟩ + i - n + ∎ where + open ≡-Reasoning + +refl-≤s : {x : ℕ } → x ≤ suc x +refl-≤s {zero} = z≤n +refl-≤s {suc x} = s≤s (refl-≤s {x}) + +a≤sa = refl-≤s + +n-m<n : (n m : ℕ ) → n - m ≤ n +n-m<n zero zero = z≤n +n-m<n (suc n) zero = s≤s (n-m<n n zero) +n-m<n zero (suc m) = z≤n +n-m<n (suc n) (suc m) = ≤-trans (n-m<n n m ) refl-≤s + +n-n-m=m : {m n : ℕ } → m ≤ n → m ≡ (n - (n - m)) +n-n-m=m {0} {zero} z≤n = refl +n-n-m=m {0} {suc n} z≤n = n-n-m=m {0} {n} z≤n +n-n-m=m {suc m} {suc n} (s≤s m≤n) = sym ( begin + suc n - ( n - m ) ≡⟨ sn-m=sn-m (n-m<n n m) ⟩ + suc (n - ( n - m )) ≡⟨ cong (λ k → suc k ) (sym (n-n-m=m m≤n)) ⟩ + suc m + ∎ ) where + open ≡-Reasoning + m+= : {i j m : ℕ } → m + i ≡ m + j → i ≡ j m+= {i} {j} {zero} refl = refl m+= {i} {j} {suc m} eq = m+= {i} {j} {m} ( cong (λ k → pred k ) eq ) @@ -238,12 +273,6 @@ ... | tri≈ ¬a refl ¬c = case2 ≤-refl ... | tri> ¬a ¬b c = case2 (<to≤ c) -refl-≤s : {x : ℕ } → x ≤ suc x -refl-≤s {zero} = z≤n -refl-≤s {suc x} = s≤s (refl-≤s {x}) - -a≤sa = refl-≤s - refl-≤ : {x : ℕ } → x ≤ x refl-≤ {zero} = z≤n refl-≤ {suc x} = s≤s (refl-≤ {x}) @@ -696,15 +725,15 @@ m ∎ where open ≤-Reasoning 0<factor : { m k : ℕ } → k > 0 → m > 0 → (d : Dividable k m ) → Dividable.factor d > 0 -0<factor {m} {k} k>0 m>0 d with Dividable.factor d | inspect Dividable.factor d -... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< ff1 m>0 ) where +0<factor {m} {k} k>0 m>0 d with Dividable.factor d in eq1 +... | zero = ⊥-elim ( nat-≡< ff1 m>0 ) where ff1 : 0 ≡ m ff1 = begin 0 ≡⟨⟩ 0 * k + 0 ≡⟨ cong (λ j → j * k + 0) (sym eq1) ⟩ Dividable.factor d * k + 0 ≡⟨ Dividable.is-factor d ⟩ m ∎ where open ≡-Reasoning -... | suc t | _ = s≤s z≤n +... | suc t = s≤s z≤n div→k≤m : { m k : ℕ } → k > 1 → m > 0 → Dividable k m → m ≥ k div→k≤m {m} {k} k>1 m>0 d with <-cmp m k
--- a/automaton-in-agda/src/non-regular.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Sun Sep 24 11:32:01 2023 +0900 @@ -312,7 +312,21 @@ count1 x + count1 y + count1 z ∎ where open ≡-Reasoning -- this takes very long time to check and needs 10GB bb22 : count0 y ≡ count1 y - bb22 = ? + bb22 = begin + count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( + begin + count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ + (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ + (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ + (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z + ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ + count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z + ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ + count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ + count1 y ∎ where open ≡-Reasoning -- -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y --
--- a/automaton-in-agda/src/pumping.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/pumping.agda Sun Sep 24 11:32:01 2023 +0900 @@ -65,7 +65,7 @@ open Data.Maybe -open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) open import Relation.Binary.Definitions open import Data.Unit using (⊤ ; tt) open import Data.Nat.Properties
--- a/automaton-in-agda/src/regular-star.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/regular-star.agda Sun Sep 24 11:32:01 2023 +0900 @@ -74,7 +74,7 @@ open Found closed-in-star← : contain (M-Star A ) x ≡ true → Star (contain A) x ≡ true - closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA {!!} x C + closed-in-star← C with subset-construction-lemma← (SNFA-exist A ) NFA (Star-NFA-start A) x C ... | CC = {!!}