include "ASM/Util.ma".
include "ASM/Arithmetic.ma".

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 ⊢ (??%?);
        >associative_plus in ⊢ (???%); @eq_f >commutative_plus
        whd in ⊢ (??%?); @eq_f2 // >commutative_times in ⊢ (???(??%));
        <associative_times //
    | <plus_n_O normalize <plus_n_O @eq_f <associative_times
      <commutative_times in ⊢ (???%); <associative_times // 
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 … (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 …
      (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.