 Timestamp:
 Oct 11, 2011, 5:48:31 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/RTLabsToRTL.ma
r1356 r1358 590 590 foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ? 591 591 ] (refl … the_list) counter_proof. 592 [1: cut(reference > 0) 593 [2: #REFERENCE_HYP 592 [1: cases daemon (* XXX: to do *) 594 593 2: generalize in match counter_proof; 595 594 >identity … … 605 604 ] 606 605 qed. 607 608 609 let rec foldi_strong_from_until_internal610 (a: Type[0]) (b: Type[0]) (the_list: list b)611 (f: ∀j: nat. ∀proof: j ≤ the_list. a → b → a) (m: nat) (i: nat) (res: a)612 (proof: i ≤ the_list) (m_length_proof: m = the_list)613 on the_list: a ≝614 match the_list return λx. the_list = x → i ≤ x → a with615 [ nil ⇒ λidentity. λsnd_proof. res616  cons hd tl ⇒ λidentity. λsnd_proof.617 match geb i m return λx. geb i m = x → a with618 [ true ⇒ λabsrd_prf. res619  false ⇒ λotherwise.620 let f' ≝ λj. λthrd_proof: j ≤ tl. f j ? in621 foldi_strong_from_until_internal a b tl f' m (S i) (f' i ? res hd) ? ?622 ] (refl … (geb i m))623 ] (refl … the_list) proof.624 [1: generalize in match otherwise;625 >m_length_proof626 >identity627 #HYP628 cases(geb_false_nge … HYP)629 #HYP2630 cases(ge_m_n_False_to_lt_m_n … HYP2)631 2:632 qed.633 634 definition foldi_strong_from_until ≝635 λa: Type[0].636 λb: Type[0].637 λn: nat.638 λm: nat.639 λthe_list: list b.640 λf: (∀i: nat. ∀proof: i ≤ the_list. a → b → a).641 λseed: a.642 λlength_proof: m = the_list.643 foldi_strong_from_until_internal a b the_list f m 0 seed ? length_proof.644 //645 qed.646 606 647 607 definition foldi_strong ≝ … … 649 609 λb: Type[0]. 650 610 λthe_list: list b. 651 λf: (∀i: nat. ∀proof: i ≤the_list. a → b → a).611 λf: (∀i: nat. ∀proof: i < the_list. a → b → a). 652 612 λseed: a. 653 foldi_strong_from_until a b 0 (the_list) the_list f seed. 613 foldi_strong_internal a b (the_list) the_list f seed 0 ?. 614 // 615 qed. 654 616 655 617 definition translate_mul ≝ … … 677 639 in 678 640 let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in 679 let f' ≝ λi. λi_proof: i ≤srcrs2. f i ? in641 let f' ≝ λi. λi_proof: i < srcrs2. f i ? in 680 642 let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in 681 643 add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def … … 683 645 >tmp_destrs_prf 684 646 >regs_proof 685 assumption647 /2/ 686 648 qed. 687 649
Note: See TracChangeset
for help on using the changeset viewer.