Changeset 1062 for src/ASM/Util.ma
 Timestamp:
 Jul 11, 2011, 2:09:03 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1061 r1062 2 2 include "basics/types.ma". 3 3 include "arithmetics/nat.ma". 4 5 include "ASM/JMCoercions.ma". 4 6 5 7 (* let's implement a daemon not used by automation *) … … 12 14 with precedence 10 13 15 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 16 17 definition hd ≝ 18 λA: Type[0]. 19 λl: list A. 20 λproof: 0 < l. 21 match l return λx. 0 < x → A with 22 [ nil ⇒ λnil_absrd. ? 23  cons hd tl ⇒ λcons_prf. hd 24 ]. 25 normalize in nil_absrd; 26 cases(not_le_Sn_O 0) 27 #HYP 28 cases(HYP nil_absrd) 29 qed. 30 31 definition tail ≝ 32 λA: Type[0]. 33 λl: list A. 34 λproof: 0 < l. 35 match l return λx. 0 < x → list A with 36 [ nil ⇒ λnil_absrd. ? 37  cons hd tl ⇒ λcons_prf. tl 38 ]. 39 normalize in nil_absrd; 40 cases(not_le_Sn_O 0) 41 #HYP 42 cases(HYP nil_absrd) 43 qed. 44 45 let rec split 46 (A: Type[0]) (l: list A) (index: nat) (proof: index < l) 47 on index ≝ 48 match index return λx. x < l → (list A) × (list A) with 49 [ O ⇒ λzero_prf. 〈[], l〉 50  S index' ⇒ λsucc_prf. 51 match l return λx. S index' < x → (list A) × (list A) with 52 [ nil ⇒ λnil_absrd. ? 53  cons hd tl ⇒ λcons_prf. 54 let 〈l1, l2〉 ≝ split A tl index' ? in 55 〈hd :: l1, l2〉 56 ] succ_prf 57 ] proof. 58 [1: normalize in nil_absrd; 59 cases(not_le_Sn_O (S index')) 60 #HYP 61 cases(HYP nil_absrd) 62 2: normalize in cons_prf; 63 normalize 64 @le_S_S_to_le 65 assumption 66 ] 67 qed. 14 68 15 69 let rec nth_safe … … 67 121 ]. 68 122 123 (* 69 124 axiom reduce_strong: 70 125 ∀A: Type[0]. … … 72 127 ∀right: list A. 73 128 Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret) . 74 75 (* 129 *) 130 131 include "ASM/FoldStuff.ma". 132 76 133 let rec reduce_strong 77 (A: Type[0]) (left: list A) (right: list A) (prf:  left  =  right ) on left ≝ 134 (A: Type[0]) (left: list A) (right: list A) (prf:  left  =  right ) on left 135 : Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  ≝ 78 136 match left return λx. x = right → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 79 137 [ nil ⇒ … … 86 144 [ nil ⇒ λcons_nil_absrd_prf. ? 87 145  cons hd' tl' ⇒ λcons_cons_prf. 88 let tail_call ≝ reduce_strong A tl tl' ? in ? 146 let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (* 147 [ dp clr their_proof ⇒ ? (* 148 let 〈commonl, commonr〉 ≝ clr in ? *) 149 ]*) 89 150 ] 90 151 ] prf. … … 96 157  3: normalize in cons_nil_absrd_prf; 97 158 destruct(cons_nil_absrd_prf) 159  4: 98 160 ] 99 qed. 100 *) 161 qed. 101 162 102 163 axiom reduce_length:
Note: See TracChangeset
for help on using the changeset viewer.