Mercurial > hg > Members > kono > Proof > ZF-in-agda
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 |