[3] | 1 | (**************************************************************************) |
---|
| 2 | (* ___ *) |
---|
| 3 | (* ||M|| *) |
---|
| 4 | (* ||A|| A project by Andrea Asperti *) |
---|
| 5 | (* ||T|| *) |
---|
| 6 | (* ||I|| Developers: *) |
---|
| 7 | (* ||T|| The HELM team. *) |
---|
| 8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
| 9 | (* \ / *) |
---|
| 10 | (* \ / This file is distributed under the terms of the *) |
---|
| 11 | (* v GNU General Public License Version 2 *) |
---|
| 12 | (* *) |
---|
| 13 | (**************************************************************************) |
---|
| 14 | |
---|
[487] | 15 | include "basics/types.ma". |
---|
| 16 | include "basics/list.ma". |
---|
| 17 | include "basics/logic.ma". |
---|
[10] | 18 | include "binary/Z.ma". |
---|
| 19 | include "binary/positive.ma". |
---|
[3] | 20 | |
---|
[487] | 21 | lemma eq_rect_Type0_r: |
---|
[3] | 22 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
[487] | 23 | #A #a #P #p #x0 #p0 @(eq_rect_r ??? p0) assumption. |
---|
| 24 | qed. |
---|
[3] | 25 | |
---|
[487] | 26 | lemma eq_rect_r2: |
---|
[3] | 27 | ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → P x p. |
---|
[487] | 28 | #A #a #x #p cases p; #P #H assumption. |
---|
| 29 | qed. |
---|
[3] | 30 | |
---|
[487] | 31 | lemma eq_rect_Type2_r: |
---|
[3] | 32 | ∀A.∀a.∀P: ∀x:A. eq ? x a → Type[2]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
[487] | 33 | #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption. |
---|
| 34 | qed. |
---|
[3] | 35 | |
---|
[487] | 36 | lemma eq_rect_CProp0_r: |
---|
[16] | 37 | ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p. |
---|
[487] | 38 | #A #a #P #p #x0 #p0 @(eq_rect_r2 ??? p0) assumption. |
---|
| 39 | qed. |
---|
[16] | 40 | |
---|
[487] | 41 | lemma sym_neq : ∀A.∀x,y:A. x ≠ y → y ≠ x. |
---|
| 42 | #A #x #y *;#H @nmk #H' /2/; |
---|
| 43 | qed. |
---|
[3] | 44 | |
---|
| 45 | (* stolen from logic/connectives.ma to give Prop version. *) |
---|
| 46 | notation > "hvbox(a break \liff b)" |
---|
| 47 | left associative with precedence 25 |
---|
| 48 | for @{ 'iff $a $b }. |
---|
| 49 | |
---|
| 50 | notation "hvbox(a break \leftrightarrow b)" |
---|
| 51 | left associative with precedence 25 |
---|
| 52 | for @{ 'iff $a $b }. |
---|
| 53 | |
---|
| 54 | interpretation "logical iff" 'iff x y = (iff x y). |
---|
| 55 | |
---|
| 56 | (* bool *) |
---|
| 57 | |
---|
[487] | 58 | definition xorb : bool → bool → bool ≝ |
---|
[3] | 59 | λx,y. match x with [ false ⇒ y | true ⇒ notb y ]. |
---|
| 60 | |
---|
| 61 | |
---|
| 62 | (* TODO: move to Z.ma *) |
---|
| 63 | |
---|
[487] | 64 | lemma eqZb_z_z : ∀z.eqZb z z = true. |
---|
| 65 | #z cases z;normalize;//; |
---|
| 66 | qed. |
---|
[3] | 67 | |
---|
| 68 | (* XXX: divides goes to arithmetics *) |
---|
[487] | 69 | inductive dividesP (n,m:Pos) : Prop ≝ |
---|
[10] | 70 | | witness : ∀p:Pos.m = times n p → dividesP n m. |
---|
| 71 | interpretation "positive divides" 'divides n m = (dividesP n m). |
---|
| 72 | interpretation "positive not divides" 'ndivides n m = (Not (dividesP n m)). |
---|
[3] | 73 | |
---|
[487] | 74 | definition dividesZ : Z → Z → Prop ≝ |
---|
[10] | 75 | λx,y. match x with |
---|
| 76 | [ OZ ⇒ False |
---|
| 77 | | pos n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] |
---|
| 78 | | neg n ⇒ match y with [ OZ ⇒ True | pos m ⇒ dividesP n m | neg m ⇒ dividesP n m ] |
---|
| 79 | ]. |
---|
| 80 | |
---|
[3] | 81 | interpretation "integer divides" 'divides n m = (dividesZ n m). |
---|
| 82 | interpretation "integer not divides" 'ndivides n m = (Not (dividesZ n m)). |
---|
| 83 | |
---|
| 84 | (* should be proved in nat.ma, but it's not! *) |
---|
[487] | 85 | lemma eqb_to_Prop : ∀n,m:nat.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
| 86 | #n elim n; |
---|
| 87 | [ #m cases m; //; |
---|
| 88 | | #n' #IH #m cases m; [ /2/; | #m' whd in match (eqb (S n') (S m')) in ⊢ %; |
---|
| 89 | lapply (IH m'); cases (eqb n' m'); /2/; ] |
---|
| 90 | ] qed. |
---|
[3] | 91 | |
---|
[487] | 92 | lemma pos_eqb_to_Prop : ∀n,m:Pos.match eqb n m with [ true ⇒ n = m | false ⇒ n ≠ m ]. |
---|
| 93 | #n #m @eqb_elim //; qed. |
---|
[10] | 94 | |
---|
[487] | 95 | lemma injective_Z_of_nat : injective ? ? Z_of_nat. |
---|
| 96 | normalize; |
---|
| 97 | #n #m cases n;cases m;normalize;//; |
---|
| 98 | [ 1,2: #n' #H destruct |
---|
| 99 | | #n' #m' #H destruct; >(succ_pos_of_nat_inj … e0) // |
---|
| 100 | ] qed. |
---|
[3] | 101 | |
---|
[487] | 102 | lemma reflexive_Zle : reflexive ? Zle. |
---|
| 103 | #x cases x; //; qed. |
---|
[3] | 104 | |
---|
[487] | 105 | lemma Zsucc_pos : ∀n. Z_of_nat (S n) = Zsucc (Z_of_nat n). |
---|
| 106 | #n cases n;normalize;//;qed. |
---|
[3] | 107 | |
---|
[487] | 108 | lemma Zsucc_le : ∀x:Z. x ≤ Zsucc x. |
---|
| 109 | #x cases x; //; |
---|
| 110 | #n cases n; //; qed. |
---|
[3] | 111 | |
---|
[487] | 112 | lemma Zplus_le_pos : ∀x,y:Z.∀n. x ≤ y → x ≤ y+pos n. |
---|
| 113 | #x #y |
---|
| 114 | @pos_elim |
---|
| 115 | [ 2: #n' #IH ] |
---|
| 116 | >(Zplus_Zsucc_Zpred y ?) |
---|
| 117 | [ >(Zpred_Zsucc (pos n')) |
---|
| 118 | #H @(transitive_Zle ??? (IH H)) >(Zplus_Zsucc ??) |
---|
| 119 | @Zsucc_le |
---|
| 120 | | #H @(transitive_Zle ??? H) >(Zplus_z_OZ ?) @Zsucc_le |
---|
| 121 | ] qed. |
---|
[3] | 122 | |
---|
| 123 | (* XXX: Zmax must go to arithmetics *) |
---|
[487] | 124 | definition Zmax : Z → Z → Z ≝ |
---|
[3] | 125 | λx,y.match Z_compare x y with |
---|
| 126 | [ LT ⇒ y |
---|
| 127 | | _ ⇒ x ]. |
---|
| 128 | |
---|
[487] | 129 | lemma Zmax_l: ∀x,y. x ≤ Zmax x y. |
---|
| 130 | #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y); |
---|
| 131 | /3/; cases x; /3/; qed. |
---|
[3] | 132 | |
---|
[487] | 133 | lemma Zmax_r: ∀x,y. y ≤ Zmax x y. |
---|
| 134 | #x #y whd in ⊢ (??%); lapply (Z_compare_to_Prop x y); cases (Z_compare x y); |
---|
| 135 | cases x; /3/; qed. |
---|
[3] | 136 | |
---|
[487] | 137 | theorem Zle_to_Zlt: ∀x,y:Z. x ≤ y → Zpred x < y. |
---|
| 138 | #x #y cases x; |
---|
| 139 | [ cases y; |
---|
| 140 | [ 1,2: // |
---|
| 141 | | #n @False_ind |
---|
| 142 | ] |
---|
| 143 | | #n cases y; |
---|
| 144 | [ normalize; @False_ind |
---|
| 145 | | #m @(pos_cases … n) /2/; |
---|
| 146 | | #m normalize; @False_ind |
---|
| 147 | ] |
---|
| 148 | | #n cases y; /2/; |
---|
| 149 | ] qed. |
---|
[10] | 150 | |
---|
[487] | 151 | theorem Zlt_to_Zle_to_Zlt: ∀n,m,p:Z. n < m → m ≤ p → n < p. |
---|
| 152 | #n #m #p #Hlt #Hle <(Zpred_Zsucc n) @Zle_to_Zlt |
---|
| 153 | @(transitive_Zle … Hle) /2/; |
---|
| 154 | qed. |
---|
[3] | 155 | |
---|
[487] | 156 | definition decidable_eq_Z_Type : ∀z1,z2:Z.(z1 = z2) + (z1 ≠ z2). |
---|
| 157 | #z1 #z2 lapply (eqZb_to_Prop z1 z2);cases (eqZb z1 z2);normalize;#H |
---|
| 158 | [% // |
---|
| 159 | |%2 //] |
---|
| 160 | qed. |
---|
[3] | 161 | |
---|
[487] | 162 | lemma eqZb_false : ∀z1,z2. z1≠z2 → eqZb z1 z2 = false. |
---|
| 163 | #z1 #z2 lapply (eqZb_to_Prop z1 z2); cases (eqZb z1 z2); //; |
---|
| 164 | #H #H' @False_ind @(absurd ? H H') |
---|
| 165 | qed. |
---|
[3] | 166 | |
---|
| 167 | (* Z.ma *) |
---|
| 168 | |
---|
[487] | 169 | definition Zge: Z → Z → Prop ≝ |
---|
[3] | 170 | λn,m:Z.m ≤ n. |
---|
| 171 | |
---|
| 172 | interpretation "integer 'greater or equal to'" 'geq x y = (Zge x y). |
---|
| 173 | |
---|
[487] | 174 | definition Zgt: Z → Z → Prop ≝ |
---|
[3] | 175 | λn,m:Z.m<n. |
---|
| 176 | |
---|
| 177 | interpretation "integer 'greater than'" 'gt x y = (Zgt x y). |
---|
| 178 | |
---|
| 179 | interpretation "integer 'not greater than'" 'ngtr x y = (Not (Zgt x y)). |
---|
| 180 | |
---|
[487] | 181 | let rec Zleb (x:Z) (y:Z) : bool ≝ |
---|
[3] | 182 | match x with |
---|
| 183 | [ OZ ⇒ |
---|
| 184 | match y with |
---|
| 185 | [ OZ ⇒ true |
---|
| 186 | | pos m ⇒ true |
---|
| 187 | | neg m ⇒ false ] |
---|
| 188 | | pos n ⇒ |
---|
| 189 | match y with |
---|
| 190 | [ OZ ⇒ false |
---|
| 191 | | pos m ⇒ leb n m |
---|
| 192 | | neg m ⇒ false ] |
---|
| 193 | | neg n ⇒ |
---|
| 194 | match y with |
---|
| 195 | [ OZ ⇒ true |
---|
| 196 | | pos m ⇒ true |
---|
| 197 | | neg m ⇒ leb m n ]]. |
---|
| 198 | |
---|
[487] | 199 | let rec Zltb (x:Z) (y:Z) : bool ≝ |
---|
[3] | 200 | match x with |
---|
| 201 | [ OZ ⇒ |
---|
| 202 | match y with |
---|
| 203 | [ OZ ⇒ false |
---|
| 204 | | pos m ⇒ true |
---|
| 205 | | neg m ⇒ false ] |
---|
| 206 | | pos n ⇒ |
---|
| 207 | match y with |
---|
| 208 | [ OZ ⇒ false |
---|
[10] | 209 | | pos m ⇒ leb (succ n) m |
---|
[3] | 210 | | neg m ⇒ false ] |
---|
| 211 | | neg n ⇒ |
---|
| 212 | match y with |
---|
| 213 | [ OZ ⇒ true |
---|
| 214 | | pos m ⇒ true |
---|
[10] | 215 | | neg m ⇒ leb (succ m) n ]]. |
---|
[3] | 216 | |
---|
| 217 | |
---|
| 218 | |
---|
[487] | 219 | theorem Zle_to_Zleb_true: ∀n,m. n ≤ m → Zleb n m = true. |
---|
| 220 | #n #m cases n;cases m; //; |
---|
| 221 | [ 1,2: #m' normalize; #H @(False_ind ? H) |
---|
| 222 | | 3,5: #n' #m' normalize; @le_to_leb_true |
---|
| 223 | | 4: #n' #m' normalize; #H @(False_ind ? H) |
---|
| 224 | ] qed. |
---|
[3] | 225 | |
---|
[487] | 226 | theorem Zleb_true_to_Zle: ∀n,m.Zleb n m = true → n ≤ m. |
---|
| 227 | #n #m cases n;cases m; //; |
---|
| 228 | [ 1,2: #m' normalize; #H destruct |
---|
| 229 | | 3,5: #n' #m' normalize; @leb_true_to_le |
---|
| 230 | | 4: #n' #m' normalize; #H destruct |
---|
| 231 | ] qed. |
---|
[3] | 232 | |
---|
[487] | 233 | theorem Zleb_false_to_not_Zle: ∀n,m.Zleb n m = false → n ≰ m. |
---|
| 234 | #n #m #H % #H' >(Zle_to_Zleb_true … H') in H #H destruct; |
---|
| 235 | qed. |
---|
[3] | 236 | |
---|
[487] | 237 | theorem Zlt_to_Zltb_true: ∀n,m. n < m → Zltb n m = true. |
---|
| 238 | #n #m cases n;cases m; //; |
---|
| 239 | [ normalize; #H @(False_ind ? H) |
---|
| 240 | | 2,3: #m' normalize; #H @(False_ind ? H) |
---|
| 241 | | 4,6: #n' #m' normalize; @le_to_leb_true |
---|
| 242 | | #n' #m' normalize; #H @(False_ind ? H) |
---|
| 243 | ] qed. |
---|
[3] | 244 | |
---|
[487] | 245 | theorem Zltb_true_to_Zlt: ∀n,m. Zltb n m = true → n < m. |
---|
| 246 | #n #m cases n;cases m; //; |
---|
| 247 | [ normalize; #H destruct |
---|
| 248 | | 2,3: #m' normalize; #H destruct |
---|
| 249 | | 4,6: #n' #m' @leb_true_to_le |
---|
| 250 | | #n' #m' normalize; #H destruct |
---|
| 251 | ] qed. |
---|
[3] | 252 | |
---|
[487] | 253 | theorem Zltb_false_to_not_Zlt: ∀n,m.Zltb n m = false → n ≮ m. |
---|
| 254 | #n #m #H % #H' >(Zlt_to_Zltb_true … H') in H #H destruct; |
---|
| 255 | qed. |
---|
[3] | 256 | |
---|
[487] | 257 | theorem Zleb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. |
---|
[3] | 258 | (n ≤ m → P true) → (n ≰ m → P false) → P (Zleb n m). |
---|
[487] | 259 | #n #m #P #Hle #Hnle |
---|
| 260 | lapply (refl ? (Zleb n m)); |
---|
| 261 | elim (Zleb n m) in ⊢ ((???%)→%); |
---|
| 262 | #Hb |
---|
| 263 | [ @Hle @(Zleb_true_to_Zle … Hb) |
---|
| 264 | | @Hnle @(Zleb_false_to_not_Zle … Hb) |
---|
| 265 | ] qed. |
---|
[3] | 266 | |
---|
[487] | 267 | theorem Zltb_elim_Type0: ∀n,m:Z. ∀P:bool → Type[0]. |
---|
[3] | 268 | (n < m → P true) → (n ≮ m → P false) → P (Zltb n m). |
---|
[487] | 269 | #n #m #P #Hlt #Hnlt |
---|
| 270 | lapply (refl ? (Zltb n m)); |
---|
| 271 | elim (Zltb n m) in ⊢ ((???%)→%); |
---|
| 272 | #Hb |
---|
| 273 | [ @Hlt @(Zltb_true_to_Zlt … Hb) |
---|
| 274 | | @Hnlt @(Zltb_false_to_not_Zlt … Hb) |
---|
| 275 | ] qed. |
---|
[3] | 276 | |
---|
[487] | 277 | lemma monotonic_Zle_Zsucc: monotonic Z Zle Zsucc. |
---|
| 278 | #x #y cases x; cases y; /2/; |
---|
| 279 | #n #m @(pos_cases … n) @(pos_cases … m) |
---|
| 280 | [ //; |
---|
| 281 | | #n' /2/; |
---|
| 282 | | #m' #H @False_ind normalize in H; @(absurd … (not_le_succ_one m')) /2/; |
---|
| 283 | | #n' #m' #H normalize in H; |
---|
| 284 | >(Zsucc_neg_succ n') >(Zsucc_neg_succ m') /2/; |
---|
| 285 | ] qed. |
---|
[181] | 286 | |
---|
[487] | 287 | lemma monotonic_Zle_Zpred: monotonic Z Zle Zpred. |
---|
| 288 | #x #y cases x; cases y; |
---|
| 289 | [ 1,2,7,8,9: /2/; |
---|
| 290 | | 3,4: #m normalize; *; |
---|
| 291 | | #m #n @(pos_cases … n) @(pos_cases … m) |
---|
| 292 | [ 1,2: /2/; |
---|
| 293 | | #n' normalize; #H @False_ind @(absurd … (not_le_succ_one n')) /2/; |
---|
| 294 | | #n' #m' >(Zpred_pos_succ n') >(Zpred_pos_succ m') /2/; |
---|
| 295 | ] |
---|
| 296 | | #m #n normalize; *; |
---|
| 297 | ] qed. |
---|
[181] | 298 | |
---|
[487] | 299 | lemma monotonic_Zle_Zplus_r: ∀n.monotonic Z Zle (λm.n + m). |
---|
| 300 | #n cases n; //; #n' #a #b #H |
---|
| 301 | [ @(pos_elim … n') |
---|
| 302 | [ <(Zsucc_Zplus_pos_O a) <(Zsucc_Zplus_pos_O b) /2/; |
---|
| 303 | | #n'' #H >(?:pos (succ n'') = Zsucc (pos n'')) //; |
---|
| 304 | >(Zplus_Zsucc …) >(Zplus_Zsucc …) /2/; |
---|
| 305 | ] |
---|
| 306 | | @(pos_elim … n') |
---|
| 307 | [ <(Zpred_Zplus_neg_O a) <(Zpred_Zplus_neg_O b) /2/; |
---|
| 308 | | #n'' #H >(?:neg (succ n'') = Zpred (neg n'')) //; |
---|
| 309 | >(Zplus_Zpred …) >(Zplus_Zpred …) /2/; |
---|
| 310 | ] |
---|
| 311 | ] qed. |
---|
[181] | 312 | |
---|
[487] | 313 | lemma monotonic_Zle_Zplus_l: ∀n.monotonic Z Zle (λm.m + n). |
---|
| 314 | /2/; qed. |
---|
[181] | 315 | |
---|
[487] | 316 | let rec Z_times (x:Z) (y:Z) : Z ≝ |
---|
[15] | 317 | match x with |
---|
[11] | 318 | [ OZ ⇒ OZ |
---|
| 319 | | pos n ⇒ |
---|
| 320 | match y with |
---|
| 321 | [ OZ ⇒ OZ |
---|
| 322 | | pos m ⇒ pos (n*m) |
---|
| 323 | | neg m ⇒ neg (n*m) |
---|
| 324 | ] |
---|
| 325 | | neg n ⇒ |
---|
| 326 | match y with |
---|
| 327 | [ OZ ⇒ OZ |
---|
| 328 | | pos m ⇒ neg (n*m) |
---|
| 329 | | neg m ⇒ pos (n*m) |
---|
| 330 | ] |
---|
| 331 | ]. |
---|
[3] | 332 | interpretation "integer multiplication" 'times x y = (Z_times x y). |
---|
| 333 | |
---|
| 334 | (* Borrowed from standard-library/didactic/exercises/duality.ma with precedences tweaked *) |
---|
[10] | 335 | notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. |
---|
| 336 | notation < "'if' \nbsp term 19 e \nbsp 'then' \nbsp term 19 t \nbsp 'else' \nbsp term 48 f \nbsp" non associative with precedence 19 for @{ 'if_then_else $e $t $f }. |
---|
[3] | 337 | interpretation "Formula if_then_else" 'if_then_else e t f = (if_then_else ? e t f). |
---|
| 338 | |
---|
| 339 | (* datatypes/list.ma *) |
---|
| 340 | |
---|
[487] | 341 | theorem nil_append_nil_both: |
---|
| 342 | ∀A:Type[0]. ∀l1,l2:list A. |
---|
[3] | 343 | l1 @ l2 = [] → l1 = [] ∧ l2 = []. |
---|
[487] | 344 | #A #l1 #l2 cases l1; |
---|
| 345 | [ cases l2; |
---|
| 346 | [ /2/ |
---|
| 347 | | #h #t #H destruct; |
---|
| 348 | ] |
---|
| 349 | | cases l2; |
---|
| 350 | [ normalize; #h #t #H destruct; |
---|
| 351 | | normalize; #h1 #t1 #h2 #h3 #H destruct; |
---|
| 352 | ] |
---|
| 353 | ] qed. |
---|
[3] | 354 | |
---|
| 355 | (* division *) |
---|
| 356 | |
---|
[487] | 357 | inductive natp : Type[0] ≝ |
---|
[10] | 358 | | pzero : natp |
---|
| 359 | | ppos : Pos → natp. |
---|
[3] | 360 | |
---|
[487] | 361 | definition natp0 ≝ |
---|
[10] | 362 | λn. match n with [ pzero ⇒ pzero | ppos m ⇒ ppos (p0 m) ]. |
---|
| 363 | |
---|
[487] | 364 | definition natp1 ≝ |
---|
[10] | 365 | λn. match n with [ pzero ⇒ ppos one | ppos m ⇒ ppos (p1 m) ]. |
---|
| 366 | |
---|
[487] | 367 | let rec divide (m,n:Pos) on m ≝ |
---|
[10] | 368 | match m with |
---|
| 369 | [ one ⇒ |
---|
| 370 | match n with |
---|
| 371 | [ one ⇒ 〈ppos one,pzero〉 |
---|
| 372 | | _ ⇒ 〈pzero,ppos one〉 |
---|
| 373 | ] |
---|
| 374 | | p0 m' ⇒ |
---|
| 375 | match divide m' n with |
---|
[487] | 376 | [ pair q r ⇒ |
---|
[10] | 377 | match r with |
---|
| 378 | [ pzero ⇒ 〈natp0 q,pzero〉 |
---|
| 379 | | ppos r' ⇒ |
---|
| 380 | match partial_minus (p0 r') n with |
---|
| 381 | [ MinusNeg ⇒ 〈natp0 q, ppos (p0 r')〉 |
---|
| 382 | | MinusZero ⇒ 〈natp1 q, pzero〉 |
---|
| 383 | | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 |
---|
| 384 | ] |
---|
| 385 | ] |
---|
| 386 | ] |
---|
| 387 | | p1 m' ⇒ |
---|
| 388 | match divide m' n with |
---|
[487] | 389 | [ pair q r ⇒ |
---|
[10] | 390 | match r with |
---|
| 391 | [ pzero ⇒ match n with [ one ⇒ 〈natp1 q,pzero〉 | _ ⇒ 〈natp0 q,ppos one〉 ] |
---|
| 392 | | ppos r' ⇒ |
---|
| 393 | match partial_minus (p1 r') n with |
---|
| 394 | [ MinusNeg ⇒ 〈natp0 q, ppos (p1 r')〉 |
---|
| 395 | | MinusZero ⇒ 〈natp1 q, pzero〉 |
---|
| 396 | | MinusPos r'' ⇒ 〈natp1 q, ppos r''〉 |
---|
| 397 | ] |
---|
| 398 | ] |
---|
| 399 | ] |
---|
| 400 | ]. |
---|
| 401 | |
---|
[487] | 402 | definition div ≝ λm,n. fst ?? (divide m n). |
---|
| 403 | definition mod ≝ λm,n. snd ?? (divide m n). |
---|
[3] | 404 | |
---|
[487] | 405 | definition pairdisc ≝ |
---|
| 406 | λA,B.λx,y:Prod A B. |
---|
[3] | 407 | match x with |
---|
[487] | 408 | [(pair t0 t1) ⇒ |
---|
[3] | 409 | match y with |
---|
[487] | 410 | [(pair u0 u1) ⇒ |
---|
[3] | 411 | ∀P: Type[1]. |
---|
| 412 | (∀e0: (eq A (R0 ? t0) u0). |
---|
| 413 | ∀e1: (eq (? u0 e0) (R1 ? t0 ? t1 u0 e0) u1).P) → P ] ]. |
---|
| 414 | |
---|
[487] | 415 | lemma pairdisc_elim : ∀A,B,x,y.x = y → pairdisc A B x y. |
---|
| 416 | #A #B #x #y #e >e cases y; |
---|
| 417 | #a #b normalize;#P #PH @PH % |
---|
| 418 | qed. |
---|
[3] | 419 | |
---|
[487] | 420 | lemma pred_minus: ∀n,m. pred n - m = pred (n-m). |
---|
| 421 | @pos_elim /3/; |
---|
| 422 | qed. |
---|
[3] | 423 | |
---|
[487] | 424 | lemma minus_plus_distrib: ∀n,m,p:Pos. m-(n+p) = m-n-p. |
---|
| 425 | @pos_elim |
---|
| 426 | [ // |
---|
| 427 | | #n #IH #m #p >(succ_plus_one …) >(IH m one) /2/; |
---|
| 428 | ] qed. |
---|
[10] | 429 | |
---|
[487] | 430 | theorem plus_minus_r: |
---|
[10] | 431 | ∀m,n,p:Pos. m < n → p+(n-m) = (p+n)-m. |
---|
[487] | 432 | #m #n #p #le >(commutative_plus …) |
---|
| 433 | >(commutative_plus p ?) @plus_minus //; qed. |
---|
[3] | 434 | |
---|
[487] | 435 | lemma plus_minus_le: ∀m,n,p:Pos. m≤n → m+p-n≤p. |
---|
| 436 | #m #n #p elim m;/2/; qed. |
---|
[10] | 437 | (* |
---|
[487] | 438 | lemma le_to_minus: ∀m,n. m≤n → m-n = 0. |
---|
| 439 | #m #n elim n; |
---|
| 440 | [ <(minus_n_O …) /2/; |
---|
| 441 | | #n' #IH #le inversion le; /2/; #n'' #A #B #C destruct; |
---|
| 442 | >(eq_minus_S_pred …) >(IH A) /2/ |
---|
| 443 | ] qed. |
---|
[10] | 444 | *) |
---|
[487] | 445 | lemma minus_times_distrib_l: ∀n,m,p:Pos. n < m → p*m-p*n = p*(m-n). |
---|
| 446 | #n #m #p (*elim (decidable_lt n m);*)#lt |
---|
| 447 | (*[*) @(pos_elim … p) //;#p' #IH |
---|
| 448 | <(times_succn_m …) <(times_succn_m …) <(times_succn_m …) |
---|
| 449 | >(minus_plus_distrib …) |
---|
| 450 | <(plus_minus … lt) <IH |
---|
| 451 | >(plus_minus_r …) /2/; |
---|
| 452 | qed. |
---|
| 453 | (*| |
---|
| 454 | lapply (not_lt_to_le … lt); #le |
---|
| 455 | @(pos_elim … p) //; #p' |
---|
| 456 | cut (m-n = one); [ /3/ ] |
---|
| 457 | #mn >mn >(times_n_one …) >(times_n_one …) |
---|
| 458 | #H <H in ⊢ (???%) |
---|
| 459 | @sym_eq @le_n_one_to_eq <H |
---|
| 460 | >(minus_plus_distrib …) @monotonic_le_minus_l |
---|
[3] | 461 | /2/; |
---|
[487] | 462 | ] qed. |
---|
[3] | 463 | |
---|
[487] | 464 | lemma S_pred_m_n: ∀m,n. m > n → S (pred (m-n)) = m-n. |
---|
| 465 | #m #n #H lapply (refl ? (m-n));elim (m-n) in ⊢ (???% → %);//; |
---|
| 466 | #H' lapply (minus_to_plus … H'); /2/; |
---|
| 467 | <(plus_n_O …) #H'' >H'' in H #H |
---|
| 468 | @False_ind @(absurd ? H ( not_le_Sn_n n)) |
---|
| 469 | qed. |
---|
[10] | 470 | *) |
---|
[3] | 471 | |
---|
[487] | 472 | let rec natp_plus (n,m:natp) ≝ |
---|
[10] | 473 | match n with |
---|
| 474 | [ pzero ⇒ m |
---|
| 475 | | ppos n' ⇒ match m with [ pzero ⇒ n | ppos m' ⇒ ppos (n'+m') ] |
---|
| 476 | ]. |
---|
[3] | 477 | |
---|
[487] | 478 | let rec natp_times (n,m:natp) ≝ |
---|
[10] | 479 | match n with |
---|
| 480 | [ pzero ⇒ pzero |
---|
| 481 | | ppos n' ⇒ match m with [ pzero ⇒ pzero | ppos m' ⇒ ppos (n'*m') ] |
---|
| 482 | ]. |
---|
[3] | 483 | |
---|
[487] | 484 | inductive natp_lt : natp → Pos → Prop ≝ |
---|
[10] | 485 | | plt_zero : ∀n. natp_lt pzero n |
---|
| 486 | | plt_pos : ∀n,m. n < m → natp_lt (ppos n) m. |
---|
| 487 | |
---|
[487] | 488 | lemma lt_p0: ∀n:Pos. one < p0 n. |
---|
| 489 | #n normalize; /2/; qed. |
---|
[10] | 490 | |
---|
[487] | 491 | lemma lt_p1: ∀n:Pos. one < p1 n. |
---|
| 492 | #n' normalize; >(?:p1 n' = succ (p0 n')) //; qed. |
---|
[10] | 493 | |
---|
[487] | 494 | lemma divide_by_one: ∀m. divide m one = 〈ppos m,pzero〉. |
---|
| 495 | #m elim m; |
---|
| 496 | [ //; |
---|
| 497 | | 2,3: #m' #IH normalize; >IH //; |
---|
| 498 | ] qed. |
---|
[10] | 499 | |
---|
[487] | 500 | lemma pos_nonzero2: ∀n. ∀P:Pos→Type[0]. ∀Q:Type[0]. match succ n with [ one ⇒ Q | p0 p ⇒ P (p0 p) | p1 p ⇒ P (p1 p) ] = P (succ n). |
---|
| 501 | #n #P #Q @succ_elim /2/; qed. |
---|
[10] | 502 | |
---|
[487] | 503 | lemma partial_minus_to_Prop: ∀n,m. |
---|
[10] | 504 | match partial_minus n m with |
---|
| 505 | [ MinusNeg ⇒ n < m |
---|
| 506 | | MinusZero ⇒ n = m |
---|
| 507 | | MinusPos r ⇒ n = m+r |
---|
| 508 | ]. |
---|
[487] | 509 | #n #m lapply (pos_compare_to_Prop n m); lapply (minus_to_plus n m); |
---|
| 510 | normalize; cases (partial_minus n m); /2/; qed. |
---|
[10] | 511 | |
---|
[487] | 512 | lemma double_lt1: ∀n,m:Pos. n<m → p1 n < p0 m. |
---|
| 513 | #n #m #lt elim lt; /2/; |
---|
| 514 | qed. |
---|
[3] | 515 | |
---|
[487] | 516 | lemma double_lt2: ∀n,m:Pos. n<m → p1 n < p1 m. |
---|
| 517 | #n #m #lt @(transitive_lt ? (p0 m) ?) /2/; |
---|
| 518 | qed. |
---|
[10] | 519 | |
---|
[487] | 520 | lemma double_lt3: ∀n,m:Pos. n<succ m → p0 n < p1 m. |
---|
| 521 | #n #m #lt inversion lt; |
---|
| 522 | [ #H >(succ_injective … H) //; |
---|
| 523 | | #p #H1 #H2 #H3 >(succ_injective … H3) |
---|
| 524 | @(transitive_lt ? (p0 p) ?) /2/; |
---|
| 525 | ] |
---|
| 526 | qed. |
---|
[10] | 527 | |
---|
[487] | 528 | lemma double_lt4: ∀n,m:Pos. n<m → p0 n < p0 m. |
---|
| 529 | #n #m #lt elim lt; /2/; |
---|
| 530 | qed. |
---|
[10] | 531 | |
---|
| 532 | |
---|
| 533 | |
---|
[487] | 534 | lemma plt_lt: ∀n,m:Pos. natp_lt (ppos n) m → n<m. |
---|
| 535 | #n #m #lt inversion lt; |
---|
| 536 | [ #p #H destruct; |
---|
| 537 | | #n' #m' #lt #e1 #e2 destruct @lt |
---|
| 538 | ] qed. |
---|
[3] | 539 | |
---|
[487] | 540 | lemma lt_foo: ∀a,b:Pos. b+a < p0 b → a<b. |
---|
| 541 | #a #b /2/; qed. |
---|
[10] | 542 | |
---|
[487] | 543 | lemma lt_foo2: ∀a,b:Pos. b+a < p1 b → a<succ b. |
---|
| 544 | #a #b >(?:p1 b = succ (p0 b)) /2/; qed. |
---|
[10] | 545 | |
---|
[487] | 546 | lemma p0_plus: ∀n,m:Pos. p0 (n+m) = p0 n + p0 m. |
---|
| 547 | /2/; qed. |
---|
[10] | 548 | |
---|
[487] | 549 | lemma pair_eq1: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → a1 = a2. |
---|
| 550 | #A #B #a1 #a2 #b1 #b2 #H destruct // |
---|
| 551 | qed. |
---|
[10] | 552 | |
---|
[487] | 553 | lemma pair_eq2: ∀A,B. ∀a1,a2:A. ∀b1,b2:B. 〈a1,b1〉 = 〈a2,b2〉 → b1 = b2. |
---|
| 554 | #A #B #a1 #a2 #b1 #b2 #H destruct // |
---|
| 555 | qed. |
---|
[10] | 556 | |
---|
[487] | 557 | theorem divide_ok : ∀m,n,dv,md. |
---|
[10] | 558 | divide m n = 〈dv,md〉 → |
---|
| 559 | ppos m = natp_plus (natp_times dv (ppos n)) md ∧ natp_lt md n. |
---|
[487] | 560 | #m #n @(pos_cases … n) |
---|
| 561 | [ >(divide_by_one m) #dv #md #H destruct /2/ |
---|
| 562 | | #n' elim m; |
---|
| 563 | [ #dv #md normalize; >(pos_nonzero …) #H destruct /3/ |
---|
| 564 | | #m' #IH #dv #md whd in ⊢ (??%? → ?(???%)?); |
---|
| 565 | lapply (refl ? (divide m' (succ n'))); |
---|
| 566 | elim (divide m' (succ n')) in ⊢ (???% → % → ?); |
---|
| 567 | #dv' #md' #DIVr elim (IH … DIVr); |
---|
| 568 | whd in ⊢ (? → ? → ??%? → ?); |
---|
| 569 | cases md'; |
---|
| 570 | [ cases dv'; normalize; |
---|
| 571 | [ #H destruct |
---|
| 572 | | #dv'' #Hr1 #Hr2 >(pos_nonzero …) #H destruct % /2/ |
---|
| 573 | ] |
---|
| 574 | | cases dv'; [ 2: #dv'' ] @succ_elim |
---|
| 575 | normalize; #n #md'' #Hr1 #Hr2 |
---|
| 576 | lapply (plt_lt … Hr2); #Hr2' |
---|
| 577 | lapply (partial_minus_to_Prop md'' n); |
---|
| 578 | cases (partial_minus md'' n); [ 3,6,9,12: #r'' ] normalize |
---|
| 579 | #lt #e destruct % [ /3/ | *: /2/ ] @plt_pos |
---|
| 580 | [ 1,3,5,7: @double_lt1 /2/; |
---|
| 581 | | 2,4: @double_lt3 /2/; |
---|
| 582 | | *: @double_lt2 /2/; |
---|
| 583 | ] |
---|
| 584 | ] |
---|
| 585 | | #m' #IH #dv #md whd in ⊢ (??%? → ?); |
---|
| 586 | lapply (refl ? (divide m' (succ n'))); |
---|
| 587 | elim (divide m' (succ n')) in ⊢ (???% → % → ?); |
---|
| 588 | #dv' #md' #DIVr elim (IH … DIVr); |
---|
| 589 | whd in ⊢ (? → ? → ??%? → ?); cases md'; |
---|
| 590 | [ cases dv'; normalize; |
---|
| 591 | [ #H destruct; |
---|
| 592 | | #dv'' #Hr1 #Hr2 #H destruct; /3/; |
---|
| 593 | ] |
---|
| 594 | | (*cases dv'; [ 2: #dv'' ] @succ_elim |
---|
| 595 | normalize; #n #md'' #Hr1 #Hr2 *) #md'' #Hr1 #Hr2 |
---|
| 596 | lapply (plt_lt … Hr2); #Hr2' |
---|
| 597 | whd in ⊢ (??%? → ?); |
---|
| 598 | lapply (partial_minus_to_Prop (p0 md'') (succ n')); |
---|
| 599 | cases (partial_minus (p0 md'') (succ n')); [ 3(*,6,9,12*): #r'' ] |
---|
| 600 | cases dv' in Hr1 ⊢ %; [ 2,4,6: #dv'' ] normalize |
---|
| 601 | #Hr1 destruct [ 1,2,3: >(p0_plus ? md'') ] |
---|
| 602 | #lt #e [ 1,3,4,6: >lt ] |
---|
| 603 | <(pair_eq1 ?????? e) <(pair_eq2 ?????? e) |
---|
| 604 | normalize in ⊢ (?(???%)?); % /2/; @plt_pos |
---|
| 605 | [ cut (succ n' + r'' < p0 (succ n')); /2/; |
---|
| 606 | | cut (succ n' + r'' < p0 (succ n')); /2/; |
---|
| 607 | | /2/; |
---|
| 608 | | /2/; |
---|
| 609 | ] |
---|
| 610 | ] |
---|
| 611 | ] |
---|
| 612 | ] qed. |
---|
[10] | 613 | |
---|
[487] | 614 | lemma mod0_divides: ∀m,n,dv:Pos. |
---|
[10] | 615 | divide n m = 〈ppos dv,pzero〉 → m∣n. |
---|
[487] | 616 | #m #n #dv #DIVIDE %{dv} lapply (divide_ok … DIVIDE) *; (* XXX: need ; or it eats normalize *) |
---|
| 617 | normalize #H destruct // |
---|
| 618 | qed. |
---|
[10] | 619 | |
---|
[487] | 620 | lemma divides_mod0: ∀dv,m,n:Pos. |
---|
[10] | 621 | n = dv*m → divide n m = 〈ppos dv,pzero〉. |
---|
[487] | 622 | #dv #m #n #DIV lapply (refl ? (divide n m)); |
---|
| 623 | elim (divide n m) in ⊢ (???% → ?); #dv' #md' #DIVIDE |
---|
| 624 | lapply (divide_ok … DIVIDE); *; |
---|
| 625 | cases dv' in DIVIDE ⊢ %; [ 2: #dv'' ] |
---|
| 626 | cases md'; [ 2,4: #md'' ] #DIVIDE normalize; |
---|
| 627 | >DIV in ⊢ (% → ?) #H #lt destruct; |
---|
| 628 | [ lapply (plus_to_minus … e0); |
---|
| 629 | >(commutative_times …) >(commutative_times dv'' …) |
---|
| 630 | cut (dv'' < dv); [ cut (dv''*m < dv*m); /2/; ] #dvlt |
---|
| 631 | >(minus_times_distrib_l …) //; |
---|
[10] | 632 | |
---|
[487] | 633 | (*cut (0 < dv-dv'); [ lapply (not_le_to_lt … nle); /2/ ] |
---|
| 634 | #Hdv *) #H' cut (md'' ≥ m); /2/; lapply (plt_lt … lt); #A #B @False_ind |
---|
| 635 | @(absurd ? B (lt_to_not_le … A)) |
---|
[10] | 636 | |
---|
[487] | 637 | | @False_ind @(absurd ? (plt_lt … lt) ?) /2/; |
---|
[10] | 638 | |
---|
[487] | 639 | | >DIVIDE cut (dv = dv''); /2/; |
---|
| 640 | ] |
---|
| 641 | qed. |
---|
[10] | 642 | |
---|
[487] | 643 | lemma dec_divides: ∀m,n:Pos. (m∣n) + ¬(m∣n). |
---|
| 644 | #m #n lapply (refl ? (divide n m)); elim (divide n m) in ⊢ (???% → %); |
---|
| 645 | #dv #md cases md; cases dv; |
---|
| 646 | [ #DIVIDES lapply (divide_ok … DIVIDES); *; normalize; #H destruct |
---|
| 647 | | #dv' #H %1 @mod0_divides /2/; |
---|
| 648 | | #md' #DIVIDES %2 @nmk *; #dv' |
---|
| 649 | >(commutative_times …) #H lapply (divides_mod0 … H); |
---|
| 650 | >DIVIDES #H' |
---|
| 651 | destruct; |
---|
| 652 | | #md' #dv' #DIVIDES %2 @nmk *; #dv' |
---|
| 653 | >(commutative_times …) #H lapply (divides_mod0 … H); |
---|
| 654 | >DIVIDES #H' |
---|
| 655 | destruct; |
---|
| 656 | ] qed. |
---|
[3] | 657 | |
---|
[487] | 658 | theorem dec_dividesZ: ∀p,q:Z. (p∣q) + ¬(p∣q). |
---|
| 659 | #p #q cases p; |
---|
| 660 | [ cases q; normalize; [ %2 /2/; | *: #m %2 /2/; ] |
---|
| 661 | | *: #n cases q; normalize; /2/; |
---|
| 662 | ] qed. |
---|
[3] | 663 | |
---|
[487] | 664 | definition natp_to_Z ≝ |
---|
[10] | 665 | λn. match n with [ pzero ⇒ OZ | ppos p ⇒ pos p ]. |
---|
[3] | 666 | |
---|
[487] | 667 | definition natp_to_negZ ≝ |
---|
[10] | 668 | λn. match n with [ pzero ⇒ OZ | ppos p ⇒ neg p ]. |
---|
[3] | 669 | |
---|
| 670 | (* TODO: check these definitions are right. They are supposed to be the same |
---|
| 671 | as Zdiv/Zmod in Coq. *) |
---|
[487] | 672 | definition divZ ≝ λx,y. |
---|
[10] | 673 | match x with |
---|
| 674 | [ OZ ⇒ OZ |
---|
| 675 | | pos n ⇒ |
---|
| 676 | match y with |
---|
[3] | 677 | [ OZ ⇒ OZ |
---|
[10] | 678 | | pos m ⇒ natp_to_Z (fst ?? (divide n m)) |
---|
[487] | 679 | | neg m ⇒ match divide n m with [ pair q r ⇒ |
---|
[10] | 680 | match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] |
---|
[3] | 681 | ] |
---|
[10] | 682 | | neg n ⇒ |
---|
| 683 | match y with |
---|
| 684 | [ OZ ⇒ OZ |
---|
[487] | 685 | | pos m ⇒ match divide n m with [ pair q r ⇒ |
---|
[10] | 686 | match r with [ pzero ⇒ natp_to_negZ q | _ ⇒ Zpred (natp_to_negZ q) ] ] |
---|
| 687 | | neg m ⇒ natp_to_Z (fst ?? (divide n m)) |
---|
| 688 | ] |
---|
[3] | 689 | ]. |
---|
| 690 | |
---|
[487] | 691 | definition modZ ≝ λx,y. |
---|
[10] | 692 | match x with |
---|
| 693 | [ OZ ⇒ OZ |
---|
| 694 | | pos n ⇒ |
---|
| 695 | match y with |
---|
[3] | 696 | [ OZ ⇒ OZ |
---|
[10] | 697 | | pos m ⇒ natp_to_Z (snd ?? (divide n m)) |
---|
[487] | 698 | | neg m ⇒ match divide n m with [ pair q r ⇒ |
---|
[14] | 699 | match r with [ pzero ⇒ OZ | _ ⇒ y+(natp_to_Z r) ] ] |
---|
[3] | 700 | ] |
---|
[10] | 701 | | neg n ⇒ |
---|
| 702 | match y with |
---|
| 703 | [ OZ ⇒ OZ |
---|
[487] | 704 | | pos m ⇒ match divide n m with [ pair q r ⇒ |
---|
[14] | 705 | match r with [ pzero ⇒ OZ | _ ⇒ y-(natp_to_Z r) ] ] |
---|
[10] | 706 | | neg m ⇒ natp_to_Z (snd ?? (divide n m)) |
---|
| 707 | ] |
---|
[3] | 708 | ]. |
---|
| 709 | |
---|
| 710 | interpretation "natural division" 'divide m n = (div m n). |
---|
| 711 | interpretation "natural modulus" 'module m n = (mod m n). |
---|
| 712 | interpretation "integer division" 'divide m n = (divZ m n). |
---|
| 713 | interpretation "integer modulus" 'module m n = (modZ m n). |
---|
[14] | 714 | |
---|
[487] | 715 | lemma Zminus_Zlt: ∀x,y:Z. y>0 → x-y < x. |
---|
| 716 | #x #y cases y; |
---|
| 717 | [ #H @(False_ind … H) |
---|
| 718 | | #m #_ cases x; //; #n |
---|
| 719 | whd in ⊢ (?%?); |
---|
| 720 | lapply (pos_compare_to_Prop n m); |
---|
| 721 | cases (pos_compare n m); /2/ |
---|
| 722 | #lt whd <(minus_Sn_m … lt) /2/; |
---|
| 723 | | #m #H @(False_ind … H) |
---|
| 724 | ] qed. |
---|
[14] | 725 | |
---|
[487] | 726 | lemma pos_compare_lt: ∀n,m:Pos. n<m → pos_compare n m = LT. |
---|
| 727 | #n #m #lt lapply (pos_compare_to_Prop n m); cases (pos_compare n m); |
---|
| 728 | [ //; |
---|
| 729 | | 2,3: #H @False_ind @(absurd ? lt ?) /3/; |
---|
| 730 | ] qed. |
---|
[14] | 731 | |
---|
[487] | 732 | theorem modZ_lt_mod: ∀x,y:Z. y>0 → 0 ≤ x \mod y ∧ x \mod y < y. |
---|
| 733 | #x #y cases y; |
---|
| 734 | [ #H @(False_ind … H) |
---|
| 735 | | #m #_ cases x; |
---|
| 736 | [ % //; |
---|
| 737 | | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m)); |
---|
| 738 | cases (divide n m) in ⊢ (???% → %); #dv #md #H |
---|
| 739 | elim (divide_ok … H); #e #l elim l; /2/; |
---|
| 740 | | #n whd in ⊢ (?(??%)(?%?)); lapply (refl ? (divide n m)); |
---|
| 741 | cases (divide n m) in ⊢ (???% → %); #dv #md #H |
---|
| 742 | elim (divide_ok … H); #e #l elim l; |
---|
| 743 | [ /2/; |
---|
| 744 | | #md' #m' #l' % |
---|
| 745 | [ whd in ⊢ (??%); >(pos_compare_n_m_m_n …) |
---|
| 746 | >(pos_compare_lt … l') //; |
---|
| 747 | | @Zminus_Zlt //; |
---|
| 748 | ] |
---|
| 749 | ] |
---|
| 750 | ] |
---|
| 751 | | #m #H @(False_ind … H) |
---|
| 752 | ] qed. |
---|