Changeset 1928 for src/ASM/ASMCostsSplit.ma
- Timestamp:
- May 9, 2012, 1:36:35 PM (8 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/ASM/ASMCostsSplit.ma
r1921 r1928 1 1 include "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 2 include "ASM/UtilBranch.ma". 141 3 include alias "arithmetics/nat.ma". 142 4 include alias "basics/logic.ma". … … 426 288 qed. 427 289 428 (*429 let rec traverse_code_internal430 (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 447 290 definition traverse_code: 448 291 ∀code_memory: BitVectorTrie Byte 16.
Note: See TracChangeset
for help on using the changeset viewer.