Changeset 1928 for src/ASM/ASMCostsSplit.ma

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:

• src/ASM/ASMCostsSplit.ma (modified) (2 diffs)

src/ASM/ASMCostsSplit.ma

@@ -1 +1 @@
 include "ASM/ASMCosts.ma".
-include alias "arithmetics/nat.ma".
-include alias "basics/logic.ma".
-
-
-(* Also extracts an equality proof (useful when not using Russell). *)
-notation > "hvbox('let' 〈ident x,ident y〉 'as' ident E 'return' ty ≝ t 'in' s)"
- with precedence 10
-for @{ match $t return λx.∀${ident E}: x = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
-        λ${ident E}.$s ] (refl ? $t) }.
-
-(*
-lemma test:
-  ∀c: nat × nat.
-    Σx: nat. ∃y: nat. c = 〈x, y〉 ≝
-  λc: nat × nat. let 〈left, right〉 as T return Σx: ?. ? ≝ c in left.
-*)
-
-notation > "hvbox('deplet' 〈ident x,ident y〉 'as' ident E  ≝ t 'in' s)"
- with precedence 10
-for @{ match $t return λx.∀${ident E}: x = $t. Σz: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
-        λ${ident E}.$s ] (refl ? $t) }.
-
-(*
-notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
- with precedence 10
-for @{ match $t return λx.x = $t → ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
-       match ${fresh xy} return λx. ? = $t → ? with [ mk_Prod ${ident x} ${ident y} ⇒
-        λ${ident E}.$s ] ] (refl ? $t) }. *)
-
-notation > "hvbox('deplet' 〈ident x,ident y,ident z〉 'as' ident E ≝ t 'in' s)"
- with precedence 10
-for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
-       match ${fresh xy} return λx.∀${ident E}:? = $t. Σu: ?. ? with [ mk_Prod ${ident x} ${ident y} ⇒
-        λ${ident E}.$s ] ] (refl ? $t) }.
-
-notation > "hvbox('let' 〈ident x,ident y,ident z〉 'as' ident E 'return' ty ≝ t 'in' s)"
- with precedence 10
-for @{ match $t return λx.∀${fresh w}:x = $t. Σq: ?. ? with [ mk_Prod ${fresh xy} ${ident z} ⇒
-       match ${fresh xy} return λx.∀${ident E}:? = $t. $ty with [ mk_Prod ${ident x} ${ident y} ⇒
-        λ${ident E}.$s ] ] (refl ? $t) }.
-
-definition nat_of_bool: bool → nat ≝
-  λb: bool.
-  match b with
-  [ true ⇒ 1
-  | false ⇒ 0
-  ].
-
-lemma blah:
-  ∀n: nat.
-  ∀bv: BitVector n.
-  ∀buffer: nat.
-    nat_of_bitvector_aux n buffer bv = nat_of_bitvector n bv + (buffer * 2^n).
-  #n #bv elim bv
-  [1:
-    #buffer elim buffer try %
-    #buffer' #inductive_hypothesis
-    normalize <times_n_1 %
-  |2:
-    #n' #hd #tl #inductive_hypothesis
-    #buffer cases hd normalize
-    >inductive_hypothesis
-    >inductive_hypothesis
-    [1:
-      change with (
-        ? + (2 * buffer + 1) * ?) in ⊢ (??%?);
-      change with (
-        ? + buffer * (2 * 2^n')) in ⊢ (???%);
-      cases daemon
-    ]
-  ]
-  cases daemon
-qed.
-
-lemma nat_of_bitvector_aux_hd_tl:
-  ∀n: nat.
-  ∀tl: BitVector n.
-  ∀hd: bool.
-    nat_of_bitvector (S n) (hd:::tl) =
-      nat_of_bitvector n tl + (nat_of_bool hd * 2^n).
-  #n #tl elim tl
-  [1:
-    #hd cases hd %
-  |2:
-    #n' #hd' #tl' #inductive_hypothesis #hd
-    cases hd whd in ⊢ (??%?); normalize nodelta
-    >inductive_hypothesis cases hd' normalize nodelta
-    normalize in match (nat_of_bool ?);
-    normalize in match (nat_of_bool ?);
-    [4:
-      normalize in match (2 * ?);
-      <plus_n_O <plus_n_O %
-    |3:
-      normalize in match (2 * ?);
-      normalize in match (0 + 1);
-      <plus_n_O
-      normalize in match (1 * ?);
-      <plus_n_O
-      cases daemon
-      (* XXX: lemma *)
-    |*:
-      cases daemon
-    ]
-  ]
-qed.
-
-lemma succ_nat_of_bitvector_aux_half_add_1:
-  ∀n: nat.
-  ∀bv: BitVector n.
-  ∀buffer: nat.
-  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
-    S (nat_of_bitvector_aux n buffer bv) =
-      nat_of_bitvector … (\snd (half_add n (bitvector_of_nat … 1) bv)).
-  #n #bv elim bv
-  [1:
-    #buffer normalize #absurd
-    cases (lt_to_not_zero … absurd)
-  |2:
-    #n' #hd #tl #inductive_hypothesis #buffer
-    cases daemon
-  ]
-qed.
-    
-lemma succ_nat_of_bitvector_half_add_1:
-  ∀n: nat.
-  ∀bv: BitVector n.
-  ∀power_proof: nat_of_bitvector … bv < 2^n - 1.
-    S (nat_of_bitvector … bv) = nat_of_bitvector …
-      (\snd (half_add n (bitvector_of_nat … 1) bv)).
-  #n #bv elim bv
-  [1:
-    normalize #absurd
-    cases (lt_to_not_zero … absurd)
-  |2:
-    #n' #hd #tl #inductive_hypothesis
-    cases daemon
-  ]
-qed.
-    
+include "ASM/UtilBranch.ma".
 include alias "arithmetics/nat.ma".
 include alias "basics/logic.ma".
@@ -426 +288 @@
 qed.
 
-(*
-let rec traverse_code_internal
-  (code_memory: BitVectorTrie Byte 16) (cost_labels: BitVectorTrie costlabel 16)
-    (program_counter: Word) (fixed_program_size: nat) (program_size: nat)
-      (reachable_program_counter_witness:
-          ∀lbl: costlabel.
-          ∀program_counter: Word. Some … lbl = lookup_opt … program_counter cost_labels →
-            reachable_program_counter code_memory fixed_program_size program_counter)
-        (good_program_witness: good_program code_memory fixed_program_size)
-        (program_size_invariant: program_size = 0 ∨ nat_of_bitvector … program_counter + program_size = fixed_program_size)
-        (fixed_program_size_limit: fixed_program_size < 2^16)
-        on program_size:
-          Σcost_map: identifier_map CostTag nat.
-            (∀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) ∧
-            (∀k. ∀k_pres:present … cost_map k. ∃pc. lookup_opt … pc cost_labels = Some … k →
-              ∃reachable_witness: reachable_program_counter code_memory fixed_program_size pc.
-                pi1 … (block_cost code_memory pc fixed_program_size cost_labels reachable_witness good_program_witness) = lookup_present … k_pres) ≝
-*)
-
 definition traverse_code:
   ∀code_memory: BitVectorTrie Byte 16.