Changeset 1060 for src/ASM/Util.ma
- Timestamp:
- Jul 8, 2011, 12:17:14 PM (10 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/Util.ma
r1059 r1060 12 12 with precedence 10 13 13 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 14 15 let rec nth_safe 16 (elt_type: Type[0]) (index: nat) (the_list: list elt_type) 17 (proof: index < | the_list |) 18 on index ≝ 19 match index return λs. s < | the_list | → elt_type with 20 [ O ⇒ 21 match the_list return λt. 0 < | t | → elt_type with 22 [ nil ⇒ λnil_absurd. ? 23 | cons hd tl ⇒ λcons_proof. hd 24 ] 25 | S index' ⇒ 26 match the_list return λt. S index' < | t | → elt_type with 27 [ nil ⇒ λnil_absurd. ? 28 | cons hd tl ⇒ 29 λcons_proof. nth_safe elt_type index' tl ? 30 ] 31 ] proof. 32 [ normalize in nil_absurd; 33 cases (not_le_Sn_O 0) 34 #ABSURD 35 elim (ABSURD nil_absurd) 36 | normalize in nil_absurd; 37 cases (not_le_Sn_O (S index')) 38 #ABSURD 39 elim (ABSURD nil_absurd) 40 | normalize in cons_proof 41 @le_S_S_to_le 42 assumption 43 ] 44 qed. 45 46 definition last_safe ≝ 47 λelt_type: Type[0]. 48 λthe_list: list elt_type. 49 λproof : 0 < | the_list |. 50 nth_safe elt_type (|the_list| - 1) the_list ?. 51 normalize /2/ 52 qed. 14 53 15 54 let rec reduce … … 28 67 ]. 29 68 69 axiom reduce_strong: 70 ∀A: Type[0]. 71 ∀left: list A. 72 ∀right: list A. 73 Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) |. 74 30 75 (* 31 76 let rec reduce_strong … … 34 79 [ nil ⇒ 35 80 match right return λy. | [ ] | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with 36 [ nil ⇒ λnil_nil_prf. dp ? 〈〈[ ], [ ]〉, 〈[ ], [ ]〉〉?37 | cons hd tl ⇒ λnil_cons_a srd_prf. ?81 [ nil ⇒ λnil_nil_prf. ? 82 | cons hd tl ⇒ λnil_cons_absrd_prf. ? 38 83 ] 39 84 | cons hd tl ⇒ 40 85 match right return λy. | hd::tl | = | y | → Σret: ((list A) × (list A)) × ((list A) × (list A)). | \fst (\fst ret) | = | \fst (\snd ret) | with 41 86 [ nil ⇒ λcons_nil_absrd_prf. ? 42 | cons hd' tl' ⇒ λcons_cons_prf. ? 87 | cons hd' tl' ⇒ λcons_cons_prf. 88 let tail_call ≝ reduce_strong A tl tl' ? in ? 43 89 ] 44 90 ] prf. 45 *) 46 91 [ 5: normalize in cons_cons_prf; 92 destruct(cons_cons_prf) 93 assumption 94 | 2: normalize in nil_cons_absrd_prf; 95 destruct(nil_cons_absrd_prf) 96 | 3: normalize in cons_nil_absrd_prf; 97 destruct(cons_nil_absrd_prf) 98 ] 99 qed. 100 *) 101 47 102 axiom reduce_length: 48 103 ∀A: Type[0].
Note: See TracChangeset
for help on using the changeset viewer.