Changeset 1571 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 28, 2011, 1:39:49 PM (8 years ago)
Author:
mulligan
Message:

small changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1570 r1571  
    248248qed.
    249249
    250 axiom current_instruction_cost_non_zero:
     250lemma current_instruction_cost_non_zero:
    251251  ∀s: Status.
    252     current_instruction_cost s > 0.
     252    0 ≤ current_instruction_cost s.
     253  //
     254qed.
     255
     256lemma le_monotonic_plus:
     257  ∀m, n, o: nat.
     258    m ≤ n → m + o ≤ n + o.
     259  #m #n #o #hyp
     260  elim o
     261  [ //
     262  | #o' #ind_hyp
     263    <plus_n_Sm <plus_n_Sm
     264    @le_S_S
     265    assumption
     266  ]
     267qed.
     268
     269lemma le_plus_to_minus_l:
     270  ∀m, n, o: nat.
     271    n ≤ o → m ≤ o - n → m + n ≤ o.
     272  #m #n #o #le_hyp #hyp
     273  generalize in match (le_monotonic_plus m (o - n) n hyp);
     274  generalize in match (plus_minus_m_m o n le_hyp);
     275  #assm <assm in ⊢ (% → ?); #finished assumption
     276qed.
    253277   
    254 axiom minus_m_n_gt_o_0_le_n_m:
     278lemma minus_m_n_le_n_m:
    255279  ∀m, n, o.
    256   m - n = o → o > 0 → n ≤ m.
     280    m - n = o → o > 0 → n ≤ m.
     281  #m #n #o #eq_hyp
     282  cases o
     283  [ #absrd normalize in absrd; @le
     284  normalize in ⊢ (% → ?);
     285  <eq_hyp in ⊢ (% → ?);
     286  #lt_hyp
     287  generalize in match (le_plus_to_minus_l 1 n m ? lt_hyp);
     288  [1: /2/ |
     289qed.
     290 
    257291
    258292let rec compute_max_trace_label_label_cost_is_ok
Note: See TracChangeset for help on using the changeset viewer.