Changeset 782 for src/ASM/Util.ma

Timestamp:

Apr 28, 2011, 5:36:33 PM (9 years ago)

Author:

mulligan

Message:

More work on rtl-ertl pass from today, plus resolved conflict.

File:

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

src/ASM/Util.ma

@@ -2 +2 @@
 include "basics/types.ma".
 include "arithmetics/nat.ma".
+  
+lemma eq_rect_Type0_r :
+  ∀A: Type[0].
+  ∀a:A.
+  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
+  #A #a #P #H #x #p
+  generalize in match H
+  generalize in match P
+  cases p
+  //
+qed.
+  
+let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝
+  match n return λo. o < length A l → A with
+  [ O ⇒
+    match l return λm. 0 < length A m → A with
+    [ nil ⇒ λabsd1. ?
+    | cons hd tl ⇒ λprf1. hd
+    ]
+  | S n' ⇒
+    match l return λm. S n' < length A m → A with
+    [ nil ⇒ λabsd2. ?
+    | cons hd tl ⇒ λprf2. safe_nth A n' tl ?
+    ]
+  ] ?.
+  [ 1:
+    @ p
+  | 4:
+    normalize in prf2
+    normalize
+    @ le_S_S_to_le
+    assumption
+  | 2:
+    normalize in absd1;
+    cases (not_le_Sn_O O)
+    # H
+    elim (H absd1)
+  | 3:
+    normalize in absd2;
+    cases (not_le_Sn_O (S n'))
+    # H
+    elim (H absd2)
+  ]
+qed.
   
 let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝
@@ -128 +172 @@
 
 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O.
-
-lemma eq_rect_Type0_r :
-  ∀A: Type[0].
-  ∀a:A.
-  ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.
-  #A #a #P #H #x #p
-  generalize in match H
-  generalize in match P
-  cases p
-  //
-qed.
-
 
 notation "hvbox(t⌈o ↦ h⌉)"