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

State before:
n : ℕ
⊢ encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
Tactic:
refine Nat.binaryRec' (n := n) Memory.zero_def'.symm ?hi
State after:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (n = 0 → b = true) →
      encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2)) →
        encode (Nat.bit b n) =
          Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

State before:
case hi
n : ℕ
⊢ ∀ (b : Bool) (n : ℕ),
    (n = 0 → b = true) →
      encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2)) →
        encode (Nat.bit b n) =
          Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
intro b n hn _
State after:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

State before:
case hi
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
apply Eq.trans
State after:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) = ?hi.b

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ ?hi.b = Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

case hi.b
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Memory

State before:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (Nat.bit b n) = ?hi.b

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ ?hi.b = Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

case hi.b
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Memory
Tactic:
apply congrArg (encode (α := List Bool))
State after:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Nat.bits (Nat.bit b n) = ?m.80295

n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ List Bool

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode ?m.80295 =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

State before:
case hi.h₁
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ Nat.bits (Nat.bit b n) = ?m.80295

n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ List Bool

case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode ?m.80295 =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
apply Nat.bits_append_bit _ _ hn
State after:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (b :: Nat.bits n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))

State before:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode (b :: Nat.bits n) =
    Memory.mk (decide (Nat.bit b n ≠ 0)) (encode (decide (Nat.bit b n % 2 = 1))) (encode (Nat.bit b n / 2))
Tactic:
apply Memory.mk_inj_iff.mpr
State after:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0) ∧
    encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)

State before:
case hi.h₂
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0) ∧
    encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Tactic:
apply And.intro
State after:
case hi.h₂.left
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0)

case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)

State before:
case hi.h₂.left
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ true = decide (Nat.bit b n ≠ 0)

case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Tactic:
exact Eq.symm (decide_eq_true λ h ↦ absurd ((Nat.bit_eq_zero.mp h).right.symm.trans (hn (Nat.bit_eq_zero.mp h).left)) Bool.noConfusion)
State after:
case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)

State before:
case hi.h₂.right
n✝ : ℕ
b : Bool
n : ℕ
hn : n = 0 → b = true
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
⊢ encode b = encode (decide (Nat.bit b n % 2 = 1)) ∧ encodeList (Nat.bits n) = encode (Nat.bit b n / 2)
Tactic:
cases b <;> simp [-Nat.bit_false, -Nat.bit_true, Nat.bit_mod_two, Nat.bit_div_2]
State after:
case hi.h₂.right.false
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → false = true
⊢ encodeList (Nat.bits n) = encode n

case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n

State before:
case hi.h₂.right.false
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → false = true
⊢ encodeList (Nat.bits n) = encode n

case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n
Tactic:
rfl
State after:
case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n

State before:
case hi.h₂.right.true
n✝ n : ℕ
a✝ : encode n = Memory.mk (decide (n ≠ 0)) (encode (decide (n % 2 = 1))) (encode (n / 2))
hn : n = 0 → true = true
⊢ encodeList (Nat.bits n) = encode n
Tactic:
rfl
State after:
no goals