Changeset 2670 for src


Ignore:
Timestamp:
Feb 15, 2013, 11:27:59 AM (7 years ago)
Author:
campbell
Message:

Clean up from recent commits.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2669 r2670  
    7878
    7979(* TODO: obs eq *)
    80 
    81 definition trace_starts : ∀S. execution S io_out io_in → S → Prop ≝
    82 λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].
    83 
    84 (* TODO: too many of these lemmas, slim it down*)
    85 
    86 lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
    87   split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →
    88   ∃a'. a = 〈tr,s〉::a' ∧
    89   ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨
    90   (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).
    91 #fx #g #tr #s #n #a #b
    92 >exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);
    93 cases (is_final … s)
    94 [ whd in ⊢ (??%? → ?); cases (split_trace ?????)
    95   [ #E whd in E:(??%%); destruct
    96   | * #a' #b' #E whd in E:(??%%); destruct
    97     %{a'} %{(refl ??)} %1 %{(refl ??)} %
    98   ]
    99 | #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct
    100   %{[ ]} %{(refl ??)} %2 %{r} /4/
    101 ] qed.
    102 
    103 lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.
    104   split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →
    105   ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧
    106   ∃a'. a = 〈tr,s'〉::a' ∧
    107   ((is_final … fx g s' = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s')) n = Some ? 〈a',b〉) ∨
    108   (∃r. is_final … fx g s' = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s')).
    109 #fx #g #s #n #a #b
    110 cases (step … fx g s)
    111 [ #o #i whd in ⊢ (??%? → ?); #E destruct
    112 | * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split
    113 | #err #E whd in E:(??%%); destruct
    114 ] qed.
    115 
    116 lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.
    117   split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →
    118   a = [〈tr,s〉] ∧
    119   ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨
    120   (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).
    121 #fx #g #tr #s #a #b #split
    122 cases (split_trace_S … split)
    123 #a' * #E1 *
    124 [ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}
    125   %1 %{notfinal} %
    126 | * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}
    127   %2 %{r} %{final} %
    128 ] qed.
    129  
    130 
    131 lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
    132   split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →
    133   ∃a'. a = 〈tr,s〉::a' ∧
    134   is_final … fx g s = None ? ∧
    135   ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧
    136   split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.
    137 #fx #g #tr #s #n #a #b #splitSS
    138 cases (split_trace_S … splitSS)
    139 #a' * #E1 *
    140 [ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]
    141   cases (step … s) in splitS ⊢ %;
    142   [ #o #i #E whd in E:(??%%); destruct
    143   | * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS
    144   | #m  #E whd in E:(??%%); destruct
    145   ]
    146 | * #r * * * #final #En #Ea #Eb destruct
    147 ] qed.
    14880
    14981lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current.
     
    344276  measurable (ms_C1 MS) p1 m n stack_cost max →
    345277  ∃m',n'. measurable (ms_C2 MS) p2 m' n' stack_cost max.
    346 * #C1 #C2 #compiled #inv #rel #sim_normal #sim_call_return #sim_cost #sim_init
    347 #p1 #p2 #m #n #stack_cost #max #compiled
    348 whd in ⊢ (% → ?); letin C1' ≝ (mk_classified_system C1 ????) letin g1 ≝ (make_global ?? C1 ?)
    349 * #prefix * #suffix * #subtrace * #remainder
    350 * * * * #split1 #split2 #subtrace_ok #terminates #max_ok
    351 
    352 *)
     278
  • src/common/Measurable.ma

    r2669 r2670  
    7777qed.
    7878
    79 (* TODO: move*)
    80 lemma max_O_n : ∀n. max O n = n.
    81 * //
    82 qed.
    83 
    84 lemma max_n_O : ∀n. max n O = n.
    85 * //
    86 qed.
    87 
    88 lemma associative_max : associative nat max.
    89 #n #m #o normalize
    90 @(leb_elim n m)
    91 [ normalize @(leb_elim m o) normalize #H1 #H2
    92   [ >(le_to_leb_true n o) /2/
    93   | >(le_to_leb_true n m) //
    94   ]
    95 | normalize @(leb_elim m o) normalize #H1 #H2
    96   [ %
    97   | >(not_le_to_leb_false … H2)
    98     >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/
    99   ]
    100 ] qed.
    101 
    10279
    10380lemma max_stack_steps : ∀C,trace,a,m.
     
    11693] qed.
    11794
    118 (*
    119 lemma max_stack_step : ∀C,a,m,tr,s.
    120   m ≤ \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉).
    121 #C #a #m #tr #s
    122 whd in match (measure_stack_aux ???);
    123 generalize in match (cs_stack C s); cases (cs_classify C s) normalize
    124 #f @(leb_elim m) normalize #H /2/
    125 qed.
    126 
    127 lemma max_stack_steps : ∀C. ∀am. ∀trace.
    128   \snd am ≤ \snd (foldl … (measure_stack_aux C) am trace).
    129 #C * #a #m #trace
    130 @foldl_inv
    131 [ * #a' #m' * #tr #s #H @(transitive_le … H) @max_stack_step
    132 | //
    133 ] qed.
    134 
    135 lemma max_stack_step' : ∀C,a,m,a',m',tr,s.
    136   a ≤ a' → m ≤ m' →
    137   \snd (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \snd (measure_stack_aux C 〈a',m'〉 〈tr,s〉).
    138 #C #a #m #a' #m' #tr #s #H1 #H2
    139 whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);
    140 generalize in match (cs_stack C s); cases (cs_classify C s) #f
    141 whd in ⊢ (?(??%)(??%));
    142 [ @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'-f I)) /2/ ]
    143 | 2,4,5: @to_max /2 by max_r, max_l/
    144 | @to_max [ @(transitive_le … m') /2/ | @(transitive_le … (a'+f I)) /2/ ]
    145 ] qed.
    146 
    147 lemma max_stack_step'' : ∀C,a,m,a',m',tr,s.
    148   a ≤ a' →
    149   \fst (measure_stack_aux C 〈a,m〉 〈tr,s〉) ≤ \fst (measure_stack_aux C 〈a',m'〉 〈tr,s〉).
    150 #C #a #m #a' #m' #tr #s #H1
    151 whd in match (measure_stack_aux ???);whd in match (measure_stack_aux ???);
    152 generalize in match (cs_stack C s); cases (cs_classify C s) #f
    153 whd in ⊢ (?%%); /2/
    154 qed.
    155 
    156 lemma max_stack_steps' : ∀C. ∀trace,am,am'.
    157   \fst am ≤ \fst am' → \snd am ≤ \snd am' →
    158   \snd (foldl … (measure_stack_aux C) am trace) ≤ \snd (foldl … (measure_stack_aux C) am' trace).
    159 #C #trace elim trace
    160 [ * #a #m * #a' #m' #H1 #H2 @H2
    161 | * #tr #s #tl #IH * #a #m * #a' #m' #H1 #H2 @IH [ @max_stack_step'' // | @max_stack_step' // ]
    162 ] qed.
    163 
    164 lemma max_stack_append_l : ∀C,ex1,ex2.
    165   max_stack C ex1 ≤ max_stack C (ex1@ex2).
    166 #C #ex1 #ex2 whd in ⊢ (??%);
    167 whd in match (measure_stack ? (ex1@ex2));
    168 >foldl_append
    169 @max_stack_steps
    170 qed.
    171 
    172 lemma max_stack_append_r : ∀C,ex1,ex2.
    173   max_stack C ex2 ≤ max_stack C (ex1@ex2).
    174 #C #ex1 #ex2 whd in ⊢ (??%);
    175 whd in match (measure_stack ? (ex1@ex2));
    176 >foldl_append
    177 @max_stack_steps' //
    178 qed.
    179 *)(*
    180 lemma max_stack_append : ∀C,ex1,ex2.
    181   max (max_stack C ex1) (max_stack C ex2) = max_stack C (ex1@ex2).
    182 #C #ex1 #ex2
    183 whd in match (max_stack ??); whd in match (max_stack ? (ex1@ex2));
    184 whd in match (measure_stack ??); whd in match (measure_stack ? (ex1@ex2));
    185 generalize in match 〈O,O〉; elim ex1
    186 [ * #a #m whd in ⊢ (??(?%?)%); >max_stack_steps
    187 
    188 elim ex1
    189 [ #ex2 >max_O_n %
    190 | * #tr #s #tl #IH #ex2
    191   whd in match (max_stack ??); whd in match (measure_stack ??);
    192   lapply (refl ? (measure_stack_aux C 〈O,O〉 〈tr,s〉))
    193   cases (measure_stack_aux ???) in ⊢ (???% → %);
    194   #a #m #M
    195  
    196  #ex2
    197 @le_to_le_to_eq
    198 [ @to_max //
    199 |
    200  whd in ⊢ (???%);
    201 
    202 whd in match (measure_stack ? (ex1@ex2));
    203 >foldl_append
    204 @max_stack_steps' //
    205 *)
    20695lemma max_stack_append : ∀C,c1,ex1,ex2.
    20796  max (max_stack C c1 ex1) (max_stack C (stack_after C c1 ex1) ex2) = max_stack C c1 (ex1@ex2).
  • src/utilities/extranat.ma

    r2286 r2670  
    6161[ @H
    6262| @(transitive_le … H) @(transitive_le … (not_le_to_lt … H')) //
     63] qed.
     64
     65lemma max_O_n : ∀n. max O n = n.
     66* //
     67qed.
     68
     69lemma max_n_O : ∀n. max n O = n.
     70* //
     71qed.
     72
     73lemma associative_max : associative nat max.
     74#n #m #o normalize
     75@(leb_elim n m)
     76[ normalize @(leb_elim m o) normalize #H1 #H2
     77  [ >(le_to_leb_true n o) /2/
     78  | >(le_to_leb_true n m) //
     79  ]
     80| normalize @(leb_elim m o) normalize #H1 #H2
     81  [ %
     82  | >(not_le_to_leb_false … H2)
     83    >(not_le_to_leb_false n o) // @lt_to_not_le @(transitive_lt … m) /2/
     84  ]
    6385] qed.
    6486
Note: See TracChangeset for help on using the changeset viewer.