# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1571235387 -32400
# Node ID ba5ee7eb2866b4edc3f6c5952d24a0e18b915f69
# Parent  ff4f57e17df57353f1b8cb90ad603d65bff995ae
fix graph

diff -r ff4f57e17df5 -r ba5ee7eb2866 a02/agda/practice-logic.agda
--- a/a02/agda/practice-logic.agda	Wed Oct 16 10:35:43 2019 +0900
+++ b/a02/agda/practice-logic.agda	Wed Oct 16 23:16:27 2019 +0900
@@ -47,7 +47,6 @@
 
 Lemma4 : Set
 Lemma4 = B -> A -> (B ∧ A)
-
 lemma4 : Lemma4
 lemma4 = \b -> \a -> {!!}
 
@@ -65,7 +64,9 @@
 Lemma6 = B -> ( A ∨ B )
 
 lemma6 : Lemma6
-lemma6 = \b ->  {!!}
+lemma6 = \b -> {!!}
+
+open _∧_
 
 ex1 : {A B : Set} → ( A ∧ B ) → A 
 ex1 a∧b = {!!}
@@ -76,20 +77,20 @@
 ex3 : {A B : Set} → A → B → ( A ∧ B ) 
 ex3 a b = {!!}
 
-ex4 : {A B : Set} → A → ( A ∧ A ) 
+ex4 : {A : Set} → A → ( A ∧ A ) 
 ex4 a  = record { and1 = {!!} ;  and2 = {!!} }
 
 ex5 : {A B C : Set} → ( A ∧ B ) ∧ C  →  A ∧ (B ∧ C) 
-ex5 a∧b∧c = record { and1 = {!!} ; and2 = {!!} }
+ex5 a∧b∧c = {!!}
 
 ex6 : {A B C : Set} → ( (A → B ) ∧ ( B →  C) )  → A → C
-ex6  =  {!!}
+ex6  p a = {!!} 
 
 ex7 : {A : Set} → ( A ∨ A ) → A
-ex7 =  ?
+ex7 = {!!}
 
 ex8 : {A B : Set} → B → ( A ∨ ( B → A ) ) → A
-ex8 = ?
+ex8 = {!!}
 
 open import Relation.Nullary
 open import Relation.Binary
@@ -99,7 +100,11 @@
 contra-position {A} {B}  f ¬b a = {!!}
 
 double-neg :  {A : Set } → A → ¬ ¬ A
-double-neg = {!!}
+double-neg x y = y x
+
+
+lemma :  {A : Set } →  A ∨ ( ¬ A ) → ¬ ¬ A → A
+lemma = {!!}
 
 double-neg2 :  {A : Set } → ¬ ¬ ¬ A → ¬ A
 double-neg2 = {!!}
diff -r ff4f57e17df5 -r ba5ee7eb2866 a02/lecture.ind
--- a/a02/lecture.ind	Wed Oct 16 10:35:43 2019 +0900
+++ b/a02/lecture.ind	Wed Oct 16 23:16:27 2019 +0900
@@ -340,10 +340,12 @@
     mul zero x = ?
     mul (suc x) y = ?
 
---問題1.4 Nat 
+--問題2.4 Nat 
 
 ? を埋めて掛け算を完成させよう。
 
+<a href="agda/practice-nat.agda"> data </a> <!---  Exercise 2.4 --->
+
 --Equality
 
 自然数を導入したので方程式を記述したい。そのためには等式を導入する必要がある。導入は
diff -r ff4f57e17df5 -r ba5ee7eb2866 agda/chap0.agda
--- a/agda/chap0.agda	Wed Oct 16 10:35:43 2019 +0900
+++ b/agda/chap0.agda	Wed Oct 16 23:16:27 2019 +0900
@@ -2,7 +2,7 @@
 
 open import Data.List
 open import Data.Nat hiding (_⊔_)
-open import Data.Integer hiding (_⊔_)
+open import Data.Integer hiding (_⊔_ ;  _≟_ ; _+_ )
 open import Data.Product
 
 A : List ℕ
@@ -64,15 +64,33 @@
     vertex : Set v
     edge : vertex  → vertex → Set v'
 
-data edge012a :  ℕ → ℕ →  Set where
-    e012a-1 : edge012a 1 2
-    e012a-2 : edge012a 2 3
-    e012a-3 : edge012a 3 4
-    e012a-4 : edge012a 4 5
-    e012a-5 : edge012a 5 1
+open Graph
+
+-- open import Data.Fin hiding ( _≟_ )
+open import Data.Empty
+open import Relation.Nullary
+open import Data.Unit  hiding ( _≟_ )
+
+
+-- data Dec (P : Set) : Set where
+--    yes :   P → Dec P
+--    no  : ¬ P → Dec P
+--
+--  _≟_ :  (s t : ℕ ) → Dec ( s ≡ t )
+
+open import Data.Bool  hiding ( _≟_ )
+
+conn : List ( ℕ × ℕ ) → ℕ → ℕ → Bool
+conn [] _ _ = false
+conn ((n1 , m1 ) ∷ t ) n m  with n ≟ n1 | m ≟ m1
+conn ((n1 , m1) ∷ t) n m | yes refl | yes refl  = true
+conn ((n1 , m1) ∷ t) n m | _ | _ = conn t n m 
+
+list012a : List ( ℕ × ℕ )
+list012a = (1 , 2) ∷ (2 , 3) ∷ (3 , 4) ∷ (4 , 5) ∷ (5 , 1) ∷ [] 
 
 graph012a : Graph {Zero} {Zero} 
-graph012a = record { vertex = ℕ  ; edge = edge012a } -- ; e-list =  e012a-1 ∷ e012a-2 ∷ e012a-3 ∷ e012a-4 ∷ e012a-5 ∷ [] }
+graph012a = record { vertex = ℕ  ; edge = λ s t → (conn list012a s t) ≡ true }
 
 data edge012b :  ℕ → ℕ →  Set where
     e012b-1 : edge012b 1 2
@@ -82,19 +100,42 @@
     e012b-5 : edge012b 2 4
     e012b-6 : edge012b 3 4
 
+edge? : (E : ℕ → ℕ →  Set) → ( a b : ℕ ) → Set
+edge? E a b = Dec ( E a b ) 
+
+lemma3 : ( a b : ℕ ) → edge? edge012b a b
+lemma3 1 2  = yes e012b-1
+lemma3 1 3  = yes e012b-2
+lemma3 1 4  = yes e012b-3
+lemma3 2 3  = yes e012b-4
+lemma3 2 4  = yes e012b-5
+lemma3 3 4  = yes e012b-6
+lemma3 1 1  = no ( λ () )
+lemma3 2 1  = no ( λ () )
+lemma3 2 2  = no ( λ () )
+lemma3 3 1  = no ( λ () )
+lemma3 3 2  = no ( λ () )
+lemma3 3 3  = no ( λ () )
+lemma3 0 _  = no ( λ () )
+lemma3 _ 0  = no ( λ () )
+lemma3 _ (suc (suc (suc (suc (suc _)))))  = no ( λ () )
+lemma3 (suc (suc (suc (suc _)))) _  = no ( λ () )
+
 graph012b : Graph {Zero} {Zero}
 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
+    indirect :  ( z : V  ) -> E x z  ->  connected {V} E z y -> connected E x y
+
+lemma1 : connected ( edge graph012a ) 1 2
+lemma1 = direct refl
 
-open import Data.Empty
-open import Relation.Nullary
+lemma1-2 : connected ( edge graph012a ) 1 3
+lemma1-2 = indirect 2 refl (direct refl) 
 
--- data Dec (P : Set) : Set where
---    yes :   P → Dec P
---    no  : ¬ P → Dec P
+lemma2 : connected ( edge graph012b ) 1 2
+lemma2 = direct e012b-1 
 
 reachable :  { V : Set } ( E : V -> V -> Set ) ( x y : V ) -> Set
 reachable {V} E X Y = Dec ( connected {V} E X Y )
@@ -102,7 +143,11 @@
 dag :  { V : Set } ( E : V -> V -> Set ) ->  Set
 dag {V} E =  ∀ (n : V)  →  ¬ ( connected E n n )
 
+dgree : List ( ℕ × ℕ ) → ℕ → ℕ 
+dgree [] _ = 0
+dgree ((e , e1) ∷ t)  e0 with e0 ≟ e | e0 ≟ e1
+dgree ((e , e1) ∷ t) e0 | yes _ | _ = 1 + (dgree t e0)
+dgree ((e , e1) ∷ t) e0 | _ | yes p = 1 + (dgree t e0)
+dgree ((e , e1) ∷ t) e0 | no _ | no _ = dgree t e0
 
-all-edge-012a : List ?
-all-edge-012a = e012a-1 ∷ e012a-2 ∷ e012a-3 ∷ e012a-4 ∷ e012a-5 ∷ []
-
+lemma6 = dgree list012a 2
diff -r ff4f57e17df5 -r ba5ee7eb2866 index.ind
--- a/index.ind	Wed Oct 16 10:35:43 2019 +0900
+++ b/index.ind	Wed Oct 16 23:16:27 2019 +0900
@@ -54,3 +54,7 @@
 
 電子メールおよび ura.ie.classes.automaton のニュースグループを使用する。
 
+問題に関しては、問題ごとに別なメールで、以下のタイトルで
+    Subject: Automaton Lecture Exercise 1.1
+kono@ie.u-ryukyu.ac.jp まで送ること。
+