Changeset 782 for src/ASM/Util.ma
- Timestamp:
- Apr 28, 2011, 5:36:33 PM (9 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r777 r782 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 5 lemma eq_rect_Type0_r : 6 ∀A: Type[0]. 7 ∀a:A. 8 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p. 9 #A #a #P #H #x #p 10 generalize in match H 11 generalize in match P 12 cases p 13 // 14 qed. 15 16 let rec safe_nth (A: Type[0]) (n: nat) (l: list A) (p: n < length A l) on n: A ≝ 17 match n return λo. o < length A l → A with 18 [ O ⇒ 19 match l return λm. 0 < length A m → A with 20 [ nil ⇒ λabsd1. ? 21 | cons hd tl ⇒ λprf1. hd 22 ] 23 | S n' ⇒ 24 match l return λm. S n' < length A m → A with 25 [ nil ⇒ λabsd2. ? 26 | cons hd tl ⇒ λprf2. safe_nth A n' tl ? 27 ] 28 ] ?. 29 [ 1: 30 @ p 31 | 4: 32 normalize in prf2 33 normalize 34 @ le_S_S_to_le 35 assumption 36 | 2: 37 normalize in absd1; 38 cases (not_le_Sn_O O) 39 # H 40 elim (H absd1) 41 | 3: 42 normalize in absd2; 43 cases (not_le_Sn_O (S n')) 44 # H 45 elim (H absd2) 46 ] 47 qed. 4 48 5 49 let rec nub_by_internal (A: Type[0]) (f: A → A → bool) (l: list A) (n: nat) on n ≝ … … 128 172 129 173 definition fold_left_i ≝ λA,B,f,x. fold_left_i_aux A B f x O. 130 131 lemma eq_rect_Type0_r :132 ∀A: Type[0].133 ∀a:A.134 ∀P: ∀x:A. eq ? x a → Type[0]. P a (refl A a) → ∀x: A.∀p:eq ? x a. P x p.135 #A #a #P #H #x #p136 generalize in match H137 generalize in match P138 cases p139 //140 qed.141 142 174 143 175 notation "hvbox(t⌈o ↦ h⌉)"
Note: See TracChangeset
for help on using the changeset viewer.