case mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h }) = { val := xs, property := h }
n : ℕ
v : Bitvec n
⊢ Bitvec.ofNat n (Bitvec.toNat v) = v
cases' v with xs h
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ ↑(Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h })) = ↑{ val := xs, property := h }
case mk
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h }) = { val := xs, property := h }
apply Subtype.ext
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Vector.toList (Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h })) = xs
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ ↑(Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h })) = ↑{ val := xs, property := h }
change Vector.toList _ = xs
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldl addLsb 0 xs)) = xs
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Vector.toList (Bitvec.ofNat n (Bitvec.toNat { val := xs, property := h })) = xs
dsimp [Bitvec.toNat, bitsToNat]
case mk.a
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldl addLsb 0 xs)) = xs
case mk.a
n : ℕ
xs : List Bool
h : List.length xs = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldl addLsb 0 xs)) = xs
rw [← List.length_reverse] at h
case mk.a
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (List.reverse xs))) =
    List.reverse (List.reverse xs)
case mk.a
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldl addLsb 0 xs)) = xs
rw [← List.reverse_reverse xs, List.foldl_reverse]
case mk.a
n : ℕ
xs ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys)) = List.reverse ys
case mk.a
n : ℕ
xs : List Bool
h : List.length (List.reverse xs) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (List.reverse xs))) =
    List.reverse (List.reverse xs)
generalize xs.reverse = ys at h⊢
case mk.a
n : ℕ
ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys)) = List.reverse ys
case mk.a
n : ℕ
xs ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys)) = List.reverse ys
clear xs
case mk.a.nil
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
n : ℕ
h : List.length [] = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 [])) = List.reverse []

case mk.a.cons
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
n : ℕ
h : List.length (ys_head :: ys_tail) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
case mk.a
n : ℕ
ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys)) = List.reverse ys
induction' ys with ys_head ys_tail ys_ih generalizing n
case mk.a.nil.refl
n : ℕ
ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat (List.length []) (List.foldr (fun x y => addLsb y x) 0 [])) = List.reverse []
case mk.a.nil
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
n : ℕ
h : List.length [] = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 [])) = List.reverse []
cases h
no goals
case mk.a.nil.refl
n : ℕ
ys : List Bool
h : List.length ys = n
⊢ Vector.toList (Bitvec.ofNat (List.length []) (List.foldr (fun x y => addLsb y x) 0 [])) = List.reverse []
simp [Bitvec.ofNat]
case mk.a.cons
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
n : ℕ
h : succ (List.length ys_tail) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
case mk.a.cons
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
n : ℕ
h : List.length (ys_head :: ys_tail) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
simp only [← Nat.succ_eq_add_one, List.length] at h
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList
      (Bitvec.ofNat (succ (List.length ys_tail)) (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
case mk.a.cons
n✝ : ℕ
ys : List Bool
h✝ : List.length ys = n✝
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
n : ℕ
h : succ (List.length ys_tail) = n
⊢ Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
subst n
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList
        (Bitvec.ofNat (List.length ys_tail) (addLsb (List.foldr (fun x y => addLsb y x) 0 ys_tail) ys_head / 2)) ++
      [decide (addLsb (List.foldr (fun x y => addLsb y x) 0 ys_tail) ys_head % 2 = 1)] =
    List.reverse ys_tail ++ [ys_head]
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList
      (Bitvec.ofNat (succ (List.length ys_tail)) (List.foldr (fun x y => addLsb y x) 0 (ys_head :: ys_tail))) =
    List.reverse (ys_head :: ys_tail)
simp only [Bitvec.ofNat, Vector.toList_cons, Vector.toList_nil, List.reverse_cons,
  Vector.toList_append, List.foldr]
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList (Bitvec.ofNat (List.length ys_tail) (List.foldr (fun x y => addLsb y x) 0 ys_tail)) ++ [ys_head] =
    List.reverse ys_tail ++ [ys_head]
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList
        (Bitvec.ofNat (List.length ys_tail) (addLsb (List.foldr (fun x y => addLsb y x) 0 ys_tail) ys_head / 2)) ++
      [decide (addLsb (List.foldr (fun x y => addLsb y x) 0 ys_tail) ys_head % 2 = 1)] =
    List.reverse ys_tail ++ [ys_head]
erw [addLsb_div_two, decide_addLsb_mod_two]
case mk.a.cons.e_a
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList (Bitvec.ofNat (List.length ys_tail) (List.foldr (fun x y => addLsb y x) 0 ys_tail)) =
    List.reverse ys_tail
case mk.a.cons
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList (Bitvec.ofNat (List.length ys_tail) (List.foldr (fun x y => addLsb y x) 0 ys_tail)) ++ [ys_head] =
    List.reverse ys_tail ++ [ys_head]
congr
case mk.a.cons.e_a.h
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ List.length ys_tail = List.length ys_tail
case mk.a.cons.e_a
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ Vector.toList (Bitvec.ofNat (List.length ys_tail) (List.foldr (fun x y => addLsb y x) 0 ys_tail)) =
    List.reverse ys_tail
apply ys_ih
no goals
case mk.a.cons.e_a.h
n : ℕ
ys : List Bool
h : List.length ys = n
ys_head : Bool
ys_tail : List Bool
ys_ih :
  ∀ {n : ℕ},
    List.length ys_tail = n →
      Vector.toList (Bitvec.ofNat n (List.foldr (fun x y => addLsb y x) 0 ys_tail)) = List.reverse ys_tail
⊢ List.length ys_tail = List.length ys_tail
rfl