Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/logic.agda @ 403:c298981108c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 1466e18c8180
children a60132983557
comparison
equal deleted inserted replaced
402:093e386c10a2 403:c298981108c1
1 {-# OPTIONS --cubical-compatible --safe #-}
2
1 module logic where 3 module logic where
2 4
3 open import Level 5 open import Level
4 open import Relation.Nullary 6 open import Relation.Nullary
5 open import Relation.Binary hiding (_⇔_ ) 7 open import Relation.Binary hiding (_⇔_ )
7 9
8 10
9 data Bool : Set where 11 data Bool : Set where
10 true : Bool 12 true : Bool
11 false : Bool 13 false : Bool
12
13 data Two : Set where
14 i0 : Two
15 i1 : Two
16 14
17 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where 15 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
18 constructor ⟪_,_⟫ 16 constructor ⟪_,_⟫
19 field 17 field
20 proj1 : A 18 proj1 : A
25 case2 : B → A ∨ B 23 case2 : B → A ∨ B
26 24
27 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m) 25 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
28 _⇔_ A B = ( A → B ) ∧ ( B → A ) 26 _⇔_ A B = ( A → B ) ∧ ( B → A )
29 27
30 ∧-exch : {n m : Level} {A : Set n} { B : Set m } → A ∧ B → B ∧ A
31 ∧-exch p = ⟪ _∧_.proj2 p , _∧_.proj1 p ⟫
32
33 ∨-exch : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → B ∨ A
34 ∨-exch (case1 x) = case2 x
35 ∨-exch (case2 x) = case1 x
36
37 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A 28 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
38 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a ) 29 contra-position {n} {m} {A} {B} f ¬b a = ¬b ( f a )
39 30
40 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A 31 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
41 double-neg A notnot = notnot A 32 double-neg A notnot = notnot A
44 double-neg2 notnot A = notnot ( double-neg A ) 35 double-neg2 notnot A = notnot ( double-neg A )
45 36
46 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) ) 37 de-morgan : {n : Level } {A B : Set n} → A ∧ B → ¬ ( (¬ A ) ∨ (¬ B ) )
47 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and )) 38 de-morgan {n} {A} {B} and (case1 ¬A) = ⊥-elim ( ¬A ( _∧_.proj1 and ))
48 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and )) 39 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
49
50 de-morgan∨ : {n : Level } {A B : Set n} → A ∨ B → ¬ ( (¬ A ) ∧ (¬ B ) )
51 de-morgan∨ {n} {A} {B} (case1 a) and = ⊥-elim ( _∧_.proj1 and a )
52 de-morgan∨ {n} {A} {B} (case2 b) and = ⊥-elim ( _∧_.proj2 and b )
53 40
54 dont-or :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B 41 dont-or :　{n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ A → B
55 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a ) 42 dont-or {A} {B} (case1 a) ¬A = ⊥-elim ( ¬A a )
56 dont-or {A} {B} (case2 b) ¬A = b 43 dont-or {A} {B} (case2 b) ¬A = b
57 44
69 56
70 _\/_ : Bool → Bool → Bool 57 _\/_ : Bool → Bool → Bool
71 false \/ false = false 58 false \/ false = false
72 _ \/ _ = true 59 _ \/ _ = true
73 60
74 not : Bool → Bool 61 not_ : Bool → Bool
75 not true = false 62 not true = false
76 not false = true 63 not false = true
77 64
78 _<=>_ : Bool → Bool → Bool 65 _<=>_ : Bool → Bool → Bool
79 true <=> true = true 66 true <=> true = true
80 false <=> false = true 67 false <=> false = true
81 _ <=> _ = false 68 _ <=> _ = false
82 69
70 infixr 130 _\/_
71 infixr 140 _/\_
72
83 open import Relation.Binary.PropositionalEquality 73 open import Relation.Binary.PropositionalEquality
84
85 not-not-bool : { b : Bool } → not (not b) ≡ b
86 not-not-bool {true} = refl
87 not-not-bool {false} = refl
88 74
89 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where 75 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
90 field 76 field
91 fun← : S → R 77 fun← : S → R
92 fun→ : R → S 78 fun→ : R → S
95 81
96 injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m) 82 injection : {n m : Level} (R : Set n) (S : Set m) (f : R → S ) → Set (n Level.⊔ m)
97 injection R S f = (x y : R) → f x ≡ f y → x ≡ y 83 injection R S f = (x y : R) → f x ≡ f y → x ≡ y
98 84
99 85
86 not-not-bool : { b : Bool } → not (not b) ≡ b
87 not-not-bool {true} = refl
88 not-not-bool {false} = refl
89
100 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t) 90 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
101 ¬t=f true () 91 ¬t=f true ()
102 ¬t=f false () 92 ¬t=f false ()
103
104 infixr 130 _\/_
105 infixr 140 _/\_
106 93
107 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B 94 ≡-Bool-func : {A B : Bool } → ( A ≡ true → B ≡ true ) → ( B ≡ true → A ≡ true ) → A ≡ B
108 ≡-Bool-func {true} {true} a→b b→a = refl 95 ≡-Bool-func {true} {true} a→b b→a = refl
109 ≡-Bool-func {false} {true} a→b b→a with b→a refl 96 ≡-Bool-func {false} {true} a→b b→a with b→a refl
110 ... | () 97 ... | ()
128 115
129 ¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥ 116 ¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥
130 ¬-bool refl () 117 ¬-bool refl ()
131 118
132 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥ 119 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
133 lemma-∧-0 {true} {true} refl ()
134 lemma-∧-0 {true} {false} () 120 lemma-∧-0 {true} {false} ()
135 lemma-∧-0 {false} {true} () 121 lemma-∧-0 {false} {true} ()
136 lemma-∧-0 {false} {false} () 122 lemma-∧-0 {false} {false} ()
123 lemma-∧-0 {true} {true} eq1 ()
137 124
138 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥ 125 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
139 lemma-∧-1 {true} {true} refl ()
140 lemma-∧-1 {true} {false} () 126 lemma-∧-1 {true} {false} ()
141 lemma-∧-1 {false} {true} () 127 lemma-∧-1 {false} {true} ()
142 lemma-∧-1 {false} {false} () 128 lemma-∧-1 {false} {false} ()
129 lemma-∧-1 {true} {true} eq1 ()
143 130
144 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true 131 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
145 bool-and-tt refl refl = refl 132 bool-and-tt refl refl = refl
146 133
147 bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true 134 bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true
148 bool-∧→tt-0 {true} {true} refl = refl 135 bool-∧→tt-0 {true} {true} eq = refl
149 bool-∧→tt-0 {false} {_} () 136 bool-∧→tt-0 {false} {_} ()
150 137
151 bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true 138 bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true
152 bool-∧→tt-1 {true} {true} refl = refl 139 bool-∧→tt-1 {true} {true} eq = refl
153 bool-∧→tt-1 {true} {false} () 140 bool-∧→tt-1 {true} {false} ()
154 bool-∧→tt-1 {false} {false} () 141 bool-∧→tt-1 {false} {false} ()
155 142
156 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b 143 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b
157 bool-or-1 {false} {true} refl = refl 144 bool-or-1 {false} {true} eq = refl
158 bool-or-1 {false} {false} refl = refl 145 bool-or-1 {false} {false} eq = refl
159 bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a 146 bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a
160 bool-or-2 {true} {false} refl = refl 147 bool-or-2 {true} {false} eq = refl
161 bool-or-2 {false} {false} refl = refl 148 bool-or-2 {false} {false} eq = refl
162 149
163 bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true 150 bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true
164 bool-or-3 {true} = refl 151 bool-or-3 {true} = refl
165 bool-or-3 {false} = refl 152 bool-or-3 {false} = refl
166 153
167 bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true 154 bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true
168 bool-or-31 {true} {true} refl = refl 155 bool-or-31 {true} {true} eq = refl
169 bool-or-31 {false} {true} refl = refl 156 bool-or-31 {false} {true} eq = refl
170 157
171 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true 158 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true
172 bool-or-4 {true} = refl 159 bool-or-4 {true} = refl
173 bool-or-4 {false} = refl 160 bool-or-4 {false} = refl
174 161
175 bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true 162 bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true
176 bool-or-41 {true} {b} refl = refl 163 bool-or-41 {true} {b} eq = refl
177 164
178 bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false 165 bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false
179 bool-and-1 {false} {b} refl = refl 166 bool-and-1 {false} {b} eq = refl
180 bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false 167 bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false
181 bool-and-2 {true} {false} refl = refl 168 bool-and-2 {true} {false} eq = refl
182 bool-and-2 {false} {false} refl = refl 169 bool-and-2 {false} {false} eq = refl
170 bool-and-2 {true} {true} ()
171 bool-and-2 {false} {true} ()
183 172
184 173
185 open import Data.Nat
186 open import Data.Nat.Properties
187
188 _≥b_ : ( x y : ℕ) → Bool
189 x ≥b y with <-cmp x y
190 ... | tri< a ¬b ¬c = false
191 ... | tri≈ ¬a b ¬c = true
192 ... | tri> ¬a ¬b c = true
193
194 _>b_ : ( x y : ℕ) → Bool
195 x >b y with <-cmp x y
196 ... | tri< a ¬b ¬c = false
197 ... | tri≈ ¬a b ¬c = false
198 ... | tri> ¬a ¬b c = true
199
200 _≤b_ : ( x y : ℕ) → Bool
201 x ≤b y = y ≥b x
202
203 _<b_ : ( x y : ℕ) → Bool
204 x <b y = y >b x
205
206 open import Relation.Binary.PropositionalEquality
207
208 ¬i0≡i1 : ¬ ( i0 ≡ i1 )
209 ¬i0≡i1 ()
210
211 ¬i0→i1 : {x : Two} → ¬ (x ≡ i0 ) → x ≡ i1
212 ¬i0→i1 {i0} ne = ⊥-elim ( ne refl )
213 ¬i0→i1 {i1} ne = refl
214
215 ¬i1→i0 : {x : Two} → ¬ (x ≡ i1 ) → x ≡ i0
216 ¬i1→i0 {i0} ne = refl
217 ¬i1→i0 {i1} ne = ⊥-elim ( ne refl )
218