Changeset 3401
- Timestamp:
- Dec 6, 2013, 8:58:20 PM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
LTS/Language.ma
r3400 r3401 85 85 ]. 86 86 87 (* 87 88 lemma eq_instructions_elim : ∀ P : bool → Prop.∀p,i1,i2.(i1 = i2 → P true) → 88 89 (i1 ≠ i2 → P false) → P (eq_instructions p i1 i2). 89 90 #P #p #i1 elim i1 90 [ * normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ 91 (* destruct(EQ) gives no choice for ID(instructions_discr) *) cases daemon ] 92 cases daemon (*TODO*) 93 qed. 91 [* normalize [/2/ ] #x [|*: #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ 92 lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') 93 | #rt * normalize [2: #rt' cases (dec_eq … rt rt') #H [>(\b H) | >(\bf H) ] /2/ 94 #_ #K @K % #abs lapply (eq_to_jmeq ??? abs) #abs' destruct(abs') @(absurd ?? H) //] 95 [|*: #x #y #z [2,3: #w1 #w2 [#w3] |4,5: #w1]] #_ #H2 @H2 % #EQ 96 lapply (eq_to_jmeq ??? EQ) #EQ' destruct(EQ') 97 | cases daemon (*TODO*) 98 qed. 99 *) 94 100 95 101 record env_params : Type[1] ≝ … … 393 399 (* ---------------------------------------- *) ⊢ 394 400 eqb_list D p1 p2 ≡ eqb X p1 p2. 395 check NonFunctionalLabel396 401 397 402 definition associative_list : DeqSet → Type[0] → Type[0] ≝ … … 410 415 | cons x xs ⇒ if (a == \fst x) then \snd x else get_element … xs a 411 416 ]. 412 417 418 let rec domain_of_associative_list (A :DeqSet) (B : Type[0]) (l: associative_list A B) on l : list A ≝ 419 match l with 420 [ nil ⇒ [] 421 | cons x xs ⇒ \fst x :: domain_of_associative_list … xs 422 ]. 423 424 lemma get_element_append_l: 425 ∀A,B. ∀l1,l2: associative_list A B. ∀x. 426 x ∈ domain_of_associative_list … l1 → 427 get_element … (l1@l2) x = get_element … l1 x. 428 #A #B #l1 elim l1 normalize [ #l2 #x * ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) 429 #H [ >(\b H) | >(\bf H) ] normalize /2/ 430 qed. 431 432 lemma get_element_append_r: 433 ∀A,B. ∀l1,l2: associative_list A B. ∀x. 434 ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l1)) → 435 get_element ?? (l1@l2) x = get_element … l2 x. 436 #A #B #l1 elim l1 normalize [ #l2 #x // ] #hd #tl #IH #l2 #x cases (dec_eq … x (\fst hd)) 437 #H [ >(\b H) | >(\bf H) ] normalize /2 by/ * #K cases (K I) 438 qed. 439 413 440 definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ 414 441 λx.〈a_non_functional_label x,S x〉. … … 755 782 ] 756 783 qed. 757 784 785 lemma lab_map_in_domain: ∀p.∀i: Instructions p. 786 ∀x,n,l. 787 x ∈ domain_of_associative_list … (lab_map p (call_post_trans … i n l)) → 788 x ∈ get_labels_of_code … i. 789 cases daemon 790 qed. 791 758 792 lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . 759 793 no_duplicates … (l1 @ l2) → x ∈ l1 → x ∈ l2 → False. … … 814 848 >Hx % 815 849 ] 816 |3: whd in H1; #x #Hx <H1 (*no duplicates *) cases daemon 850 |3: whd in H1; #x #Hx <H1 851 [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l2 // >Hx // ] 852 whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); 853 >get_element_append_r [ >get_element_append_r // % #K lapply (lab_map_in_domain … K) 854 #K2 cases no_dup; #_ * #_ #no_dup3 855 @(memb_no_duplicates_append … x … (no_duplicates_append_r … no_dup3)) // ] 856 % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #dup3 857 @(memb_no_duplicates_append … x … dup3) // >memb_append_l2 // >Hx // ] 858 cases no_dup #_ * #A1 #_ % #A2 <A2 in A1; * #K @K >memb_append_l2 // 859 >memb_append_l2 // @Hx ] cases no_dup #A1 #_ % #A2 <A2 in A1; * #K @K 860 >memb_cons // >memb_append_l2 // >memb_append_l2 // @Hx 817 861 |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] 818 862 ] 819 820 863 normalize nodelta >IH2 // 821 [2: #x #Hx whd in H2; (*come sopra*) cases daemon 864 [2: #x #Hx <H2 865 [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l1 // >Hx // ] 866 whd in ⊢ (???%); >memb_append_l2 [2: >memb_append_l1] // 867 cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) 822 868 |3: (*no duplicates ok *) cases daemon 823 |4: (* come sopra *) cases daemon869 |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l 824 870 ] 825 871 >m_return_bind >IH1 // 826 [2,3,4: cases daemon (*come sopra*) ] 872 [2: #x #Hx <H2 873 [2: >memb_cons // >memb_cons // >memb_append_l1 // @Hx ] 874 >memb_append_l1 875 cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) 876 |3: cases daemon (*come sopra*) 877 |4: cases no_dup #_ * #_ @no_duplicates_append_l 878 ] 827 879 >m_return_bind normalize nodelta whd in H1; <H1 828 880 [2: whd in match (get_labels_of_code ??); whd in match (memb ???); … … 832 884 whd in match (memb ???); >(\b (refl …)) % ] 833 885 whd in match (get_element ????); @eq_costlabel_elim normalize nodelta 834 [ #ABS cases daemon (* no duplicates*) ] #_ whd in match (get_element ????);886 [ #ABS cases daemon (*CSC: FALSO!! *) ] #_ whd in match (get_element ????); 835 887 >(\b (refl …)) normalize nodelta >(\b (refl …)) % 836 888 |*: cases daemon (*TODO*)
Note: See TracChangeset
for help on using the changeset viewer.