Changeset 1358 for src/RTLabs


Ignore:
Timestamp:
Oct 11, 2011, 5:48:31 PM (8 years ago)
Author:
mulligan
Message:

got rtlabs to rtl compiling, foldi_strong needs examining

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabsToRTL.ma

    r1356 r1358  
    590590      foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ?
    591591  ] (refl … the_list) counter_proof.
    592   [1: cut(reference > 0)
    593       [2: #REFERENCE_HYP
     592  [1: cases daemon (* XXX: to do *)
    594593  |2: generalize in match counter_proof;
    595594      >identity
     
    605604  ]
    606605qed.
    607      
    608 
    609 let rec foldi_strong_from_until_internal
    610   (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 with
    615   [ nil        ⇒ λidentity. λsnd_proof. res
    616   | cons hd tl ⇒ λidentity. λsnd_proof.
    617     match geb i m return λx. geb i m = x → a with
    618     [ true  ⇒ λabsrd_prf. res
    619     | false ⇒ λotherwise.
    620       let f' ≝ λj. λthrd_proof: j ≤ |tl|. f j ? in
    621         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_proof
    626       >identity
    627       #HYP
    628       cases(geb_false_nge … HYP)
    629       #HYP2
    630       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.
    646606 
    647607definition foldi_strong ≝
     
    649609  λb: Type[0].
    650610  λ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).
    652612  λ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  //
     615qed.
    654616 
    655617definition translate_mul ≝
     
    677639      in
    678640        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 ? in
     641        let f' ≝ λi. λi_proof: i < |srcrs2|. f i ? in
    680642        let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in
    681643          add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
     
    683645  >tmp_destrs_prf
    684646  >regs_proof
    685   assumption
     647  /2/
    686648qed.
    687649
Note: See TracChangeset for help on using the changeset viewer.