Changeset 1060 for src/ASM/Util.ma

Timestamp:

Jul 8, 2011, 12:17:14 PM (9 years ago)

Author:

mulligan

Message:

work from this morning and yesterday

File:

• src/ASM/Util.ma (modified) (3 diffs)

src/ASM/Util.ma

@@ -12 +12 @@
  with precedence 10
 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }.
+
+let rec nth_safe
+  (elt_type: Type[0]) (index: nat) (the_list: list elt_type)
+  (proof: index < | the_list |)
+    on index ≝
+  match index return λs. s < | the_list | → elt_type with
+  [ O ⇒
+    match the_list return λt. 0 < | t | → elt_type with
+    [ nil        ⇒ λnil_absurd. ?
+    | cons hd tl ⇒ λcons_proof. hd
+    ]
+  | S index' ⇒
+    match the_list return λt. S index' < | t | → elt_type with
+    [ nil ⇒ λnil_absurd. ?
+    | cons hd tl ⇒
+      λcons_proof. nth_safe elt_type index' tl ?
+    ]
+  ] proof.
+  [ normalize in nil_absurd;
+    cases (not_le_Sn_O 0)
+    #ABSURD
+    elim (ABSURD nil_absurd)
+  | normalize in nil_absurd;
+    cases (not_le_Sn_O (S index'))
+    #ABSURD
+    elim (ABSURD nil_absurd)
+  | normalize in cons_proof
+    @le_S_S_to_le
+    assumption
+  ]
+qed.
+
+definition last_safe ≝
+  λelt_type: Type[0].
+  λthe_list: list elt_type.
+  λproof   : 0 < | the_list |.
+    nth_safe elt_type (|the_list| - 1) the_list ?.
+  normalize /2/
+qed.
 
 let rec reduce 
@@ -28 +67 @@
   ].
 
+axiom reduce_strong:
+  ∀A: Type[0].
+  ∀left: list A.
+  ∀right: list A.
+    Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |.
+
 (*
 let rec reduce_strong
@@ -34 +79 @@
   [ nil ⇒
     match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
-    [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉 ?
-    | cons hd tl ⇒ λnil_cons_asrd_prf. ?
+    [ nil ⇒ λnil_nil_prf. ?
+    | cons hd tl ⇒ λnil_cons_absrd_prf. ?
     ]
   | cons hd tl ⇒
     match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with
     [ nil ⇒ λcons_nil_absrd_prf. ?
-    | cons hd' tl' ⇒ λcons_cons_prf. ?
+    | cons hd' tl' ⇒ λcons_cons_prf.
+      let tail_call ≝ reduce_strong A tl tl' ? in ?
     ]
   ] prf.
-*)
-
+  [ 5: normalize in cons_cons_prf;
+       destruct(cons_cons_prf)
+       assumption
+  | 2: normalize in nil_cons_absrd_prf;
+       destruct(nil_cons_absrd_prf)
+  | 3: normalize in cons_nil_absrd_prf;
+       destruct(cons_nil_absrd_prf)
+  ]
+qed.
+*)   
+  
 axiom reduce_length:
   ∀A: Type[0].