# Changeset 3403

Ignore:
Timestamp:
Dec 19, 2013, 6:42:35 PM (6 years ago)
Message:

File:
1 edited

Unmodified
Removed
• ## LTS/Language.ma

 r3402 qed. lemma get_element_append_l1 : ∀A,B. ∀l1,l2: associative_list A B. ∀x. ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) → get_element ?? (l1@l2) x = get_element … l1 x. #A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ] #l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize [ * #H @⊥ @H % ] #H @IH assumption qed. definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝ λx.〈a_non_functional_label x,S x〉. qed. lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False. #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); inversion (x == x1) normalize nodelta [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % | #_ @IH // ] qed. lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) → (∀x.x ∈ l3 → x ∈ dom3) → same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l → same_to_keep_on dom2 l2 l. #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2 #x #Hx inversion (x ∈ l2) [ #EQkeep

memb_append_l2 // >memb_append_l1 // ] >memb_append_l2 // >memb_append_l1 // >Hx // | #EQno_keep

memb_append_l2 // >memb_append_l1 // >Hx // | @sym_eq @memb_not_append [2: @memb_not_append //] [ memb_append_l2 | >memb_append_l1] // >Hx // | @sub_set3 >H1 // | @sub_set1 >H1 // ] ] ] qed. lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l. no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) → (∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) → same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l → same_fresh_map_on … dom2 l2 l. #dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1 whd #x #Hx

memb_append_l2 // >memb_append_l1 // >Hx //] >get_element_append_r [ >get_element_append_l1 // ] % #K [ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS [ memb_append_l2 | >memb_append_l1 ] // >Hx // qed. lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p. ∀x,n,l. qed. lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A . no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False. #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???); inversion (x == x1) normalize nodelta [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H % | #_ @IH // ] qed. lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ. #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?); #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 // [2: #x #Hx whd in H2; inversion(x ∈ lab_to_keep … (call_post_trans …)) [ #EQkeep

memb_append_l2 // >memb_append_l2 // ] whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r >memb_append_l2 // >memb_append_l2 // >Hx % | #EQno_keep

memb_append_l2 // >memb_append_l2 // >Hx % ] @sym_eq @memb_not_append [| @memb_not_append //] inversion(x ∈ lab_to_keep ??) // #Hlab @⊥ lapply(lab_to_keep_in_domain ????? (eq_true_to_b … Hlab)) #ABS cases no_dup #_ * #_ #ABS1 [ @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // | memb_append_l2 // >ABS % [2: whd  in match (get_labels_of_code ??) in H2; change with ([?;?]@?) in match (?::?) in H2; associative_append >associative_append in ⊢ (??%? → ?); #H2 @(same_to_keep_on_append … H2) // [ >append_nil whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ] #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r [ >memb_append_l1 | >memb_append_l2 ] // @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |3: -H2 whd in match (get_labels_of_code ??) in H1; change with ([?;?]@?) in match (?::?) in H1; associative_append change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?); associative_append in ⊢ (??%? → ?); #H1 @(same_fresh_map_on_append … H1) // [ >append_nil >associative_append // ] #x whd in match (memb ???); inversion(x == ltrue) [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue % | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse) [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse % | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r >domain_of_associative_list_append in Hx; #H cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ] // @(lab_map_in_domain … (eq_true_to_b … H2)) ] >Hx % ] |3: whd in H1; #x #Hx

memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l2 // >Hx // ] whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >get_element_append_r [ >get_element_append_r // % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #no_dup3 @(memb_no_duplicates_append … x … (no_duplicates_append_r … no_dup3)) // ] % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #dup3 @(memb_no_duplicates_append … x … dup3) // >memb_append_l2 // >Hx // ] cases no_dup #_ * #A1 #_ % #A2 memb_append_l2 // >memb_append_l2 // @Hx ] cases no_dup #A1 #_ % #A2 memb_cons // >memb_append_l2 // >memb_append_l2 // @Hx ] |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |] ] normalize nodelta >IH2 // [2: #x #Hx

memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l1 // >Hx // ] whd in ⊢ (???%); >memb_append_l2 [2: >memb_append_l1] // cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) |3: (*no duplicates ok *) cases daemon [2: whd  in match (get_labels_of_code ??) in H2; change with ([?;?]@?) in match (?::?) in H2; domain_of_associative_list_append #H cases(memb_append … H) [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta normalize #EQ destruct | #H1 @orb_Prop_r @orb_Prop_r @(lab_map_in_domain … (eq_true_to_b … H1)) ] |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l ] >m_return_bind >IH1 // [2: #x #Hx

memb_cons // >memb_cons // >memb_append_l1 // @Hx ] >memb_append_l1 cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) |3: cases daemon (*come sopra*) [2:  whd  in match (get_labels_of_code ??) in H2; change with ([?;?]@?) in match (?::?) in H2; change with ([ ] @ ?) in match (lab_to_keep ??) in H2; >associative_append in H2 : (??%?); #H2 @(same_to_keep_on_append … H2) // [ #x *] #x #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2] // @(lab_to_keep_in_domain … (eq_true_to_b … Hx)) |3:  whd  in match (get_labels_of_code ??) in H1; change with ([?;?]@?) in match (?::?) in H1; change with ([?;?]@?) in match (?::?::?) in H1 : (??%?); @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ] // @(lab_map_in_domain … (eq_true_to_b … Hx)) |4: cases no_dup #_ * #_ @no_duplicates_append_l ]

Note: See TracChangeset for help on using the changeset viewer.