Mercurial > hg > Members > kono > Proof > automaton
changeset 266:e5cf49902db3
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 17 Nov 2021 16:12:30 +0900 |
| parents | c47634c830f3 |
| children | ae70f96cb60c |
| files | a01/lecture.ind a02/agda/data1.agda a02/agda/lambda.agda a02/agda/level1.agda a02/agda/list.agda a02/agda/record1.agda a02/lecture.ind automaton-in-agda/src/automaton-ex.agda automaton-in-agda/src/bijection.agda automaton-in-agda/src/flcagl.agda automaton-in-agda/src/logic.agda automaton-in-agda/src/nat.agda automaton-in-agda/src/regular-language.agda index.ind |
| diffstat | 14 files changed, 394 insertions(+), 424 deletions(-) [+] |
line wrap: on
line diff
--- a/a01/lecture.ind Thu Jul 08 08:41:05 2021 +0900 +++ b/a01/lecture.ind Wed Nov 17 16:12:30 2021 +0900 @@ -74,6 +74,10 @@ SMVなどのモデル検査系を使えるようにする。 +--問題1.1 論文管理と論文検索 + + +<a href="../exercise/006.html"> 論文管理 Zotero </a> <!--- Exercise 1.1 --->
--- a/a02/agda/data1.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/a02/agda/data1.agda Wed Nov 17 16:12:30 2021 +0900 @@ -1,32 +1,77 @@ module data1 where data _∨_ (A B : Set) : Set where - p1 : A → A ∨ B - p2 : B → A ∨ B + case1 : A → A ∨ B + case2 : B → A ∨ B ex1 : {A B : Set} → A → ( A ∨ B ) -ex1 = {!!} +ex1 a = case1 a ex2 : {A B : Set} → B → ( A ∨ B ) -ex2 = {!!} +ex2 = λ b → case2 b ex3 : {A B : Set} → ( A ∨ A ) → A -ex3 = {!!} +ex3 (case1 x) = x +ex3 (case2 x) = x ex4 : {A B C : Set} → A ∨ ( B ∨ C ) → ( A ∨ B ) ∨ C ex4 = {!!} record _∧_ A B : Set where field - π1 : A - π2 : B + proj1 : A + proj2 : B open _∧_ +ex3' : {A B : Set} → ( A ∨ B ) → A ∧ B -- this is wrong +ex3' = {!!} + +ex4' : {A B : Set} → ( A ∧ B ) → A ∨ B +ex4' = {!!} + --- 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 ⊥ : Set where + +⊥-elim : {A : Set } -> ⊥ -> A +⊥-elim = {!!} + +¬_ : Set → Set +¬ A = A → ⊥ + + +record PetResearch ( Cat Dog Goat Rabbit : Set ) : Set where + field + fact1 : ( Cat ∨ Dog ) → ¬ Goat + fact2 : ¬ Cat → ( Dog ∨ Rabbit ) + fact3 : ¬ ( Cat ∨ Goat ) → Rabbit + +postulate + lem : (a : Set) → a ∨ ( ¬ a ) + +module tmp ( Cat Dog Goat Rabbit : Set ) (p : PetResearch Cat Dog Goat Rabbit ) where + + open PetResearch + + problem0 : Cat ∨ Dog ∨ Goat ∨ Rabbit + problem0 with lem Cat | lem Goat + ... | case1 cat | y = case1 (case1 {!!}) + ... | case2 x | case1 goat = case1 {!!} + ... | case2 ¬cat | case2 ¬goat = case2 (fact3 p lemma1 ) where + lemma1 : ¬ (Cat ∨ Goat) + lemma1 (case1 cat) = ¬cat cat + lemma1 (case2 goat) = {!!} + + problem1 : Goat → ¬ Dog + problem1 = {!!} + + problem2 : Goat → Rabbit + problem2 = {!!} + + data Three : Set where t1 : Three t2 : Three @@ -58,14 +103,6 @@ ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) -data ⊥ : Set where - -⊥-elim : {A : Set } -> ⊥ -> A -⊥-elim () - -¬_ : Set → Set -¬ A = A → ⊥ - data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where direct : E x y -> connected E x y
--- a/a02/agda/lambda.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/a02/agda/lambda.agda Wed Nov 17 16:12:30 2021 +0900 @@ -1,35 +1,67 @@ -module lambda ( T : Set) ( t : T ) where - +module lambda ( A B : Set) (a : A ) (b : B ) where -A→A : (A : Set ) → ( A → A ) -A→A = λ A → λ ( a : A ) → a +-- λ-intro +-- +-- A +-- -------- id +-- A +-- -------- λ-intro ( = λ ( x : A ) → x ) +-- A → A + +A→A : A → A +A→A = λ ( x : A ) → x + +A→A'' : A → A +A→A'' = λ x → x -lemma2 : (A : Set ) → A → A -lemma2 A a = {!!} +A→A' : A → A +A→A' x = x + +lemma2 : (A : Set ) → A → A -- これは A → ( A → A ) とは違う +lemma2 = {!!} + +λ-intro : {A B : Set } → A → B → ( A → B ) -- {} implicit variable +λ-intro _ b = λ _ → b -- _ anonymous variable -→intro : {A B : Set } → A → B → ( A → B ) -→intro _ b = λ x → b +-- λ-intro {A} {B} a b = λ a → b -→elim : {A B : Set } → A → ( A → B ) → B +-- λ-elim +-- +-- A A → B +-- ----------------- λ-elim +-- B + +→elim : A → ( A → B ) → B →elim a f = f 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 +ex1 {A} {B} = {!!} -- ( A → B ) → A → B ex2 : {A : Set} → Set ex2 {A} = A → ( A → A ) proof2 : {A : Set } → ex2 {A} -proof2 = {!!} +proof2 {A} = {!!} where + p1 : {!!} --- ex2 {A} を C-C C-N する + p1 = {!!} -ex3 : {A B : Set} → A → B +ex3 : A → B -- インチキの例 ex3 a = {!!} -ex4 : {A B : Set} → A → B → B -ex4 {A}{B} a b = {!!} +ex4 : {A B : Set} → A → (B → B) -- 仮定を無視してる +ex4 {A}{B} a b = b + +--- [A]₁ not used --- a +--- ──────────────────── +--- [B]₂ --- b +--- ──────────────────── (₂) +--- B → B +--- ──────────────────── (₁) λ-intro +--- A → (B → B) + + +ex4' : A → (B → B) -- インチキできる / 仮定を使える +ex4' = {!!} ex5 : {A B : Set} → A → B → A ex5 = {!!} @@ -37,18 +69,33 @@ postulate - Domain : Set - Range : Set + Domain : Set -- Range Domain : Set + Range : Set -- codomain Domain → Range, coRange ← coDomain r : Range ex6 : Domain → Range ex6 a = {!!} -ex7 : {A : Set} → A → T -ex7 a = {!!} -ex11 : (A B : Set) → ( A → B ) → A → B -ex11 = {!!} +--- A → B +-- : +--- A → B +--- ─────────────────────────── +--- ( A → B ) → A → B +--- +--- [A]₁ [A → B ]₂ +--- ─────────────────────────── λ-elim +--- B +--- ─────────────────────────── ₁ +--- A → B +--- ─────────────────────────── ₂ +--- ( A → B ) → A → B + +-- +-- 上の二つの図式に対応する二つの証明に対応するラムダ項がある +-- +ex11 : ( A → B ) → A → B +ex11 = {!!} ex12 : (A B : Set) → ( A → B ) → A → B ex12 = {!!}
--- a/a02/agda/level1.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/a02/agda/level1.agda Wed Nov 17 16:12:30 2021 +0900 @@ -8,6 +8,9 @@ ex2 : { A B : Set} → ( A → B ) → Set ex2 {A} {B} A→B = ex1 {A} {B} +ex7 : {A B : Set} → Set _ +ex7 {A} {B} = lemma2 ( A → B ) _ -- → A → B + -- record FuncBad (A B : Set) : Set where -- field
--- a/a02/agda/list.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/a02/agda/list.agda Wed Nov 17 16:12:30 2021 +0900 @@ -10,16 +10,21 @@ infixr 40 _::_ data List (A : Set ) : Set where [] : List A - _::_ : A → List A → List A + _::_ : A → List A → List A +-- +-- A List A +-- -------------- [] ---------------- _::_ +-- List A List A +-- infixl 30 _++_ _++_ : {A : Set } → List A → List A → List A -[] ++ ys = ys -(x :: xs) ++ ys = x :: (xs ++ ys) +[] ++ y = y +(x :: x₁) ++ y = x :: (x₁ ++ y ) l1 = a :: [] -l2 = a :: b :: a :: c :: [] +l2 = a :: b :: a :: c :: [] l3 = l1 ++ l2 @@ -58,9 +63,55 @@ (x :: xs) ++ (ys ++ zs) ∎ -open import Data.Nat +-- open import Data.Nat + +data Nat : Set where + zero : Nat + suc : Nat → Nat + +_+_ : Nat → Nat → Nat +zero + y = y +suc x + y = suc (x + y) + +sym1 : {A : Set} → {a b : A} → a ≡ b → b ≡ a +sym1 {_} {a} {.a} refl = refl + +trans1 : {A : Set} → {a b c : A} → a ≡ b → b ≡ c → a ≡ c +trans1 {_} {a} {b} {.a} refl refl = refl + +cong1 : {A B : Set} → {a b : A} → (f : A → B) → a ≡ b → f a ≡ f b +cong1 f refl = refl + +induction : (P : (x : Nat) → Set) → (initial : P zero ) → (induction-setp : ((x : Nat) → P x → P (suc x))) → (x : Nat) → P x +induction P initial induction-setp zero = initial +induction P initial induction-setp (suc x) = induction-setp x ( induction P initial induction-setp x) -length : {L : Set} → List L → ℕ +induction' : (P : (x : Nat) → Set) → (initial : P zero ) → (induction-setp : ((x : Nat) → P x → P (suc x))) → (x : Nat) → P x +induction' P initial induction-setp x = {!!} where + ind1 : {!!} → P x + ind1 = {!!} + ++-comm : {x y : Nat} → x + y ≡ y + x ++-comm {zero} {y} = sym1 lemma01 where + lemma01 : {y : Nat} → y + zero ≡ y + lemma01 {zero} = refl -- (zero + zero ) → zero → zero + zero ≡ zero + lemma01 {suc y} = cong1 (λ x → suc x) (lemma01 {y}) --- (suc y + zero) ≡ suc y + -- suc (y + zero) ≡ suc y ← y + zero ≡ y ++-comm {suc x} {y} = {!!} + +_*_ : Nat → Nat → Nat +zero * y = zero +suc x * y = y + (x * y) + +-- +-- * * * * * +-- * * * ≡ * * +-- * * + +*-comm : {x y : Nat} → x * y ≡ y * x +*-comm = {!!} + +length : {L : Set} → List L → Nat length [] = zero length (_ :: T ) = suc ( length T ) @@ -69,8 +120,8 @@ lemma [] (_ :: _) = refl lemma (H :: T) L = let open ≡-Reasoning in begin - ? - ≡⟨ ? ⟩ - ? + {!!} + ≡⟨ {!!} ⟩ + {!!} ∎
--- a/a02/agda/record1.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/a02/agda/record1.agda Wed Nov 17 16:12:30 2021 +0900 @@ -5,10 +5,19 @@ π1 : A π2 : B +ex0 : {A B : Set} → A ∧ B → A +ex0 = _∧_.π1 + +ex1 : {A B : Set} → ( A ∧ B ) → A +ex1 a∧b = _∧_.π1 a∧b + open _∧_ -ex1 : {A B : Set} → ( A ∧ B ) → A -ex1 a∧b = {!!} +ex0' : {A B : Set} → A ∧ B → A +ex0' = π1 + +ex1' : {A B : Set} → ( A ∧ B ) → A +ex1' a∧b = π1 a∧b ex2 : {A B : Set} → ( A ∧ B ) → B ex2 a∧b = {!!} @@ -22,6 +31,22 @@ ex5 : {A B C : Set} → ( A ∧ B ) ∧ C → A ∧ (B ∧ C) ex5 a∧b∧c = record { π1 = {!!} ; π2 = {!!} } +-- +-- [(A → B ) ∧ ( B → C) ]₁ +-- ──────────────────────────────────── π1 +-- [(A → B ) ∧ ( B → C) ]₁ (A → B ) [A]₂ +-- ──────────────────────────── π2 ─────────────────────── λ-elim +-- ( B → C) B +-- ─────────────────────────────────────────── λ-elim +-- C +-- ─────────────────────────────────────────── λ-intro₂ +-- A → C +-- ─────────────────────────────────────────── λ-intro₁ +-- ( (A → B ) ∧ ( B → C) ) → A → C + ex6 : {A B C : Set} → ( (A → B ) ∧ ( B → C) ) → A → C -ex6 = {!!} +ex6 x a = {!!} +ex6' : {A B C : Set} → (A → B ) → ( B → C) → A → C +ex6' = {!!} +
--- a/a02/lecture.ind Thu Jul 08 08:41:05 2021 +0900 +++ b/a02/lecture.ind Wed Nov 17 16:12:30 2021 +0900 @@ -70,7 +70,7 @@ --関数適用による証明 -導入 除去 + 導入 除去 A : @@ -117,6 +117,20 @@ <a href="agda.html"> agda の細かい構文の話 </a> +Unicode入力 + +<a href="https://agda.readthedocs.io/en/v2.6.0.1/tools/emacs-mode.html"> Unicode入力 </a> + +--重要 + + 空白が入らないものは一単語になる (A→A は一単語、A → A とは別) + + A:Set は間違いで、A : Set + + A → B → C は、 A → ( B → C ) のこと + + f x y は (f x) y のこと + ---問題2.1 Agdaによる関数と証明 @@ -128,7 +142,7 @@ --record または ∧ -導入 除去 + 導入 除去 A B A ∧ B A ∧ B ------------- ----------- π1 ---------- π2 @@ -268,343 +282,10 @@ 最低限5題をまとめてレポートで提出せよ -<a href="agda/practice-logic.agda"> practice-logic</a> <!--- Exercise 2.2 ---> - - - ---data または 排他的論理和(Sum) - -ここで扱っている論理(直観主義論理)では∧に対称的な形で∨を定義することはしない。導入は対称的になるが除去はおかしくなってしまう。 -そこで次のように定義することになっている。 - -除去 導入 - A B - : : - A ∨ B C C A B - ------------------------ ----------- case1 ---------- case2 - C A ∨ B A ∨ B - - - data _∨_ (A B : Set) : Set where - case1 : A → A ∨ B - case2 : B → A ∨ B - -dataはCで言えばcase文とunion に相当する。Scala のCase Classもこれである。Cと違いunionにはどの型が入っているかを区別するtagが付いている。 - -case1 と case2 は A ∨ B を構成する constructor (推論ではintroduction)であり、case 文が eliminator に相当する。 - -Haskellと同様にp1/p2はパターンマッチで場合分けする。 - - ex3 : {A B : Set} → ( A ∨ A ) → A - ex3 = ? - -場合分けには、? の部分にcursolを合わせて C-C C-C すると場合分けを生成してくれる。 - - ex3 : {A B : Set} → ( A ∨ A ) → A - ex3 (case1 x) = ? - ex3 (case2 x) = ? - - ----問題2.3 Agdaのdata - - -<a href="agda/data1.agda"> data </a> <!--- Exercise 2.3 ---> - ---有限な集合と Nat - -data は有限な要素を持つ集合を構成できる。 - - data Three : Set where - t1 : Three - t2 : Three - t3 : Three - - open Three - - data 3Ring : (dom cod : Three) → Set where - r1 : 3Ring t1 t2 - r2 : 3Ring t2 t3 - r3 : 3Ring t3 t1 - -これは、三つのVertexとEdgeを持つグラフをdataで表してみたものである。 - -任意の個数を表すためには自然数(Natural Number)を作る必要がある。ペアノの公理が有名だが、dataを使って以下のように構成する。 - - 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 = ? - ---問題2.4 Nat - -? を埋めて掛け算を完成させよう。 - -<a href="agda/practice-nat.agda"> data </a> <!--- Exercise 2.4 ---> +<a href="agda/record1.agda"> record1</a> <!--- Exercise 2.2 ---> ---Equality - -自然数を導入したので方程式を記述したい。そのためには等式を導入する必要がある。導入は - - --------------- - x == x - -だが、ここには隠れた仮定がある。x は何かの集合の要素なはず。 - - { x : A } - --------------- - x == x - -さらに左辺と右辺は等しいが、 - - add zero zero == zero - -では左辺と右辺は項として同じではない。計算して同じということにして欲しい。つまり、 - - Agdaの項には計算していくと決まった形に落ちる - -という性質があって欲しい。この計算はλ項に対して定義する必要がある。この計算をreduction(縮約)、 -決まった形をnormal form(正規形)と言う。 - -<a href="reduction.html">Reduction</a> - -Agda での定義は以下のようになる。 - - data _==_ {A : Set } : A → A → Set where - refl : {x : A} → x == x - -refl は reflection (反映) の略である。refl は 等式のconstructorになる。 - -Elmination は変数の置き換えになる。 - - x == y f x y - ------------------------ - f x x +--Sum type -x == y は入力の型であり、refl とうパターンでしか受けられない。この時に、x と y が等しい必要がある。 - -しかし、x と y は項なので変数を含むことがある。Agda に等しいことを確信させる必要がある。 -この問題はパターンマッチの時にもすででていた。これは項(正規化された)を再帰的に比較していく -手順が必要になる。これは単一化(Unification)と呼ばれる。 - -<a href="unification.html">Unification</a> - - 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 = ? - ---問題 2.4 - -以上の証明を refl を使って完成させてみよう。 - -<a href="agda/equality.agda"> equality </a> <!--- Exercise 2.4 ---> - ---問題 2.5 - -<a href="agda/practice-nat.agda"> nat の例題 </a> <!--- Exercise 2.5 ---> - ---集合のLevel - -論理式は型であり、それは基本的はSetになっている。例えば、A → B は Set である。 - - ex1 : { A B : Set} → Set - ex1 {A} {B} = A → B - -Agda は高階論理なので、論理式自体を返す論理式も作ることができる。 - - ex2 : { A B : Set} → ( A → B ) → Set - ex2 {A} {B} A→B = ex1 {A} {B} +<a href="sumtype.html"> Sum type 排他的論理和</a> -では、これを論理式を要素として持つ直積を作ってみよう。 - - record FuncBad (A B : Set) : Set where - field - func : A → B → Set - -Agda は以下のように文句をいう。 - - The type of the constructor does not fit in the sort of the - datatype, since Set₁ is not less or equal than Set - when checking the definition of FuncBad - -自己参照的な集合の定義を避けるために集合には階(level)という概念が導入されている。 - - open import Level - record Func {n : Level} (A B : Set n ) : Set (suc n) where - field - func : A → B → Set n - -のように集合の階(Level)を明示する必要がある。 - ---問題1.5 集合のLevel - -level が合うように ? を埋めよ。 - -<a href="agda/level1.agda"> level </a> <!--- Exercise 2.5 ---> - ---List - -List は cons か nil かどちらかの構造で、cons は List を再帰的に含んでいる。 - - 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 - -等式の変形を利用して、List の結合法則を証明してみよう。 - - 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 ? - -≡⟨⟩ などの定義はどこにあるのか? - ---問題2.6 List - -lemma を等式の変形を利用して証明してみよ。 - -<a href="agda/list.agda"> List </a> <!--- Exercise 2.6 ---> - ---DAGと否定 - -グラフには接続されてない二点が存在する。それを表現するために否定¬と矛盾⊥を導入する。 - - ⊥ - ------------- ⊥-elim - A - -矛盾からは何でも導くことができる。この場合、A はSetである。⊥ を導入する推論規則はない。 - -これは、contructor のない data で表すことができる。 - - data ⊥ : Set where - -⊥-elim は以下のように証明できる。 - - ⊥-elim : {A : Set } -> ⊥ -> A - ⊥-elim () - -() は「何にもmatchしないパターン」である。これは型を指定した時に「可能な入力がない」必要がある。つまり、このケースは起こり得ない -ことを Agda が納得する必要がある。納得できないと error message がでる。 - - λ () - -という構文も存在する。 - -⊥ を使って否定は以下のように定義される。 - - ¬_ : Set → Set - ¬ A = A → ⊥ - -否定には入力があることを意識しておこう。 - - 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 - -矢印をたどって繋がっている点は接続(connected)されていると言う。 - - 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 - -直接繋がっているか、間接的に繋がっているかどちからになる。この構造は自然数に似ている。 - -t0 と t1 が TwoArrow の場合に繋がっていることを証明してみる。 - - lemma1 : connected TwoArrow t0 t1 - lemma1 = ? - -t1 から t0 にはいけない。 - - lemma2 : ¬ ( connected TwoArrow t1 t0 ) - lemma2 = ? - -dag (Directed Acyclic Graph) は、すべての点(Vertex)で自分自身につながる経路(Edge)がないグラフ - - dag : { V : Set } ( E : V -> V -> Set ) -> Set - dag {V} E = ∀ (n : V) → ¬ ( connected E n n ) - ---問題2.7 DAGと否定 - -TwoArrow が dag で、Circle が dag ではないことを証明してみよう。 - - lemma4 : dag TwoArrow - lemma4 = ? - - lemma5 : ¬ ( dag Circle ) - lemma5 = ? - -<a href="agda/dag.agda"> DAG </a> <!--- Exercise 2.7 ---> - ---教科書の第一章 - -<a href="../agda/chap0.agda"> chapter 0 </a> -
--- a/automaton-in-agda/src/automaton-ex.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/automaton-ex.agda Wed Nov 17 16:12:30 2021 +0900 @@ -4,6 +4,7 @@ open import Data.List open import Data.Maybe open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Binary.Definitions open import Relation.Nullary using (¬_; Dec; yes; no) open import logic @@ -18,7 +19,8 @@ data In2 : Set where i0 : In2 i1 : In2 -transitionQ : StatesQ → In2 → StatesQ + +transitionQ : StatesQ → In2 → StatesQ transitionQ q1 i0 = q1 transitionQ q1 i1 = q2 transitionQ q2 i0 = q3 @@ -39,6 +41,7 @@ test1 : accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ false test1 = refl test2 = accept a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) +test3 = trace a1 q1 ( i0 ∷ i1 ∷ i0 ∷ i1 ∷ [] ) data States1 : Set where sr : States1 @@ -68,9 +71,70 @@ example1-3 = reachable am1 sr st ( i1 ∷ i1 ∷ i1 ∷ [] ) +-- data Dec' (A : Set) : Set where +-- yes' : A → Dec' A +-- no' : ¬ A → Dec' A +-- +-- ieq' : (i i' : In2 ) → Dec' ( i ≡ i' ) +-- ieq' i0 i0 = yes' refl +-- ieq' i1 i1 = yes' refl +-- ieq' i0 i1 = no' ( λ () ) +-- ieq' i1 i0 = no' ( λ () ) + ieq : (i i' : In2 ) → Dec ( i ≡ i' ) ieq i0 i0 = yes refl ieq i1 i1 = yes refl ieq i0 i1 = no ( λ () ) ieq i1 i0 = no ( λ () ) +-- p.83 problem 1.4 +-- +-- w has at least three i0's and at least two i1's + +count-chars : List In2 → In2 → ℕ +count-chars [] _ = 0 +count-chars (h ∷ t) x with ieq h x +... | yes y = suc ( count-chars t x ) +... | no n = count-chars t x + +test11 : count-chars ( i1 ∷ i1 ∷ i0 ∷ [] ) i0 ≡ 1 +test11 = refl + +ex1_4a : (x : List In2) → Bool +ex1_4a x = ( count-chars x i0 ≥b 3 ) /\ ( count-chars x i1 ≥b 2 ) + +language' : { Σ : Set } → Set +language' {Σ} = List Σ → Bool + +lang14a : language' {In2} +lang14a = ex1_4a + +open _∧_ + +am14a-tr : ℕ ∧ ℕ → In2 → ℕ ∧ ℕ +am14a-tr p i0 = record { proj1 = suc (proj1 p) ; proj2 = proj2 p } +am14a-tr p i1 = record { proj1 = proj1 p ; proj2 = suc (proj2 p) } + +am14a : Automaton (ℕ ∧ ℕ) In2 +am14a = record { δ = am14a-tr ; aend = λ x → ( proj1 x ≥b 3 ) /\ ( proj2 x ≥b 2 )} + +data am14s : Set where + a00 : am14s + a10 : am14s + a20 : am14s + a30 : am14s + a01 : am14s + a11 : am14s + a21 : am14s + a31 : am14s + a02 : am14s + a12 : am14s + a22 : am14s + a32 : am14s + +am14a-tr' : am14s → In2 → am14s +am14a-tr' a00 i0 = a10 +am14a-tr' _ _ = a10 + +am14a' : Automaton am14s In2 +am14a' = record { δ = am14a-tr' ; aend = λ x → {!!} }
--- a/automaton-in-agda/src/bijection.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/bijection.agda Wed Nov 17 16:12:30 2021 +0900 @@ -98,13 +98,10 @@ open _∧_ -record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) (n→nxn : ℕ → ℕ ∧ ℕ) : Set where +record NN ( i : ℕ) (nxn→n : ℕ → ℕ → ℕ) : Set where field - j k sum stage : ℕ - nn : j + k ≡ sum - ni : i ≡ j + stage -- not used + j k : ℕ k1 : nxn→n j k ≡ i - k0 : n→nxn i ≡ ⟪ j , k ⟫ nn-unique : {j0 k0 : ℕ } → nxn→n j0 k0 ≡ i → ⟪ j , k ⟫ ≡ ⟪ j0 , k0 ⟫ i≤0→i≡0 : {i : ℕ } → i ≤ 0 → i ≡ 0 @@ -123,11 +120,11 @@ nxn→n zero (suc j) = j + suc (nxn→n zero j) nxn→n (suc i) zero = suc i + suc (nxn→n i zero) nxn→n (suc i) (suc j) = suc i + suc j + suc (nxn→n i (suc j)) + nn : ( i : ℕ) → NN i nxn→n n→nxn : ℕ → ℕ ∧ ℕ - n→nxn zero = ⟪ 0 , 0 ⟫ - n→nxn (suc i) with n→nxn i - ... | ⟪ x , zero ⟫ = ⟪ zero , suc x ⟫ - ... | ⟪ x , suc y ⟫ = ⟪ suc x , y ⟫ + n→nxn n = ⟪ NN.j (nn n) , NN.k (nn n) ⟫ + k0 : {i : ℕ } → n→nxn i ≡ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ + k0 {i} = refl nxn→n0 : { j k : ℕ } → nxn→n j k ≡ 0 → ( j ≡ 0 ) ∧ ( k ≡ 0 ) nxn→n0 {zero} {zero} eq = ⟪ refl , refl ⟫ @@ -191,56 +188,64 @@ suc ((i + 1) + (i + suc (nxn→n 0 i))) ≡⟨ cong suc (+-assoc i 1 (i + suc (nxn→n 0 i))) ⟩ suc (i + suc (i + suc (nxn→n 0 i))) ∎ where open ≡-Reasoning + nni>j : {i : ℕ} → suc i > NN.j (nn i) ----- -- -- create the invariant NN for all n -- - nn : ( i : ℕ) → NN i nxn→n n→nxn nn zero = record { j = 0 ; k = 0 ; sum = 0 ; stage = 0 ; nn = refl ; ni = refl ; k1 = refl ; k0 = refl ; nn-unique = λ {j0} {k0} eq → cong₂ (λ x y → ⟪ x , y ⟫) (sym (proj1 (nxn→n0 eq))) (sym (proj2 (nxn→n0 {j0} {k0} eq))) } nn (suc i) with NN.k (nn i) | inspect NN.k (nn i) - ... | zero | record { eq = eq } = record { k = suc (NN.sum (nn i)) ; j = 0 ; sum = suc (NN.sum (nn i)) ; stage = suc (NN.sum (nn i)) + (NN.stage (nn i)) + ... | zero | record { eq = eq } = record { k = suc (sum ) ; j = 0 ; sum = suc (sum ) ; stage = suc (sum ) + (stage ) ; nn = refl ; ni = nn01 ; k1 = nn02 ; k0 = nn03 ; nn-unique = nn04 } where --- --- increment the stage --- - sum = NN.sum (nn i) - stage = NN.stage (nn i) + sum = NN.j (nn i) + NN.k (nn i) + stage = minus i (NN.j (nn i)) j = NN.j (nn i) + NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum + NNnn = sym refl + NNni : i ≡ NN.j (nn i) + stage + NNni = begin + i ≡⟨ sym (minus+n {i} {NN.j (nn i)} (nni>j {i} )) ⟩ + stage + NN.j (nn i) ≡⟨ +-comm stage _ ⟩ + NN.j (nn i) + stage ∎ where open ≡-Reasoning nn01 : suc i ≡ 0 + (suc sum + stage ) nn01 = begin - suc i ≡⟨ cong suc (NN.ni (nn i)) ⟩ + suc i ≡⟨ cong suc (NNni ) ⟩ suc ((NN.j (nn i) ) + stage ) ≡⟨ cong (λ k → suc (k + stage )) (+-comm 0 _ ) ⟩ suc ((NN.j (nn i) + 0 ) + stage ) ≡⟨ cong (λ k → suc ((NN.j (nn i) + k) + stage )) (sym eq) ⟩ - suc ((NN.j (nn i) + NN.k (nn i)) + stage ) ≡⟨ cong (λ k → suc ( k + stage )) (NN.nn (nn i)) ⟩ + suc ((NN.j (nn i) + NN.k (nn i)) + stage ) ≡⟨ cong (λ k → suc ( k + stage )) (NNnn ) ⟩ 0 + (suc sum + stage ) ∎ where open ≡-Reasoning nn02 : nxn→n 0 (suc sum) ≡ suc i nn02 = begin sum + suc (nxn→n 0 sum) ≡⟨ sym (+-assoc sum 1 (nxn→n 0 sum)) ⟩ (sum + 1) + nxn→n 0 sum ≡⟨ cong (λ k → k + nxn→n 0 sum ) (+-comm sum 1 )⟩ suc (sum + nxn→n 0 sum) ≡⟨ cong suc (nid20 sum ) ⟩ - suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NN.nn (nn i))) ⟩ + suc (nxn→n sum 0) ≡⟨ cong (λ k → suc (nxn→n k 0 )) (sym (NNnn )) ⟩ suc (nxn→n (NN.j (nn i) + (NN.k (nn i)) ) 0) ≡⟨ cong₂ (λ j k → suc (nxn→n (NN.j (nn i) + j) k )) eq (sym eq) ⟩ suc (nxn→n (NN.j (nn i) + 0 ) (NN.k (nn i))) ≡⟨ cong (λ k → suc ( nxn→n k (NN.k (nn i)))) (+-comm (NN.j (nn i)) 0) ⟩ suc (nxn→n (NN.j (nn i)) (NN.k (nn i))) ≡⟨ cong suc (NN.k1 (nn i) ) ⟩ suc i ∎ where open ≡-Reasoning - nn03 : n→nxn (suc i) ≡ ⟪ 0 , suc (NN.sum (nn i)) ⟫ -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫ + nn03 : n→nxn (suc i) ≡ ⟪ 0 , suc (sum ) ⟫ -- k0 : n→nxn i ≡ ⟪ NN.j (nn i) = sum , NN.k (nn i) = 0 ⟫ nn03 with n→nxn i | inspect n→nxn i ... | ⟪ x , zero ⟫ | record { eq = eq1 } = begin + ⟪ {!!} , {!!} ⟫ ≡⟨ {!!} ⟩ ⟪ zero , suc x ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (sym (cong proj1 eq1)) ⟩ - ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 (NN.k0 (nn i))) ⟩ + ⟪ zero , suc (proj1 (n→nxn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (cong proj1 refl) ⟩ ⟪ zero , suc (NN.j (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫) (+-comm 0 _ ) ⟩ ⟪ zero , suc (NN.j (nn i) + 0) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc (NN.j (nn i) + k) ⟫ ) (sym eq) ⟩ - ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NN.nn (nn i)) ⟩ + ⟪ zero , suc (NN.j (nn i) + NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ zero , suc k ⟫ ) (NNnn ) ⟩ ⟪ 0 , suc sum ⟫ ∎ where open ≡-Reasoning - ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 (NN.k0 (nn i)))) (begin + ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 refl)) (begin suc (NN.k (nn i)) ≡⟨ cong suc eq ⟩ suc 0 ≤⟨ s≤s z≤n ⟩ suc y ≡⟨ sym (cong proj2 eq1) ⟩ proj2 (n→nxn i) ∎ )) where open ≤-Reasoning -- nid2 : (i j : ℕ) → suc (nxn→n i (suc j)) ≡ nxn→n (suc i) j - nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (NN.sum (nn i)) ⟫ ≡ ⟪ j0 , k0 ⟫ + nn04 : {j0 k0 : ℕ} → nxn→n j0 k0 ≡ suc i → ⟪ 0 , suc (sum ) ⟫ ≡ ⟪ j0 , k0 ⟫ nn04 {zero} {suc k0} eq1 = cong (λ k → ⟪ 0 , k ⟫ ) (cong suc (sym nn08)) where -- eq : nxn→n zero (suc k0) ≡ suc i -- nn07 : nxn→n k0 0 ≡ i nn07 = cong pred ( begin @@ -252,7 +257,7 @@ k0 ≡⟨ cong proj1 (sym (NN.nn-unique (nn i) nn07)) ⟩ NN.j (nn i) ≡⟨ +-comm 0 _ ⟩ NN.j (nn i) + 0 ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ - NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩ + NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ sum ∎ where open ≡-Reasoning nn04 {suc j0} {k0} eq1 = ⊥-elim ( nat-≡< (cong proj2 (nn06 nn05)) (subst (λ k → k < suc k0) (sym eq) (s≤s z≤n))) where nn05 : nxn→n j0 (suc k0) ≡ i @@ -264,18 +269,28 @@ i ∎ where open ≡-Reasoning nn06 : nxn→n j0 (suc k0) ≡ i → ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ≡ ⟪ j0 , suc k0 ⟫ nn06 = NN.nn-unique (nn i) - ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = NN.sum (nn i) ; stage = NN.stage (nn i) ; nn = nn10 - ; ni = cong suc (NN.ni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where + ... | suc k | record {eq = eq} = record { k = k ; j = suc (NN.j (nn i)) ; sum = sum ; stage = stage ; nn = nn10 + ; ni = cong suc (NNni (nn i)) ; k1 = nn11 ; k0 = nn12 ; nn-unique = nn13 } where --- --- increment in a stage --- - nn10 : suc (NN.j (nn i)) + k ≡ NN.sum (nn i) + sum = NN.j (nn i) + NN.k (nn i) + stage = minus i (NN.j (nn i)) + j = NN.j (nn i) + NNnn : NN.j (nn i) + NN.k (nn i) ≡ sum + NNnn = sym refl + NNni : i ≡ NN.j (nn i) + stage + NNni = begin + i ≡⟨ sym (minus+n {i} {NN.j (nn i)} (nni>j {i} )) ⟩ + stage + NN.j (nn i) ≡⟨ +-comm stage _ ⟩ + NN.j (nn i) + stage ∎ where open ≡-Reasoning + nn10 : suc (NN.j (nn i)) + k ≡ sum nn10 = begin suc (NN.j (nn i)) + k ≡⟨ cong (λ x → x + k) (+-comm 1 _) ⟩ (NN.j (nn i) + 1) + k ≡⟨ +-assoc (NN.j (nn i)) 1 k ⟩ NN.j (nn i) + suc k ≡⟨ cong (λ k → NN.j (nn i) + k) (sym eq) ⟩ - NN.j (nn i) + NN.k (nn i) ≡⟨ NN.nn (nn i) ⟩ - NN.sum (nn i) ∎ where open ≡-Reasoning + NN.j (nn i) + NN.k (nn i) ≡⟨ NNnn ⟩ + sum ∎ where open ≡-Reasoning nn11 : nxn→n (suc (NN.j (nn i))) k ≡ suc i -- nxn→n ( NN.j (nn i)) (NN.k (nn i) ≡ i nn11 = begin nxn→n (suc (NN.j (nn i))) k ≡⟨ sym (nid2 (NN.j (nn i)) k) ⟩ @@ -291,13 +306,14 @@ ... | ⟪ x , zero ⟫ | record { eq = eq1 } = ⊥-elim ( nat-≡< (sym (cong proj2 eq1)) (subst (λ k → 0 < k ) ( begin suc k ≡⟨ sym eq ⟩ - NN.k (nn i) ≡⟨ cong proj2 (sym (NN.k0 (nn i)) ) ⟩ + NN.k (nn i) ≡⟨ cong proj2 (sym refl ) ⟩ proj2 (n→nxn i) ∎ ) (s≤s z≤n )) ) where open ≡-Reasoning -- eq1 n→nxn i ≡ ⟪ x , zero ⟫ ... | ⟪ x , suc y ⟫ | record { eq = eq1 } = begin -- n→nxn i ≡ ⟪ x , suc y ⟫ + ⟪ {!!} , {!!} ⟫ ≡⟨ {!!} ⟩ ⟪ suc x , y ⟫ ≡⟨ refl ⟩ ⟪ suc x , pred (suc y) ⟫ ≡⟨ cong (λ k → ⟪ suc (proj1 k) , pred (proj2 k) ⟫) ( begin ⟪ x , suc y ⟫ ≡⟨ sym eq1 ⟩ - n→nxn i ≡⟨ NN.k0 (nn i) ⟩ + n→nxn i ≡⟨ refl ⟩ ⟪ NN.j (nn i) , NN.k (nn i) ⟫ ∎ ) ⟩ ⟪ suc (NN.j (nn i)) , pred (NN.k (nn i)) ⟫ ≡⟨ cong (λ k → ⟪ suc (NN.j (nn i)) , pred k ⟫) eq ⟩ ⟪ suc (NN.j (nn i)) , k ⟫ ∎ where open ≡-Reasoning @@ -320,13 +336,21 @@ nn15 = NN.nn-unique (nn i) nn14 n-id : (i : ℕ) → nxn→n (proj1 (n→nxn i)) (proj2 (n→nxn i)) ≡ i - n-id i = subst (λ k → nxn→n (proj1 k) (proj2 k) ≡ i ) (sym (NN.k0 (nn i))) (NN.k1 (nn i)) + n-id i = subst (λ k → nxn→n (proj1 k) (proj2 k) ≡ i ) (sym refl) (NN.k1 (nn i)) nn-id : (j k : ℕ) → n→nxn (nxn→n j k) ≡ ⟪ j , k ⟫ nn-id j k = begin - n→nxn (nxn→n j k) ≡⟨ NN.k0 (nn (nxn→n j k)) ⟩ + n→nxn (nxn→n j k) ≡⟨ refl ⟩ ⟪ NN.j (nn (nxn→n j k)) , NN.k (nn (nxn→n j k)) ⟫ ≡⟨ NN.nn-unique (nn (nxn→n j k)) refl ⟩ ⟪ j , k ⟫ ∎ where open ≡-Reasoning + nni>j {zero} = refl-≤ + nni>j {suc i} = {!!} + -- nni>j {i} {n} = begin + -- suc (NN.j n) ≤⟨ {!!} ⟩ + -- suc (nxn→n (NN.j n) (NN.k n)) ≡⟨ {!!} ⟩ + -- suc i ∎ where + -- open ≤-Reasoning + -- [] 0
--- a/automaton-in-agda/src/flcagl.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/flcagl.agda Wed Nov 17 16:12:30 2021 +0900 @@ -1,3 +1,4 @@ +{-# OPTIONS --sized-types #-} open import Relation.Nullary open import Relation.Binary.PropositionalEquality module flcagl @@ -118,7 +119,8 @@ Setoid._≈_ (Bis i) = _≅⟨ i ⟩≅_ Setoid.isEquivalence (Bis i) = ≅isEquivalence i - import Relation.Binary.EqReasoning as EqR + -- import Relation.Binary.EqReasoning as EqR + import Relation.Binary.Reasoning.Setoid as EqR ≅trans′ : ∀ i (k l m : Lang ∞) ( p : k ≅⟨ i ⟩≅ l ) ( q : l ≅⟨ i ⟩≅ m ) → k ≅⟨ i ⟩≅ m @@ -402,7 +404,8 @@ δ (composeA da1 s2 da2) (s1 , ss2) a = δ da1 s1 a , δs da2 (if ν da1 s1 then s2 ∷ ss2 else ss2) a -import Relation.Binary.EqReasoning as EqR +-- import Relation.Binary.EqReasoning as EqR +import Relation.Binary.Reasoning.Setoid as EqR composeA-gen : ∀{i S1 S2} (da1 : DA S1) (da2 : DA S2) → ∀(s1 : S1)(s2 : S2)(ss : List ∞ S2) → lang (composeA da1 s2 da2) (s1 , ss) ≅⟨ i ⟩≅ lang da1 s1 · lang da2 s2 ∪ lang (powA da2) ss
--- a/automaton-in-agda/src/logic.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/logic.agda Wed Nov 17 16:12:30 2021 +0900 @@ -170,3 +170,23 @@ bool-and-2 {false} {false} refl = refl +open import Data.Nat +open import Data.Nat.Properties + +_≥b_ : ( x y : ℕ) → Bool +x ≥b y with <-cmp x y +... | tri< a ¬b ¬c = false +... | tri≈ ¬a b ¬c = true +... | tri> ¬a ¬b c = true + +_>b_ : ( x y : ℕ) → Bool +x >b y with <-cmp x y +... | tri< a ¬b ¬c = false +... | tri≈ ¬a b ¬c = false +... | tri> ¬a ¬b c = true + +_≤b_ : ( x y : ℕ) → Bool +x ≤b y = y ≥b x + +_<b_ : ( x y : ℕ) → Bool +x <b y = y >b x
--- a/automaton-in-agda/src/nat.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/nat.agda Wed Nov 17 16:12:30 2021 +0900 @@ -439,7 +439,7 @@ ... | tri≈ ¬a b ¬c = Finduction.fzero I (sym b) ... | tri< lt _ _ = f-induction0 p (f p) (<to≤ (Finduction.decline I lt)) where f-induction0 : (p : P) → (x : ℕ) → (f (Finduction.pnext I p)) ≤ x → Q p - f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) where + f-induction0 p zero le = Finduction.ind I (Finduction.fzero I (fi0 _ le)) f-induction0 p (suc x) le with <-cmp (f (Finduction.pnext I p)) (suc x) ... | tri< (s≤s a) ¬b ¬c = f-induction0 p x a ... | tri≈ ¬a b ¬c = Finduction.ind I (f-induction0 (Finduction.pnext I p) x (y<sx→y≤x f1)) where
--- a/automaton-in-agda/src/regular-language.agda Thu Jul 08 08:41:05 2021 +0900 +++ b/automaton-in-agda/src/regular-language.agda Wed Nov 17 16:12:30 2021 +0900 @@ -44,7 +44,8 @@ {-# TERMINATING #-} Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ} -Star {Σ} A = split A ( Star {Σ} A ) +Star {Σ} A [] = true +Star {Σ} A (h ∷ t) = split A ( Star {Σ} A ) (h ∷ t) open import automaton-ex @@ -56,6 +57,9 @@ ) test-AB→split {_} {A} {B} = refl +star-nil : {Σ : Set} → ( A : language {Σ} ) → Star A [] ≡ true +star-nil A = refl + open RegularLanguage isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set isRegular A x r = A x ≡ contain r x
--- a/index.ind Thu Jul 08 08:41:05 2021 +0900 +++ b/index.ind Wed Nov 17 16:12:30 2021 +0900 @@ -47,6 +47,7 @@ <ol> <li><a href="a01/lecture.html"> オートマトンの概要</a> <li><a href="a02/lecture.html"> Agdaによる数学的構造の定義と証明</a> +<li><a href="a02/sumtype.html"> Sum type または data </a> <li><a href="a03/lecture.html"> 決定性オートマトン</a> <li><a href="a04/lecture.html"> 非決定性オートマトン </a> <li><a href="a05/lecture.html"> 正規表現</a> @@ -66,3 +67,9 @@ Subject: Automaton Lecture Exercise 1.1 kono@ie.u-ryukyu.ac.jp まで送ること。 +--Zotero + +論文管理用のソフトウェア + +https://www.zotero.org +