Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/chap0.agda @ 405:af8f630b7e60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents 3fa72793620b
children
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module chap0 where 3 module chap0 where
2 4
3 open import Data.List 5 open import Data.List
4 open import Data.Nat hiding (_⊔_) 6 open import Data.Nat hiding (_⊔_)
5 -- open import Data.Integer hiding (_⊔_ ; _≟_ ; _+_ ) 7 -- open import Data.Integer hiding (_⊔_ ; _≟_ ; _+_ )
147 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where 149 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where
148 direct : E x y → connected E x y 150 direct : E x y → connected E x y
149 indirect : ( z : V ) -> E x z → connected {V} E z y → connected E x y 151 indirect : ( z : V ) -> E x z → connected {V} E z y → connected E x y
150 152
151 lemma1 : connected ( edge graph012a ) 1 2 153 lemma1 : connected ( edge graph012a ) 1 2
152 lemma1 = direct refl where 154 lemma1 = direct refl
153 155
154 lemma1-2 : connected ( edge graph012a ) 1 3 156 lemma1-2 : connected ( edge graph012a ) 1 3
155 lemma1-2 = indirect 2 refl (direct refl ) 157 lemma1-2 = indirect 2 refl (direct refl )
156 158
157 lemma2 : connected ( edge graph012b ) 1 2 159 lemma2 : connected ( edge graph012b ) 1 2
186 lemma7 = dgree-c list012a 2 ( λ n → n ) 188 lemma7 = dgree-c list012a 2 ( λ n → n )
187 189
188 even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0 190 even2 : (n : ℕ ) → n % 2 ≡ 0 → (n + 2) % 2 ≡ 0
189 even2 0 refl = refl 191 even2 0 refl = refl
190 even2 1 () 192 even2 1 ()
191 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 193 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
192 194
193 sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ 195 sum-of-dgree : ( g : List ( ℕ × ℕ )) → ℕ
194 sum-of-dgree [] = 0 196 sum-of-dgree [] = 0
195 sum-of-dgree ((e , e1) ∷ t) = 2 + sum-of-dgree t 197 sum-of-dgree ((e , e1) ∷ t) = 2 + sum-of-dgree t
196 198
200 sum-of-dgree ((e , e1) ∷ t) % 2 202 sum-of-dgree ((e , e1) ∷ t) % 2
201 ≡⟨⟩ 203 ≡⟨⟩
202 (2 + sum-of-dgree t ) % 2 204 (2 + sum-of-dgree t ) % 2
203 ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) ) ⟩ 205 ≡⟨ cong ( λ k → k % 2 ) ( +-comm 2 (sum-of-dgree t) ) ⟩
204 (sum-of-dgree t + 2) % 2 206 (sum-of-dgree t + 2) % 2
205 ≡⟨ [a+n]%n≡a%n (sum-of-dgree t) _ ⟩ 207 ≡⟨ ? ⟩ -- [a+n]%n≡a%n (sum-of-dgree t) _ ⟩
206 sum-of-dgree t % 2 208 sum-of-dgree t % 2
207 ≡⟨ dgree-even t ⟩ 209 ≡⟨ dgree-even t ⟩
208 0 210 0
209 ∎ where open ≡-Reasoning 211 ∎ where open ≡-Reasoning
210 212