Changeset 3403 for LTS/Language.ma


Ignore:
Timestamp:
Dec 19, 2013, 6:42:35 PM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3402 r3403  
    438438qed.
    439439
     440lemma get_element_append_l1 :
     441 ∀A,B. ∀l1,l2: associative_list A B. ∀x.
     442  ¬ (bool_to_Prop (x ∈ domain_of_associative_list … l2)) →
     443   get_element ?? (l1@l2) x = get_element … l1 x.
     444#A #B #l1 elim l1 normalize [2: #x #xs #IH #l2 #a #H >IH // ]
     445#l2 elim l2 // #y #ys #IH #a normalize cases(a == \fst y) normalize
     446[ * #H @⊥ @H % ] #H @IH assumption
     447qed.
     448   
    440449definition fresh_nf_label : ℕ → NonFunctionalLabel × ℕ ≝
    441450λx.〈a_non_functional_label x,S x〉.
     
    752761qed.
    753762
     763lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
     764no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
     765#A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
     766inversion (x == x1) normalize nodelta
     767[ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
     768| #_ @IH //
     769]
     770qed.
     771
     772
     773lemma same_to_keep_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l.
     774no_duplicates … (dom1@dom2@dom3) → (∀x.x ∈ l1 → x ∈ dom1) →
     775(∀x.x ∈ l3 → x ∈ dom3) →
     776same_to_keep_on (dom1@dom2@dom3) (l1@l2@l3) l →
     777same_to_keep_on dom2 l2 l.
     778#dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #sub_set1 #sub_set3 #H2
     779#x #Hx inversion (x ∈ l2)
     780 [ #EQkeep <H2 [> memb_append_l2 // >memb_append_l1 // ]
     781   >memb_append_l2 // >memb_append_l1 // >Hx //
     782 | #EQno_keep <H2
     783   [2: >memb_append_l2 // >memb_append_l1 // >Hx //
     784   | @sym_eq @memb_not_append [2: @memb_not_append //]
     785   [ <associative_append in no_dup; #no_dup ]
     786   lapply(memb_no_duplicates_append … x … no_dup) #H
     787   inversion(memb ???) // #H1 cases H
     788   [1,4: [>memb_append_l2 | >memb_append_l1] // >Hx //
     789   | @sub_set3 >H1 //
     790   | @sub_set1 >H1 //
     791   ]
     792   ]
     793 ]
     794qed.
     795
     796lemma same_fresh_map_on_append : ∀dom1,dom2,dom3,l1,l2,l3,l.
     797no_duplicates … (dom1 @dom2 @ dom3) → (∀x.x ∈ domain_of_associative_list … l1 → x ∈ dom1) →
     798(∀x.x ∈ domain_of_associative_list … l3 → x ∈ dom3) →
     799same_fresh_map_on … (dom1 @dom2 @dom3) (l1 @l2 @ l3) l →
     800same_fresh_map_on … dom2 l2 l.
     801#dom1 #dom2 #dom3 #l1 #l2 #l3 #l #no_dup #subset1 #subset3 whd in ⊢ (% → ?); #H1
     802whd #x #Hx <H1
     803[2: >memb_append_l2 // >memb_append_l1 // >Hx //]
     804>get_element_append_r [ >get_element_append_l1 // ] % #K
     805[ lapply(subset3 … K) | lapply(subset1 … K) ] #ABS
     806[ <associative_append in no_dup; #no_dup] @(memb_no_duplicates_append … x … no_dup)
     807// [>memb_append_l2 | >memb_append_l1 ] // >Hx //
     808qed.
     809
     810
    754811lemma lab_to_keep_in_domain : ∀p.∀i : Instructions p.
    755812∀x,n,l.
     
    826883qed.
    827884
    828 lemma memb_no_duplicates_append : ∀A : DeqSet.∀x.∀l1,l2 : list A .
    829 no_duplicates … (l1 @ l2) → x ∈  l1 → x ∈ l2 → False.
    830 #A #x #l1 elim l1 // #x1 #xs #IH #l2 * #H1 #H2 whd in match (memb ???);
    831 inversion (x == x1) normalize nodelta
    832 [ #H3 #_ #H4 >memb_append_l2 in H1; [2: <(\P H3) @H4 ] * #H @H %
    833 | #_ @IH //
    834 ]
    835 qed.
     885 
    836886 
    837887lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
     
    868918  #no_dup #m #keep * #gen_lab #t_code #fresh #lab_map #lab_keep #l whd in ⊢ (??%? → ?);
    869919  #EQ destruct(EQ) #H1 #H2 whd in ⊢ (??%?); >IH3 //
    870   [2: #x #Hx whd in H2; inversion(x ∈ lab_to_keep … (call_post_trans …))
    871     [ #EQkeep <H2 [ >memb_append_l2 // >memb_append_l2 // ]
    872       whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r >memb_append_l2 //
    873       >memb_append_l2 // >Hx %
    874     | #EQno_keep <H2
    875       [2: whd in match (get_labels_of_code ??); @orb_Prop_r @orb_Prop_r
    876           >memb_append_l2 // >memb_append_l2 // >Hx % ] @sym_eq @memb_not_append
    877          [| @memb_not_append //] inversion(x ∈ lab_to_keep ??) // #Hlab @⊥
    878          lapply(lab_to_keep_in_domain ????? (eq_true_to_b … Hlab)) #ABS     
    879          cases no_dup #_ * #_ #ABS1
    880          [ @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 //
    881          | <associative_append in ABS1; #ABS1       
    882            @(memb_no_duplicates_append … x … ABS1) // >memb_append_l2 // >ABS %
     920  [2: whd  in match (get_labels_of_code ??) in H2;
     921      change with ([?;?]@?) in match (?::?) in H2;
     922      <associative_append in H2; <associative_append
     923      <(append_nil … (?@?)) <associative_append in ⊢ (??%? → ?);
     924      <(append_nil … (?@?)) in ⊢ (??%? → ?); >associative_append
     925      >associative_append in ⊢ (??%? → ?); #H2
     926      @(same_to_keep_on_append … H2) // [ >append_nil
     927      whd in ⊢ (??%); whd in no_dup:(??%); >associative_append // ]
     928      #x #Hx cases (memb_append … Hx) -Hx #Hx @orb_Prop_r @orb_Prop_r
     929      [ >memb_append_l1 | >memb_append_l2 ] //
     930      @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
     931  |3: -H2 whd in match (get_labels_of_code ??) in H1;
     932      change with ([?;?]@?) in match (?::?) in H1;
     933      <associative_append in H1; <associative_append     
     934      <(append_nil … (?@?)) >associative_append
     935      change with ([?;?]@?) in match (?::?::?) in ⊢ (??%? → ?);
     936      <associative_append in ⊢ (??%? → ?);
     937      <associative_append in ⊢ (??%? → ?);
     938      <(append_nil … (?@?)) in ⊢ (??%? → ?);
     939      >associative_append in ⊢ (??%? → ?); #H1
     940      @(same_fresh_map_on_append … H1) //
     941      [ >append_nil >associative_append // ]
     942      #x whd in match (memb ???); inversion(x == ltrue)
     943      [ #Hltrue normalize nodelta #_ whd in match (memb ???); >Hltrue %
     944      | #Hltrue normalize nodelta whd in match (memb ???); inversion(x == lfalse)
     945         [ #Hlfalse #_ @orb_Prop_r @orb_Prop_l >Hlfalse %
     946         | #Hlfalse normalize nodelta #Hx @orb_Prop_r @orb_Prop_r
     947           >domain_of_associative_list_append in Hx; #H
     948           cases(memb_append … H) #H2 [ >memb_append_l1 | >memb_append_l2 ]
     949           // @(lab_map_in_domain … (eq_true_to_b … H2))
    883950         ]
    884          >Hx %
    885     ]
    886   |3: whd in H1; #x #Hx <H1
    887     [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l2 // >Hx // ]
    888     whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%); >(\bf ?) [ whd in ⊢ (???%);
    889     >get_element_append_r [ >get_element_append_r // % #K lapply (lab_map_in_domain … K)
    890     #K2 cases no_dup; #_ * #_ #no_dup3
    891     @(memb_no_duplicates_append … x … (no_duplicates_append_r … no_dup3)) // ]
    892     % #K lapply (lab_map_in_domain … K) #K2 cases no_dup; #_ * #_ #dup3
    893     @(memb_no_duplicates_append … x … dup3) // >memb_append_l2 // >Hx // ]
    894     cases no_dup #_ * #A1 #_ % #A2 <A2 in A1; * #K @K >memb_append_l2 //
    895     >memb_append_l2 // @Hx ] cases no_dup #A1 #_ % #A2 <A2 in A1; * #K @K
    896     >memb_cons // >memb_append_l2 // >memb_append_l2 // @Hx
     951      ]
    897952  |4: cases no_dup #_ * #_ #H @no_duplicates_append_r [2: @(no_duplicates_append_r … H) |]
    898953  ]
    899954  normalize nodelta >IH2 //
    900   [2: #x #Hx <H2
    901     [2: >memb_cons // >memb_cons // >memb_append_l2 // >memb_append_l1 // >Hx // ]
    902     whd in ⊢ (???%); >memb_append_l2 [2: >memb_append_l1] //
    903     cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*)
    904   |3: (*no duplicates ok *) cases daemon
     955  [2: whd  in match (get_labels_of_code ??) in H2;
     956   change with ([?;?]@?) in match (?::?) in H2;
     957   <associative_append in H2; #H2
     958   @(same_to_keep_on_append … H2) // #x #Hx [ @orb_Prop_r @orb_Prop_r ]
     959   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
     960  |3: whd  in match (get_labels_of_code ??) in H1;
     961   change with ([?;?]@?) in match (?::?) in H1;
     962   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
     963   <associative_append in H1; <associative_append in ⊢ (??%? → ?); #H1
     964   @(same_fresh_map_on_append … H1) // [2: /2 by lab_map_in_domain/ ]
     965   #x >domain_of_associative_list_append #H cases(memb_append … H)
     966   [ whd in ⊢ (??%? → ?%); cases(x == ltrue) // normalize nodelta
     967     whd in ⊢ (??%? → ?%); cases(x == lfalse) // normalize nodelta
     968     normalize #EQ destruct
     969   | #H1 @orb_Prop_r @orb_Prop_r
     970     @(lab_map_in_domain … (eq_true_to_b … H1))
     971   ]
    905972  |4: cases no_dup #_ * #_ #K lapply (no_duplicates_append_r … K) @no_duplicates_append_l
    906973  ]
    907974  >m_return_bind >IH1 //
    908   [2: #x #Hx <H2
    909     [2: >memb_cons // >memb_cons // >memb_append_l1 // @Hx ]
    910     >memb_append_l1
    911     cases daemon (*CSC: strange goal here; do we need a lemma? but is the goal true?*) 
    912   |3: cases daemon (*come sopra*)
     975  [2:  whd  in match (get_labels_of_code ??) in H2;
     976   change with ([?;?]@?) in match (?::?) in H2;
     977   change with ([ ] @ ?) in match (lab_to_keep ??) in H2;
     978   >associative_append in H2 : (??%?); #H2
     979   @(same_to_keep_on_append … H2) // [ #x *] #x #Hx cases(memb_append … Hx)
     980   -Hx #Hx [ >memb_append_l1 | >memb_append_l2] //
     981   @(lab_to_keep_in_domain … (eq_true_to_b … Hx))
     982  |3:  whd  in match (get_labels_of_code ??) in H1;
     983   change with ([?;?]@?) in match (?::?) in H1;
     984   change with ([?;?]@?) in match (?::?::?) in H1 : (??%?);
     985    @(same_fresh_map_on_append … H1) // #x >domain_of_associative_list_append
     986    #Hx cases(memb_append … Hx) -Hx #Hx [ >memb_append_l1 | >memb_append_l2 ]
     987    // @(lab_map_in_domain … (eq_true_to_b … Hx))
    913988  |4: cases no_dup #_ * #_ @no_duplicates_append_l
    914989  ]
Note: See TracChangeset for help on using the changeset viewer.