Changeset 1358 for src/RTLabs/RTLabsToRTL.ma

Timestamp:

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

Author:

mulligan

Message:

got rtlabs to rtl compiling, foldi_strong needs examining

File:

• src/RTLabs/RTLabsToRTL.ma (modified) (5 diffs)

src/RTLabs/RTLabsToRTL.ma

@@ -590 +590 @@
       foldi_strong_internal a b reference tl f' (f counter ? seed hd) (S counter) ?
   ] (refl … the_list) counter_proof.
-  [1: cut(reference > 0)
-      [2: #REFERENCE_HYP
+  [1: cases daemon (* XXX: to do *)
   |2: generalize in match counter_proof;
       >identity
@@ -605 +604 @@
   ]
 qed.
-      
-
-let rec foldi_strong_from_until_internal
-  (a: Type[0]) (b: Type[0]) (the_list: list b)
-    (f: ∀j: nat. ∀proof: j ≤ |the_list|. a → b → a) (m: nat) (i: nat) (res: a)
-      (proof: i ≤ |the_list|) (m_length_proof: m = |the_list|)
-        on the_list: a ≝
-  match the_list return λx. the_list = x → i ≤ |x| → a with
-  [ nil        ⇒ λidentity. λsnd_proof. res
-  | cons hd tl ⇒ λidentity. λsnd_proof.
-    match geb i m return λx. geb i m = x → a with
-    [ true  ⇒ λabsrd_prf. res
-    | false ⇒ λotherwise.
-      let f' ≝ λj. λthrd_proof: j ≤ |tl|. f j ? in
-        foldi_strong_from_until_internal a b tl f' m (S i) (f' i ? res hd) ? ?
-    ] (refl … (geb i m))
-  ] (refl … the_list) proof. 
-  [1: generalize in match otherwise;
-      >m_length_proof
-      >identity
-      #HYP
-      cases(geb_false_nge … HYP)
-      #HYP2
-      cases(ge_m_n_False_to_lt_m_n … HYP2)
-  |2: 
-qed.    
-
-definition foldi_strong_from_until ≝
-  λa: Type[0].
-  λb: Type[0].
-  λn: nat.
-  λm: nat.
-  λthe_list: list b.
-  λf: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
-  λseed: a.
-  λlength_proof: m = |the_list|.
-    foldi_strong_from_until_internal a b the_list f m 0 seed ? length_proof.
-  //
-qed.
   
 definition foldi_strong ≝
@@ -649 +609 @@
   λb: Type[0].
   λthe_list: list b.
-  λf: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
+  λf: (∀i: nat. ∀proof: i < |the_list|. a → b → a).
   λseed: a.
-    foldi_strong_from_until a b 0 (|the_list|) the_list f seed.
+    foldi_strong_internal a b (|the_list|) the_list f seed 0 ?.
+  //
+qed.
   
 definition translate_mul ≝
@@ -677 +639 @@
       in
         let f ≝ translate_muli globals dummy tmpr destrs tmp_destrs fresh_srcrs1 start_lbl in
-        let f' ≝ λi. λi_proof: i ≤ |srcrs2|. f i ? in
+        let f' ≝ λi. λi_proof: i < |srcrs2|. f i ? in
         let insts_mul ≝ foldi_strong … srcrs2 f' [ ] in
           add_translates rtl_params1 globals (insts_init @ insts_mul) start_lbl dest_lbl def
@@ -683 +645 @@
   >tmp_destrs_prf
   >regs_proof
-  assumption
+  /2/
 qed.