Theorem: HMem.Encoding.decode_succ (HMem/Encoding/Basic.lean)

State before:
hd tl : Memory
⊢ decode ℕ (Memory.mk true hd tl) = Option.map (fun n => 2 * n + Bool.toNat (Memory.getv hd)) (decode ℕ tl)
Tactic:
simp [decode_nat]
State after:
hd tl : Memory
⊢ Option.map (Nat.ofBits ∘ fun b => Memory.getv hd :: b) (decode (List Bool) tl) =
    Option.map ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) (decode (List Bool) tl)

State before:
hd tl : Memory
⊢ Option.map (Nat.ofBits ∘ fun b => Memory.getv hd :: b) (decode (List Bool) tl) =
    Option.map ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) (decode (List Bool) tl)
Tactic:
apply congrArg₂ Option.map _ rfl
State after:
hd tl : Memory
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) = (fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits

State before:
hd tl : Memory
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) = (fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits
Tactic:
apply funext
State after:
case h
hd tl : Memory
⊢ ∀ (x : List Bool),
    (Nat.ofBits ∘ fun b => Memory.getv hd :: b) x = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) x

State before:
case h
hd tl : Memory
⊢ ∀ (x : List Bool),
    (Nat.ofBits ∘ fun b => Memory.getv hd :: b) x = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) x
Tactic:
intro xs
State after:
case h
hd tl : Memory
xs : List Bool
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) xs = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) xs

State before:
case h
hd tl : Memory
xs : List Bool
⊢ (Nat.ofBits ∘ fun b => Memory.getv hd :: b) xs = ((fun n => 2 * n + Bool.toNat (Memory.getv hd)) ∘ Nat.ofBits) xs
Tactic:
simp [Nat.ofBits]
State after:
case h
hd tl : Memory
xs : List Bool
⊢ Nat.bit (Memory.getv hd) (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat (Memory.getv hd)

State before:
case h
hd tl : Memory
xs : List Bool
⊢ Nat.bit (Memory.getv hd) (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat (Memory.getv hd)
Tactic:
match HMem.Memory.getv hd with
| true => simp [← Nat.two_mul]
| false => simp [← Nat.two_mul]
State after:
no goals

State before:
hd tl : Memory
xs : List Bool
⊢ Nat.bit true (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat true
Tactic:
simp [← Nat.two_mul]
State after:
no goals

State before:
hd tl : Memory
xs : List Bool
⊢ Nat.bit false (Nat.ofBits xs) = 2 * Nat.ofBits xs + Bool.toNat false
Tactic:
simp [← Nat.two_mul]
State after:
no goals