Changeset 2644 for src/common


Ignore:
Timestamp:
Feb 7, 2013, 4:42:54 PM (7 years ago)
Author:
campbell
Message:

Commit some work on FEMeasurable before trying to do something nicer
than exec_inf_aux/split_trace.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/FEMeasurable.ma

    r2618 r2644  
    6464λS,t,s. match t with [ e_step _ s' _ ⇒ s = s' | _ ⇒ False ].
    6565
     66(* TODO: too many of these lemmas, slim it down*)
     67
     68lemma split_trace_S : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
     69  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S n) = Some ? 〈a,b〉 →
     70  ∃a'. a = 〈tr,s〉::a' ∧
     71  ((is_final … fx g s = None ? ∧ split_trace … (exec_inf_aux ?? fx g (step … fx g s)) n = Some ? 〈a',b〉) ∨
     72  (∃r. is_final … fx g s = Some ? r ∧ n = 0 ∧ a' = [ ] ∧ b = e_stop … tr r s)).
     73#fx #g #tr #s #n #a #b
     74>exec_inf_aux_unfold whd in ⊢ (??(????%?)? → ?);
     75cases (is_final … s)
     76[ whd in ⊢ (??%? → ?); cases (split_trace ?????)
     77  [ #E whd in E:(??%%); destruct
     78  | * #a' #b' #E whd in E:(??%%); destruct
     79    %{a'} %{(refl ??)} %1 %{(refl ??)} %
     80  ]
     81| #r cases n [2:#n'] whd in ⊢ (??%? → ?); #E destruct
     82  %{[ ]} %{(refl ??)} %2 %{r} /4/
     83] qed.
     84
     85lemma split_trace_S' : ∀fx:trans_system io_out io_in. ∀g,s,n,a,b.
     86  split_trace … (exec_inf_aux ?? fx g (step … fx g s)) (S n) = Some ? 〈a,b〉 →
     87  ∃tr,s'. step … fx g s = Value … 〈tr,s'〉 ∧
     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 #s #n #a #b
     92cases (step … fx g s)
     93[ #o #i whd in ⊢ (??%? → ?); #E destruct
     94| * #tr #s' #split %{tr} %{s'} %{(refl …)} @split_trace_S @split
     95| #err #E whd in E:(??%%); destruct
     96] qed.
     97
     98lemma split_trace_1 : ∀fx:trans_system io_out io_in. ∀g,tr,s,a,b.
     99  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) 1 = Some ? 〈a,b〉 →
     100  a = [〈tr,s〉] ∧
     101  ((is_final … fx g s = None ? ∧ b = exec_inf_aux ?? fx g (step … fx g s)) ∨
     102  (∃r. is_final … fx g s = Some ? r ∧ b = e_stop … tr r s)).
     103#fx #g #tr #s #a #b #split
     104cases (split_trace_S … split)
     105#a' * #E1 *
     106[ * #notfinal #split' whd in split':(??%?); destruct %{(refl ??)}
     107  %1 %{notfinal} %
     108| * #r * * * #final #_ #E2 #E3 destruct %{(refl ??)}
     109  %2 %{r} %{final} %
     110] qed.
     111 
     112
     113lemma split_trace_SS : ∀fx:trans_system io_out io_in. ∀g,tr,s,n,a,b.
     114  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr,s〉)) (S (S n)) = Some ? 〈a,b〉 →
     115  ∃a'. a = 〈tr,s〉::a' ∧
     116  is_final … fx g s = None ? ∧
     117  ∃tr',s'. step … fx g s = Value … 〈tr',s'〉 ∧
     118  split_trace … (exec_inf_aux ?? fx g (Value … 〈tr',s'〉)) (S n) = Some ? 〈a',b〉.
     119#fx #g #tr #s #n #a #b #splitSS
     120cases (split_trace_S … splitSS)
     121#a' * #E1 *
     122[ * #notfinal #splitS %{a'} % [ %{E1} @notfinal ]
     123  cases (step … s) in splitS ⊢ %;
     124  [ #o #i #E whd in E:(??%%); destruct
     125  | * #tr' #s' #splitS %{tr'} %{s'} %{(refl ??)} @splitS
     126  | #m  #E whd in E:(??%%); destruct
     127  ]
     128| * #r * * * #final #En #Ea #Eb destruct
     129] qed.
     130
     131(* WIP commented out
    66132lemma prefix_preserved :
    67133  ∀MS:meas_sim.
     
    69135  ∀INV:ms_inv MS g1 g2.
    70136  ∀max_allowed_stack.
    71   ∀trace,trace',s1,s1'.
    72   trace_starts ? trace s1 →
    73   trace_starts ? trace' s1' →
     137  ∀s1,s1',tr,tr'.
    74138  ms_rel MS g1 g2 INV s1 s1' →
     139 
     140  let trace ≝ (exec_inf_aux ?? (pcs_exec … (ms_C1 MS)) g1 (Value … 〈tr,s1〉)) in
     141  let trace' ≝ (exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr',s1'〉)) in
     142 
    75143  ∀m,prefix,suffix.
    76   split_trace ? trace m = Some ? 〈prefix,suffix〉 →
     144  split_trace trace m = Some ? 〈prefix,suffix〉 →
    77145  le (max_stack (pcs_to_cs (ms_C1 MS) ? (ms_stack MS … INV)) prefix) max_allowed_stack →
     146
    78147  ∃m',prefix',suffix'.
    79   split_trace ? trace' m' = Some ? 〈prefix',suffix'〉 ∧
    80   le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
    81   ∃s2,s2'. trace_starts ? suffix s2 ∧ trace_starts ? suffix' s2' ∧
     148    split_trace … trace' m' = Some ? 〈prefix',suffix'〉 ∧
     149    le (max_stack (pcs_to_cs (ms_C2 MS) ? (ms_stack MS … INV)) prefix') max_allowed_stack ∧
     150 
     151  ∃s2,s2',tr2,tr2'.
     152    suffix = exec_inf_aux ?? (pcs_exec …  (ms_C1 MS)) g1 (Value … 〈tr2,s2〉) ∧
     153    suffix' = exec_inf_aux ?? (pcs_exec … (ms_C2 MS)) g2 (Value … 〈tr2',s2'〉) ∧
    82154    ms_rel MS g1 g2 INV s2 s2'.
     155* #C1 #C2 #compiled #inv #stack #rel #sim_normal #sim_call_return #sim_cost #sim_init
     156#g1 #g2 #INV #max #s1 #s1' #tr #tr' #REL
     157letin trace ≝ (exec_inf_aux ?????)
     158letin trace' ≝ (exec_inf_aux ?????)
     159#m0
     160@(nat_elim1 m0)
     161*
     162[ #_ #prefix #suffix #split whd in split:(??%?); destruct
     163  #max_ok %{0} %{[]} %{trace'}
     164  % [ % // | %{s1} %{s1'} %{tr} %{tr'} /3/ ]
     165| *
     166  [ (* m = 1; just extracts the current state *)
     167    #_ #prefix #suffix #split #max_ok
     168    cases (split_trace_1 … split) #E1 #foo
     169    %{1} %{[〈tr',s1'〉]} %{(exec_inf_aux … (step … s1'))}
     170    % [ %
     171 #m #IH #prefix #suffix #split #max_ok
     172  (* clean up first step? *)
     173  cases (true_or_false_Prop … (pcs_labelled … s1))
     174  [ #CS cases (split_trace_S … split) #trace1 * #Etrace *
     175    [ * #notfinal #split1
     176    lapply (sim_cost … REL CS)
     177    [ 3: whd in match (after_n_steps ????? s1 ??);
     178      >(?:is_final ???? s1 = None ?) [ whd in ⊢ ((% → ?) → ?);
     179lapply (refl ? (pcs_classify … s1)) cases (pcs_classify … s1) in ⊢ (???% → ?);
     180[
     181| #CL
    83182
    84183theorem measured_subtrace_preserved :
     
    94193* * * * #split1 #split2 #subtrace_ok #terminates #max_ok
    95194
    96 
     195*)
Note: See TracChangeset for help on using the changeset viewer.