Changeset 985 for src/ASM/Util.ma
 Timestamp:
 Jun 16, 2011, 4:50:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r907 r985 361 361 /3/ 362 362 qed. 363 364 lemma inclusive_disjunction_true: 365 ∀b, c: bool. 366 (orb b c) = true → b = true ∨ c = true. 367 # b 368 # c 369 elim b 370 [ normalize 371 # H 372 @ or_introl 373 % 374  normalize 375 /2/ 376 ] 377 qed. 378 379 lemma conjunction_true: 380 ∀b, c: bool. 381 andb b c = true → b = true ∧ c = true. 382 # b 383 # c 384 elim b 385 normalize 386 [ /2/ 387  # K 388 destruct 389 ] 390 qed. 391 392 lemma eq_true_false: false=true → False. 393 # K 394 destruct 395 qed. 396 397 lemma inclusive_disjunction_b_true: ∀b. orb b true = true. 398 # b 399 cases b 400 % 401 qed. 402 403 definition bool_to_Prop ≝ 404 λb. match b with [ true ⇒ True  false ⇒ False ]. 405 406 coercion bool_to_Prop: ∀b:bool. Prop ≝ bool_to_Prop on _b:bool to Type[0]. 407 408 lemma eq_false_to_notb: ∀b. b = false → ¬ b. 409 *; /2/ 410 qed. 411 412 lemma length_append: 413 ∀A.∀l1,l2:list A. 414 l1 @ l2 = l1 + l2. 415 #A #l1 elim l1 416 [ // 417  #hd #tl #IH #l2 normalize <IH //] 418 qed.
Note: See TracChangeset
for help on using the changeset viewer.