Changeset 3405 for LTS/Language.ma


Ignore:
Timestamp:
Dec 19, 2013, 9:19:50 PM (6 years ago)
Author:
piccolo
Message:

closed some daemons

File:
1 edited

Legend:

Unmodified
Added
Removed
  • LTS/Language.ma

    r3404 r3405  
    10621062*)
    10631063
     1064lemma memb_append_l22 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A.
     1065¬ (x ∈ l1) → x∈ l1 @ l2 = (x ∈ l2).
     1066#A #x #l1 elim l1 normalize // #y #ys #IH #l2 cases(x==y)
     1067normalize [*] @IH
     1068qed.
     1069
     1070lemma memb_append_l12 : ∀A : DeqSet.∀x : A.∀l1,l2 : list A.
     1071¬ (x ∈ l2) → x∈ l1 @ l2 = (x ∈ l1).
     1072#A #x #l1 elim l1
     1073[ #l2 #H whd in match (append ???); @not_b_to_eq_false @Prop_notb >H % ]
     1074#y #ys #IH #l2 #H1 whd in match (memb ???); >IH //
     1075qed.
     1076
     1077
     1078lemma lookup_ok_append : ∀p,p',l,f,env_it.
     1079lookup p p' l f = return env_it → ∃l1,l2. l = l1 @ [env_it] @ l2 ∧
     1080f_name … env_it = f.
     1081#p #p' #l elim l [ #f #env_it normalize #EQ destruct]
     1082#x #xs #IH #f #env_it whd in ⊢ (??%? → ?); @eq_function_name_elim
     1083[ #EQ destruct(EQ) normalize nodelta whd in ⊢ (???% → ?); #EQ destruct
     1084  %{(nil ?)} %{xs} /2/
     1085| #Hno_f normalize nodelta #EQ_env_it cases(IH … EQ_env_it)
     1086  #l1 * #l2 * #EQ1 #EQ2 %{(x :: l1)} %{l2} >EQ1 /2/
     1087]
     1088qed.
     1089(*
     1090lemma foldr_append :
     1091  ∀A,B:Type[0]. ∀l1, l2 : list A. ∀f:A → B → B. ∀seed. foldr ?? f seed (l1 @ l2) = foldr ?? f (foldr ?? f seed l2) l1.
     1092#A #B #l1 elim l1 //
     1093#hd #tl #Hind #l2 #f #seed normalize >Hind @refl
     1094qed.
     1095*)
     1096
     1097lemma foldr_map_append :
     1098  ∀A,B:Type[0]. ∀l1, l2 : list A.
     1099   ∀f:A → list B. ∀seed.
     1100    foldr ?? (λx,acc. (f x) @ acc) seed (l1 @ l2) =
     1101     append ? (foldr ?? (λx,acc. (f x) @ acc) (nil ?) l1)
     1102       (foldr  ?? (λx,acc. (f x) @ acc) seed l2).
     1103#A #B #l1 elim l1 normalize // /3 by eq_f, trans_eq/
     1104qed.
     1105
     1106
    10641107lemma trans_env_ok : ∀p : state_params.∀ prog.
    10651108no_duplicates_labels … prog →
     
    10741117same_fresh_map_on dom m (lab_map … info) ∧ same_to_keep_on dom keep (lab_to_keep … info).
    10751118#p * #env #main @pair_elim * whd in match trans_prog; normalize nodelta
    1076 @pair_elim generalize in match O; (*probably needs invariant *) elim env
     1119@pair_elim generalize in match O; elim env
    10771120[ #fresh1 * #env' #fresh #x #_ #t_prog #m #keep #_ #_ #f #env_it normalize in ⊢ (% → ?);  #ABS destruct]
    10781121* #hd_sig #hd_lab #hd_code #tail #IH #fresh1 * #env' #fresh * #m' #keep'
     
    10911134  [ whd in ⊢ (??%?); @eq_function_name_elim [2: * #H @⊥ @H %] #_ normalize nodelta
    10921135    @eq_f cases hd_sig // ] >EQ_trans_code % [% [ % [ % [% // whd in ⊢ (??%?); >(\b (refl …)) %] % ] % | whd
    1093     #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false) [2: cases daemon (*per Hhd_lab*)]
    1094     normalize nodelta cases daemon (* needs lemma on maps *)]
    1095   | whd cases daemon (*using lab_to_keep_in_domain and H *)
     1136    #x #Hx whd in ⊢ (??%?); >(? : (x == hd_lab) = false)
     1137    [2: inversion(x==hd_lab) // #EQx_hdlab cases Hhd_lab -Hhd_lab #Hhd_lab cases Hhd_lab
     1138        >memb_append_l1 // <(\P EQx_hdlab) >Hx // ]
     1139    normalize nodelta @get_element_append_l1 % #H1  cases daemon (* needs lemma on maps using EQtail *)]
     1140  | whd #x #Hx >memb_append_l12 // inversion(memb ???) // #ABS @(memb_no_duplicates_append … x … H)
     1141    //  cases daemon (*using EQtail in a non trivial way*)
    10961142  ]
    10971143| #Hf #Henv_it cases(IH … no_dup_tail … Henv_it)
     
    11051151     [ whd in ⊢ (??%?); @eq_function_name_elim [ #ABS >ABS in Hf; * #H @⊥ @H %]
    11061152        #_ normalize nodelta assumption ]
    1107    % [2: #x #Hx <same_to_keep
    1108  
    1109    
    1110    
    1111     [ >EQ_trans_code % | >EQ_trans_code
    1112     [ >EQ_trans_code % | >EQ_trans_code whd in ⊢ (??%?);
    1113       cases(eqb_true … (a_call hd_lab) hd_lab) #_ #H1 >(H1 (refl …)) // ]]
    1114 
    1115   #EQt_prog
     1153   % [2: #x #Hx <same_to_keep // @memb_append_l22
     1154        inversion(memb ???) // #ABS lapply(lab_to_keep_in_domain … (eq_true_to_b … ABS))
     1155        #ABS1 @(memb_no_duplicates_append … x … H) //
     1156        cases(lookup_ok_append … Henv_it) #l1 * #l2 * #EQ1 #EQ2 destruct(EQ1 EQ2)
     1157        >foldr_map_append >memb_append_l2 // >foldr_map_append >memb_append_l1 //
     1158        whd in match (foldr ?????); @orb_Prop_r >memb_append_l1 // >Hx % ]
     1159   % [2: #x #Hx <same_fresh_map // (*usare get_element_append_r1 *) cases daemon ]
     1160   % // % // % // <EQ_get_el (*usare get_element_append*) cases daemon
     1161]
     1162qed.   
    11161163
    11171164
     
    12171264    [1,2,3,4,5,7: (*assurdi da fare*) cases daemon] #f' #act_p' #opt_l' #i' #_
    12181265    #EQcode_st1' #EQclean #EQstore #EQio #EQ destruct(EQ)
     1266    xxxxx
    12191267    cut(∃env_it',n.lookup p p (env … t_prog) f = return env_it' ∧
    12201268          t_code … (call_post_trans … (f_body … env_it) n (nil ?)) = f_body … env_it' ∧
Note: See TracChangeset for help on using the changeset viewer.