Changeset 1063 for src/ASM/Util.ma
 Timestamp:
 Jul 11, 2011, 5:52:11 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1062 r1063 14 14 with precedence 10 15 15 for @{ match $t with [ pair ${ident x} ${ident y} ⇒ $s ] }. 16 17 definition ltb ≝ 18 λm, n: nat. 19 leb (S m) n. 20 21 definition geb ≝ 22 λm, n: nat. 23 ltb n m. 24 25 definition gtb ≝ 26 λm, n: nat. 27 leb n m. 28 29 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *) 30 let rec eq_nat (n: nat) (m: nat) on n: bool ≝ 31 match n with 32 [ O ⇒ match m with [ O ⇒ true  _ ⇒ false ] 33  S n' ⇒ match m with [ S m' ⇒ eq_nat n' m'  _ ⇒ false ] 34 ]. 35 36 let rec remove_n_first_internal 37 (i: nat) (A: Type[0]) (l: list A) (n: nat) 38 on l ≝ 39 match l with 40 [ nil ⇒ [ ] 41  cons hd tl ⇒ 42 match eq_nat i n with 43 [ true ⇒ l 44  _ ⇒ remove_n_first_internal (S i) A tl n 45 ] 46 ]. 47 48 definition remove_n_first ≝ 49 λA: Type[0]. 50 λn: nat. 51 λl: list A. 52 remove_n_first_internal 0 A l n. 53 54 let rec foldi_from_until_internal 55 (A: Type[0]) (i: nat) (res: ?) (rem: list A) (m: nat) (f: nat → list A → A → list A) 56 on rem ≝ 57 match rem with 58 [ nil ⇒ res 59  cons e tl ⇒ 60 match geb i m with 61 [ true ⇒ res 62  _ ⇒ foldi_from_until_internal A (S i) (f i res e) tl m f 63 ] 64 ]. 65 66 definition foldi_from_until ≝ 67 λA: Type[0]. 68 λn: nat. 69 λm: nat. 70 λf: ?. 71 λa: ?. 72 λl: ?. 73 foldi_from_until_internal A 0 a (remove_n_first A n l) m f. 74 75 definition foldi_from ≝ 76 λA: Type[0]. 77 λn. 78 λf. 79 λa. 80 λl. 81 foldi_from_until A n (l) f a l. 82 83 definition foldi_until ≝ 84 λA: Type[0]. 85 λm. 86 λf. 87 λa. 88 λl. 89 foldi_from_until A 0 m f a l. 90 91 definition foldi ≝ 92 λA: Type[0]. 93 λf. 94 λa. 95 λl. 96 foldi_from_until A 0 (l) f a l. 16 97 17 98 definition hd ≝ … … 129 210 *) 130 211 131 include "ASM/FoldStuff.ma".132 133 212 let rec reduce_strong 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)  ≝ 136 match left return λx. x = right → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 137 [ nil ⇒ 138 match right return λy.  [ ]  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 139 [ nil ⇒ λnil_nil_prf. ? 140  cons hd tl ⇒ λnil_cons_absrd_prf. ? 141 ] 213 (A: Type[0]) (left: list A) (right: list A) 214 on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). \fst (\fst ret) = \fst (\snd ret) ≝ 215 match left with 216 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 142 217  cons hd tl ⇒ 143 match right return λy.  hd::tl  =  y  → Σret: ((list A) × (list A)) × ((list A) × (list A)).  \fst (\fst ret)  =  \fst (\snd ret)  with 144 [ nil ⇒ λcons_nil_absrd_prf. ? 145  cons hd' tl' ⇒ λcons_cons_prf. 146 let 〈commonl, commonr〉 ≝ eject … (reduce_strong A tl tl' ?) in ? (* 147 [ dp clr their_proof ⇒ ? (* 148 let 〈commonl, commonr〉 ≝ clr in ? *) 149 ]*) 150 ] 151 ] prf. 152 [ 5: normalize in cons_cons_prf; 153 destruct(cons_cons_prf) 154 assumption 155  2: normalize in nil_cons_absrd_prf; 156 destruct(nil_cons_absrd_prf) 157  3: normalize in cons_nil_absrd_prf; 158 destruct(cons_nil_absrd_prf) 159  4: 218 match right with 219 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 220  cons hd' tl' ⇒ 221 let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in 222 let 〈commonl, restl〉 ≝ cleft in 223 let 〈commonr, restr〉 ≝ cright in 224 〈〈hd :: commonl, restl〉, 〈hd' :: commonr, restr〉〉 225 ] 226 ]. 227 [ 1: normalize % 228  2: normalize % 229  3: normalize 230 generalize in match (sig2 … (reduce_strong A tl tl1)); 231 >p2 >p3 >p4 normalize in ⊢ (% → ?) 232 #HYP // 160 233 ] 161 234 qed. 162 163 axiom reduce_length:164 ∀A: Type[0].165 ∀left, right: list A.166 ∀prf:  left  =  right .167 \fst (\fst (reduce A left right)) = \fst (\snd (reduce A left right)).168 235 169 236 let rec map2_opt … … 527 594 ] 528 595 ]. 529 530 definition ltb ≝531 λm, n: nat.532 leb (S m) n.533 534 definition geb ≝535 λm, n: nat.536 ltb n m.537 538 definition gtb ≝539 λm, n: nat.540 leb n m.541 542 (* dpm: unless I'm being stupid, this isn't defined in the stdlib? *)543 let rec eq_nat (n: nat) (m: nat) on n: bool ≝544 match n with545 [ O ⇒ match m with [ O ⇒ true  _ ⇒ false ]546  S n' ⇒ match m with [ S m' ⇒ eq_nat n' m'  _ ⇒ false ]547 ].548 596 549 597 (* dpm: conflicts with library definitions
Note: See TracChangeset
for help on using the changeset viewer.