Changeset 1356 for src/RTLabs

Timestamp:

Oct 11, 2011, 5:33:11 PM (9 years ago)

Author:

mulligan

Message:

deleted redundant directory. added outlines for both reports, and added a few sections to report for D4.2. more work on foldi_strong in rtlabs to rtl

File:

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

src/RTLabs/RTLabsToRTL.ma

@@ -89 +89 @@
     ]
   in
-    foldl ? ? initialize_local_env_internal 〈Stub …,runiverse〉 registers.
+    foldl … initialize_local_env_internal 〈Stub …,runiverse〉 registers.
 
 definition map_list_local_env_internal ≝
@@ -550 +550 @@
   in
     translates @ tmp_destrs2'.
+    
+let rec remove_n_first_internal
+  (b: Type[0]) (n: nat) (the_list: list b) (i: nat)
+    on the_list ≝
+  match the_list with
+  [ nil        ⇒ [ ]
+  | cons hd tl ⇒
+    match eqb i n with
+    [ true  ⇒ the_list
+    | false ⇒ remove_n_first_internal b n tl (S i)
+    ]
+  ].
+    
+definition remove_n_first ≝
+  λb: Type[0].
+  λn: nat.
+  λthe_list: list b.
+    remove_n_first_internal b n the_list 0.
+
+axiom plus_m_n_eq_o_to_lt_m_o:
+  ∀m, n, o: nat.
+    m + n = o → m ≤ o.
+
+include alias "arithmetics/nat.ma".
+
+axiom minus_m_n_Sp_to_minus_m_Sn_p:
+  ∀m, n, p: nat.
+    minus m n = S p → minus m (S n) = p.
+    
+let rec foldi_strong_internal
+  (a: Type[0]) (b: Type[0]) (reference: nat) (the_list: list b)
+    (f: ∀j: nat. ∀proof: lt j (|the_list|). a → b → a) (seed: a)
+      (counter: nat) (counter_proof: minus reference counter = |the_list|)
+        on the_list: a ≝
+  match the_list return λx. the_list = x → (minus reference counter = |x|) → a with
+  [ nil        ⇒ λidentity. λbase_case. seed
+  | cons hd tl ⇒ λidentity. λstep_case.
+    let f' ≝ λj: nat. λproof: j < |tl|. f j ? in
+      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
+  |2: generalize in match counter_proof;
+      >identity
+      #HYP
+      normalize in HYP:(???%);
+      generalize in match (minus_m_n_Sp_to_minus_m_Sn_p reference counter (|tl|) HYP);
+      #ASSM assumption
+  |3: >identity
+      normalize
+      normalize in proof;
+      generalize in match(le_S … proof);
+      #HYP assumption
+  ]
+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.
   
-axiom foldi_strong:
-  ∀a: Type[0].
-  ∀b: Type[0].
-  ∀the_list: list b.
-  ∀f: (∀i: nat. ∀proof: i ≤ |the_list|. a → b → a).
-  ∀seed: a.
-    a.
+definition foldi_strong ≝
+  λa: Type[0].
+  λb: Type[0].
+  λthe_list: list b.
+  λ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.
   
 definition translate_mul ≝