comparison src/logic.agda @ 1461:fa52d72f4bb3

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