Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1929 r1946  
    33include alias "arithmetics/nat.ma".
    44include alias "basics/logic.ma".
    5    
     5
    66let rec traverse_code_internal
    77  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
     
    1616  [ O ⇒ λprogram_size_refl. empty_map CostTag nat
    1717  | S program_size' ⇒ λprogram_size_refl.
    18     deplet 〈carry, new_program_counter'〉 as NEW_PC' ≝ half_add 16 (bitvector_of_nat 16 1) program_counter in
     18    let new_program_counter' ≝ add 16 (bitvector_of_nat 16 1) program_counter in
    1919    let cost_mapping ≝ traverse_code_internal code_memory cost_labels new_program_counter' program_size' ? in
    2020    match lookup_opt … program_counter cost_labels return λx. x = lookup_opt … program_counter cost_labels → Σcost_map: ?. ? with
     
    2222    | Some lbl ⇒ λlookup_refl.
    2323      let cost ≝ block_cost code_memory program_counter cost_labels in
    24         add … cost_mapping lbl cost
     24        cic:/matita/cerco/common/Identifiers/add.fix(0,2,2) ?? cost_mapping lbl cost
    2525    ] (refl … (lookup_opt … program_counter cost_labels))
    2626  ] (refl … program_size).
     
    6363          |2:
    6464            #n' #_ #program_size_refl_Sn' -traverse_code_internal destruct
    65             cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     65            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    6666            [1:
    6767              destruct
     
    9090                  #eqb_ref_assm
    9191                  -ind_hyp
    92                   <NEW_PC' in S_assm; #relevant <relevant -relevant
     92                  <S_assm
    9393                  change with (? < ?)
    9494                  @le_neq_to_lt assumption
     
    9797                generalize in match H2; whd in ⊢ (??% → ?);
    9898                >plus_n_Sm in ⊢ (% → ?);
    99                 cut(new_program_counter' = \snd (half_add 16 (bitvector_of_nat 16 1) program_counter))
    100                 [1:
    101                   <NEW_PC' %
     99                cut(new_program_counter' = add 16 (bitvector_of_nat 16 1) program_counter)
     100                [1: %
    102101                |2:
    103102                  #new_program_counter_assm' >new_program_counter_assm'
     
    188187              @(transitive_le ? (S (nat_of_bitvector … program_counter)))
    189188              [1:
    190                 cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     189                cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    191190                [1:
    192191                  destruct
     
    198197                  @le_S_S @le_S_S @le_O_n
    199198                |2:
    200                   #Sn_refl_assm >Sn_refl_assm <NEW_PC' @le_n
     199                  #Sn_refl_assm >Sn_refl_assm @le_n
    201200                ]
    202201              |2:
     
    209208            destruct
    210209            @(transitive_le … H2)
    211             cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     210            cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    212211            [1:
    213212              destruct
     
    222221              change with (S (S n' + ?) ≤ ?)
    223222              >plus_n_Sm @monotonic_le_plus_r >S_assm
    224               <NEW_PC' @le_n
     223              @le_n
    225224            ]
    226225          ]
     
    243242        @eq_f >program_size_refl_Sn <plus_n_Sm
    244243        change with (? = (S ?) + ?) @eq_f2 try %
    245         cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (\snd  (half_add 16 (bitvector_of_nat 16 1) program_counter)))
     244        cut((S (nat_of_bitvector 16 program_counter)) = nat_of_bitvector 16 (add 16 (bitvector_of_nat 16 1) program_counter))
    246245        [1:
    247246          destruct
     
    254253        |2:
    255254          #S_assm
    256           cut(new_program_counter' = \snd (half_add … (bitvector_of_nat … 1) program_counter))
    257           [1:
    258             <NEW_PC' %
     255          cut(new_program_counter' = add … (bitvector_of_nat … 1) program_counter)
     256          [1: %
    259257          |2:
    260258           #new_program_counter_assm' >new_program_counter_assm'
    261259           cases program_size_invariant
    262260           [1:
    263              #destruct_assm destruct
     261             #destruct_assm @⊥ >destruct_assm in program_size_refl; #abs destruct(abs)
    264262           |2:
    265263             #program_size_invariant
Note: See TracChangeset for help on using the changeset viewer.