Ignore:
Timestamp:
May 9, 2012, 1:36:35 PM (8 years ago)
Author:
mulligan
Message:

Moved code from in ASM/ASMCosts*.ma and ASM/CostsProof.ma that should rightfully be in another file. Added a new file, ASM/UtilBranch.ma for code that should rightfully be in ASM/Util.ma but is incomplete (i.e. daemons).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASMCostsSplit.ma

    r1921 r1928  
    11include "ASM/ASMCosts.ma".
    2 include alias "arithmetics/nat.ma".
    3 include alias "basics/logic.ma".
    4 
    5 
    6 (* Also extracts an equality proof (useful when not using Russell). *)
    7 notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
    8  with precedence 10
    9 for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    10         λ${ident E}.$s ] (refl ? $t) }.
    11 
    12 (*
    13 lemma test:
    14   ∀c: nat × nat.
    15     Σx: nat. ∃y: nat. c = 〈x, y〉 ≝
    16   λc: nat × nat. let 〈left, right〉 as T return Σx: ?. ? ≝ c in left.
    17 *)
    18 
    19 notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
    20  with precedence 10
    21 for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
    22         λ${ident E}.$s ] (refl ? $t) }.
    23 
    24 (*
    25 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    26  with precedence 10
    27 for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
    28        match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
    29         λ${ident E}.$s ] ] (refl ? $t) }. *)
    30 
    31 notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
    32  with precedence 10
    33 for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
    34        match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
    35         λ${ident E}.$s ] ] (refl ? $t) }.
    36 
    37 notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
    38  with precedence 10
    39 for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
    40        match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
    41         λ${ident E}.$s ] ] (refl ? $t) }.
    42 
    43 definition nat_of_bool: bool → nat ≝
    44   λb: bool.
    45   match b with
    46   [ true ⇒ 1
    47   | false ⇒ 0
    48   ].
    49 
    50 lemma blah:
    51   ∀n: nat.
    52   ∀bv: BitVector n.
    53   ∀buffer: nat.
    54     nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
    55   #n #bv elim bv
    56   [1:
    57     #buffer elim buffer try %
    58     #buffer' #inductive_hypothesis
    59     normalize <times_n_1 %
    60   |2:
    61     #n' #hd #tl #inductive_hypothesis
    62     #buffer cases hd normalize
    63     >inductive_hypothesis
    64     >inductive_hypothesis
    65     [1:
    66       change with (
    67         ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
    68       change with (
    69         ? + buffer * (2 * 2^n')) in ⊢ (???%);
    70       cases daemon
    71     ]
    72   ]
    73   cases daemon
    74 qed.
    75 
    76 lemma nat_of_bitvector_aux_hd_tl:
    77   ∀n: nat.
    78   ∀tl: BitVector n.
    79   ∀hd: bool.
    80     nat_of_bitvector (S n) (hd:::tl) =
    81       nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
    82   #n #tl elim tl
    83   [1:
    84     #hd cases hd %
    85   |2:
    86     #n' #hd' #tl' #inductive_hypothesis #hd
    87     cases hd whd in ⊢ (??%?); normalize nodelta
    88     >inductive_hypothesis cases hd' normalize nodelta
    89     normalize in match (nat_of_bool ?);
    90     normalize in match (nat_of_bool ?);
    91     [4:
    92       normalize in match (2 * ?);
    93       <plus_n_O <plus_n_O %
    94     |3:
    95       normalize in match (2 * ?);
    96       normalize in match (0 + 1);
    97       <plus_n_O
    98       normalize in match (1 * ?);
    99       <plus_n_O
    100       cases daemon
    101       (* XXX: lemma *)
    102     |*:
    103       cases daemon
    104     ]
    105   ]
    106 qed.
    107 
    108 lemma succ_nat_of_bitvector_aux_half_add_1:
    109   ∀n: nat.
    110   ∀bv: BitVector n.
    111   ∀buffer: nat.
    112   ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    113     S (nat_of_bitvector_aux n buffer bv) =
    114       nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
    115   #n #bv elim bv
    116   [1:
    117     #buffer normalize #absurd
    118     cases (lt_to_not_zero … absurd)
    119   |2:
    120     #n' #hd #tl #inductive_hypothesis #buffer
    121     cases daemon
    122   ]
    123 qed.
    124    
    125 lemma succ_nat_of_bitvector_half_add_1:
    126   ∀n: nat.
    127   ∀bv: BitVector n.
    128   ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
    129     S (nat_of_bitvector … bv) = nat_of_bitvector …
    130       (\snd (half_add n (bitvector_of_nat … 1) bv)).
    131   #n #bv elim bv
    132   [1:
    133     normalize #absurd
    134     cases (lt_to_not_zero … absurd)
    135   |2:
    136     #n' #hd #tl #inductive_hypothesis
    137     cases daemon
    138   ]
    139 qed.
    140    
     2include "ASM/UtilBranch.ma".
    1413include alias "arithmetics/nat.ma".
    1424include alias "basics/logic.ma".
     
    426288qed.
    427289
    428 (*
    429 let rec traverse_code_internal
    430   (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
    431     (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
    432       (reachable_program_counter_witness:
    433           ∀lbl: costlabel.
    434           ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
    435             reachable_program_counter code_memory fixed_program_size program_counter)
    436         (good_program_witness: good_program code_memory fixed_program_size)
    437         (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
    438         (fixed_program_size_limit: fixed_program_size < 2^16)
    439         on program_size:
    440           Σcost_map: identifier_map CostTag nat.
    441             (∀pc,k. nat_of_bitvector … program_counter ≤ nat_of_bitvector 16 pc → nat_of_bitvector … pc < program_size + nat_of_bitvector … program_counter → lookup_opt … pc cost_labels = Some … k → present … cost_map k) ∧
    442             (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
    443               ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
    444                 pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
    445 *)
    446 
    447290definition traverse_code:
    448291  ∀code_memory: BitVectorTrie Byte 16.
Note: See TracChangeset for help on using the changeset viewer.