Mercurial > hg > Members > kono > Proof > automaton

comparison a02/agda/data1.agda @ 406:a60132983557

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 Wed, 08 Nov 2023 21:35:54 +0900
parents 407684f806e4
children
comparison
equal deleted inserted replaced
405:af8f630b7e60 406:a60132983557
26 proj2 : B 26 proj2 : B
27 27
28 open _∧_ 28 open _∧_
29 29
30 ex3' : {A B : Set} → ( A ∨ B ) → A ∧ B -- this is wrong 30 ex3' : {A B : Set} → ( A ∨ B ) → A ∧ B -- this is wrong
31 ex3' = ? 31 ex3' (case1 x) = ?
32 ex3' (case2 x) = ?
32 33
33 ex4' : {A B : Set} → ( A ∧ B ) → A ∨ B 34 ex4' : {A B : Set} → ( A ∧ B ) → A ∨ B
34 ex4' ab = case1 (proj1 ab ) 35 ex4' ⟪ a , b ⟫ = ?
35 36
36 --- ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∨ B ) → C ) is wrong 37 --- ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∨ B ) → C ) is wrong
37 ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∧ B ) → C ) 38 ex5 : {A B C : Set} → (( A → C ) ∨ ( B → C ) ) → ( ( A ∧ B ) → C )
38 ex5 (case1 a→c) ab = a→c (proj1 ab) 39 ex5 = ?
39 ex5 (case2 b→c) ab = b→c (proj2 ab)
40 40
41 data ⊥ : Set where 41 data ⊥ : Set where
42 42
43 ⊥-elim : {A : Set } -> ⊥ -> A 43 ⊥-elim : {A : Set } → ⊥ → A
44 ⊥-elim = {!!} 44 ⊥-elim ()
45 45
46 ¬_ : Set → Set 46 ¬_ : Set → Set
47 ¬ A = A → ⊥ 47 ¬ A = A → ⊥
48 48
49 49
74 74
75 problem2 : Goat → Rabbit 75 problem2 : Goat → Rabbit
76 problem2 = {!!} 76 problem2 = {!!}
77 77
78 78
79 data Nat : Set where
80 zero : Nat
81 suc : Nat → Nat
82
83 one : Nat
84 one = suc zero
85
86 five : Nat
87 five = suc (suc (suc (suc (suc zero))))
88
89 add : ( a b : Nat ) → Nat
90 add zero x = x
91 add (suc x) y = suc ( add x y )
92
93 data _≡_ {A : Set } : ( x y : A ) → Set where
94 refl : {x : A} → x ≡ x
95
96 test11 : add one five ≡ suc five
97 test11 = refl
98
99 mul : ( a b : Nat ) → Nat
100 mul zero x = zero
101 mul (suc x) y = add y (mul x y)
102
103 ex6 : Nat
104 ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
105
106 ex7 : mul ( suc ( suc zero)) (suc ( suc ( suc zero)) ) ≡ suc (suc (suc (suc (suc (suc zero)))))
107 ex7 = refl
108
79 data Three : Set where 109 data Three : Set where
80 t1 : Three 110 t1 : Three
81 t2 : Three 111 t2 : Three
82 t3 : Three 112 t3 : Three
83 113
93 data 3Ring : (dom cod : Three) → Set where 123 data 3Ring : (dom cod : Three) → Set where
94 r1 : 3Ring t1 t2 124 r1 : 3Ring t1 t2
95 r2 : 3Ring t2 t3 125 r2 : 3Ring t2 t3
96 r3 : 3Ring t3 t1 126 r3 : 3Ring t3 t1
97 127
98 data Nat : Set where
99 zero : Nat
100 suc : Nat → Nat
101
102 add : ( a b : Nat ) → Nat
103 add zero x = x
104 add (suc x) y = suc ( add x y )
105
106 mul : ( a b : Nat ) → Nat
107 mul zero x = zero
108 mul (suc x) y = add y (mul x y)
109
110 ex6 : Nat
111 ex6 = mul ( suc ( suc zero)) (suc ( suc ( suc zero)) )
112
113 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where 128 data connected { V : Set } ( E : V -> V -> Set ) ( x y : V ) : Set where
114 direct : E x y -> connected E x y 129 direct : E x y -> connected E x y
115 indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y 130 indirect : { z : V } -> E x z -> connected {V} E z y -> connected E x y
116 131
117 dag : { V : Set } ( E : V -> V -> Set ) -> Set 132 dag : { V : Set } ( E : V -> V -> Set ) → Set
118 dag {V} E = ∀ (n : V) → ¬ ( connected E n n ) 133 dag {V} E = ∀ (n : V) → ¬ ( connected E n n )
119 134
120 lemma : ¬ (dag 3Ring ) 135 lemma : ¬ (dag 3Ring )
121 lemma r = r t1 ( indirect r1 (indirect r2 (direct r3 ))) 136 lemma r = ?
137
138 -- t1 → t2 → t3
139 --
140 data 3Line : (dom cod : Three) → Set where
141 line1 : 3Line t1 t2
142 line2 : 3Line t2 t3
143
144 lemma1 : dag 3Line
145 lemma1 = ?
146
147
148