Changeset 1064 for src/ASM/Util.ma
 Timestamp:
 Jul 12, 2011, 5:52:07 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1063 r1064 33 33  S n' ⇒ match m with [ S m' ⇒ eq_nat n' m'  _ ⇒ false ] 34 34 ]. 35 36 let rec fold_left2 37 (A: Type[0]) (B: Type[0]) (C: Type[0]) (f: A → B → C → A) (accu: A) 38 (left: list B) (right: list C) (proof: left = right) 39 on left: A ≝ 40 match left return λx. x = right → A with 41 [ nil ⇒ λnil_prf. 42 match right return λx. [ ] = x → A with 43 [ nil ⇒ λnil_nil_prf. accu 44  cons hd tl ⇒ λcons_nil_absrd. ? 45 ] nil_prf 46  cons hd tl ⇒ λcons_prf. 47 match right return λx. hd::tl = x → A with 48 [ nil ⇒ λcons_nil_absrd. ? 49  cons hd' tl' ⇒ λcons_cons_prf. 50 fold_left2 … f (f accu hd hd') tl tl' ? 51 ] cons_prf 52 ] proof. 53 [ 1: normalize in cons_nil_absrd; 54 destruct(cons_nil_absrd) 55  2: normalize in cons_nil_absrd; 56 destruct(cons_nil_absrd) 57  3: normalize in cons_cons_prf; 58 @injective_S 59 assumption 60 ] 61 qed. 35 62 36 63 let rec remove_n_first_internal … … 96 123 foldi_from_until A 0 (l) f a l. 97 124 98 definition hd ≝125 definition hd_safe ≝ 99 126 λA: Type[0]. 100 127 λl: list A. … … 103 130 [ nil ⇒ λnil_absrd. ? 104 131  cons hd tl ⇒ λcons_prf. hd 105 ] .132 ] proof. 106 133 normalize in nil_absrd; 107 134 cases(not_le_Sn_O 0) … … 110 137 qed. 111 138 112 definition tail ≝139 definition tail_safe ≝ 113 140 λA: Type[0]. 114 141 λl: list A. … … 117 144 [ nil ⇒ λnil_absrd. ? 118 145  cons hd tl ⇒ λcons_prf. tl 119 ] .146 ] proof. 120 147 normalize in nil_absrd; 121 148 cases(not_le_Sn_O 0) … … 491 518 [ nil ⇒ nil A 492 519  cons hd tl ⇒ (rev A tl) @ [ hd ] 493 ]. 520 ]. 521 522 lemma append_length: 523 ∀A: Type[0]. 524 ∀l, r: list A. 525 (l @ r) = l + r. 526 #A #L #R 527 elim L 528 [ % 529  #HD #TL #IH 530 normalize >IH % 531 ] 532 qed. 533 534 lemma append_nil: 535 ∀A: Type[0]. 536 ∀l: list A. 537 l @ [ ] = l. 538 #A #L 539 elim L // 540 qed. 541 542 lemma rev_append: 543 ∀A: Type[0]. 544 ∀l, r: list A. 545 rev A (l @ r) = rev A r @ rev A l. 546 #A #L #R 547 elim L 548 [ normalize >append_nil % 549  #HD #TL #IH 550 normalize >IH 551 @associative_append 552 ] 553 qed. 554 555 lemma rev_length: 556 ∀A: Type[0]. 557 ∀l: list A. 558 rev A l = l. 559 #A #L 560 elim L 561 [ % 562  #HD #TL #IH 563 normalize 564 >(append_length A (rev A TL) [HD]) 565 normalize /2/ 566 ] 567 qed. 494 568 495 569 notation > "'if' term 19 e 'then' term 19 t 'else' term 48 f" non associative with precedence 19
Note: See TracChangeset
for help on using the changeset viewer.