Changeset 3406 for LTS/Language.ma


Ignore:
Timestamp:
Dec 23, 2013, 10:22:24 AM (6 years ago)
Author:
piccolo
Message:
 
File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3405 r3406  
    883883qed.
    884884
    885  
     885lemma eq_a_non_functional_label :
     886∀c1,c2.c1 == c2 → a_non_functional_label c1 == a_non_functional_label c2.
     887#c1 #c2 #EQ cases(eqb_true DEQNonFunctionalLabel c1 c2) #H1 #_ lapply(H1 (eq_true_to_b … EQ)) -EQ
     888#EQ destruct >(\b (refl …)) @I
     889qed.
    886890 
    887891lemma inverse_call_post_trans : ∀p : instr_params.∀i1 : Instructions p.∀n : ℕ.
     
    9991003      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
    10001004      >(\b (refl …)) %
    1001 |*: cases daemon (*TODO*)
    1002 ]
     1005| #loop #ltrue #i1 #lfalse #i2 #IH1 #IH2 #n #no_dup #m #keep #info #l whd in ⊢ (??%? → ?);
     1006  #EQ destruct(EQ) whd in match (get_labels_of_code ??); #fresh_map #keep_on
     1007  whd in ⊢ (??%?); >IH2
     1008  [ normalize nodelta >IH1
     1009    [ >m_return_bind <fresh_map [2: @orb_Prop_l >(\b (refl …)) % ]
     1010      whd in match (get_element ????);
     1011      inversion(a_non_functional_label ltrue == a_non_functional_label lfalse)
     1012      #Hltrue normalize nodelta
     1013      [ cases no_dup whd in match (memb ???);
     1014        cases(eqb_true … (a_non_functional_label ltrue) (a_non_functional_label lfalse))
     1015        #H1 #_ lapply(H1 Hltrue) #EQ destruct(EQ) >(\b (refl …)) * #ABS @⊥ @ABS % ]
     1016      whd in match (get_element ????); >(\b (refl …)) normalize nodelta >(\b (refl …))
     1017      <fresh_map [2: @orb_Prop_r @orb_Prop_l >(\b (refl …)) % ]
     1018      whd in match (get_element ????); >(\b (refl …)) normalize nodelta
     1019      >(\b (refl …)) %
     1020    | change with ([?;?]@?@?) in keep_on : (?%??); change with ((nil ?) @ ? @ ?) in keep_on : (??%?);
     1021      @(same_to_keep_on_append … keep_on) // [ #x * | #x /2 by lab_to_keep_in_domain/ ]
     1022    | change with ([?;?]@?@?) in fresh_map : (?%%?); @(same_fresh_map_on_append … fresh_map)
     1023      /2 by lab_map_in_domain/ #x whd in match (memb ???); inversion(x==lfalse) #Hlfalse
     1024      normalize nodelta
     1025      [ #_ @orb_Prop_r whd in match (memb ???); >Hlfalse %
     1026      | whd in match (memb ???); inversion(x==ltrue) #Hltrue normalize nodelta [2: *] #_
     1027        @orb_Prop_l >Hltrue %
     1028      ]
     1029    | %
     1030    | cases no_dup #_ * #_ /2/
     1031    |
     1032    ]
     1033  | change with ([?;?]@?@?) in keep_on : (?%??); <associative_append in keep_on;
     1034    <(append_nil … (?@?)) <(append_nil … (?@?)) in ⊢ (??%? → ?);
     1035    >associative_append in ⊢ (??%? → ?); #keep_on  @(same_to_keep_on_append … keep_on)
    10031036qed.
    10041037
Note: See TracChangeset for help on using the changeset viewer.