|
431
|
1 module logic where
|
|
|
2
|
|
|
3 open import Level
|
|
|
4 open import Relation.Nullary
|
|
|
5 open import Relation.Binary hiding (_⇔_ )
|
|
|
6 open import Data.Empty
|
|
|
7
|
|
1175
|
8
|
|
|
9 data Bool : Set where
|
|
|
10 true : Bool
|
|
|
11 false : Bool
|
|
431
|
12
|
|
|
13 data Two : Set where
|
|
|
14 i0 : Two
|
|
|
15 i1 : Two
|
|
|
16
|
|
|
17 record _∧_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
18 constructor ⟪_,_⟫
|
|
|
19 field
|
|
|
20 proj1 : A
|
|
|
21 proj2 : B
|
|
|
22
|
|
|
23 data _∨_ {n m : Level} (A : Set n) ( B : Set m ) : Set (n ⊔ m) where
|
|
|
24 case1 : A → A ∨ B
|
|
|
25 case2 : B → A ∨ B
|
|
|
26
|
|
|
27 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m ) → Set (n ⊔ m)
|
|
|
28 _⇔_ A B = ( A → B ) ∧ ( B → A )
|
|
|
29
|
|
1175
|
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
|
|
431
|
37 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 )
|
|
|
39
|
|
|
40 double-neg : {n : Level } {A : Set n} → A → ¬ ¬ A
|
|
|
41 double-neg A notnot = notnot A
|
|
|
42
|
|
|
43 double-neg2 : {n : Level } {A : Set n} → ¬ ¬ ¬ A → ¬ A
|
|
|
44 double-neg2 notnot A = notnot ( double-neg A )
|
|
|
45
|
|
|
46 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 ))
|
|
|
48 de-morgan {n} {A} {B} and (case2 ¬B) = ⊥-elim ( ¬B ( _∧_.proj2 and ))
|
|
|
49
|
|
1175
|
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
|
|
431
|
54 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 )
|
|
|
56 dont-or {A} {B} (case2 b) ¬A = b
|
|
|
57
|
|
|
58 dont-orb : {n m : Level} {A : Set n} { B : Set m } → A ∨ B → ¬ B → A
|
|
|
59 dont-orb {A} {B} (case2 b) ¬B = ⊥-elim ( ¬B b )
|
|
|
60 dont-orb {A} {B} (case1 a) ¬B = a
|
|
|
61
|
|
1175
|
62 infixr 130 _∧_
|
|
|
63 infixr 140 _∨_
|
|
|
64 infixr 150 _⇔_
|
|
|
65
|
|
|
66 _/\_ : Bool → Bool → Bool
|
|
|
67 true /\ true = true
|
|
|
68 _ /\ _ = false
|
|
|
69
|
|
|
70 _\/_ : Bool → Bool → Bool
|
|
|
71 false \/ false = false
|
|
|
72 _ \/ _ = true
|
|
|
73
|
|
|
74 not : Bool → Bool
|
|
|
75 not true = false
|
|
|
76 not false = true
|
|
|
77
|
|
|
78 _<=>_ : Bool → Bool → Bool
|
|
|
79 true <=> true = true
|
|
|
80 false <=> false = true
|
|
|
81 _ <=> _ = false
|
|
|
82
|
|
|
83 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
|
|
|
89 record Bijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
|
|
|
90 field
|
|
|
91 fun← : S → R
|
|
|
92 fun→ : R → S
|
|
|
93 fiso← : (x : R) → fun← ( fun→ x ) ≡ x
|
|
|
94 fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x
|
|
|
95
|
|
|
96 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
|
|
|
98
|
|
|
99
|
|
|
100 ¬t=f : (t : Bool ) → ¬ ( not t ≡ t)
|
|
|
101 ¬t=f true ()
|
|
|
102 ¬t=f false ()
|
|
|
103
|
|
|
104 infixr 130 _\/_
|
|
|
105 infixr 140 _/\_
|
|
|
106
|
|
|
107 ≡-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
|
|
|
109 ≡-Bool-func {false} {true} a→b b→a with b→a refl
|
|
|
110 ... | ()
|
|
|
111 ≡-Bool-func {true} {false} a→b b→a with a→b refl
|
|
|
112 ... | ()
|
|
|
113 ≡-Bool-func {false} {false} a→b b→a = refl
|
|
|
114
|
|
|
115 bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
|
|
|
116 bool-≡-? true true = yes refl
|
|
|
117 bool-≡-? true false = no (λ ())
|
|
|
118 bool-≡-? false true = no (λ ())
|
|
|
119 bool-≡-? false false = yes refl
|
|
|
120
|
|
|
121 ¬-bool-t : {a : Bool} → ¬ ( a ≡ true ) → a ≡ false
|
|
|
122 ¬-bool-t {true} ne = ⊥-elim ( ne refl )
|
|
|
123 ¬-bool-t {false} ne = refl
|
|
|
124
|
|
|
125 ¬-bool-f : {a : Bool} → ¬ ( a ≡ false ) → a ≡ true
|
|
|
126 ¬-bool-f {true} ne = refl
|
|
|
127 ¬-bool-f {false} ne = ⊥-elim ( ne refl )
|
|
|
128
|
|
|
129 ¬-bool : {a : Bool} → a ≡ false → a ≡ true → ⊥
|
|
|
130 ¬-bool refl ()
|
|
|
131
|
|
|
132 lemma-∧-0 : {a b : Bool} → a /\ b ≡ true → a ≡ false → ⊥
|
|
|
133 lemma-∧-0 {true} {true} refl ()
|
|
|
134 lemma-∧-0 {true} {false} ()
|
|
|
135 lemma-∧-0 {false} {true} ()
|
|
|
136 lemma-∧-0 {false} {false} ()
|
|
|
137
|
|
|
138 lemma-∧-1 : {a b : Bool} → a /\ b ≡ true → b ≡ false → ⊥
|
|
|
139 lemma-∧-1 {true} {true} refl ()
|
|
|
140 lemma-∧-1 {true} {false} ()
|
|
|
141 lemma-∧-1 {false} {true} ()
|
|
|
142 lemma-∧-1 {false} {false} ()
|
|
|
143
|
|
|
144 bool-and-tt : {a b : Bool} → a ≡ true → b ≡ true → ( a /\ b ) ≡ true
|
|
|
145 bool-and-tt refl refl = refl
|
|
|
146
|
|
|
147 bool-∧→tt-0 : {a b : Bool} → ( a /\ b ) ≡ true → a ≡ true
|
|
|
148 bool-∧→tt-0 {true} {true} refl = refl
|
|
|
149 bool-∧→tt-0 {false} {_} ()
|
|
|
150
|
|
|
151 bool-∧→tt-1 : {a b : Bool} → ( a /\ b ) ≡ true → b ≡ true
|
|
|
152 bool-∧→tt-1 {true} {true} refl = refl
|
|
|
153 bool-∧→tt-1 {true} {false} ()
|
|
|
154 bool-∧→tt-1 {false} {false} ()
|
|
|
155
|
|
|
156 bool-or-1 : {a b : Bool} → a ≡ false → ( a \/ b ) ≡ b
|
|
|
157 bool-or-1 {false} {true} refl = refl
|
|
|
158 bool-or-1 {false} {false} refl = refl
|
|
|
159 bool-or-2 : {a b : Bool} → b ≡ false → (a \/ b ) ≡ a
|
|
|
160 bool-or-2 {true} {false} refl = refl
|
|
|
161 bool-or-2 {false} {false} refl = refl
|
|
|
162
|
|
|
163 bool-or-3 : {a : Bool} → ( a \/ true ) ≡ true
|
|
|
164 bool-or-3 {true} = refl
|
|
|
165 bool-or-3 {false} = refl
|
|
|
166
|
|
|
167 bool-or-31 : {a b : Bool} → b ≡ true → ( a \/ b ) ≡ true
|
|
|
168 bool-or-31 {true} {true} refl = refl
|
|
|
169 bool-or-31 {false} {true} refl = refl
|
|
|
170
|
|
|
171 bool-or-4 : {a : Bool} → ( true \/ a ) ≡ true
|
|
|
172 bool-or-4 {true} = refl
|
|
|
173 bool-or-4 {false} = refl
|
|
|
174
|
|
|
175 bool-or-41 : {a b : Bool} → a ≡ true → ( a \/ b ) ≡ true
|
|
|
176 bool-or-41 {true} {b} refl = refl
|
|
|
177
|
|
|
178 bool-and-1 : {a b : Bool} → a ≡ false → (a /\ b ) ≡ false
|
|
|
179 bool-and-1 {false} {b} refl = refl
|
|
|
180 bool-and-2 : {a b : Bool} → b ≡ false → (a /\ b ) ≡ false
|
|
|
181 bool-and-2 {true} {false} refl = refl
|
|
|
182 bool-and-2 {false} {false} refl = refl
|
|
|
183
|
|
|
184
|
|
|
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
|
|
1174
|
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
|
