--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/a02/agda/logic.agda	Wed Oct 23 19:21:16 2019 +0900
@@ -0,0 +1,50 @@
+module logic where
+
+open import Level
+open import Relation.Nullary
+open import Relation.Binary
+open import Data.Empty
+
+
+data Bool : Set where
+   true : Bool
+   false : Bool
+
+record  _∧_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   field
+      proj1 : A
+      proj2 : B
+
+data  _∨_  {n m : Level} (A  : Set n) ( B : Set m ) : Set (n ⊔ m) where
+   case1 : A → A ∨ B
+   case2 : B → A ∨ B
+
+_⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
+_⇔_ A B =  ( A → B ) ∧ ( B → A )
+
+contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
+contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
+
+double-neg : {n  : Level } {A : Set n} → A → ¬ ¬ A
+double-neg A notnot = notnot A
+
+double-neg2 : {n  : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
+double-neg2 notnot A = notnot ( double-neg A )
+
+de-morgan : {n  : Level } {A B : Set n} →  A ∧ B  → ¬ ( (¬ A ) ∨ (¬ B ) )
+de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
+de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
+
+dont-or :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ A → B
+dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
+dont-or {A} {B} (case2 b) ¬A = b
+
+dont-orb :　{n m : Level} {A  : Set n} { B : Set m } →  A ∨ B → ¬ B → A
+dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
+dont-orb {A} {B} (case1 a) ¬B = a
+
+
+infixr  130 _∧_
+infixr  140 _∨_
+infixr  150 _⇔_
+

--- a/a02/agda/practice-nat.agda	Wed Oct 23 12:51:29 2019 +0900
+++ b/a02/agda/practice-nat.agda	Wed Oct 23 19:21:16 2019 +0900
@@ -3,31 +3,38 @@
 open import Data.Nat 
 open import Data.Empty
 open import Relation.Nullary
-open import  Relation.Binary.PropositionalEquality
-open import  practice-logic
+open import Relation.Binary.PropositionalEquality
+open import logic
 
-
+-- hint : it has two inputs, use recursion
 nat-<> : { x y : ℕ } → x < y → y < x → ⊥
-nat-<>  = {!!}
+nat-<> = {!!}
 
+-- hint : use recursion
 nat-<≡ : { x : ℕ } → x < x → ⊥
-nat-<≡  = {!!}
+nat-<≡ = {!!}
 
+-- hint : use refl and recursion
 nat-≡< : { x y : ℕ } → x ≡ y → x < y → ⊥
 nat-≡< = {!!}
 
 ¬a≤a : {la : ℕ} → suc la ≤ la → ⊥
-¬a≤a  = {!!}
+¬a≤a = {!!}
 
+-- hint : make case with la first
 a<sa : {la : ℕ} → la < suc la 
 a<sa = {!!}
 
+-- hint  : ¬ has an input, use recursion
 =→¬< : {x : ℕ  } → ¬ ( x < x )
 =→¬< = {!!}
 
+-- hint : two inputs, try nat-<>
 >→¬< : {x y : ℕ  } → (x < y ) → ¬ ( y < x )
 >→¬< = {!!}
 
+-- hint : make cases on all arguments. return case1 or case2
+-- hint : use with on suc case
 <-∨ : { x y : ℕ } → x < suc y → ( (x ≡ y ) ∨ (x < y) )
 <-∨ = {!!}
 

--- a/a02/lecture.ind	Wed Oct 23 12:51:29 2019 +0900
+++ b/a02/lecture.ind	Wed Oct 23 19:21:16 2019 +0900
@@ -405,11 +405,15 @@
     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 --->
 
-<a href="agda/practice-nat.agda"> equality </a> <!---  Exercise 2.5 --->
+--問題 2.5
+
+<a href="agda/practice-nat.agda"> nat の例題 </a> <!---  Exercise 2.5 --->
 
 --集合のLevel 
 
@@ -598,3 +602,7 @@
 
 <a href="agda/dag.agda"> DAG </a> <!---  Exercise 2.7 --->
 
+--教科書の第一章
+
+<a href="../agda/chap0.agda"> chapter 0 </a> 
+

--- a/a03/lecture.ind	Wed Oct 23 12:51:29 2019 +0900
+++ b/a03/lecture.ind	Wed Oct 23 19:21:16 2019 +0900
@@ -132,4 +132,20 @@
 <a href=""> </a>  <!---  Exercise 3.1 --->
 
 
+--Regular Language
 
+Language とは?
+
+Regular Language とは?
+
+--Regular Languageの演算
+
+Concatenation
+
+Union
+
+Star
+
+
+
+

--- a/agda/chap0.agda	Wed Oct 23 12:51:29 2019 +0900
+++ b/agda/chap0.agda	Wed Oct 23 19:21:16 2019 +0900
@@ -18,7 +18,7 @@
 
 
 ListProduct : {A B : Set } → List A → List B → List ( A × B )
-ListProduct = {!!}
+ListProduct  = {!!}
 
 ex05 : List ( ℕ × Literal )
 ex05 = ListProduct A B   -- (1 , x) ∷ (1 , y) ∷ (1 , z) ∷ (2 , x) ∷ (2 , y) ∷ (2 , z) ∷ [] 
@@ -98,7 +98,7 @@
 list012a = (1 , 2) ∷ (2 , 3) ∷ (3 , 4) ∷ (4 , 5) ∷ (5 , 1) ∷ [] 
 
 graph012a : Graph {Zero} {Zero} 
-graph012a = record { vertex = ℕ  ; edge = λ s t → (conn list012a s t) ≡ true }
+graph012a = record { vertex = ℕ ; edge = λ s t → (conn list012a s t) ≡ true }
 
 data edge012b :  ℕ → ℕ →  Set where
     e012b-1 : edge012b 1 2
@@ -133,14 +133,14 @@
 graph012b = record { vertex = ℕ  ; edge = edge012b }
 
 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
+    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 ( edge graph012a ) 1 2
-lemma1 = direct refl
+lemma1 = direct refl  where
 
 lemma1-2 : connected ( edge graph012a ) 1 3
-lemma1-2 = indirect 2 refl (direct refl) 
+lemma1-2 = indirect 2 refl (direct refl ) 
 
 lemma2 : connected ( edge graph012b ) 1 2
 lemma2 = direct e012b-1 
@@ -185,14 +185,14 @@
 dgree-even : ( g : List ( ℕ × ℕ )) → sum-of-dgree g % 2 ≡ 0
 dgree-even [] = refl
 dgree-even ((e , e1) ∷ t) = begin
-      sum-of-dgree ((e , e1) ∷ t) % 2
-   ≡⟨⟩
-      (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) _  ⟩
-      sum-of-dgree t % 2
-   ≡⟨ dgree-even t ⟩
-      0
-   ∎ where open ≡-Reasoning
+       sum-of-dgree ((e , e1) ∷ t) % 2 
+    ≡⟨⟩
+       (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) _ ⟩
+       sum-of-dgree t % 2
+    ≡⟨ dgree-even t ⟩
+       0
+    ∎ where open ≡-Reasoning