Changeset 2682 for src


Ignore:
Timestamp:
Feb 19, 2013, 7:24:20 PM (7 years ago)
Author:
campbell
Message:

Don't apply inv in after_n_steps to last state.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/labelSimulation.ma

    r2677 r2682  
    10211021    >shift_fst whd in match (seq_of_labeled_statement ?);
    10221022    cases (step_with_labels_partial … RG (State f s k e m) (State (\fst (label_function u0 f)) (\fst (label_statement s u)) k' e m) tr s2 (swl_state … K) EX)
    1023     #n #H %{(S n)} @(after_n_m 1 (S n) … H) % /2/
     1023    #n #H %{(S n)} @(after_n_m 1 (S n) … H) // % /2/
    10241024    #trx #sx * /3/
    10251025(* but for LScase it's just like the cases in step_with_labels_partial *)
  • src/common/Executions.ma

    r2487 r2682  
    6767  cases (step … s) [ #o #K * | 3: #m * ]
    6868  * #tr' #s'
    69   whd in ⊢ (% → ?); cases (inv s') [2: *]
     69  whd in ⊢ (% → ?);
    7070  #AW %{tr'} %{s'} %{AW}
    7171  lapply (refl ? (is_final … s')) cases (is_final … s') in ⊢ (???% → %);
  • src/common/SmallstepExec.ma

    r2669 r2682  
    6060   not (reducible to) a value.
    6161   
    62    An invariant is also asserted on every state other than the initial one.
     62   An invariant is also asserted on every intermediate state (i.e., everything
     63   other than the first and last states).
    6364
    6465   For example, we state a property to prove by something like
     
    103104let rec assert (b:bool) (P:Prop) on b ≝
    104105if b then P else False.
     106
     107let rec assert_nz (n:nat) (b:bool) (P:Prop) on n ≝
     108match n with
     109[ O ⇒ P
     110| _ ⇒ assert b P
     111].
    105112
    106113let rec after_aux (avs:await_value_stuff)
     
    114121  [ None ⇒
    115122    await_value avs (step ?? (avs_exec avs) (avs_g avs) s) (λtr',s.
    116       assert (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))
     123      assert_nz n' (avs_inv avs s) (after_aux avs n' s (tr ⧺ tr') P))
    117124  | _ ⇒ False
    118125  ]
    119126].
     127
     128lemma assert_nz_lift : ∀n,b,P,Q.
     129  (P → Q) →
     130  assert_nz n b P →
     131  assert_nz n b Q.
     132* [ /2/ | #n * [ normalize /2/ | #P #Q #_ * ] ]
     133qed.
    120134
    121135definition after_n_steps : nat →
     
    139153  * #tr'' #s''
    140154  whd in ⊢ (% → %);
    141   cases (avs_inv avs s'') [ 2: * ]
    142   whd in ⊢ (% → %);
     155  @assert_nz_lift
    143156  >Eapp_assoc @IH
    144157] qed.
     
    156169lemma after_n_m : ∀n,m,O,I,exec,g,inv,P,Q,s,s'.
    157170  after_n_steps m O I exec g s' inv Q →
     171  (notb (eqb m 0) → inv s') →
    158172  after_n_steps n O I exec g s inv (λtr1,s1. s' = s1 ∧ (∀tr'',s''. Q tr'' s'' → P (tr1⧺tr'') s'')) →
    159173  after_n_steps (n+m) O I exec g s inv P.
    160 #n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → % → %); generalize in match E0; elim n
    161 [ #tr #s #s' #H whd in ⊢ (% → %); * #E destruct #H2
     174#n #m #O #I #exec #g #inv #P #Q whd in ⊢ (? → ? → ? → ? → % → %); generalize in match E0; elim n
     175[ #tr #s #s' #H #INVs' whd in ⊢ (% → %); * #E destruct #H2
    162176  whd in H; <(E0_right tr) generalize in match E0 in H ⊢ %;
    163177  generalize in match s; -s
     
    168182    whd in ⊢ (% → %);
    169183    cases (step O I exec g s) [1,3: normalize //] * #tr'' #s'' whd in ⊢ (% → %);
    170     cases (inv s'') [2: * ]
     184    @assert_nz_lift
    171185    >Eapp_assoc @IH ]
    172 | #n' #IH #tr #s #s' #H whd in ⊢ (% → %);
     186| #n' #IH #tr #s #s' #H #INVs' whd in ⊢ (% → %);
    173187  cases (is_final … s) [2: #r * ]
    174188  whd in ⊢ (% → %);
    175189  cases (step O I exec g s) [1,3: normalize // ]
    176190  * #tr1 #s1 whd in ⊢ (% → %);
     191  cases n' in IH H ⊢ %; [ cases m in INVs' ⊢ %;
     192    [ #Is' #IH #H @IH [ // | * #H cases (H (refl ??)) ]
     193    | #m' #Is' #IH #H * #E destruct >Is' [ #X @(IH … H) [ @Is' | % // @X ] | % #E destruct ] ] ]
     194  #n'' #IH #H
    177195  cases (inv s1) [2:*]
    178   @IH @H
     196  @IH assumption
    179197] qed.
    180198
    181199(* Inversion lemmas. *)
     200
     201lemma assert_nz_inv : ∀n,b,P.
     202  assert_nz n b P →
     203  (n = 0 ∨ bool_to_Prop b) ∧ P.
     204* [ /3/ | #n * [ #P #p % /2/ @p | #P * ] ]
     205qed.
    182206
    183207lemma after_1_of_n_steps : ∀n,O,I,exec,g,inv,P,s.
     
    186210  is_final … exec g s = None ? ∧
    187211  step … exec g s = Value … 〈tr,s'〉 ∧
    188   bool_to_Prop (inv s') ∧
     212  (notb (eqb n 0) → bool_to_Prop (inv s')) ∧
    189213  after_n_steps n O I exec g s' inv (λtr'',s''. P (tr⧺tr'') s'').
    190214#n #O #I #exec #g #inv #P #s
     
    194218  cases (step … s)
    195219  [ #o #k *
    196   | * #tr #s' whd in ⊢ (% → ?); >E0_left <(E0_right tr) #AFTER
    197     %{tr} %{s'} cases (inv s') in AFTER ⊢ %; #AFTER % /3/ cases AFTER
     220  | * #tr #s' whd in ⊢ (% → ?); #ASSERT cases (assert_nz_inv … ASSERT) * #H #AFTER
     221    %{tr} %{s'} % [1,3: % [1,3: /2/ | *: >H /4 by notb_Prop, absurd, nmk, I/ ] |*: /2/ ]
    198222  | #m *
    199223  ]
     
    205229  ∃tr,s'. is_final … exec g s = None ? ∧
    206230    step ?? exec g s = Value … 〈tr,s'〉 ∧
    207     bool_to_Prop (inv s') ∧ P tr s'.
     231    P tr s'.
    208232#O #I #exec #g #inv #P #s #AFTER
    209233cases (after_1_of_n_steps … AFTER)
    210 #tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%[%]] // whd in FIN; >E0_right in FIN; //
     234#tr * #s' * * * #NF #STEP #INV #FIN %{tr} %{s'} % [%] // whd in FIN; >E0_right in FIN; //
    211235qed.
    212236
     
    477501| #m #IH #O #I #fx #g #s #trace #s' #EXEC
    478502  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
    479   @(after_n_m 1 … (IH … STEPS))
     503  @(after_n_m 1 … (IH … STEPS)) //
    480504  whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #E destruct %
    481505] qed.
     
    484508  exec_steps n O I fx g s = OK ? 〈trace,s'〉 →
    485509  all ? (λstr. inv (\fst str)) (tail … trace) →
    486   inv s' →
    487510  P (gather_trace ? trace) s' →
    488511  after_n_steps n O I fx g s inv P.
    489512#n elim n
    490513[ #O #I #fx #g #s #trace #s' #inv #P #EXEC whd in EXEC:(??%?); destruct
    491   #ALL #FI #p whd @p
     514  #ALL #p whd @p
    492515| #m #IH #O #I #fx #g #s #trace #s' #inv #P #EXEC
    493516  cases (exec_steps_S … EXEC) #NOTFINAL * #tr1 * #s1 * #tl * * #E1 #STEP #STEPS
    494517  destruct
    495   #ALL #FALL cut (bool_to_Prop (inv s1) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
     518  #ALL cut ((notb (eqb m 0) → bool_to_Prop (inv s1)) ∧ bool_to_Prop (all ? (λst. inv (\fst st)) (tail … tl)))
    496519  [ cases m in STEPS;
    497     [ whd in ⊢ (??%? → ?); #E destruct /2/
     520    [ whd in ⊢ (??%? → ?); #E destruct % [ * #H cases (H (refl ??)) | /2/ ]
    498521    | #m' #STEPS cases (exec_steps_S … STEPS) #_ * #tr'' * #s'' * #tl'' * * #E #_ #_ destruct
    499       whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; /2/
     522      whd in ALL:(?%); cases (inv s1) in ALL ⊢ %; [ /2/ | * ]
    500523    ]
    501524  ] * #i1 #itl
    502   #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ??))
     525  #p @(after_n_m 1 … (λtr,s. P (tr1⧺tr) s) … (IH … STEPS itl ?))
    503526  [ @p
    504   | @FALL
    505   | whd >NOTFINAL whd >STEP whd >i1 whd %{(refl ??)} #tr'' #s'' #p' @p'
     527  | @i1
     528  | whd >NOTFINAL whd >STEP whd %{(refl ??)} #tr'' #s'' #p' @p'
    506529  ]
    507530] qed.
Note: See TracChangeset for help on using the changeset viewer.