Changeset 2441 for src/Clight/frontend_misc.ma
 Timestamp:
 Nov 7, 2012, 6:02:50 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2438 r2441 75 75 match e with 76 76 [ None ⇒ None ? 77  Some x ⇒ f x ] = Some ? res → 77  Some x ⇒ f x ] = Some ? res → 78 78 ∃x. e = Some ? x ∧ f x = Some ? res. 79 79 #A #B #e #res #f cases e normalize nodelta 80 80 [ 1: #Habsurd destruct (Habsurd) 81  2: #a #Heq %{a} @conj >Heq @refl ] 81  2: #a #Heq %{a} @conj >Heq @refl ] 82 82 qed. 83 83 … … 330 330 lemma mem_append_backwards : ∀A:Type[0]. ∀elt : A. ∀l1,l2. (mem … elt l1) ∨ (mem … elt l2) → mem … elt (l1 @ l2) . 331 331 #A #elt #l1 #l2 #H elim (mem_append … elt l1 l2) #_ #H' @H' @H qed. 332 333 (* "Observational" equivalence on list implies concrete equivalence. Useful to 334 * prove equality from some reasoning on indexings. Needs a particular induction 335 * principle. *) 336 337 let rec double_list_ind 338 (A : Type[0]) 339 (P : list A → list A → Prop) 340 (base_nil : P [ ] [ ]) 341 (base_l1 : ∀hd1,l1. P (hd1::l1) [ ]) 342 (base_l2 : ∀hd2,l2. P [ ] (hd2::l2)) 343 (ind : ∀hd1,hd2,tl1,tl2. P tl1 tl2 → P (hd1 :: tl1) (hd2 :: tl2)) 344 (l1, l2 : list A) on l1 ≝ 345 match l1 with 346 [ nil ⇒ 347 match l2 with 348 [ nil ⇒ base_nil 349  cons hd2 tl2 ⇒ base_l2 hd2 tl2 ] 350  cons hd1 tl1 ⇒ 351 match l2 with 352 [ nil ⇒ base_l1 hd1 tl1 353  cons hd2 tl2 ⇒ 354 ind hd1 hd2 tl1 tl2 (double_list_ind A P base_nil base_l1 base_l2 ind tl1 tl2) 355 ] 356 ]. 357 358 lemma nth_eq_tl : 359 ∀A:Type[0]. ∀l1,l2:list A. ∀hd1,hd2. 360 (∀i. nth_opt A i (hd1::l1) = nth_opt A i (hd2::l2)) → 361 (∀i. nth_opt A i l1 = nth_opt A i l2). 362 #A #l1 #l2 @(double_list_ind … l1 l2) 363 [ 1: #hd1 #hd2 #_ #i elim i try /2/ 364  2: #hd1' #l1' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct 365  3: #hd2' #l2' #hd1 #hd2 #H lapply (H 1) normalize #Habsurd destruct 366  4: #hd1' #hd2' #tl1' #tl2' #H #hd1 #hd2 367 #Hind 368 @(λi. Hind (S i)) 369 ] qed. 370 371 372 lemma nth_eq_to_eq : 373 ∀A:Type[0]. ∀l1,l2:list A. (∀i. nth_opt A i l1 = nth_opt A i l2) → l1 = l2. 374 #A #l1 elim l1 375 [ 1: #l2 #H lapply (H 0) normalize 376 cases l2 377 [ 1: // 378  2: #hd2 #tl2 normalize #Habsurd destruct ] 379  2: #hd1 #tl1 #Hind * 380 [ 1: #H lapply (H 0) normalize #Habsurd destruct 381  2: #hd2 #tl2 #H lapply (H 0) normalize #Heq destruct (Heq) 382 >(Hind tl2) try @refl @(nth_eq_tl … H) 383 ] 384 ] qed. 385 386 (*  *) 387 (* General results on vectors. *) 388 (*  *) 389 390 (* copied from AssemblyProof, TODO get rid of the redundant stuff. *) 391 lemma Vector_O: ∀A. ∀v: Vector A 0. v ≃ VEmpty A. 392 #A #v generalize in match (refl … 0); cases v in ⊢ (??%? → ?%%??); // 393 #n #hd #tl #abs @⊥ destruct (abs) 394 qed. 395 396 lemma Vector_Sn: ∀A. ∀n.∀v:Vector A (S n). 397 ∃hd.∃tl.v ≃ VCons A n hd tl. 398 #A #n #v generalize in match (refl … (S n)); cases v in ⊢ (??%? → ??(λ_.??(λ_.?%%??))); 399 [ #abs @⊥ destruct (abs) 400  #m #hd #tl #EQ <(injective_S … EQ) %[@hd] %[@tl] // ] 401 qed. 402 403 lemma vector_append_zero: 404 ∀A,m. 405 ∀v: Vector A m. 406 ∀q: Vector A 0. 407 v = q@@v. 408 #A #m #v #q 409 >(Vector_O A q) % 410 qed. 411 412 corollary prod_vector_zero_eq_left: 413 ∀A, n. 414 ∀q: Vector A O. 415 ∀r: Vector A n. 416 〈q, r〉 = 〈[[ ]], r〉. 417 #A #n #q #r 418 generalize in match (Vector_O A q …); 419 #hyp 420 >hyp in ⊢ (??%?); 421 % 422 qed. 423 424 lemma vsplit_eq : ∀A. ∀m,n. ∀v : Vector A ((S m) + n). ∃v1:Vector A (S m). ∃v2:Vector A n. v = v1 @@ v2. 425 # A #m #n elim m 426 [ 1: normalize #v 427 elim (Vector_Sn ?? v) #hd * #tl #Eq 428 @(ex_intro … (hd ::: [[]])) @(ex_intro … tl) 429 >Eq normalize // 430  2: #n' #Hind #v 431 elim (Vector_Sn ?? v) #hd * #tl #Eq 432 elim (Hind tl) 433 #tl1 * #tl2 #Eq_tl 434 @(ex_intro … (hd ::: tl1)) 435 @(ex_intro … tl2) 436 destruct normalize // 437 ] qed. 438 439 lemma vsplit_zero: 440 ∀A,m. 441 ∀v: Vector A m. 442 〈[[]], v〉 = vsplit A 0 m v. 443 #A #m #v 444 elim v 445 [ % 446  #n #hd #tl #ih 447 normalize in ⊢ (???%); % 448 ] 449 qed. 450 451 lemma vsplit_zero2: 452 ∀A,m. 453 ∀v: Vector A m. 454 〈[[]], v〉 = vsplit' A 0 m v. 455 #A #m #v 456 elim v 457 [ % 458  #n #hd #tl #ih 459 normalize in ⊢ (???%); % 460 ] 461 qed. 462 463 lemma vsplit_eq2 : ∀A. ∀m,n : nat. ∀v : Vector A (m + n). ∃v1:Vector A m. ∃v2:Vector A n. v = v1 @@ v2. 464 # A #m #n elim m 465 [ 1: normalize #v @(ex_intro … (VEmpty ?)) @(ex_intro … v) normalize // 466  2: #n' #Hind #v 467 elim (Vector_Sn ?? v) #hd * #tl #Eq 468 elim (Hind tl) 469 #tl1 * #tl2 #Eq_tl 470 @(ex_intro … (hd ::: tl1)) 471 @(ex_intro … tl2) 472 destruct normalize // 473 ] qed. 474 475 (* This is not very nice. Note that this axiom was copied verbatim from ASM/AssemblyProof.ma. 476 * TODO sync with AssemblyProof.ma, in a better world we shouldn't have to copy all of this. *) 477 axiom vsplit_succ: 478 ∀A, m, n. 479 ∀l: Vector A m. 480 ∀r: Vector A n. 481 ∀v: Vector A (m + n). 482 ∀hd. 483 v = l@@r → (〈l, r〉 = vsplit ? m n v → 〈hd:::l, r〉 = vsplit ? (S m) n (hd:::v)). 484 485 axiom vsplit_succ2: 486 ∀A, m, n. 487 ∀l: Vector A m. 488 ∀r: Vector A n. 489 ∀v: Vector A (m + n). 490 ∀hd. 491 v = l@@r → (〈l, r〉 = vsplit' ? m n v → 〈hd:::l, r〉 = vsplit' ? (S m) n (hd:::v)). 492 493 lemma vsplit_prod2: 494 ∀A,m,n. 495 ∀p: Vector A (m + n). 496 ∀v: Vector A m. 497 ∀q: Vector A n. 498 p = v@@q → 〈v, q〉 = vsplit' A m n p. 499 #A #m 500 elim m 501 [ #n #p #v #q #hyp 502 >hyp <(vector_append_zero A n q v) 503 >(prod_vector_zero_eq_left A …) 504 @vsplit_zero2 505  #r #ih #n #p #v #q #hyp 506 >hyp 507 cases (Vector_Sn A r v) 508 #hd #exists 509 cases exists 510 #tl #jmeq >jmeq 511 @vsplit_succ2 [1: % 2: @ih % ] 512 ] 513 qed. 514 515 lemma vsplit_prod: 516 ∀A,m,n. 517 ∀p: Vector A (m + n). 518 ∀v: Vector A m. 519 ∀q: Vector A n. 520 p = v@@q → 〈v, q〉 = vsplit A m n p. 521 #A #m 522 elim m 523 [ #n #p #v #q #hyp 524 >hyp <(vector_append_zero A n q v) 525 >(prod_vector_zero_eq_left A …) 526 @vsplit_zero 527  #r #ih #n #p #v #q #hyp 528 >hyp 529 cases (Vector_Sn A r v) 530 #hd #exists 531 cases exists 532 #tl #jmeq >jmeq 533 @vsplit_succ [1: % 2: @ih % ] 534 ] 535 qed. 536 332 537 333 538 (*  *)
Note: See TracChangeset
for help on using the changeset viewer.