Changeset 2897


Ignore:
Timestamp:
Mar 16, 2013, 9:08:21 PM (4 years ago)
Author:
campbell
Message:

Minor tidying.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/MeasurableToStructured.ma

    r2896 r2897  
    137137λS,s1,s2,tlr,stack_cost,currentfn,initial.
    138138  maximum (update_stacksize_info stack_cost (mk_stacksize_info initial 0) (extract_call_ud_from_tlr S s1 s2 tlr currentfn)).
    139 
    140 (* A bit of mucking around because we're going to build a will_return in Type[0].
    141    In principle we could drop the alternative form of will_return entirely, but
    142    time pressures don't really allow for that. *)
    143 record cft (ge:genv) (n:nat) (s:state) (hd:state×trace) (rem:list (state × trace)) (s':state) (EX:?) : Type[0] ≝ {
    144   cft_tr : trace;
    145   cft_s  : state;
    146   cft_EV : eval_statement ge s = Value ??? 〈cft_tr,cft_s〉;
    147   cft_EX : exec_steps n … RTLabs_fullexec ge cft_s = OK ? 〈rem,s'〉;
    148   cft_E  : make_flat_trace ge (S n) s (hd::rem) s' EX = ft_step ??? s cft_tr cft_s cft_EV (make_flat_trace ge n cft_s rem s' cft_EX)
    149 }.
    150 
    151 lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.
    152   ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉.
    153   cft ge n s hd trace s' EX.
    154 #ge #n #s #hd #trace #s' #EX
    155 lapply (refl ? (eval_statement ge s))
    156 cases (eval_statement ge s) in ⊢ (???% → ?);
    157 [ #o #k | 3: #m ]
    158 [ 1,2: #EV @⊥ cases (exec_steps_S … EX) #NF * #tr * #s2 * #tl * * #E1 destruct
    159   change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct
    160 ] * #tr #s1 #EV
    161 @(mk_cft … tr s1 EV)
    162 [ cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
    163   change with (eval_statement ??) in ⊢ (??%? → ?);
    164   >EV in ⊢ (% → ?); #E destruct #EX' @EX'
    165 | whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
    166   >EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?);
    167   #ST' whd in ⊢ (??%?); %
    168 ] qed.
    169139
    170140lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX.
     
    251221generalize in match (cs_callee ??);
    252222whd in match (cs_classify ??); cases (next_instruction f) //
    253 qed.
    254 
    255 (* TODO move*)
    256 lemma All2_tail : ∀A,B,P,a,b.
    257   All2 A B P a b →
    258   All2 A B P (tail A a) (tail B b).
    259 #A #B #P * [2: #ah #at] * [2,4: #bh #bt]
    260 * //
    261223qed.
    262224
     
    745707
    746708
    747 (* TODO move *)
    748 lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX.
    749   length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n.
    750 #ge #n0 elim n0
    751 [ #s1 #trace #s2 #EX %
    752 | #n #IH #s1 #trace #s2 #EX
    753   cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct
    754   cases (cons_flat_trace ?????? EX)
    755   #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH
    756 ] qed.
    757709
    758710
     
    855807    * //
    856808  ]
    857 ]]
    858 
     809]
     810
  • src/RTLabs/RTLabs_partial_traces.ma

    r2895 r2897  
    8888] qed.
    8989
     90(* Use a record to keep things in Type[0] overall, because in
     91   MeasurableToStructured we're going to build a will_return in Type[0].
     92   In principle we could drop the alternative form of will_return entirely, but
     93   time pressures don't really allow for that. *)
     94record cft (ge:genv) (n:nat) (s:state) (hd:state×trace) (rem:list (state × trace)) (s':state) (EX:?) : Type[0] ≝ {
     95  cft_tr : trace;
     96  cft_s  : state;
     97  cft_EV : eval_statement ge s = Value ??? 〈cft_tr,cft_s〉;
     98  cft_EX : exec_steps n … RTLabs_fullexec ge cft_s = OK ? 〈rem,s'〉;
     99  cft_E  : make_flat_trace ge (S n) s (hd::rem) s' EX = ft_step ??? s cft_tr cft_s cft_EV (make_flat_trace ge n cft_s rem s' cft_EX)
     100}.
     101
    90102lemma cons_flat_trace : ∀ge,n,s,hd,trace,s'.
    91103  ∀EX:exec_steps (S n) … RTLabs_fullexec ge s = return 〈hd::trace,s'〉.
    92   Σs1. ∃ST,EX'. make_flat_trace ge (S n) s (hd::trace) s' EX = ft_step ??? s (\snd hd) s1 ST (make_flat_trace ge n s1 trace s' EX').
     104  cft ge n s hd trace s' EX.
    93105#ge #n #s #hd #trace #s' #EX
    94106lapply (refl ? (eval_statement ge s))
     
    98110  change with (eval_statement ??) in ⊢ (??%? → ?); >EV #E destruct
    99111] * #tr #s1 #EV
    100 %{s1}
    101 cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
    102 change with (eval_statement ??) in ⊢ (??%? → ?); >EV in ⊢ (% → ?); #E destruct #EX'
    103 %{EV} %{EX'}
    104 whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
    105 >EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?);
    106 #ST' whd in ⊢ (??%?); %
    107 qed.
     112@(mk_cft … tr s1 EV)
     113[ cases (exec_steps_S … EX) #NF * #tr2 * #s2 * #tl * * #E1 destruct
     114  change with (eval_statement ??) in ⊢ (??%? → ?);
     115  >EV in ⊢ (% → ?); #E destruct #EX' @EX'
     116| whd in ⊢ (??%?); generalize in ⊢ (??(?%)?);
     117  >EV in ⊢ (???% → ??(match % with [_⇒?|_⇒?|_⇒?]?)?);
     118  #ST' whd in ⊢ (??%?); %
     119] qed.
    108120
    109121let rec length_flat_trace O I ge s (t:flat_trace O I ge s) on t : nat ≝
     
    112124| ft_step _ _ _ _ t' ⇒ S (length_flat_trace … t')
    113125].
     126
     127lemma make_flat_trace_length : ∀ge,n,s1,trace,s2,EX.
     128  length_flat_trace io_out io_in ge s1 (make_flat_trace ge n s1 trace s2 EX) = n.
     129#ge #n0 elim n0
     130[ #s1 #trace #s2 #EX %
     131| #n #IH #s1 #trace #s2 #EX
     132  cases (exec_steps_S … EX) #_ * #tr * #s' * #tl * * #E1 #E2 #E3 destruct
     133  cases (cons_flat_trace ?????? EX)
     134  #tr'' #s'' #ST'' #EX'' #E >E whd in ⊢ (??%?); @eq_f @IH
     135] qed.
    114136
    115137
  • src/utilities/lists.ma

    r2800 r2897  
    109109| #hda #tla #IH * [ * ] #hdb #tlb * #p #H % [ %{hda} // | /2/ ]
    110110] qed.
     111
     112lemma All2_tail : ∀A,B,P,a,b.
     113  All2 A B P a b →
     114  All2 A B P (tail A a) (tail B b).
     115#A #B #P * [2: #ah #at] * [2,4: #bh #bt]
     116* //
     117qed.
    111118
    112119let rec map_All (A,B:Type[0]) (P:A → Prop) (f:∀a. P a → B) (l:list A) (H:All A P l) on l : list B ≝
Note: See TracChangeset for help on using the changeset viewer.