Changeset 1556 for src/ASM/CostsProof.ma


Ignore:
Timestamp:
Nov 24, 2011, 5:24:10 PM (8 years ago)
Author:
mulligan
Message:

submitting to avoid conflicts

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/CostsProof.ma

    r1554 r1556  
    290290include alias "arithmetics/nat.ma".
    291291
    292 (*Useless now?
     292(*
    293293lemma minus_m_n_minus_minus_plus_1:
    294294  ∀m, n: nat.
     
    297297 /3 by lt_plus_to_minus_r, plus_minus/
    298298qed.
     299*)
    299300
    300301lemma plus_minus_rearrangement_1:
     
    313314    (m - n) + (n - o) = m - o.
    314315 /2 by plus_minus_rearrangement_1/
    315 qed.*)
     316qed.
    316317
    317318(*
     
    344345    normalize @compute_max_trace_any_label_cost_is_ok
    345346  |2:
     347    cases the_trace
     348    [1:
     349      #start_status #final_status #is_next #is_not_return #is_costed
     350      normalize nodelta;
     351      change with (
     352        let current_instruction_cost ≝ current_instruction_cost start_status in 
     353        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels start_fun_call after_fun_call call_trace in 
     354        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag after_fun_call final final_trace in 
     355        call_trace_cost+current_instruction_cost+final_trace_cost
     356      ) in ⊢ (??%?);
     357    |2:
     358      #start_status #final_status #is_next #is_return
     359    |3:
     360      #end_flag #status_pre_fun_call #status_start_fun_call #status_after_fun_call
     361      #status_final #is_next #is_call #is_after_return #fun_call_trace #after_fun_call_trace
     362      change with (
     363        let current_instruction_cost ≝ current_instruction_cost status_pre_fun_call in 
     364        let call_trace_cost ≝ compute_max_trace_label_return_cost cost_labels status_start_fun_call status_after_fun_call fun_call_trace in 
     365        let final_trace_cost ≝ compute_max_trace_any_label_cost cost_labels end_flag status_after_fun_call status_final after_fun_call_trace in 
     366          call_trace_cost+current_instruction_cost+final_trace_cost) in ⊢ (??%?);
     367      normalize nodelta;
     368      >compute_max_trace_label_return_cost_is_ok
     369      >compute_max_trace_any_label_cost_is_ok
     370    |4:
     371    ]
    346372  |3:
    347373    cases the_trace
     
    353379      normalize >compute_max_trace_label_label_cost_is_ok
    354380      >compute_max_trace_label_return_cost_is_ok
     381      >plus_minus_rearrangement_1
     382      [1: %
     383      |2:
     384      |3:
     385      ]
    355386    ]
    356387  ].
Note: See TracChangeset for help on using the changeset viewer.