Changeset 1509


Ignore:
Timestamp:
Nov 15, 2011, 5:21:28 PM (8 years ago)
Author:
mulligan
Message:

i hate subtraction over the nats

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1506 r1509  
     1
    12include "ASM/ASMCosts.ma".
    23include "ASM/WellLabeled.ma".
     
    206207    pred (m - n) = m - n - 1.
    207208  #m #n
    208   elim m
     209  cases m
    209210  [ #proof
    210211    cases(lt_to_not_zero … proof)
    211   | #m' #ind_hyp #proof
     212  | #m' #proof
    212213    normalize in ⊢ (???%)
    213214    cases n
    214215    [ normalize //
    215216    | #n' normalize
    216       <ind_hyp
     217      cases(m' - n')
     218      [ %
     219      | #Sm_n'
     220        normalize //
     221      ]
     222    ]
     223  ]
     224qed.
     225
     226lemma succ_m_plus_one:
     227  ∀m: nat.
     228    S m = m + 1.
     229  #m
     230  elim m
     231  [ %
    217232  | #m' #ind_hyp
     233    normalize
     234    <ind_hyp
     235    %
     236  ]
     237qed.
     238
     239lemma minus_m_n_minus_minus_plus_1:
     240  ∀m, n: nat.
     241  ∀proof: n < m.
     242    m - n = (m - n - 1) + 1.
     243  #m
     244  elim m
     245  [ #n #proof
     246    cases(lt_to_not_zero … proof)
     247  | #m' #ind_hyp #n
    218248    normalize
    219249    cases n
    220250    [ normalize //
    221     | #n' normalize
     251    | #n' #proof normalize
     252      <ind_hyp
     253      [ %
     254      | @le_S_S_to_le
     255        assumption
     256      ]
     257    ]
     258  ]
     259qed.
    222260
    223261lemma plus_minus_rearrangement:
     
    228266  #m #n #o
    229267  elim m
    230   [1: #proof_n_m
     268  [1: #proof_n_m 
    231269      cases(lt_to_not_zero … proof_n_m)
    232270  |2: #m' #ind_hyp
     
    237275          assumption
    238276      |1: >eq_minus_S_pred
    239           [2: /2/
    240           |3: normalize
    241               normalize in proof_n_m';
    242               elim(le_S … proof_n_m')
    243               @le_S
    244           |1:
     277          >pred_minus_1
     278          [1: >(succ_m_plus_one (m' - n))
     279              >(associative_plus (m' - n) 1 (o - m' - 1))
     280              <commutative_plus in match (1 + (o - m' - 1));
     281              <(minus_m_n_minus_minus_plus_1 o m') in match (o - m' - 1 + 1)
     282              [1: >ind_hyp
     283                [1: %
     284                |2: normalize
     285                    normalize in proof_m_o;
     286                    @le_S_S_to_le
     287                    @(le_S ? ? proof_m_o)
     288                |3: cases daemon (* XXX: problem here *)
     289                ]
     290              |2: normalize in proof_m_o;
     291                  normalize
     292                  @le_S_S_to_le
     293                  @(le_S (S (S m')) o proof_m_o)
     294              ]
     295          |2: normalize
     296              normalize in proof_m_o;
     297              @le_S_S_to_le
     298              @(le_S (S (S m')) o proof_m_o)
    245299          ]
     300      ]
     301  ]
     302qed.
    246303
    247304lemma status_execution_progresses_processor_clock:
Note: See TracChangeset for help on using the changeset viewer.