Mercurial > hg > Members > kono > Proof > automaton
changeset 405:af8f630b7e60
...
line wrap: on
line diff
--- a/automaton-in-agda/src/automaton-ex.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/automaton-ex.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + module automaton-ex where open import Data.Nat @@ -102,6 +103,24 @@ test11 : count-chars ( i1 ∷ i1 ∷ i0 ∷ [] ) i0 ≡ 1 test11 = refl +_≥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 + ex1_4a : (x : List In2) → Bool ex1_4a x = ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 ) @@ -138,5 +157,5 @@ am14a-tr' a00 i0 = a10 am14a-tr' _ _ = a10 -am14a' : Automaton am14s In2 -am14a' = record { δ = am14a-tr' ; aend = λ x → {!!} } +-- am14a' : Automaton am14s In2 +-- am14a' = record { δ = am14a-tr' ; aend = λ x → {!!} }
--- a/automaton-in-agda/src/cfg.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/cfg.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} + module cfg where open import Level renaming ( suc to succ ; zero to Zero )
--- a/automaton-in-agda/src/cfg1.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/cfg1.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} + module cfg1 where open import Level renaming ( suc to succ ; zero to Zero ) @@ -35,7 +37,7 @@ field cfg : Symbol → Body Symbol top : Symbol - eq? : Symbol → Symbol → Bool + eqP : Symbol → Symbol → Bool typeof : Symbol → Node Symbol infixr 80 _｜_ @@ -64,11 +66,11 @@ cfg-language1 : {Symbol : Set} → CFGGrammer Symbol → Seq Symbol → List Symbol → Bool cfg-language1 cg Error x = false cfg-language1 cg (S ， seq) x with typeof cg S -cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eq? cg x x' /\ cfg-language1 cg seq t +cfg-language1 cg (_ ， seq) (x' ∷ t) | T x = eqP cg x x' /\ cfg-language1 cg seq t cfg-language1 cg (_ ， seq) [] | T x = false cfg-language1 cg (_ ， seq) x | N nonTerminal = split (cfg-language0 cg (cfg cg nonTerminal) )(cfg-language1 cg seq ) x cfg-language1 cg (S ．) x with typeof cg S -cfg-language1 cg (_ ．) (x' ∷ []) | T x = eq? cg x x' +cfg-language1 cg (_ ．) (x' ∷ []) | T x = eqP cg x x' cfg-language1 cg (_ ．) _ | T x = false cfg-language1 cg (_ ．) x | N nonTerminal = cfg-language0 cg (cfg cg nonTerminal) x @@ -117,7 +119,7 @@ IFGrammer = record { cfg = cfg' ; top = statement - ; eq? = token-eq? + ; eqP = token-eq? ; typeof = typeof-IFG } where cfg' : IFToken → Body IFToken @@ -168,7 +170,7 @@ E1Grammer = record { cfg = cfgE ; top = expr - ; eq? = E1-token-eq? + ; eqP = E1-token-eq? ; typeof = typeof-E1 } where cfgE : E1Token → Body E1Token @@ -286,7 +288,7 @@ pda→cfg pda = record { cfg = {!!} ; top = {!!} - ; eq? = {!!} + ; eqP = {!!} ; typeof = {!!} } @@ -299,6 +301,6 @@ field cdg : Seq Symbol → Body Symbol top : Symbol - eq? : Symbol → Symbol → Bool + eqP : Symbol → Symbol → Bool typeof : Symbol → Node Symbol
--- a/automaton-in-agda/src/chap0.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/chap0.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module chap0 where open import Data.List @@ -149,7 +151,7 @@ indirect : ( z : V ) -> E x z → connected {V} E z y → connected E x y lemma1 : connected ( edge graph012a ) 1 2 -lemma1 = direct refl where +lemma1 = direct refl lemma1-2 : connected ( edge graph012a ) 1 3 lemma1-2 = indirect 2 refl (direct refl ) @@ -188,7 +190,7 @@ even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0 even2 0 refl = refl even2 1 () -even2 (suc (suc n)) eq = trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n +even2 (suc (suc n)) eq = ? -- trans ([a+n]%n≡a%n n _) eq -- [a+n]%n≡a%n : ∀ a n → (a + suc n) % suc n ≡ a % suc n sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ sum-of-dgree [] = 0 @@ -202,7 +204,7 @@ (2 + sum-of-dgree t ) % 2 ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) ) ⟩ (sum-of-dgree t + 2) % 2 - ≡⟨ [a+n]%n≡a%n (sum-of-dgree t) _ ⟩ + ≡⟨ ? ⟩ -- [a+n]%n≡a%n (sum-of-dgree t) _ ⟩ sum-of-dgree t % 2 ≡⟨ dgree-even t ⟩ 0
--- a/automaton-in-agda/src/derive.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/derive.agda Sun Sep 24 18:02:04 2023 +0900 @@ -5,6 +5,7 @@ open import Data.List hiding ( [_] ) open import Data.Empty open import finiteSet +open import finiteFunc open import fin module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where @@ -74,7 +75,7 @@ -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -- open import nfa -open import Data.Nat +open import Data.Nat hiding (eq?) open import Data.Nat.Properties hiding ( eq? ) open import nat open import finiteSetUtil @@ -261,10 +262,10 @@ sb01 : (isb : ISB (r & r₁)) → ( ISB.is-sub isb ≡ sub&1 _ _ _ ? ) ∨ ( ISB.is-sub isb ≡ sub&2 _ _ _ ? ) ∨ ( ISB.is-sub isb ≡ subst (λ k → SB ? ?) ? (sub&& _ _ _ ? ? )) - sb01 isb with ISB.is-sub isb | inspect ISB.is-sub isb - ... | sub&1 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case1 refl - ... | sub&2 .r .r₁ .(ISB.s isb) t | record { eq = refl } = case2 (case1 refl) - ... | sub&& .r .r₁ z x t | record { eq = refl } = case2 (case2 refl) + sb01 isb with ISB.is-sub isb in eq + ... | sub&1 .r .r₁ .(ISB.s isb) t = case1 ? + ... | sub&2 .r .r₁ .(ISB.s isb) t = case2 (case1 ?) + ... | sub&& .r .r₁ z x t = case2 (case2 ?) sb00 : ISB r → Bool sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub&1 _ _ _ is-sub } sbempty? (r || r₁) f with f record { s = r ; is-sub = sub|1 ? } | f record { s = r₁ ; is-sub = sub|2 ? }
--- a/automaton-in-agda/src/deriveUtil.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/deriveUtil.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module deriveUtil where open import Level renaming ( suc to succ ; zero to Zero )
--- a/automaton-in-agda/src/even.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/even.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module even where open import Data.Nat
--- a/automaton-in-agda/src/extended-automaton.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/extended-automaton.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,4 +1,6 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + +-- {-# OPTIONS --allow-unsolved-metas #-} module extended-automaton where open import Level renaming ( suc to succ ; zero to Zero )
--- a/automaton-in-agda/src/finiteSetUtil.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/finiteSetUtil.agda Sun Sep 24 18:02:04 2023 +0900 @@ -27,7 +27,7 @@ module _ {Q : Set } (F : FiniteSet Q) where open FiniteSet F - equal?-refl : { x : Q } → equal? x x ≡ true + equal?-refl : { x : Q } → equal? x x ≡ true equal?-refl {x} with F←Q x ≟ F←Q x ... | yes eq = refl ... | no ne = ⊥-elim (ne refl) @@ -47,24 +47,24 @@ ... | yes eq = yes (subst₂ (λ j k → j ≡ k ) (finiso→ x) (finiso→ y) (cong Q←F eq) ) ... | no n = no (λ eq → n (cong F←Q eq)) End : (m : ℕ ) → (p : Q → Bool ) → Set - End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false + End m p = (i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false first-end : ( p : Q → Bool ) → End finite p first-end p i i>n = ⊥-elim (nat-≤> i>n (fin<n {finite} i) ) next-end : {m : ℕ } → ( p : Q → Bool ) → End (suc m) p → (m<n : m < finite ) → p (Q←F (fromℕ< m<n )) ≡ false → End m p - next-end {m} p prev m<n np i m<i with NP.<-cmp m (toℕ i) + next-end {m} p prev m<n np i m<i with NP.<-cmp m (toℕ i) next-end p prev m<n np i m<i | tri< a ¬b ¬c = prev i a next-end p prev m<n np i m<i | tri> ¬a ¬b c = ⊥-elim ( nat-≤> m<i c ) next-end {m} p prev m<n np i m<i | tri≈ ¬a b ¬c = subst ( λ k → p (Q←F k) ≡ false) (m<n=i i b m<n ) np where m<n=i : {n : ℕ } (i : Fin n) {m : ℕ } → m ≡ (toℕ i) → (m<n : m < n ) → fromℕ< m<n ≡ i - m<n=i i refl m<n = fromℕ<-toℕ i m<n + m<n=i i refl m<n = fromℕ<-toℕ i m<n found : { p : Q → Bool } → (q : Q ) → p q ≡ true → exists p ≡ true found {p} q pt = found1 finite (NP.≤-refl ) ( first-end p ) where found1 : (m : ℕ ) (m<n : m Data.Nat.≤ finite ) → ((i : Fin finite) → m ≤ toℕ i → p (Q←F i ) ≡ false ) → exists1 m m<n p ≡ true found1 0 m<n end = ⊥-elim ( ¬-bool (subst (λ k → k ≡ false ) (cong (λ k → p k) (finiso→ q) ) (end (F←Q q) z≤n )) pt ) found1 (suc m) m<n end with bool-≡-? (p (Q←F (fromℕ< m<n))) true - found1 (suc m) m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤ m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤ m<n) p} ) + found1 (suc m) m<n end | yes eq = subst (λ k → k \/ exists1 m (<to≤ m<n) p ≡ true ) (sym eq) (bool-or-4 {exists1 m (<to≤ m<n) p} ) found1 (suc m) m<n end | no np = begin p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p ≡⟨ bool-or-1 (¬-bool-t np ) ⟩ @@ -78,9 +78,9 @@ not-found2 zero _ = refl not-found2 ( suc m ) m<n with pn (Q←F (fromℕ< {m} {finite} m<n)) not-found2 (suc m) m<n | eq = begin - p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p + p (Q←F (fromℕ< m<n)) \/ exists1 m (<to≤ m<n) p ≡⟨ bool-or-1 eq ⟩ - exists1 m (<to≤ m<n) p + exists1 m (<to≤ m<n) p ≡⟨ not-found2 m (<to≤ m<n) ⟩ false ∎ where open ≡-Reasoning @@ -92,9 +92,9 @@ 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 = - found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) - not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false + found2 (suc m) m<n end | no np = + found2 m (<to≤ m<n) (next-end p end m<n (¬-bool-t np )) + not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false not-found← {p} np q = ¬-bool-t ( contra-position {_} {_} {_} {exists p ≡ true} (found q) (λ ep → ¬-bool np ep ) ) Q←F-inject : {x y : Fin finite} → Q←F x ≡ Q←F y → x ≡ y Q←F-inject eq = subst₂ (λ j k → j ≡ k ) (finiso← _) (finiso← _) (cong F←Q eq) @@ -103,16 +103,16 @@ -iso-fin : {A B : Set} → FiniteSet A → Bijection A B → FiniteSet B +iso-fin : {A B : Set} → FiniteSet A → Bijection A B → FiniteSet B iso-fin {A} {B} fin iso = record { Q←F = λ f → fun→ iso ( FiniteSet.Q←F fin f ) ; F←Q = λ b → FiniteSet.F←Q fin (fun← iso b ) - ; finiso→ = finiso→ - ; finiso← = finiso← + ; finiso→ = finiso→ + ; finiso← = finiso← } where finiso→ : (q : B) → fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) ≡ q finiso→ q = begin - fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) + fun→ iso (FiniteSet.Q←F fin (FiniteSet.F←Q fin (Bijection.fun← iso q))) ≡⟨ cong (λ k → fun→ iso k ) (FiniteSet.finiso→ fin _ ) ⟩ fun→ iso (Bijection.fun← iso q) ≡⟨ fiso→ iso _ ⟩ @@ -120,9 +120,9 @@ ∎ where open ≡-Reasoning finiso← : (f : Fin (FiniteSet.finite fin ))→ FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) ≡ f finiso← f = begin - FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) + FiniteSet.F←Q fin (Bijection.fun← iso (Bijection.fun→ iso (FiniteSet.Q←F fin f))) ≡⟨ cong (λ k → FiniteSet.F←Q fin k ) (Bijection.fiso← iso _) ⟩ - FiniteSet.F←Q fin (FiniteSet.Q←F fin f) + FiniteSet.F←Q fin (FiniteSet.Q←F fin f) ≡⟨ FiniteSet.finiso← fin _ ⟩ f ∎ where @@ -136,7 +136,7 @@ fin00 : (q : One) → one ≡ q fin00 one = refl -fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) +fin-∨1 : {B : Set} → (fb : FiniteSet B ) → FiniteSet (One ∨ B) fin-∨1 {B} fb = record { Q←F = Q←F ; F←Q = F←Q @@ -149,7 +149,7 @@ Q←F (suc f) = case2 (FiniteSet.Q←F fb f) F←Q : One ∨ B → Fin (suc b) F←Q (case1 one) = zero - F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) + F←Q (case2 f ) = suc (FiniteSet.F←Q fb f) finiso→ : (q : One ∨ B) → Q←F (F←Q q) ≡ q finiso→ (case1 one) = refl finiso→ (case2 b) = cong (λ k → case2 k ) (FiniteSet.finiso→ fb b) @@ -158,7 +158,7 @@ finiso← (suc f) = cong ( λ k → suc k ) (FiniteSet.finiso← fb f) -fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B → FiniteSet (Fin a ∨ B) +fin-∨2 : {B : Set} → ( a : ℕ ) → FiniteSet B → FiniteSet (Fin a ∨ B) fin-∨2 {B} zero fb = iso-fin fb iso where iso : Bijection B (Fin zero ∨ B) iso = record { @@ -168,7 +168,7 @@ ; fiso← = λ _ → refl } where fun←1 : Fin zero ∨ B → B - fun←1 (case2 x) = x + fun←1 (case2 x) = x fiso→1 : (f : Fin zero ∨ B ) → case2 (fun←1 f) ≡ f fiso→1 (case2 x) = refl fin-∨2 {B} (suc a) fb = iso-fin (fin-∨1 (fin-∨2 a fb) ) iso @@ -193,9 +193,9 @@ fun→ (FiniteSet→Fin fin) f = FiniteSet.Q←F fin f fiso← (FiniteSet→Fin fin) = FiniteSet.finiso← fin fiso→ (FiniteSet→Fin fin) = FiniteSet.finiso→ fin - + -fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) +fin-∨ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∨ B) fin-∨ {A} {B} fa fb = iso-fin (fin-∨2 a fb ) iso2 where a = FiniteSet.finite fa ia = FiniteSet→Fin fa @@ -211,14 +211,14 @@ open import Data.Product hiding ( map ) -fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) +fin-× : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A × B) fin-× {A} {B} fa fb with FiniteSet→Fin fa ... | a=f = iso-fin (fin-×-f a ) iso-1 where a = FiniteSet.finite fa b = FiniteSet.finite fb iso-1 : Bijection (Fin a × B) ( A × B ) - fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x) - fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x) + fun← iso-1 x = ( FiniteSet.F←Q fa (proj₁ x) , proj₂ x) + fun→ iso-1 x = ( FiniteSet.Q←F fa (proj₁ x) , proj₂ x) fiso← iso-1 x = lemma where lemma : (FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj₁ x)) , proj₂ x) ≡ ( proj₁ x , proj₂ x ) lemma = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso← fa _ ) @@ -234,19 +234,19 @@ fiso→ iso-2 (zero , b ) = refl fiso→ iso-2 (suc a , b ) = refl - fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) + fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 open _∧_ -fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) +fin-∧ : {A B : Set} → FiniteSet A → FiniteSet B → FiniteSet (A ∧ B) fin-∧ {A} {B} fa fb with FiniteSet→Fin fa -- same thing for our tool ... | a=f = iso-fin (fin-×-f a ) iso-1 where a = FiniteSet.finite fa b = FiniteSet.finite fb iso-1 : Bijection (Fin a ∧ B) ( A ∧ B ) - fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x} + fun← iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x} fun→ iso-1 x = record { proj1 = FiniteSet.Q←F fa (proj1 x) ; proj2 = proj2 x} fiso← iso-1 x = lemma where lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x } @@ -263,7 +263,7 @@ fiso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl fiso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl - fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B) + fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B) fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () ; finite = 0 } fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 @@ -292,12 +292,12 @@ cast-iso refl (suc f) = cong ( λ k → suc k ) ( cast-iso refl f ) -fin2List : {n : ℕ } → FiniteSet (Vec Bool n) +fin2List : {n : ℕ } → FiniteSet (Vec Bool n) fin2List {zero} = record { Q←F = λ _ → Vec.[] ; F←Q = λ _ → # 0 - ; finiso→ = finiso→ - ; finiso← = finiso← + ; finiso→ = finiso→ + ; finiso← = finiso← } where Q = Vec Bool zero finiso→ : (q : Q) → [] ≡ q @@ -309,7 +309,7 @@ QtoR : Vec Bool (suc n) → Vec Bool n ∨ Vec Bool n QtoR ( true ∷ x ) = case1 x QtoR ( false ∷ x ) = case2 x - RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) + RtoQ : Vec Bool n ∨ Vec Bool n → Vec Bool (suc n) RtoQ ( case1 x ) = true ∷ x RtoQ ( case2 x ) = false ∷ x isoRQ : (x : Vec Bool (suc n) ) → RtoQ ( QtoR x ) ≡ x @@ -329,17 +329,17 @@ qb1 : (q : Q) → toℕ (FiniteSet.F←Q fin q) < n → Bool qb1 q q<n = Q→B q (NP.<-trans q<n a<sa) -List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool +List2Func : { Q : Set } → {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → Q → Bool List2Func {Q} {zero} fin (s≤s z≤n) [] q = false List2Func {Q} {suc n} fin (s≤s n<m) (h ∷ t) q with FiniteSet.F←Q fin q ≟ fromℕ< n<m ... | yes _ = h ... | no _ = List2Func {Q} fin (NP.<-trans n<m a<sa ) t q -open import Level renaming ( suc to Suc ; zero to Zero) +open import Level renaming ( suc to Suc ; zero to Zero) L2F : {Q : Set } {n : ℕ } → (fin : FiniteSet Q ) → n < suc (FiniteSet.finite fin) → Vec Bool n → (q : Q ) → toℕ (FiniteSet.F←Q fin q ) < n → Bool -L2F fin n<m x q q<n = List2Func fin n<m x q +L2F fin n<m x q q<n = List2Func fin n<m x q L2F-iso : { Q : Set } → (fin : FiniteSet Q ) → (f : Q → Bool ) → (q : Q ) → (L2F fin a<sa (F2L fin a<sa (λ q _ → f q) )) q (toℕ<n _) ≡ f q L2F-iso {Q} fin f q = l2f m a<sa (toℕ<n _) where @@ -352,93 +352,25 @@ lemma13 {suc n} {suc nq} n<m nt (s≤s nq≤n) = s≤s (lemma13 {n} {nq} (NP.<-trans a<sa n<m ) (λ eq → nt ( cong ( λ k → suc k ) eq )) nq≤n) lemma3f : {a b : ℕ } → (lt : a < b ) → fromℕ< (s≤s lt) ≡ suc (fromℕ< lt) lemma3f (s≤s lt) = refl - lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m + lemma12f : {n m : ℕ } → (n<m : n < m ) → (f : Fin m ) → toℕ f ≡ n → f ≡ fromℕ< n<m lemma12f {zero} {suc m} (s≤s z≤n) zero refl = refl lemma12f {suc n} {suc m} (s≤s n<m) (suc f) refl = subst ( λ k → suc f ≡ k ) (sym (lemma3f n<m) ) ( cong ( λ k → suc k ) ( lemma12f {n} {m} n<m f refl ) ) l2f : (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n ) → (L2F fin n<m (F2L fin n<m (λ q _ → f q))) q q<n ≡ f q l2f zero (s≤s z≤n) () - l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m - l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin - f (FiniteSet.Q←F fin (fromℕ< n<m)) + l2f (suc n) (s≤s n<m) (s≤s n<q) with FiniteSet.F←Q fin q ≟ fromℕ< n<m + l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p = begin + f (FiniteSet.Q←F fin (fromℕ< n<m)) ≡⟨ cong ( λ k → f (FiniteSet.Q←F fin k )) (sym p) ⟩ f (FiniteSet.Q←F fin ( FiniteSet.F←Q fin q )) ≡⟨ cong ( λ k → f k ) (FiniteSet.finiso→ fin _ ) ⟩ - f q + f q ∎ where open ≡-Reasoning l2f (suc n) (s≤s n<m) (s≤s n<q) | no ¬p = l2f n (NP.<-trans n<m a<sa) (lemma11f n<m ¬p n<q) -Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) +Fin2Finite : ( n : ℕ ) → FiniteSet (Fin n) Fin2Finite n = record { F←Q = λ x → x ; Q←F = λ x → x ; finiso← = λ q → refl ; finiso→ = λ q → refl } -data fin-less { n : ℕ } { A : Set } (fa : FiniteSet A ) (n<m : n < FiniteSet.finite fa ) : Set where - elm1 : (elm : A ) → toℕ (FiniteSet.F←Q fa elm ) < n → fin-less fa n<m - -get-elm : { n : ℕ } { A : Set } {fa : FiniteSet A } {n<m : n < FiniteSet.finite fa } → fin-less fa n<m → A -get-elm (elm1 a _ ) = a - -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-< : {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 ) - 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)) - ≡⟨ toℕ-fromℕ< _ ⟩ - toℕ x - ∎ where - open ≡-Reasoning - fun← iso (elm1 elm x) = fromℕ< x - fun→ iso x = elm1 (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m ))) to<n where - x<n : toℕ x < n - x<n = toℕ<n x - to<n : toℕ (FiniteSet.F←Q fa (FiniteSet.Q←F fa (fromℕ< (NP.<-trans x<n n<m)))) < n - to<n = subst (λ k → toℕ k < n ) (sym (FiniteSet.finiso← fa _ )) (subst (λ k → k < n ) (sym ( toℕ-fromℕ< (NP.<-trans x<n n<m) )) x<n ) - fiso← iso x = lemma2 where - lemma2 : fromℕ< (subst (λ k → toℕ k < n) (sym - (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) - (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) ≡ x - lemma2 = begin - fromℕ< (subst (λ k → toℕ k < n) (sym - (FiniteSet.finiso← fa (fromℕ< (NP.<-trans (toℕ<n x) n<m)))) (subst (λ k → k < n) - (sym (toℕ-fromℕ< (NP.<-trans (toℕ<n x) n<m))) (toℕ<n x))) - ≡⟨⟩ - fromℕ< ( subst (λ k → toℕ ( k ) < n ) (sym (FiniteSet.finiso← fa _ )) lemma6 ) - ≡⟨ lemma10 (cong (λ k → toℕ k) (FiniteSet.finiso← fa _ ) ) ⟩ - fromℕ< lemma6 - ≡⟨ lemma10 (lemma11 n<m ) ⟩ - fromℕ< ( toℕ<n x ) - ≡⟨ fromℕ<-toℕ _ _ ⟩ - x - ∎ where - 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) = ? 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) - ≡⟨ toℕ-fromℕ< _ ⟩ - toℕ (FiniteSet.F←Q fa elm) - ∎ where open ≡-Reasoning - lemma : FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) ≡ elm - lemma = begin - FiniteSet.Q←F fa (fromℕ< (NP.<-trans (toℕ<n (Bijection.fun← iso (elm1 elm x))) n<m)) - ≡⟨⟩ - 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 k) (lemma10 refl ) ⟩ - 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 ) - ≡⟨ FiniteSet.finiso→ fa _ ⟩ - elm - ∎ where open ≡-Reasoning - open import Data.List open FiniteSet @@ -473,28 +405,28 @@ ... | false = phase1 finq q qs dup-in-list : { Q : Set } (finq : FiniteSet Q) (q : Q) (qs : List Q ) → Bool -dup-in-list {Q} finq q qs = phase1 finq q qs +dup-in-list {Q} finq q qs = phase1 finq q qs -- -- if length of the list is longer than kinds of a finite set, there is a duplicate -- prove this based on the theorem on Data.Fin -- -dup-in-list+fin : { Q : Set } (finq : FiniteSet Q) +dup-in-list+fin : { Q : Set } (finq : FiniteSet Q) → (q : Q) (qs : List Q ) → fin-dup-in-list (F←Q finq q) (map (F←Q finq) qs) ≡ true → dup-in-list finq q qs ≡ true 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 + → phase2 finq q qs ≡ true 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 - i-phase1 : (qs : List Q) → fin-phase1 (F←Q finq q) (map (F←Q finq) qs) ≡ true - → phase1 finq q qs ≡ true + 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 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 @@ -523,13 +455,13 @@ open import bijection using ( InjectiveF ; Is ) --- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) +-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) -inject-fin : {A B : Set} (fa : FiniteSet A ) - → (fi : InjectiveF B A) +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 with finite fa in eq1 +inject-fin {A} {B} fa fi is-B with finite fa in eq1 ... | zero = record { finite = 0 ; Q←F = λ () @@ -551,7 +483,7 @@ 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 + 0<fa = <-transˡ (s≤s z≤n) pfa<fa count-B : ℕ → ℕ count-B zero with is-B (Q←F fa ( fromℕ< {0} 0<fa )) @@ -582,46 +514,93 @@ 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 <-cmp (finite fa) 1 + 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 )) + 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 : count-B 0 ≡ 1 -- in-equality does not work we have to repeat the proof 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)) + 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 lem14) where lem14 : count-B (suc i) ≡ count-B i - lem14 with <-cmp (finite fa) (suc i) + lem14 with <-cmp (finite fa) (suc i) ... | tri< a ¬b ¬c = refl ... | tri≈ ¬a b ¬c = ⊥-elim ( ¬a a ) ... | tri> ¬a ¬b c = ⊥-elim ( ¬a a ) ... | 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₁ = refl-≤≡ (sym lem14 ) where + lem14 : count-B (suc i) ≡ count-B i + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a ¬b ¬c = refl + ... | tri≈ ¬a b ¬c = refl + ... | tri> ¬a ¬b c = ⊥-elim ( ¬c c ) ... | 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 ?)) a≤sa - ... | yes isb0 | no nisb1 = refl-≤≡ (sym ?) - ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym ?)) a≤sa - ... | no nisb0 | no nisb1 = refl-≤≡ (sym ?) + ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c with is-B (Q←F fa (fromℕ< c)) + ... | yes isb = refl-≤≡ (sym lem14) where + lem14 : count-B (suc i) ≡ suc (count-B i) + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | yes isb = refl + ... | no ne = ⊥-elim (ne record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | no nisb = refl-≤≡ (sym lem14) where + lem14 : count-B (suc i) ≡ count-B i + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | yes isb = ⊥-elim (nisb record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | no ne = refl + 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 lem14)) a≤sa where + lem14 : count-B (suc i) ≡ suc (count-B i) + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | no ne = ⊥-elim (ne record {a = Is.a isb0 ; fa=c = trans (Is.fa=c isb0) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | yes isb = refl + ... | yes isb0 | no nisb1 = refl-≤≡ (sym lem14) where + lem14 : count-B (suc i) ≡ suc (count-B i) + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | no ne = ⊥-elim (ne record {a = Is.a isb0 ; fa=c = trans (Is.fa=c isb0) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | yes isb = refl + ... | no nisb0 | yes isb1 = ≤-trans (refl-≤≡ (sym lem14)) a≤sa where + lem14 : count-B (suc i) ≡ count-B i + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | no ne = refl + ... | yes isb = ⊥-elim (nisb0 record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | no nisb0 | no nisb1 = refl-≤≡ (sym lem14) where + lem14 : count-B (suc i) ≡ count-B i + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | no ne = refl + ... | yes isb = ⊥-elim (nisb0 record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) lem31 : (b : B) → 0 < count-B (toℕ (F←Q fa (f b))) lem31 b = lem32 (toℕ (F←Q fa (f b))) refl where - lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i + lem32 : (i : ℕ) → toℕ (F←Q fa (f b)) ≡ i → 0 < count-B i lem32 zero eq with is-B (Q←F fa ( fromℕ< {0} 0<fa )) - ... | yes isb = s≤s z≤n + ... | yes isb = s≤s z≤n ... | no nisb = ⊥-elim ( nisb record { a = b ; fa=c = lem33 } ) where lem33 : f b ≡ Q←F fa ( fromℕ< {0} 0<fa ) lem33 = begin @@ -630,11 +609,11 @@ 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) + 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 + ... | 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) lem33 = begin @@ -643,41 +622,45 @@ Q←F fa ( fromℕ< (fin<n _) ) ≡⟨ cong (λ k → Q←F fa k) (fromℕ<-cong _ _ eq (fin<n _) c ) ⟩ Q←F fa ( fromℕ< c ) ∎ where open ≡-Reasoning - + cb<mb : (b : B) → pred (count-B (toℕ (F←Q fa (f b)))) < maxb cb<mb b = sx≤y→x<y ( begin - suc ( pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩ - count-B (toℕ (F←Q fa (f b))) ≤⟨ lem02 ⟩ + suc ( pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩ + count-B (toℕ (F←Q fa (f b))) ≤⟨ lem02 ⟩ count-B (finite fa) ∎ ) where open ≤-Reasoning lem02 : count-B (toℕ (F←Q fa (f b))) ≤ count-B (finite fa) - lem02 = count-B-mono (<to≤ (fin<n {_} (F←Q fa (f b)))) + lem02 = count-B-mono (<to≤ (fin<n {_} (F←Q fa (f b)))) cb00 : (n : ℕ) → n < count-B (finite fa) → CountB n cb00 n n<cb = lem09 (finite fa) (count-B (finite fa)) (<-transˡ a<sa n<cb) refl where - lem06 : (i j : ℕ) → (i<fa : i < finite fa) (j<fa : j < finite fa) + lem06 : (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 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) + 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 i < count-B j - lem20 zero (suc j) i<j i<fa j<fa bi bj with <-cmp (finite fa) (suc 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 )) | is-B (Q←F fa (fromℕ< c)) + ... | 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 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 _ | yes _ = lem25 where + ... | yes isb1 | yes _ = lem25 where + lem14 : count-B 0 ≡ 1 + lem14 with is-B (Q←F fa ( fromℕ< 0<fa )) + ... | no ne = ⊥-elim (ne record {a = Is.a isb1 ; fa=c = trans (Is.fa=c isb1) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | yes isb = refl lem25 : 2 ≤ suc (count-B j) lem25 = begin - 2 ≡⟨ cong suc (sym ?) ⟩ + 2 ≡⟨ cong suc (sym lem14) ⟩ 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) 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 @@ -687,7 +670,7 @@ 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)) + ... | 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) @@ -706,11 +689,15 @@ ... | 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 )) + 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)) + ... | case1 eq2 = record { b = Is.a isb ; cb = 0 ; b=cn = lem10 ; cb=n = trans lem14 (sym (trans eq2 eq)) ; cb-inject = λ cb1 c1<fa b1 eq → lem06 0 cb1 0<fa c1<fa isb b1 eq } where + lem14 : count-B 0 ≡ 1 + lem14 with is-B (Q←F fa ( fromℕ< 0<fa )) + ... | no ne = ⊥-elim (ne record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) + ... | yes isb = refl lem10 : 0 ≡ toℕ (F←Q fa (f (Is.a isb))) lem10 = begin 0 ≡⟨ sym ( toℕ-fromℕ< 0<fa ) ⟩ @@ -718,14 +705,21 @@ 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) + 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 ? (sym (trans eq2 eq )) + ... | case1 eq2 = record { b = Is.a isb ; cb = suc i ; b=cn = lem11 ; cb=n = trans lem14 (sym (trans eq2 eq )) ; cb-inject = λ cb1 c1<fa b1 eq → lem06 (suc i) cb1 c c1<fa isb b1 eq } where + lem14 : count-B (suc i) ≡ suc (count-B i) + lem14 with <-cmp (finite fa) (suc i) + ... | tri< a₂ ¬b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri≈ ¬a₂ b₂ ¬c₂ = ⊥-elim (¬c₂ c) + ... | tri> ¬a₂ ¬b₂ c₂ with is-B (Q←F fa ( fromℕ< c₂ )) + ... | yes isb = refl + ... | no ne = ⊥-elim (ne record {a = Is.a isb ; fa=c = trans (Is.fa=c isb) (cong (λ k → Q←F fa k) (lemma10 refl )) } ) lem11 : suc i ≡ toℕ (F←Q fa (f (Is.a isb))) lem11 = begin suc i ≡⟨ sym ( toℕ-fromℕ< c) ⟩ @@ -734,14 +728,14 @@ toℕ (F←Q fa (f (Is.a isb))) ∎ where open ≡-Reasoning ... | case2 (s≤s lt) = lem09 i j lt (cong pred eq) - iso0 : (x : Fin maxb) → fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡ x + iso0 : (x : Fin maxb) → fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡ x iso0 x = begin - fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡⟨ fromℕ<-cong _ _ ( begin + fromℕ< (cb<mb (CountB.b (cb00 (toℕ x) (fin<n _)))) ≡⟨ fromℕ<-cong _ _ ( begin pred (count-B (toℕ (F←Q fa (f (CountB.b (cb00 (toℕ x) (fin<n _))))))) ≡⟨ sym (cong (λ k → pred (count-B k)) (CountB.b=cn CB)) ⟩ pred (count-B (CountB.cb CB)) ≡⟨ cong pred (CountB.cb=n CB) ⟩ pred (suc (toℕ x)) ≡⟨ refl ⟩ - toℕ x ∎ ) (cb<mb (CountB.b CB)) (fin<n _) ⟩ - fromℕ< (fin<n {_} x) ≡⟨ fromℕ<-toℕ _ (fin<n {_} x) ⟩ + toℕ x ∎ ) (cb<mb (CountB.b CB)) (fin<n _) ⟩ + fromℕ< (fin<n {_} x) ≡⟨ fromℕ<-toℕ _ (fin<n {_} x) ⟩ x ∎ where open ≡-Reasoning CB = cb00 (toℕ x) (fin<n _) @@ -757,17 +751,17 @@ CB = cb00 (toℕ (fromℕ< (cb<mb b))) (fin<n _) isb : Is B A f (Q←F fa (fromℕ< (fin<n {_} (F←Q fa (f b)) ))) isb = record { a = b ; fa=c = lem33 } where - lem33 : f b ≡ Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) + lem33 : f b ≡ Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) lem33 = begin f b ≡⟨ sym (finiso→ fa _) ⟩ Q←F fa (F←Q fa (f b)) ≡⟨ cong (Q←F fa) (sym (fromℕ<-toℕ _ (fin<n (F←Q fa (f b))))) ⟩ - Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) ∎ + Q←F fa (fromℕ< (fin<n (F←Q fa (f b)))) ∎ lem30 : count-B (CountB.cb CB) ≡ count-B (toℕ (F←Q fa (InjectiveF.f fi b))) lem30 = begin count-B (CountB.cb CB) ≡⟨ CountB.cb=n CB ⟩ suc (toℕ (fromℕ< (cb<mb b))) ≡⟨ cong suc (toℕ-fromℕ< (cb<mb b)) ⟩ suc (pred (count-B (toℕ (F←Q fa (f b))))) ≡⟨ sucprd (lem31 b) ⟩ - count-B (toℕ (F←Q fa (f b))) ∎ + count-B (toℕ (F←Q fa (f b))) ∎ -- end
--- a/automaton-in-agda/src/flcagl.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/flcagl.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} + {-# OPTIONS --sized-types #-} open import Relation.Nullary open import Relation.Binary.PropositionalEquality
--- a/automaton-in-agda/src/gcd.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/gcd.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,4 +1,6 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + +-- {-# OPTIONS --allow-unsolved-metas #-} module gcd where open import Data.Nat @@ -16,7 +18,7 @@ gcd1 : ( i i0 j j0 : ℕ ) → ℕ gcd1 zero i0 zero j0 with <-cmp i0 j0 ... | tri< a ¬b ¬c = i0 -... | tri≈ ¬a refl ¬c = i0 +... | tri≈ ¬a b ¬c = i0 ... | tri> ¬a ¬b c = j0 gcd1 zero i0 (suc zero) j0 = 1 gcd1 zero zero (suc (suc j)) j0 = j0 @@ -46,7 +48,7 @@ gcdmm : (n m : ℕ) → gcd1 n m n m ≡ m gcdmm zero m with <-cmp m m ... | tri< a ¬b ¬c = refl -... | tri≈ ¬a refl ¬c = refl +... | tri≈ ¬a b ¬c = refl ... | tri> ¬a ¬b c = refl gcdmm (suc n) m = subst (λ k → k ≡ m) (sym (gcd22 n m n m )) (gcdmm n m ) @@ -56,7 +58,7 @@ ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl ... | tri≈ ¬a b ¬c | tri< a ¬b ¬c₁ = ⊥-elim (nat-≡< (sym b) a) -... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl +... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = b ... | tri≈ ¬a b ¬c | tri> ¬a₁ ¬b c = ⊥-elim (nat-≡< b c) ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (nat-≡< b c) @@ -317,7 +319,7 @@ ... | tri< a ¬b ¬c | tri≈ ¬a b ¬c₁ = ⊥-elim (¬b (sym b)) ... | tri< a ¬b ¬c | tri> ¬a ¬b₁ c = refl ... | tri≈ ¬a refl ¬c | tri< a ¬b ¬c₁ = ⊥-elim (¬b refl) - ... | tri≈ ¬a refl ¬c | tri≈ ¬a₁ refl ¬c₁ = refl + ... | tri≈ ¬a b ¬c | tri≈ ¬a₁ b₁ ¬c₁ = refl ... | tri≈ ¬a refl ¬c | tri> ¬a₁ ¬b c = ⊥-elim (¬b refl) ... | tri> ¬a ¬b c | tri< a ¬b₁ ¬c = refl ... | tri> ¬a ¬b c | tri≈ ¬a₁ b ¬c = ⊥-elim (¬b (sym b)) @@ -694,7 +696,11 @@ 1 ∎ where open ≡-Reasoning m*n=m→n : {m n : ℕ } → 0 < m → m * n ≡ m * 1 → n ≡ 1 -m*n=m→n {suc m} {n} (s≤s lt) eq = *-cancelˡ-≡ m eq +m*n=m→n {suc m} {n} (s≤s lt) eq = begin + n ≡⟨ *-cancelˡ-≡ n 1 (suc m) ( begin + suc m * n ≡⟨ eq ⟩ + suc m * 1 ∎ ) ⟩ + 1 ∎ where open ≡-Reasoning gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j gcd-is-gratest {i} {j} {k} i>0 j>0 k>1 ki kj = div→k≤m k>1 (gcd>0 i j i>0 j>0 ) gcd001 where @@ -712,16 +718,16 @@ jd : Dividable d (suc j) jd = proj2 (gcd-dividable (suc i) (suc j)) cop : gcd (Dividable.factor id) (Dividable.factor jd) ≡ 1 - cop with (gcd (Dividable.factor id) (Dividable.factor jd)) | inspect (gcd (Dividable.factor id)) (Dividable.factor jd) - ... | zero | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym eq1) (gcd>0 (Dividable.factor id) (Dividable.factor jd) + cop with (gcd (Dividable.factor id) (Dividable.factor jd)) in eq + ... | zero = ⊥-elim ( nat-≡< (sym eq) (gcd>0 (Dividable.factor id) (Dividable.factor jd) (0<factor d>0 (s≤s z≤n) id) (0<factor d>0 (s≤s z≤n) jd) )) - ... | suc zero | record { eq = eq1 } = refl - ... | suc (suc t) | record { eq = eq1 } = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where + ... | suc zero = refl + ... | suc (suc t) = ⊥-elim ( nat-≤> (gcd-is-gratest {suc i} {(suc j)} (s≤s z≤n) (s≤s z≤n) co1 d1id d1jd ) gcd<d1 ) where -- gcd-is-gratest : { i j k : ℕ } → i > 0 → j > 0 → k > 1 → Dividable k i → Dividable k j → k ≤ gcd i j d1 : ℕ d1 = gcd (Dividable.factor id) (Dividable.factor jd) d1>1 : gcd (Dividable.factor id) (Dividable.factor jd) > 1 - d1>1 = subst (λ k → 1 < k ) (sym eq1) (s≤s (s≤s z≤n)) + d1>1 = subst (λ k → 1 < k ) (sym eq) (s≤s (s≤s z≤n)) mul1 : {x : ℕ} → 1 * x ≡ x mul1 {zero} = refl mul1 {suc x} = begin
--- a/automaton-in-agda/src/halt.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/halt.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible #-} + module halt where open import Level renaming ( zero to Zero ; suc to Suc ) @@ -92,8 +94,8 @@ h-just h y eq with h y h-just h y refl | true = refl TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y - TN1 h y with h y | inspect h y - ... | true | record { eq = eq1 } = begin + TN1 h y with h y in eq1 + ... | true = begin Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩ true ∎ where tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ just true @@ -101,7 +103,7 @@ tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩ h1 h y ≡⟨ h-just h y eq1 ⟩ just true ∎ - ... | false | record { eq = eq1 } = begin + ... | false = begin Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩ false ∎ where tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ nothing
--- a/automaton-in-agda/src/induction-ex.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/induction-ex.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,4 +1,5 @@ -{-# OPTIONS --guardedness --sized-types #-} +{-# OPTIONS --cubical-compatible --guardedness --sized-types #-} + module induction-ex where open import Relation.Binary.PropositionalEquality
--- a/automaton-in-agda/src/lang-text.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/lang-text.agda Sun Sep 24 18:02:04 2023 +0900 @@ -3,7 +3,7 @@ open import Data.List open import Data.String open import Data.Char -open import Data.Char.Unsafe +-- open import Data.Char.Unsafe open import Relation.Binary.PropositionalEquality open import Relation.Nullary open import logic @@ -36,19 +36,19 @@ ex15c : Set -- w is any string not in a*b* -ex15c = (w : String ) → ( ¬ (contains w "ab" ≡ true ) /\ ( ¬ (contains w "ba" ≡ true ) +ex15c = (w : String ) → ( ¬ (contains w "ab" ≡ true )) /\ ( ¬ (contains w "ba" ≡ true ) ) -ex15d : {!!} -ex15d = {!!} +ex15d : ? +ex15d = ? -ex15e : {!!} -ex15e = {!!} +ex15e : ? +ex15e = ? -ex15f : {!!} -ex15f = {!!} +ex15f : ? +ex15f = ? -ex15g : {!!} -ex15g = {!!} +ex15g : ? +ex15g = ? -ex15h : {!!} -ex15h = {!!} +ex15h : ? +ex15h = ?
--- a/automaton-in-agda/src/libbijection.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/libbijection.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module libbijection where open import Level renaming ( zero to Zero ; suc to Suc ) @@ -7,7 +9,7 @@ open import Data.Nat.Properties open import Relation.Nullary open import Data.Empty -open import Data.Unit hiding ( _≤_ ) +open import Data.Unit open import Relation.Binary.Core hiding (_⇔_) open import Relation.Binary.Definitions open import Relation.Binary.PropositionalEquality
--- a/automaton-in-agda/src/nfa.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/nfa.agda Sun Sep 24 18:02:04 2023 +0900 @@ -254,9 +254,9 @@ to-list1 : {Q : Set } (qs : Q → Bool ) → (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ qs all ) ≡ true to-list1 qs [] = refl -to-list1 qs (x ∷ all) with qs x | inspect qs x -... | false | record { eq = eq } = to-list1 qs all -... | true | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) ) +to-list1 qs (x ∷ all) with qs x in eq +... | false = to-list1 qs all +... | true = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) ) existsS1-valid : ¬ ( (qs : States1 → Bool ) → ( existsS1 qs ≡ true ) ) existsS1-valid n = ¬-bool refl ( n ( λ x → false ))
--- a/automaton-in-agda/src/non-regular.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module non-regular where open import Data.Nat @@ -66,8 +68,10 @@ t5 : ( n : ℕ ) → Set t5 n = inputnn1 ( inputnn0 n ) ≡ true -cons-inject : {A : Set} {x1 x2 : List A } { a : A } → a ∷ x1 ≡ a ∷ x2 → x1 ≡ x2 -cons-inject refl = refl +import Level + +cons-inject : {n : Level.Level } (A : Set n) { a b : A } {x1 x2 : List A} → a ∷ x1 ≡ b ∷ x2 → x1 ≡ x2 +cons-inject _ refl = refl append-[] : {A : Set} {x1 : List A } → x1 ++ [] ≡ x1 append-[] {A} {[]} = refl @@ -90,23 +94,23 @@ nn01 : (i : ℕ) → inputnn1 ( inputnn0 i ) ≡ true nn01 i = subst₂ (λ j k → inputnn1-i1 j k ≡ true) (sym (nn07 i 0 refl)) (sym (nn09 i)) (nn04 i) where nn07 : (j x : ℕ) → x + j ≡ i → proj1 ( inputnn1-i0 x (input-addi0 j (input-addi1 i))) ≡ x + j - nn07 zero x eq with input-addi1 i | inspect input-addi1 i - ... | [] | _ = +-comm 0 _ - ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where + nn07 zero x eq with input-addi1 i in eq1 + ... | [] = +-comm 0 _ + ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) nn08 zero () nn08 (suc i) () - ... | i1 ∷ t | _ = +-comm 0 _ + ... | i1 ∷ t = +-comm 0 _ nn07 (suc j) x eq = trans (nn07 j (suc x) (trans (cong (λ k → k + j) (+-comm 1 _ )) (trans (+-assoc x _ _) eq)) ) (trans (+-assoc 1 x _) (trans (cong (λ k → k + j) (+-comm 1 _) ) (+-assoc x 1 _) )) nn09 : (x : ℕ) → proj2 ( inputnn1-i0 0 (input-addi0 x (input-addi1 i))) ≡ input-addi1 i - nn09 zero with input-addi1 i | inspect input-addi1 i - ... | [] | _ = refl - ... | i0 ∷ t | record { eq = eq1 } = ⊥-elim ( nn08 i eq1 ) where + nn09 zero with input-addi1 i in eq1 + ... | [] = refl + ... | i0 ∷ t = ⊥-elim ( nn08 i eq1 ) where nn08 : (i : ℕ) → ¬ (input-addi1 i ≡ i0 ∷ t ) nn08 zero () nn08 (suc i) () - ... | i1 ∷ t | _ = refl + ... | i1 ∷ t = refl nn09 (suc j) = trans (nn30 (input-addi0 j (input-addi1 i)) 0) (nn09 j ) nn04 : (i : ℕ) → inputnn1-i1 i (input-addi1 i) ≡ true nn04 zero = refl @@ -267,7 +271,7 @@ nn18 (i0 ∷ t) eq = t nn19 : (a : List In2 ) → (eq : i0 ∷ x₁ ≡ a ++ ( i1 ∷ i0 ∷ i1i0.b li) ) → x₁ ≡ nn18 a eq ++ i1 ∷ i0 ∷ i1i0.b li - nn19 (i0 ∷ a) eq = cons-inject eq + nn19 (i0 ∷ a) eq = cons-inject In2 eq nn17 (i1 ∷ x₁) i eq li = nn20 (i1 ∷ x₁) i eq li where -- second half nn20 : (x : List In2) → (i : ℕ) → inputnn1-i1 i x ≡ true → i1i0 x → ⊥ @@ -281,7 +285,7 @@ nn21 (x ∷ a) (i0 ∷ x₁) (suc i) () eq0 nn21 [] (i1 ∷ i0 ∷ x₁) (suc zero) () eq0 nn21 [] (i1 ∷ i0 ∷ x₁) (suc (suc i)) () eq0 - nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject eq0) + nn21 (i1 ∷ a) (i1 ∷ x₁) (suc i) eq1 eq0 = nn21 a x₁ i eq1 (cons-inject In2 eq0) nn11 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → ¬ ( inputnn1 (x ++ y ++ y ++ z) ≡ true ) nn11 x y z ny xyz xyyz = ⊥-elim ( nn12 (x ++ y ++ y ++ z ) xyyz record { a = x ++ i1i0.a (bb23 bb22 ) ; b = i1i0.b (bb23 bb22) ++ z ; i10 = bb24 } ) where @@ -313,19 +317,20 @@ -- this takes very long time to check and needs 10GB bb22 : count0 y ≡ count1 y 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)) ∎ ))) ⟩ + count0 y ≡⟨ ? ⟩ +-- 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 @@ -366,9 +371,9 @@ (x ++ i1i0.a (bb23 bb22)) ++ i1 ∷ i0 ∷ i1i0.b (bb23 bb22) ++ z ∎ where open ≡-Reasoning nn10 : (x y z : List In2 ) → ¬ y ≡ [] → inputnn1 (x ++ y ++ z) ≡ true → inputnn1 (x ++ y ++ y ++ z) ≡ false - nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) | inspect inputnn1 (x ++ y ++ y ++ z) - ... | true | record { eq = eq1 } = ⊥-elim ( nn11 x y z my eq eq1 ) - ... | false | _ = refl + nn10 x y z my eq with inputnn1 (x ++ y ++ y ++ z) in eq1 + ... | true = ⊥-elim ( nn11 x y z my eq eq1 ) + ... | false = refl
--- a/automaton-in-agda/src/prime.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/prime.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module prime where open import Data.Nat
--- a/automaton-in-agda/src/pumping.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/pumping.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module pumping where open import Data.Nat @@ -115,10 +117,10 @@ open TA tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is - tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q - ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq + tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq + ... | true = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr } - ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) + ... | false = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta ) ; q=qd = tra-08 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where ta : TA1 fa finq (δ fa q i) qd is @@ -126,10 +128,10 @@ tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i) tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta)) - tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) ne (TA1.q=qd ta) + tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) eq (TA1.q=qd ta) tra-phase1 : (q : Q) → (is : List Σ) → (tr : Trace fa is q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true → TA fa q is - tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q - ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) + tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q in eq + ... | true = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta) ; non-nil-y = λ () ; trace-xyz = tnext q (TA1.trace-yz ta) ; trace-xyyz = tnext q tra-05 } where @@ -145,16 +147,16 @@ tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → QDSEQ finq qd z1 {q} {y2} tr → Trace fa (y2 ++ (i ∷ y1) ++ z1) q - tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q - ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz - ... | false | record { eq = ne } = ⊥-elim ( ¬-bool refl x₁ ) - tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q - ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) - ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) + tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q in eq + ... | true = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz + ... | false = ⊥-elim ( ¬-bool refl x₁ ) + tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q in eq + ... | true = ⊥-elim ( ¬-bool x₁ refl ) + ... | false = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i) tra-05 with equal→refl finq eq ... | refl = tra-04 y1 (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta) - ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) + ... | false = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) ; non-nil-y = non-nil-y ta ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where ta : TA fa (δ fa q i ) is
--- a/automaton-in-agda/src/pushdown.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/pushdown.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module pushdown where open import Level renaming ( suc to succ ; zero to Zero )
--- a/automaton-in-agda/src/regex.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/regex.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,4 +1,6 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + +-- {-# OPTIONS --allow-unsolved-metas #-} module regex where open import Level renaming ( suc to succ ; zero to Zero )
--- a/automaton-in-agda/src/regex2.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/regex2.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,4 +1,6 @@ -{-# OPTIONS --allow-unsolved-metas #-} +{-# OPTIONS --cubical-compatible --safe #-} + +-- {-# OPTIONS --allow-unsolved-metas #-} open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no)
--- a/automaton-in-agda/src/regular-language.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/regular-language.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module regular-language where open import Level renaming ( suc to Suc ; zero to Zero ) @@ -31,10 +33,10 @@ Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} Concat {Σ} A B = split A B -{-# TERMINATING #-} -Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ} -Star1 {Σ} A [] = true -Star1 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t) +-- {-# TERMINATING #-} +-- Star1 : {Σ : Set} → ( A : language {Σ} ) → language {Σ} +-- Star1 {Σ} A [] = true +-- Star0 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t) -- Terminating version of Star1 --
--- a/automaton-in-agda/src/root2.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/root2.agda Sun Sep 24 18:02:04 2023 +0900 @@ -1,3 +1,5 @@ +{-# OPTIONS --cubical-compatible --safe #-} + module root2 where open import Data.Nat @@ -86,7 +88,7 @@ df = Dividable.factor dm dn : Dividable p n dn = divdable^2 n p 1<sp n>1 pn record { factor = df * df ; is-factor = begin - df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ {p0} ( begin + df * df * p + 0 ≡⟨ *-cancelʳ-≡ _ _ (suc p0) ( begin (df * df * p + 0) * p ≡⟨ cong (λ k → k * p) (+-comm (df * df * p) 0) ⟩ ((df * df) * p ) * p ≡⟨ cong (λ k → k * p) (*-assoc df df p ) ⟩ (df * (df * p)) * p ≡⟨ cong (λ k → (df * k ) * p) (*-comm df p) ⟩ @@ -196,7 +198,7 @@ Rational.i r * Rational.i r ∎ where open ≡-Reasoning *<-2 : {x y z : ℕ} → z > 0 → x < y → z * x < z * y -*<-2 {x} {y} {suc z} (s≤s z>0) x<y = *-monoʳ-< z x<y +*<-2 {x} {y} {suc z} (s≤s z>0) x<y = ? -- *-monoʳ-< z x<y r15 : {p : ℕ} → p > 1 → p < p * p r15 {p} p>1 = subst (λ k → k < p * p ) m*1=m (*<-2 (<-trans a<sa p>1) p>1 )