Changeset 1071 for src/ASM/Util.ma
 Timestamp:
 Jul 15, 2011, 2:40:40 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Util.ma
r1064 r1071 215 215 216 216 let rec reduce 217 (A: Type[0]) ( left: list A) (right: list A) on left ≝217 (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) on left ≝ 218 218 match left with 219 219 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 … … 222 222 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 223 223  cons hd' tl' ⇒ 224 let 〈cleft, cright〉 ≝ reduce A tl tl' in224 let 〈cleft, cright〉 ≝ reduce A B tl tl' in 225 225 let 〈commonl, restl〉 ≝ cleft in 226 226 let 〈commonr, restr〉 ≝ cright in … … 238 238 239 239 let rec reduce_strong 240 (A: Type[0]) ( left: list A) (right: list A)241 on left : Σret: ((list A) × (list A)) × ((list A) × (list A)). \fst (\fst ret) = \fst (\snd ret) ≝240 (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) 241 on left : Σret: ((list A) × (list A)) × ((list B) × (list B)). \fst (\fst ret) = \fst (\snd ret) ≝ 242 242 match left with 243 243 [ nil ⇒ 〈〈[ ], [ ]〉, 〈[ ], right〉〉 … … 246 246 [ nil ⇒ 〈〈[ ], left〉, 〈[ ], [ ]〉〉 247 247  cons hd' tl' ⇒ 248 let 〈cleft, cright〉 ≝ reduce_strong A tl tl' in248 let 〈cleft, cright〉 ≝ reduce_strong A B tl tl' in 249 249 let 〈commonl, restl〉 ≝ cleft in 250 250 let 〈commonr, restr〉 ≝ cright in … … 255 255  2: normalize % 256 256  3: normalize 257 generalize in match (sig2 … (reduce_strong A tl tl1));257 generalize in match (sig2 … (reduce_strong A B tl tl1)); 258 258 >p2 >p3 >p4 normalize in ⊢ (% → ?) 259 259 #HYP // … … 464 464 mapi_internal A B 0 f l. 465 465 466 let rec zip_pottier 467 (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) 468 on left ≝ 469 match left with 470 [ nil ⇒ [ ] 471  cons hd tl ⇒ 472 match right with 473 [ nil ⇒ [ ] 474  cons hd' tl' ⇒ 〈hd, hd'〉 :: zip_pottier A B tl tl' 475 ] 476 ]. 477 478 let rec zip_safe 479 (A: Type[0]) (B: Type[0]) (left: list A) (right: list B) (prf: left = right) 480 on left ≝ 481 match left return λx. x = right → list (A × B) with 482 [ nil ⇒ λnil_prf. 483 match right return λx. [ ] = x → list (A × B) with 484 [ nil ⇒ λnil_nil_prf. [ ] 485  cons hd tl ⇒ λnil_cons_absrd. ? 486 ] nil_prf 487  cons hd tl ⇒ λcons_prf. 488 match right return λx. hd::tl = x → list (A × B) with 489 [ nil ⇒ λcons_nil_absrd. ? 490  cons hd' tl' ⇒ λcons_cons_prf. 〈hd, hd'〉 :: zip_safe A B tl tl' ? 491 ] cons_prf 492 ] prf. 493 [ 1: normalize in nil_cons_absrd; 494 destruct(nil_cons_absrd) 495  2: normalize in cons_nil_absrd; 496 destruct(cons_nil_absrd) 497  3: normalize in cons_cons_prf; 498 @injective_S 499 assumption 500 ] 501 qed. 502 466 503 let rec zip (A: Type[0]) (B: Type[0]) (l: list A) (r: list B) on l: option (list (A × B)) ≝ 467 504 match l with
Note: See TracChangeset
for help on using the changeset viewer.