Mercurial > hg > Members > kono > Proof > automaton
changeset 138:7a0634a7c25a
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 18 Dec 2019 17:34:15 +0900 |
| parents | 08e2af685c69 |
| children | 3be1afb87f82 |
| files | a02/agda-install.ind a02/agda/dag.agda a02/agda/data1.agda a02/agda/equality.agda a02/agda/lambda.agda a02/agda/level1.agda a02/agda/list.agda a02/agda/record1.agda agda/cfg1.agda agda/derive.agda agda/finiteSet.agda agda/induction-ex.agda agda/induction.agda agda/nat.agda agda/pushdown.agda agda/regex1.agda agda/regular-language.agda |
| diffstat | 17 files changed, 880 insertions(+), 95 deletions(-) [+] |
line wrap: on
line diff
--- a/a02/agda-install.ind Sun Nov 24 19:13:44 2019 +0900 +++ b/a02/agda-install.ind Wed Dec 18 17:34:15 2019 +0900 @@ -45,7 +45,7 @@ Emacs から使うので、Emacs も勉強しよう。 -<a href="http://www.ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a> +<a href="http://ie.u-ryukyu.ac.jp/%7Ekono/howto/mule.html"> Emacs の使い方 </a> C-C control と C を同時に押す M-X esc を押してから X を押す
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/dag.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,75 @@ +module dag where + +-- f0 +-- -----→ +-- t0 t1 +-- -----→ +-- f1 + + +data TwoObject : Set where + t0 : TwoObject + t1 : TwoObject + + +data TwoArrow : TwoObject → TwoObject → Set where + f0 : TwoArrow t0 t1 + f1 : TwoArrow t0 t1 + + +-- r0 +-- -----→ +-- t0 t1 +-- ←----- +-- r1 + +data Circle : TwoObject → TwoObject → Set where + r0 : Circle t0 t1 + r1 : Circle t1 t0 + +data ⊥ : Set where + +⊥-elim : {A : Set } -> ⊥ -> A +⊥-elim () + +¬_ : Set → Set +¬ A = A → ⊥ + +data Bool : Set where + true : Bool + false : Bool + +data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where + direct : E x y -> connected E x y + indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y + +lemma1 : connected TwoArrow t0 t1 +lemma1 = ? + +lemma2 : ¬ ( connected TwoArrow t1 t0 ) +lemma2 x = ? + +-- lemma2 (direct ()) +-- lemma2 (indirect () (direct _)) +-- lemma2 (indirect () (indirect _ _ )) + +lemma3 : connected Circle t0 t0 +lemma3 = indirect r0 ( direct r1 ) + +data Dec (P : Set) : Set where + yes : P → Dec P + no : ¬ P → Dec P + +reachable : { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set +reachable {V} E x y = Dec ( connected {V} E x y ) + +dag : { V : Set } ( E : V -> V -> Set ) -> Set +dag {V} E = ∀ (n : V) → ¬ ( connected E n n ) + +lemma4 : dag TwoArrow +lemma4 x = ? + +lemma5 : ¬ ( dag Circle ) +lemma5 x = ⊥-elim ? + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/data1.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,62 @@ +module data1 where + +data _∨_ (A B : Set) : Set where + p1 : A → A ∨ B + p2 : B → A ∨ B + +ex1 : {A B : Set} → A → ( A ∨ B ) +ex1 = ? + +ex2 : {A B : Set} → B → ( A ∨ B ) +ex2 = ? + +ex3 : {A B : Set} → ( A ∨ A ) → A +ex3 = ? + +ex4 : {A B C : Set} → A ∨ ( B ∨ C ) → ( A ∨ B ) ∨ C +ex4 = ? + +record _∧_ A B : Set where + field + π1 : A + π2 : B + +open _∧_ + +--- ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∨ B ) → C ) is wrong +ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∧ B ) → C ) +ex5 = {!!} + +data Three : Set where + t1 : Three + t2 : Three + t3 : Three + +open Three + +infixl 110 _∨_ + + +data 3Ring : (dom cod : Three) → Set where + r1 : 3Ring t1 t2 + r2 : 3Ring t2 t3 + r3 : 3Ring t3 t1 + +data Nat : Set where + zero : Nat + suc : Nat → Nat + +add : ( a b : Nat ) → Nat +add zero x = x +add (suc x) y = suc ( add x y ) + +mul : ( a b : Nat ) → Nat +mul zero x = {!!} +mul (suc x) y = {!!} + +ex6 : Nat +ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) + + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/equality.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,20 @@ +module equality where + + +data _==_ {A : Set } : A → A → Set where + refl : {x : A} → x == x + +ex1 : {A : Set} {x : A } → x == x +ex1 = {!!} + +ex2 : {A : Set} {x y : A } → x == y → y == x +ex2 = {!!} + +ex3 : {A : Set} {x y z : A } → x == y → y == z → x == z +ex3 = {!!} + +ex4 : {A B : Set} {x y : A } { f : A → B } → x == y → f x == f y +ex4 = {!!} + + +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/lambda.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,56 @@ +module lambda ( T : Set) ( t : T ) where + + +A→A : (A : Set ) → ( A → A ) +A→A = λ A → λ ( a : A ) → a + +lemma2 : (A : Set ) → A → A +lemma2 A a = {!!} + + +ex1 : {A B : Set} → Set +ex1 {A} {B} = ( A → B ) → A → B + +ex1' : {A B : Set} → Set +ex1' {A} {B} = A → B → A → B + +ex2 : {A : Set} → Set +ex2 {A} = A → ( A → A ) + +ex3 : {A B : Set} → Set +ex3 {A}{B} = A → B + +ex4 : {A B : Set} → Set +ex4 {A}{B} = A → B → B + +ex5 : {A B : Set} → Set +ex5 {A}{B} = A → B → A + +proof5 : {A B : Set } → ex5 {A} {B} +proof5 = {!!} + + +postulate S : Set +postulate s : S + +ex6 : {A : Set} → A → S +ex6 a = {!!} + +ex7 : {A : Set} → A → T +ex7 a = {!!} + +ex11 : (A B : Set) → ( A → B ) → A → B +ex11 = {!!} + +ex12 : (A B : Set) → ( A → B ) → A → B +ex12 = {!!} + +ex13 : {A B : Set} → ( A → B ) → A → B +ex13 {A} {B} = {!!} + +ex14 : {A B : Set} → ( A → B ) → A → B +ex14 x = {!!} + +proof5' : {A B : Set} → ex5 {A} {B} +proof5' = {!!} +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/level1.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,22 @@ +module level1 where + +open import Level + +ex1 : { A B : Set} → Set +ex1 {A} {B} = A → B + +ex2 : { A B : Set} → ( A → B ) → Set +ex2 {A} {B} A→B = ex1 {A} {B} + + +-- record FuncBad (A B : Set) : Set where +-- field +-- func : A → B → Set + +record Func {n : Level} (A B : Set n ) : Set (suc n) where + field + func : A → B → Set n + +record Func2 {n : Level} (A B : Set n ) : Set {!!} where + field + func : A → B → Func A B
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/list.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,76 @@ +module list where + +postulate A : Set + +postulate a : A +postulate b : A +postulate c : A + + +infixr 40 _::_ +data List (A : Set ) : Set where + [] : List A + _::_ : A → List A → List A + + +infixl 30 _++_ +_++_ : {A : Set } → List A → List A → List A +[] ++ ys = ys +(x :: xs) ++ ys = x :: (xs ++ ys) + +l1 = a :: [] +l2 = a :: b :: a :: c :: [] + +l3 = l1 ++ l2 + +data Node ( A : Set ) : Set where + leaf : A → Node A + node : Node A → Node A → Node A + +flatten : { A : Set } → Node A → List A +flatten ( leaf a ) = a :: [] +flatten ( node a b ) = flatten a ++ flatten b + +n1 = node ( leaf a ) ( node ( leaf b ) ( leaf c )) + +open import Relation.Binary.PropositionalEquality + +++-assoc : (L : Set ) ( xs ys zs : List L ) → (xs ++ ys) ++ zs ≡ xs ++ (ys ++ zs) +++-assoc A [] ys zs = let open ≡-Reasoning in + begin -- to prove ([] ++ ys) ++ zs ≡ [] ++ (ys ++ zs) + ( [] ++ ys ) ++ zs + ≡⟨ refl ⟩ + ys ++ zs + ≡⟨⟩ + [] ++ ( ys ++ zs ) + ∎ + +++-assoc A (x :: xs) ys zs = let open ≡-Reasoning in + begin -- to prove ((x :: xs) ++ ys) ++ zs == (x :: xs) ++ (ys ++ zs) + ((x :: xs) ++ ys) ++ zs + ≡⟨ refl ⟩ + (x :: (xs ++ ys)) ++ zs + ≡⟨ refl ⟩ + x :: ((xs ++ ys) ++ zs) + ≡⟨ cong (_::_ x) (++-assoc A xs ys zs) ⟩ + x :: (xs ++ (ys ++ zs)) + ≡⟨ refl ⟩ + (x :: xs) ++ (ys ++ zs) + ∎ + +open import Data.Nat + +length : {L : Set} → List L → ℕ +length [] = zero +length (_ :: T ) = suc ( length T ) + +lemma : {L : Set} → (x y : List L ) → ( length x + length y ) ≡ length ( x ++ y ) +lemma [] [] = refl +lemma [] (_ :: _) = refl +lemma (H :: T) L = let open ≡-Reasoning in + begin + ? + ≡⟨ ? ⟩ + ? + ∎ +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/a02/agda/record1.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,27 @@ +module record1 where + +record _∧_ (A B : Set) : Set where + field + π1 : A + π2 : B + +open _∧_ + +ex1 : {A B : Set} → ( A ∧ B ) → A +ex1 a∧b = {!!} + +ex2 : {A B : Set} → ( A ∧ B ) → B +ex2 a∧b = {!!} + +ex3 : {A B : Set} → A → B → ( A ∧ B ) +ex3 a b = {!!} + +ex4 : {A B : Set} → A → ( A ∧ A ) +ex4 a = record { π1 = {!!} ; π2 = {!!} } + +ex5 : {A B C : Set} → ( A ∧ B ) ∧ C → A ∧ (B ∧ C) +ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} } + +ex6 : {A B C : Set} → ( (A → B ) ∧ ( B → C) ) → A → C +ex6 = {!!} +
--- a/agda/cfg1.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/cfg1.agda Wed Dec 18 17:34:15 2019 +0900 @@ -136,3 +136,42 @@ cfgtest8 = cfg-language IFGrammer (IF ∷ EA ∷ THEN ∷ IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] ) cfgtest9 = cfg-language IFGrammer (IF ∷ EB ∷ THEN ∷ SA ∷ ELSE ∷ SB ∷ [] ) +data E1Token : Set where + e1 : E1Token + e[ : E1Token + e] : E1Token + expr : E1Token + term : E1Token + +E1-token-eq? : E1Token → E1Token → Bool +E1-token-eq? e1 e1 = true +E1-token-eq? e[ e] = true +E1-token-eq? e] e] = true +E1-token-eq? expr expr = true +E1-token-eq? term term = true +E1-token-eq? _ _ = false + +typeof-E1 : E1Token → Node E1Token +typeof-E1 expr = N expr +typeof-E1 term = N term +typeof-E1 x = T x + +E1Grammer : CFGGrammer E1Token +E1Grammer = record { + cfg = cfgE + ; top = expr + ; eq? = E1-token-eq? + ; typeof = typeof-E1 + } where + cfgE : E1Token → Body E1Token + cfgE expr = term ． + ； + cfgE term = e1 ． + ｜ e[ ， expr ， e] ． + ； + cfgE x = Error ； + +ecfgtest1 = cfg-language E1Grammer ( e1 ∷ [] ) +ecfgtest2 = cfg-language E1Grammer ( e[ ∷ e1 ∷ e] ∷ [] ) +ecfgtest3 = cfg-language E1Grammer ( e[ ∷ e[ ∷ e1 ∷ e] ∷ e] ∷ [] ) +
--- a/agda/derive.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/derive.agda Wed Dec 18 17:34:15 2019 +0900 @@ -1,54 +1,37 @@ module derive where open import nfa -open import regex1 open import Data.Nat hiding ( _<_ ; _>_ ) open import Data.Fin hiding ( _<_ ) open import Data.List hiding ( [_] ) +open import Data.Maybe open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) open import finiteSet +open import automaton -finIn2 : FiniteSet In2 -finIn2 = record { - Q←F = Q←F' - ; F←Q = F←Q' - ; finiso→ = finiso→' - ; finiso← = finiso←' - } where - Q←F' : Fin 2 → In2 - Q←F' zero = i0 - Q←F' (suc zero) = i1 - Q←F' (suc (suc ())) - F←Q' : In2 → Fin 2 - F←Q' i0 = zero - F←Q' i1 = suc (zero) - finiso→' : (q : In2) → Q←F' (F←Q' q) ≡ q - finiso→' i0 = refl - finiso→' i1 = refl - finiso←' : (f : Fin 2) → F←Q' (Q←F' f) ≡ f - finiso←' zero = refl - finiso←' (suc zero) = refl - finiso←' (suc (suc ())) +data Regex ( Σ : Set ) : Set where + _* : Regex Σ → Regex Σ + _&_ : Regex Σ → Regex Σ → Regex Σ + _||_ : Regex Σ → Regex Σ → Regex Σ + <_> : Σ → Regex Σ + +derivation : { Σ : Set } → Regex Σ → Regex Σ → Bool +derivation = {!!} - -tr1 = < i0 > & < i1 > -tr2 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i1 ∷ [] ) -tr3 = regular-language (< i0 > & < i1 >) finIn2 ( i0 ∷ i0 ∷ [] ) -tr4 = (< i0 > * ) & < i1 > -tr5 = ( ((< i0 > * ) & < i1 > ) || ( < i1 > & ( ( < i1 > * ) || ( < i0 > * )) ) ) * - -sb : { Σ : Set } → Regex Σ → List ( Regex Σ ) -sb (x *) = map (λ r → ( r & (x *) )) ( sb x ) ++ ( sb x ) -sb (x & y) = map (λ r → ( r & y )) ( sb x ) ++ ( sb y ) -sb (x || y) = sb x ++ sb y -sb < x > = < x > ∷ [] - - -nth : { S : Set } → (x : List S ) → Fin ( length x ) → S -nth [] () -nth (s ∷ t) zero = s -nth (_ ∷ t) (suc f) = nth t f +derivation-step : { Σ : Set } → Regex Σ → Σ → Maybe (Regex Σ) +derivation-step {Σ} (r *) s with derivation-step r s +... | just ex = just ( ex & (r *) ) +... | nothing = nothing +derivation-step {Σ} (r & r₁) s with derivation-step r s +... | just ex = just ( ex & r₁ ) +... | nothing = nothing +derivation-step {Σ} (r || r₁) s with derivation-step r s | derivation-step r₁ s +... | just e | just e1 = just ( e || e1 ) +... | nothing | just e1 = just e1 +... | just e | nothing = just e +... | nothing | nothing = nothing +derivation-step {Σ} < x > s = {!!}
--- a/agda/finiteSet.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/finiteSet.agda Wed Dec 18 17:34:15 2019 +0900 @@ -249,6 +249,7 @@ 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 _ ) ISO.iso→ iso-1 x = cong ( λ k → ( k , proj₂ x ) ) (FiniteSet.finiso→ fa _ ) + iso-2 : {a : ℕ } → ISO (B ∨ (Fin a × B)) (Fin (suc a) × B) ISO.A←B iso-2 (zero , b ) = case1 b ISO.A←B iso-2 (suc fst , b ) = case2 ( fst , b ) @@ -258,6 +259,7 @@ ISO.iso← iso-2 (case2 x) = refl ISO.iso→ iso-2 (zero , b ) = refl ISO.iso→ iso-2 (suc a , b ) = refl + fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) × B) {a * b} fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () } fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 @@ -265,7 +267,7 @@ open _∧_ fin-∧ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∧ B) {a * b} -fin-∧ {A} {B} {a} {b} fa fb with FiniteSet→Fin fa +fin-∧ {A} {B} {a} {b} fa fb with FiniteSet→Fin fa -- same thing for our tool ... | a=f = iso-fin (fin-×-f a ) iso-1 where iso-1 : ISO (Fin a ∧ B) ( A ∧ B ) ISO.A←B iso-1 x = record { proj1 = FiniteSet.F←Q fa (proj1 x) ; proj2 = proj2 x} @@ -274,6 +276,7 @@ lemma : record { proj1 = FiniteSet.F←Q fa (FiniteSet.Q←F fa (proj1 x)) ; proj2 = proj2 x} ≡ record {proj1 = proj1 x ; proj2 = proj2 x } lemma = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso← fa _ ) ISO.iso→ iso-1 x = cong ( λ k → record {proj1 = k ; proj2 = proj2 x } ) (FiniteSet.finiso→ fa _ ) + iso-2 : {a : ℕ } → ISO (B ∨ (Fin a ∧ B)) (Fin (suc a) ∧ B) ISO.A←B iso-2 (record { proj1 = zero ; proj2 = b }) = case1 b ISO.A←B iso-2 (record { proj1 = suc fst ; proj2 = b }) = case2 ( record { proj1 = fst ; proj2 = b } ) @@ -283,6 +286,7 @@ ISO.iso← iso-2 (case2 x) = refl ISO.iso→ iso-2 (record { proj1 = zero ; proj2 = b }) = refl ISO.iso→ iso-2 (record { proj1 = suc a ; proj2 = b }) = refl + fin-×-f : ( a : ℕ ) → FiniteSet ((Fin a) ∧ B) {a * b} fin-×-f zero = record { Q←F = λ () ; F←Q = λ () ; finiso→ = λ () ; finiso← = λ () } fin-×-f (suc a) = iso-fin ( fin-∨ fb ( fin-×-f a ) ) iso-2 @@ -405,8 +409,7 @@ l2f : (n : ℕ ) → (n<m : n < suc m ) → (q<n : toℕ (FiniteSet.F←Q fin q ) < n ) → (L2F n<m fin (F2L n<m fin (λ 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 with inspect f q - l2f (suc n) (s≤s n<m) (s≤s n<q) | yes p | record { eq = refl } = begin + 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 ))
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/induction-ex.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,118 @@ +{-# OPTIONS --guardedness #-} +module induction-ex where + +open import Relation.Binary.PropositionalEquality +open import Size +open import Data.Bool + +data List (A : Set ) : Set where + [] : List A + _∷_ : A → List A → List A + +data Nat : Set where + zero : Nat + suc : Nat → Nat + +add : Nat → Nat → Nat +add zero x = x +add (suc x) y = suc ( add x y ) + +_++_ : {A : Set} → List A → List A → List A +[] ++ y = y +(x ∷ t) ++ y = x ∷ ( t ++ y ) + +test1 = (zero ∷ []) ++ (zero ∷ []) + +length : {A : Set } → List A → Nat +length [] = zero +length (_ ∷ t) = suc ( length t ) + +lemma1 : {A : Set} → (x y : List A ) → length ( x ++ y ) ≡ add (length x) (length y) +lemma1 [] y = refl +lemma1 (x ∷ t) y = cong ( λ k → suc k ) lemma2 where + lemma2 : length (t ++ y) ≡ add (length t) (length y) + lemma2 = lemma1 t y + +-- record List1 ( A : Set ) : Set where +-- inductive +-- field +-- nil : List1 A +-- cons : A → List1 A → List1 A +-- +-- record List2 ( A : Set ) : Set where +-- coinductive +-- field +-- nil : List2 A +-- cons : A → List2 A → List2 A + +data SList (i : Size) (A : Set) : Set where + []' : SList i A + _∷'_ : {j : Size< i} (x : A) (xs : SList j A) → SList i A + + +map : ∀{i A B} → (A → B) → SList i A → SList i B +map f []' = []' +map f ( x ∷' xs)= f x ∷' map f xs + +foldr : ∀{i} {A B : Set} → (A → B → B) → B → SList i A → B +foldr c n []' = n +foldr c n (x ∷' xs) = c x (foldr c n xs) + +any : ∀{i A} → (A → Bool) → SList i A → Bool +any p xs = foldr _∨_ false (map p xs) + +-- Sappend : {A : Set } {i j : Size } → SList i A → SList j A → SList {!!} A +-- Sappend []' y = y +-- Sappend (x ∷' x₁) y = _∷'_ {?} x (Sappend x₁ y) + +language : { Σ : Set } → Set +language {Σ} = List Σ → Bool + +record Lang (i : Size) (A : Set) : Set where + coinductive + field + ν : Bool + δ : ∀{j : Size< i} → A → Lang j A + +open Lang + +∅ : ∀ {i A} → Lang i A +ν ∅ = false +δ ∅ _ = ∅ + +∅' : {i : Size } { A : Set } → Lang i A +∅' {i} {A} = record { ν = false ; δ = lemma3 } where + lemma3 : {j : Size< i} → A → Lang j A + lemma3 {j} _ = {!!} + +∅l : {A : Set } → language {A} +∅l _ = false + +ε : ∀ {i A} → Lang i A +ν ε = true +δ ε _ = ∅ + +εl : {A : Set } → language {A} +εl [] = true +εl (_ ∷ _) = false + +_+_ : ∀ {i A} → Lang i A → Lang i A → Lang i A +ν (a + b) = ν a ∨ ν b +δ (a + b) x = δ a x + δ b x + +Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} +Union {Σ} A B x = (A x ) ∨ (B x) + +_·_ : ∀ {i A} → Lang i A → Lang i A → Lang i A +ν (a · b) = ν a ∧ ν b +δ (a · b) x = if (ν a) then ((δ a x · b ) + (δ b x )) else ( δ a x · b ) + +split : {Σ : Set} → (List Σ → Bool) + → ( List Σ → Bool) → List Σ → Bool +split x y [] = x [] ∨ y [] +split x y (h ∷ t) = (x [] ∧ y (h ∷ t)) ∨ + split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t + +Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ} +Concat {Σ} A B = split A B +
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/induction.agda Wed Dec 18 17:34:15 2019 +0900 @@ -0,0 +1,1 @@ +module induction where
--- a/agda/nat.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/nat.agda Wed Dec 18 17:34:15 2019 +0900 @@ -1,56 +1,289 @@ +{-# OPTIONS --allow-unsolved-metas #-} module nat where -open import Data.Nat renaming ( zero to Zero ; suc to Suc ; ℕ to Nat ; _⊔_ to _n⊔_ ) +open import Data.Nat +open import Data.Nat.Properties open import Data.Empty open import Relation.Nullary open import Relation.Binary.PropositionalEquality +open import Relation.Binary.Core open import logic -nat-<> : { x y : Nat } → x < y → y < x → ⊥ +nat-<> : { x y : ℕ } → x < y → y < x → ⊥ nat-<> (s≤s x<y) (s≤s y<x) = nat-<> x<y y<x -nat-≤> : { x y : Nat } → x ≤ y → y < x → ⊥ +nat-≤> : { x y : ℕ } → x ≤ y → y < x → ⊥ nat-≤> (s≤s x<y) (s≤s y<x) = nat-≤> x<y y<x -nat-<≡ : { x : Nat } → x < x → ⊥ +nat-<≡ : { x : ℕ } → x < x → ⊥ nat-<≡ (s≤s lt) = nat-<≡ lt -nat-≡< : { x y : Nat } → x ≡ y → x < y → ⊥ +nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥ nat-≡< refl lt = nat-<≡ lt -¬a≤a : {la : Nat} → Suc la ≤ la → ⊥ +¬a≤a : {la : ℕ} → suc la ≤ la → ⊥ ¬a≤a (s≤s lt) = ¬a≤a lt -a<sa : {la : Nat} → la < Suc la -a<sa {Zero} = s≤s z≤n -a<sa {Suc la} = s≤s a<sa +a<sa : {la : ℕ} → la < suc la +a<sa {zero} = s≤s z≤n +a<sa {suc la} = s≤s a<sa -=→¬< : {x : Nat } → ¬ ( x < x ) -=→¬< {Zero} () -=→¬< {Suc x} (s≤s lt) = =→¬< lt +=→¬< : {x : ℕ } → ¬ ( x < x ) +=→¬< {zero} () +=→¬< {suc x} (s≤s lt) = =→¬< lt ->→¬< : {x y : Nat } → (x < y ) → ¬ ( y < x ) +>→¬< : {x y : ℕ } → (x < y ) → ¬ ( y < x ) >→¬< (s≤s x<y) (s≤s y<x) = >→¬< x<y y<x -<-∨ : { x y : Nat } → x < Suc y → ( (x ≡ y ) ∨ (x < y) ) -<-∨ {Zero} {Zero} (s≤s z≤n) = case1 refl -<-∨ {Zero} {Suc y} (s≤s lt) = case2 (s≤s z≤n) -<-∨ {Suc x} {Zero} (s≤s ()) -<-∨ {Suc x} {Suc y} (s≤s lt) with <-∨ {x} {y} lt -<-∨ {Suc x} {Suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → Suc k ) eq) -<-∨ {Suc x} {Suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) +<-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) ) +<-∨ {zero} {zero} (s≤s z≤n) = case1 refl +<-∨ {zero} {suc y} (s≤s lt) = case2 (s≤s z≤n) +<-∨ {suc x} {zero} (s≤s ()) +<-∨ {suc x} {suc y} (s≤s lt) with <-∨ {x} {y} lt +<-∨ {suc x} {suc y} (s≤s lt) | case1 eq = case1 (cong (λ k → suc k ) eq) +<-∨ {suc x} {suc y} (s≤s lt) | case2 lt1 = case2 (s≤s lt1) -max : (x y : Nat) → Nat -max Zero Zero = Zero -max Zero (Suc x) = (Suc x) -max (Suc x) Zero = (Suc x) -max (Suc x) (Suc y) = Suc ( max x y ) +max : (x y : ℕ) → ℕ +max zero zero = zero +max zero (suc x) = (suc x) +max (suc x) zero = (suc x) +max (suc x) (suc y) = suc ( max x y ) --- _*_ : Nat → Nat → Nat +-- _*_ : ℕ → ℕ → ℕ -- _*_ zero _ = zero -- _*_ (suc n) m = m + ( n * m ) -exp : Nat → Nat → Nat -exp _ Zero = 1 -exp n (Suc m) = n * ( exp n m ) +exp : ℕ → ℕ → ℕ +exp _ zero = 1 +exp n (suc m) = n * ( exp n m ) + +minus : (a b : ℕ ) → ℕ +minus a zero = a +minus zero (suc b) = zero +minus (suc a) (suc b) = minus a b + +_-_ = minus + +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 ) + ++m= : {i j m : ℕ } → i + m ≡ j + m → i ≡ j ++m= {i} {j} {m} eq = m+= ( subst₂ (λ j k → j ≡ k ) (+-comm i _ ) (+-comm j _ ) eq ) + +less-1 : { n m : ℕ } → suc n < m → n < m +less-1 {zero} {suc (suc _)} (s≤s (s≤s z≤n)) = s≤s z≤n +less-1 {suc n} {suc m} (s≤s lt) = s≤s (less-1 {n} {m} lt) + +sa=b→a<b : { n m : ℕ } → suc n ≡ m → n < m +sa=b→a<b {0} {suc zero} refl = s≤s z≤n +sa=b→a<b {suc n} {suc (suc n)} refl = s≤s (sa=b→a<b refl) + +minus+n : {x y : ℕ } → suc x > y → minus x y + y ≡ x +minus+n {x} {zero} _ = trans (sym (+-comm zero _ )) refl +minus+n {zero} {suc y} (s≤s ()) +minus+n {suc x} {suc y} (s≤s lt) = begin + minus (suc x) (suc y) + suc y + ≡⟨ +-comm _ (suc y) ⟩ + suc y + minus x y + ≡⟨ cong ( λ k → suc k ) ( + begin + y + minus x y + ≡⟨ +-comm y _ ⟩ + minus x y + y + ≡⟨ minus+n {x} {y} lt ⟩ + x + ∎ + ) ⟩ + suc x + ∎ where open ≡-Reasoning + + +-- open import Relation.Binary.PropositionalEquality + +-- postulate extensionality : { n : Level} → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) + +-- <-≡-iff : {A B : (a b : ℕ ) → Set } → {a b : ℕ } → (A a b → B a b ) → (B a b → A a b ) → A ≡ B +-- <-≡-iff {A} {B} ab ba = {!!} + + +0<s : {x : ℕ } → zero < suc x +0<s {_} = s≤s z≤n + +<-minus-0 : {x y z : ℕ } → z + x < z + y → x < y +<-minus-0 {x} {suc _} {zero} lt = lt +<-minus-0 {x} {y} {suc z} (s≤s lt) = <-minus-0 {x} {y} {z} lt + +<-minus : {x y z : ℕ } → x + z < y + z → x < y +<-minus {x} {y} {z} lt = <-minus-0 ( subst₂ ( λ j k → j < k ) (+-comm x _) (+-comm y _ ) lt ) + +x≤x+y : {z y : ℕ } → z ≤ z + y +x≤x+y {zero} {y} = z≤n +x≤x+y {suc z} {y} = s≤s (x≤x+y {z} {y}) + +<-plus : {x y z : ℕ } → x < y → x + z < y + z +<-plus {zero} {suc y} {z} (s≤s z≤n) = s≤s (subst (λ k → z ≤ k ) (+-comm z _ ) x≤x+y ) +<-plus {suc x} {suc y} {z} (s≤s lt) = s≤s (<-plus {x} {y} {z} lt) + +<-plus-0 : {x y z : ℕ } → x < y → z + x < z + y +<-plus-0 {x} {y} {z} lt = subst₂ (λ j k → j < k ) (+-comm _ z) (+-comm _ z) ( <-plus {x} {y} {z} lt ) + +≤-plus : {x y z : ℕ } → x ≤ y → x + z ≤ y + z +≤-plus {0} {y} {zero} z≤n = z≤n +≤-plus {0} {y} {suc z} z≤n = subst (λ k → z < k ) (+-comm _ y ) x≤x+y +≤-plus {suc x} {suc y} {z} (s≤s lt) = s≤s ( ≤-plus {x} {y} {z} lt ) + +≤-plus-0 : {x y z : ℕ } → x ≤ y → z + x ≤ z + y +≤-plus-0 {x} {y} {zero} lt = lt +≤-plus-0 {x} {y} {suc z} lt = s≤s ( ≤-plus-0 {x} {y} {z} lt ) + +x+y<z→x<z : {x y z : ℕ } → x + y < z → x < z +x+y<z→x<z {zero} {y} {suc z} (s≤s lt1) = s≤s z≤n +x+y<z→x<z {suc x} {y} {suc z} (s≤s lt1) = s≤s ( x+y<z→x<z {x} {y} {z} lt1 ) + +*≤ : {x y z : ℕ } → x ≤ y → x * z ≤ y * z +*≤ lt = *-mono-≤ lt ≤-refl + +*< : {x y z : ℕ } → x < y → x * suc z < y * suc z +*< {zero} {suc y} lt = s≤s z≤n +*< {suc x} {suc y} (s≤s lt) = <-plus-0 (*< lt) + +<to<s : {x y : ℕ } → x < y → x < suc y +<to<s {zero} {suc y} (s≤s lt) = s≤s z≤n +<to<s {suc x} {suc y} (s≤s lt) = s≤s (<to<s {x} {y} lt) + +<tos<s : {x y : ℕ } → x < y → suc x < suc y +<tos<s {zero} {suc y} (s≤s z≤n) = s≤s (s≤s z≤n) +<tos<s {suc x} {suc y} (s≤s lt) = s≤s (<tos<s {x} {y} lt) + +≤to< : {x y : ℕ } → x < y → x ≤ y +≤to< {zero} {suc y} (s≤s z≤n) = z≤n +≤to< {suc x} {suc y} (s≤s lt) = s≤s (≤to< {x} {y} lt) + +refl-≤s : {x : ℕ } → x ≤ suc x +refl-≤s {zero} = z≤n +refl-≤s {suc x} = s≤s (refl-≤s {x}) + +x<y→≤ : {x y : ℕ } → x < y → x ≤ suc y +x<y→≤ {zero} {.(suc _)} (s≤s z≤n) = z≤n +x<y→≤ {suc x} {suc y} (s≤s lt) = s≤s (x<y→≤ {x} {y} lt) + +open import Data.Product + +minus<=0 : {x y : ℕ } → x ≤ y → minus x y ≡ 0 +minus<=0 {0} {zero} z≤n = refl +minus<=0 {0} {suc y} z≤n = refl +minus<=0 {suc x} {suc y} (s≤s le) = minus<=0 {x} {y} le + +minus>0 : {x y : ℕ } → x < y → 0 < minus y x +minus>0 {zero} {suc _} (s≤s z≤n) = s≤s z≤n +minus>0 {suc x} {suc y} (s≤s lt) = minus>0 {x} {y} lt + +distr-minus-* : {x y z : ℕ } → (minus x y) * z ≡ minus (x * z) (y * z) +distr-minus-* {x} {zero} {z} = refl +distr-minus-* {x} {suc y} {z} with <-cmp x y +distr-minus-* {x} {suc y} {z} | tri< a ¬b ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} (x<y→≤ a)) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} le ) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + le : x * z ≤ z + y * z + le = ≤-trans lemma (subst (λ k → y * z ≤ k ) (+-comm _ z ) (x≤x+y {y * z} {z} ) ) where + lemma : x * z ≤ y * z + lemma = *≤ {x} {y} {z} (≤to< a) +distr-minus-* {x} {suc y} {z} | tri≈ ¬a refl ¬c = begin + minus x (suc y) * z + ≡⟨ cong (λ k → k * z ) (minus<=0 {x} {suc y} refl-≤s ) ⟩ + 0 * z + ≡⟨ sym (minus<=0 {x * z} {z + y * z} (lt {x} {z} )) ⟩ + minus (x * z) (z + y * z) + ∎ where + open ≡-Reasoning + lt : {x z : ℕ } → x * z ≤ z + x * z + lt {zero} {zero} = z≤n + lt {suc x} {zero} = lt {x} {zero} + lt {x} {suc z} = ≤-trans lemma refl-≤s where + lemma : x * suc z ≤ z + x * suc z + lemma = subst (λ k → x * suc z ≤ k ) (+-comm _ z) (x≤x+y {x * suc z} {z}) +distr-minus-* {x} {suc y} {z} | tri> ¬a ¬b c = +m= {_} {_} {suc y * z} ( begin + minus x (suc y) * z + suc y * z + ≡⟨ sym (proj₂ *-distrib-+ z (minus x (suc y) ) _) ⟩ + ( minus x (suc y) + suc y ) * z + ≡⟨ cong (λ k → k * z) (minus+n {x} {suc y} (s≤s c)) ⟩ + x * z + ≡⟨ sym (minus+n {x * z} {suc y * z} (s≤s (lt c))) ⟩ + minus (x * z) (suc y * z) + suc y * z + ∎ ) where + open ≡-Reasoning + lt : {x y z : ℕ } → suc y ≤ x → z + y * z ≤ x * z + lt {x} {y} {z} le = *≤ le + +minus- : {x y z : ℕ } → suc x > z + y → minus (minus x y) z ≡ minus x (y + z) +minus- {x} {y} {z} gt = +m= {_} {_} {z} ( begin + minus (minus x y) z + z + ≡⟨ minus+n {_} {z} lemma ⟩ + minus x y + ≡⟨ +m= {_} {_} {y} ( begin + minus x y + y + ≡⟨ minus+n {_} {y} lemma1 ⟩ + x + ≡⟨ sym ( minus+n {_} {z + y} gt ) ⟩ + minus x (z + y) + (z + y) + ≡⟨ sym ( +-assoc (minus x (z + y)) _ _ ) ⟩ + minus x (z + y) + z + y + ∎ ) ⟩ + minus x (z + y) + z + ≡⟨ cong (λ k → minus x k + z ) (+-comm _ y ) ⟩ + minus x (y + z) + z + ∎ ) where + open ≡-Reasoning + lemma1 : suc x > y + lemma1 = x+y<z→x<z (subst (λ k → k < suc x ) (+-comm z _ ) gt ) + lemma : suc (minus x y) > z + lemma = <-minus {_} {_} {y} ( subst ( λ x → z + y < suc x ) (sym (minus+n {x} {y} lemma1 )) gt ) + +minus-* : {M k n : ℕ } → n < k → minus k (suc n) * M ≡ minus (minus k n * M ) M +minus-* {zero} {k} {n} lt = begin + minus k (suc n) * zero + ≡⟨ *-comm (minus k (suc n)) zero ⟩ + zero * minus k (suc n) + ≡⟨⟩ + 0 * minus k n + ≡⟨ *-comm 0 (minus k n) ⟩ + minus (minus k n * 0 ) 0 + ∎ where + open ≡-Reasoning +minus-* {suc m} {k} {n} lt with <-cmp k 1 +minus-* {suc m} {.0} {zero} lt | tri< (s≤s z≤n) ¬b ¬c = refl +minus-* {suc m} {.0} {suc n} lt | tri< (s≤s z≤n) ¬b ¬c = refl +minus-* {suc zero} {.1} {zero} lt | tri≈ ¬a refl ¬c = refl +minus-* {suc (suc m)} {.1} {zero} lt | tri≈ ¬a refl ¬c = minus-* {suc m} {1} {zero} lt +minus-* {suc m} {.1} {suc n} (s≤s ()) | tri≈ ¬a refl ¬c +minus-* {suc m} {k} {n} lt | tri> ¬a ¬b c = begin + minus k (suc n) * M + ≡⟨ distr-minus-* {k} {suc n} {M} ⟩ + minus (k * M ) ((suc n) * M) + ≡⟨⟩ + minus (k * M ) (M + n * M ) + ≡⟨ cong (λ x → minus (k * M) x) (+-comm M _ ) ⟩ + minus (k * M ) ((n * M) + M ) + ≡⟨ sym ( minus- {k * M} {n * M} (lemma lt) ) ⟩ + minus (minus (k * M ) (n * M)) M + ≡⟨ cong (λ x → minus x M ) ( sym ( distr-minus-* {k} {n} )) ⟩ + minus (minus k n * M ) M + ∎ where + M = suc m + lemma : {n k m : ℕ } → n < k → suc (k * suc m) > suc m + n * suc m + lemma {zero} {suc k} {m} (s≤s lt) = s≤s (s≤s (subst (λ x → x ≤ m + k * suc m) (+-comm 0 _ ) x≤x+y )) + lemma {suc n} {suc k} {m} lt = begin + suc (suc m + suc n * suc m) + ≡⟨⟩ + suc ( suc (suc n) * suc m) + ≤⟨ ≤-plus-0 {_} {_} {1} (*≤ lt ) ⟩ + suc (suc k * suc m) + ∎ where open ≤-Reasoning + open ≡-Reasoning
--- a/agda/pushdown.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/pushdown.agda Wed Dec 18 17:34:15 2019 +0900 @@ -20,7 +20,6 @@ : Set where field pδ : Q → Σ → Γ → Q × ( PushDown Γ ) - pstart : Q pok : Q → Bool pempty : Γ pmoves : Q → List Γ → Σ → ( Q × List Γ ) @@ -31,25 +30,23 @@ pmoves q (H ∷ T) i | qn , pop = ( qn , T ) pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) ) - paccept : List Σ → Bool - paccept L = move pstart L [] - where - move : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool - move q [] [] = pok q - move q ( H ∷ T) [] with pδ q H pempty - move q (H ∷ T) [] | qn , pop = move qn T [] - move q (H ∷ T) [] | qn , push x = move qn T (x ∷ [] ) - move q [] (_ ∷ _ ) = false - move q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH - ... | (nq , pop ) = move nq T ST - ... | (nq , push ns ) = move nq T ( ns ∷ SH ∷ ST ) + paccept : (q : Q ) ( In : List Σ ) ( sp : List Γ ) → Bool + paccept q [] [] = pok q + paccept q ( H ∷ T) [] with pδ q H pempty + paccept q (H ∷ T) [] | qn , pop = paccept qn T [] + paccept q (H ∷ T) [] | qn , push x = paccept qn T (x ∷ [] ) + paccept q [] (_ ∷ _ ) = false + paccept q ( H ∷ T ) ( SH ∷ ST ) with pδ q H SH + ... | (nq , pop ) = paccept nq T ST + ... | (nq , push ns ) = paccept nq T ( ns ∷ SH ∷ ST ) -- 0011 -- 00000111111 -inputnn : { n : ℕ } → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ -inputnn {zero} {_} _ _ s = s -inputnn {suc n} x y s = x ∷ ( inputnn {n} x y ( y ∷ s ) ) +inputnn : ( n : ℕ ) → { Σ : Set } → ( x y : Σ ) → List Σ → List Σ +inputnn zero {_} _ _ s = s +inputnn (suc n) x y s = x ∷ ( inputnn n x y ( y ∷ s ) ) + data States0 : Set where sr : States0 @@ -57,11 +54,12 @@ data In2 : Set where i0 : In2 i1 : In2 + +test0 = inputnn 5 i0 i1 [] pnn : PushDownAutomaton States0 In2 States0 pnn = record { pδ = pδ - ; pstart = sr ; pempty = sr ; pok = λ q → true } where @@ -69,7 +67,29 @@ pδ sr i0 _ = (sr , push sr) pδ sr i1 _ = (sr , pop ) -test1 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) -test2 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) +data States1 : Set where + ss : States1 + st : States1 + +pn1 : PushDownAutomaton States1 In2 States1 +pn1 = record { + pδ = pδ + ; pempty = ss + ; pok = pok1 + } where + pok1 : States1 → Bool + pok1 ss = false + pok1 st = true + pδ : States1 → In2 → States1 → States1 × PushDown States1 + pδ ss i0 _ = (ss , push ss) + pδ ss i1 _ = (st , pop) + pδ st i0 _ = (st , push ss) + pδ st i1 _ = (st , pop ) + +test1 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) [] +test2 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] ) [] test3 = PushDownAutomaton.pmoves pnn sr [] i0 +test4 = PushDownAutomaton.paccept pnn sr ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) [] +test5 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] ) [] +test6 = PushDownAutomaton.paccept pn1 ss ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) []
--- a/agda/regex1.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/regex1.agda Wed Dec 18 17:34:15 2019 +0900 @@ -49,6 +49,36 @@ repeat {Σ} x ( h ∷ t ) = split x (repeat {Σ} x) ( h ∷ t ) open import finiteSet + +fin : FiniteSet hoge +fin = record { + Q←F = Q←F + ; F←Q = F←Q + ; finiso→ = finiso→ + ; finiso← = finiso← + } where + Q←F : Fin 4 → hoge + Q←F zero = a + Q←F (suc zero) = b + Q←F (suc (suc zero)) = c + Q←F (suc (suc (suc zero))) = d + F←Q : hoge → Fin 4 + F←Q a = zero + F←Q b = suc zero + F←Q c = suc (suc zero) + F←Q d = suc (suc (suc zero)) + finiso→ : (q : hoge) → Q←F (F←Q q) ≡ q + finiso→ a = refl + finiso→ b = refl + finiso→ c = refl + finiso→ d = refl + finiso← : (f : Fin 4) → F←Q (Q←F f) ≡ f + finiso← zero = refl + finiso← (suc zero) = refl + finiso← (suc (suc zero)) = refl + finiso← (suc (suc (suc zero))) = refl + finiso← (suc (suc (suc (suc ())))) + open FiniteSet cmpi : {Σ : Set} → {n : ℕ } (fin : FiniteSet Σ {n}) → (x y : Σ ) → Dec (F←Q fin x ≡ F←Q fin y) @@ -64,3 +94,22 @@ ... | no _ = false regular-language < h > f _ = false +1r1' = (< a > & < b >) & < c > +1r1 = < a > & < b > & < c > +1any = < a > || < b > || < c > || < d > +1r2 = ( any * ) & ( < a > & < b > & < c > ) +1r3 = ( any * ) & ( < a > & < b > & < c > & < a > & < b > & < c > ) +1r4 = ( < a > & < b > & < c > ) || ( < b > & < c > & < d > ) +1r5 = ( any * ) & ( < a > & < b > & < c > || < b > & < c > & < d > ) + +test-regex : regular-language 1r1' fin ( a ∷ [] ) ≡ false +test-regex = refl + +test-regex1 : regular-language 1r1' fin ( a ∷ b ∷ c ∷ [] ) ≡ true +test-regex1 = refl + + +open import Data.Nat.DivMod + +test-regex-even : Set +test-regex-even = (s : List hoge ) → regular-language ( ( 1any || 1any ) * ) fin s ≡ true → (length s) mod 2 ≡ zero
--- a/agda/regular-language.agda Sun Nov 24 19:13:44 2019 +0900 +++ b/agda/regular-language.agda Wed Dec 18 17:34:15 2019 +0900 @@ -280,13 +280,14 @@ contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true ) → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x ) → split (accept (automaton A) qa ) (contain B) x ≡ true - contain-A [] nq fn qa cond with found← finab fn + contain-A [] nq fn qa cond with found← finab fn -- at this stage, A and B must be satisfied with [] (ab-case cond forces it) ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S) ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S))) contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true - ... | yes eq = bool-or-41 eq - ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where + ... | yes eq = bool-or-41 eq -- found A ++ B all end + ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion + --- prove ab-ase condition (we haven't checked but case2 b may happen) lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t lemma11 (case1 qa') ex with found← finab ex ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))