internlm/Lean-Github huggingface dataset:
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
s₀ s₁ : Source
⊢ encodeSource s₀ = encodeSource s₁ → s₀ = s₁
Tactic:
cases h₀:s₀ <;> cases h₁:s₁
Proof state after:
case nil.nil
s₀ s₁ : Source
h₀ : s₀ = Source.nil
h₁ : s₁ = Source.nil
⊢ encodeSource Source.nil = encodeSource Source.nil → Source.nil = Source.nil

case nil.imm
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.imm hd✝ tl✝) → Source.nil = Source.imm hd✝ tl✝

case nil.idx
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.idx hd✝ tl✝) → Source.nil = Source.idx hd✝ tl✝

case imm.nil
s₀ s₁ : Source
hd✝ : Bool
tl✝ : Source
h₀ : s₀ = Source.imm hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.imm hd✝ tl✝) = encodeSource Source.nil → Source.imm hd✝ tl✝ = Source.nil

case imm.imm
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝

case imm.idx
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.idx hd✝ tl✝

case idx.nil
s₀ s₁ hd✝ tl✝ : Source
h₀ : s₀ = Source.idx hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.idx hd✝ tl✝) = encodeSource Source.nil → Source.idx hd✝ tl✝ = Source.nil

case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝

case idx.idx
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
case imm.imm => simpa [encodeSource] using λ hhd htl ↦ ⟨hhd, encodeSource_inj htl⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝
Tactic:
case idx.idx => simpa [encodeSource] using λ hhd htl ↦ ⟨encodeSource_inj hhd, encodeSource_inj htl⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
case nil.nil
s₀ s₁ : Source
h₀ : s₀ = Source.nil
h₁ : s₁ = Source.nil
⊢ encodeSource Source.nil = encodeSource Source.nil → Source.nil = Source.nil

case nil.imm
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.imm hd✝ tl✝) → Source.nil = Source.imm hd✝ tl✝

case nil.idx
s₀ s₁ : Source
h₀ : s₀ = Source.nil
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource Source.nil = encodeSource (Source.idx hd✝ tl✝) → Source.nil = Source.idx hd✝ tl✝

case imm.nil
s₀ s₁ : Source
hd✝ : Bool
tl✝ : Source
h₀ : s₀ = Source.imm hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.imm hd✝ tl✝) = encodeSource Source.nil → Source.imm hd✝ tl✝ = Source.nil

case imm.idx
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.idx hd✝ tl✝

case idx.nil
s₀ s₁ hd✝ tl✝ : Source
h₀ : s₀ = Source.idx hd✝ tl✝
h₁ : s₁ = Source.nil
⊢ encodeSource (Source.idx hd✝ tl✝) = encodeSource Source.nil → Source.idx hd✝ tl✝ = Source.nil

case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
all_goals simp[encodeSource]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
s₀ s₁ : Source
hd✝¹ : Bool
tl✝¹ : Source
h₀ : s₀ = Source.imm hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.imm hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.imm hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
simpa [encodeSource] using λ hhd htl ↦ ⟨hhd, encodeSource_inj htl⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ tl✝ : Source
h₁ : s₁ = Source.idx hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.idx hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.idx hd✝ tl✝
Tactic:
simpa [encodeSource] using λ hhd htl ↦ ⟨encodeSource_inj hhd, encodeSource_inj htl⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeSource_inj
Proof state before:
case idx.imm
s₀ s₁ hd✝¹ tl✝¹ : Source
h₀ : s₀ = Source.idx hd✝¹ tl✝¹
hd✝ : Bool
tl✝ : Source
h₁ : s₁ = Source.imm hd✝ tl✝
⊢ encodeSource (Source.idx hd✝¹ tl✝¹) = encodeSource (Source.imm hd✝ tl✝) → Source.idx hd✝¹ tl✝¹ = Source.imm hd✝ tl✝
Tactic:
simp[encodeSource]
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
inst✝¹ : OpInstruction
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.op inst✝ next✝
Tactic:
case op.op ih _ _ => simpa [encodeProgram] using λ x y ↦ ⟨x, ih y⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
nih : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.branch inst✝ next✝
Tactic:
case branch.branch nih _ _ =>
  simpa [encodeProgram] using λ hop hf ht ↦
    ⟨ hop, funext λ | false => nih _ hf | true => nih _ ht ⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
dst✝¹ src✝¹ : Source
func✝¹ next✝¹ : Program
fih : ∀ {p₁ : Program}, encodeProgram func✝¹ = encodeProgram p₁ → func✝¹ = p₁
nih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹) =
      encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
case subroutine.subroutine fih nih _ _ _ _ =>
  simpa [encodeProgram] using λ hdst hsrc hfunc hnext ↦ ⟨ hdst, hsrc, fih hfunc, nih hnext ⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
dst✝¹ src✝¹ : Source
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.recurse dst✝ src✝ next✝
Tactic:
case recurse.recurse ih _ _ _ =>
  simpa [encodeProgram] using λ hdst hsrc hnext ↦ ⟨hdst, hsrc, ih hnext⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
inst✝¹ : OpInstruction
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
inst✝ : OpInstruction
next✝ : Program
⊢ encodeProgram (Program.op inst✝¹ next✝¹) = encodeProgram (Program.op inst✝ next✝) →
    Program.op inst✝¹ next✝¹ = Program.op inst✝ next✝
Tactic:
simpa [encodeProgram] using λ x y ↦ ⟨x, ih y⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
inst✝¹ : BranchInstruction
next✝¹ : Bool → Program
nih : ∀ (a : Bool) {p₁ : Program}, encodeProgram (next✝¹ a) = encodeProgram p₁ → next✝¹ a = p₁
inst✝ : BranchInstruction
next✝ : Bool → Program
⊢ encodeProgram (Program.branch inst✝¹ next✝¹) = encodeProgram (Program.branch inst✝ next✝) →
    Program.branch inst✝¹ next✝¹ = Program.branch inst✝ next✝
Tactic:
simpa [encodeProgram] using λ hop hf ht ↦
  ⟨ hop, funext λ | false => nih _ hf | true => nih _ ht ⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
dst✝¹ src✝¹ : Source
func✝¹ next✝¹ : Program
fih : ∀ {p₁ : Program}, encodeProgram func✝¹ = encodeProgram p₁ → func✝¹ = p₁
nih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹) =
      encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.subroutine dst✝¹ src✝¹ func✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
simpa [encodeProgram] using λ hdst hsrc hfunc hnext ↦ ⟨ hdst, hsrc, fih hfunc, nih hnext ⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
dst✝¹ src✝¹ : Source
next✝¹ : Program
ih : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.recurse dst✝ src✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.recurse dst✝ src✝ next✝
Tactic:
simpa [encodeProgram] using λ hdst hsrc hnext ↦ ⟨hdst, hsrc, ih hnext⟩
Proof state after:
no goals
Theorem: HMem.Encoding.encodeProgram_inj
Proof state before:
case recurse.subroutine
dst✝¹ src✝¹ : Source
next✝¹ : Program
next_ih✝ : ∀ {p₁ : Program}, encodeProgram next✝¹ = encodeProgram p₁ → next✝¹ = p₁
dst✝ src✝ : Source
func✝ next✝ : Program
⊢ encodeProgram (Program.recurse dst✝¹ src✝¹ next✝¹) = encodeProgram (Program.subroutine dst✝ src✝ func✝ next✝) →
    Program.recurse dst✝¹ src✝¹ next✝¹ = Program.subroutine dst✝ src✝ func✝ next✝
Tactic:
simp [encodeProgram]
Proof state after:
no goals
Theorem: BitTree.toNatHelper_acc
Proof state before:
val✝ : Fin 2
x✝ : ℕ
⊢ toNatHelper [] (bit val✝) x✝ = bound [] * x✝ + toNatHelper [] (bit val✝) 0
Tactic:
simpa [toNatHelper, bound_zero] using Nat.add_comm _ _
Proof state after:
no goals
Theorem: BitTree.toNatHelper_acc
Proof state before:
H : List Unit
left✝ right✝ : BitTree
lhs✝ : Perfect H left✝
rhs✝ : Perfect H right✝
x : ℕ
⊢ toNatHelper (() :: H) (node left✝ right✝) x = bound (() :: H) * x + toNatHelper (() :: H) (node left✝ right✝) 0
Tactic:
simp [bound_cons, toNatHelper, toNatHelper_acc H _ x, toNatHelper_acc H _ (_ + _),
  toNatHelper_acc H _ (toNatHelper _ _ _),
  left_distrib, right_distrib, ← mul_assoc, ← add_assoc]
Proof state after:
no goals
Theorem: BitTree.addWithCarry_eq_ofNat_add
Proof state before:
val✝¹ val✝ x✝ : Fin 2
⊢ addWithCarry (bit val✝¹) (bit val✝) x✝ =
    ({ val := (toNat [] (bit val✝¹) + toNat [] (bit val✝) + ↑x✝) / bound [],
        isLt := (_ : (toNat [] (bit val✝¹) + toNat [] (bit val✝) + ↑x✝) / bound [] < 2) },
      ofNat [] (toNat [] (bit val✝¹) + toNat [] (bit val✝) + ↑x✝))
Tactic:
simp [addWithCarry, toNat, toNatHelper, bound_zero]
Proof state after:
no goals
Theorem: BitTree.addWithCarry_eq_ofNat_add
Proof state before:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
⊢ ∀ {m xh xl yh yl c : ℕ}, m * xh + xl + (m * yh + yl) + c = m * (xh + yh) + (xl + yl + c)
Tactic:
intro _ _ _ _ _ _
Proof state after:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
m✝ xh✝ xl✝ yh✝ yl✝ c✝ : ℕ
⊢ m✝ * xh✝ + xl✝ + (m✝ * yh✝ + yl✝) + c✝ = m✝ * (xh✝ + yh✝) + (xl✝ + yl✝ + c✝)
Theorem: BitTree.addWithCarry_eq_ofNat_add
Proof state before:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
m✝ xh✝ xl✝ yh✝ yl✝ c✝ : ℕ
⊢ m✝ * xh✝ + xl✝ + (m✝ * yh✝ + yl✝) + c✝ = m✝ * (xh✝ + yh✝) + (xl✝ + yl✝ + c✝)
Tactic:
ring
Proof state after:
no goals
Theorem: BitTree.addWithCarry_eq_ofNat_add
Proof state before:
H : List Unit
l✝¹ r✝¹ : BitTree
lhs✝¹ : Perfect H l✝¹
rhs✝¹ : Perfect H r✝¹
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
x✝ : Fin 2
rearrange : ∀ {m xh xl yh yl c : ℕ}, m * xh + xl + (m * yh + yl) + c = m * (xh + yh) + (xl + yl + c)
⊢ addWithCarry (node l✝¹ r✝¹) (node l✝ r✝) x✝ =
    ({ val := (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝) / bound (() :: H),
        isLt := (_ : (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝) / bound (() :: H) < 2) },
      ofNat (() :: H) (toNat (() :: H) (node l✝¹ r✝¹) + toNat (() :: H) (node l✝ r✝) + ↑x✝))
Tactic:
simp [addWithCarry, @addWithCarry_eq_ofNat_add H, rearrange, toNat_node, bound_cons,
  ← Nat.div_div_eq_div_mul, Nat.mul_add_div (bound_pos _),  divBound]
Proof state after:
no goals
Theorem: BitTree.addWithCarry_negate
Proof state before:
H : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H l✝
rhs✝ : Perfect H r✝
⊢ addWithCarry (node l✝ r✝) (negate (node l✝ r✝)) 1 = (1, ofNat (() :: H) 0)
Tactic:
simp [addWithCarry, addWithCarry_negate (H := H)]
Proof state after:
no goals
Theorem: BitTree.add_toNat_negate
Proof state before:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
⊢ ∀ {m a b c d e : ℕ}, m * a + b + (m * c + d) + e = m * (a + c) + (b + d + e)
Tactic:
intro _ _ _ _ _ _
Proof state after:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
m✝ a✝ b✝ c✝ d✝ e✝ : ℕ
⊢ m✝ * a✝ + b✝ + (m✝ * c✝ + d✝) + e✝ = m✝ * (a✝ + c✝) + (b✝ + d✝ + e✝)
Theorem: BitTree.add_toNat_negate
Proof state before:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
m✝ a✝ b✝ c✝ d✝ e✝ : ℕ
⊢ m✝ * a✝ + b✝ + (m✝ * c✝ + d✝) + e✝ = m✝ * (a✝ + c✝) + (b✝ + d✝ + e✝)
Tactic:
ring
Proof state after:
no goals
Theorem: BitTree.add_toNat_negate
Proof state before:
H✝ : List Unit
l✝ r✝ : BitTree
lhs✝ : Perfect H✝ l✝
rhs✝ : Perfect H✝ r✝
rearrange : ∀ {m a b c d e : ℕ}, m * a + b + (m * c + d) + e = m * (a + c) + (b + d + e)
⊢ toNat (() :: H✝) (node l✝ r✝) + toNat (() :: H✝) (negate (node l✝ r✝)) + 1 = bound (() :: H✝)
Tactic:
simp [toNat_node, rearrange, negate, add_toNat_negate _, ← Nat.mul_succ, Nat.succ_eq_add_one, bound_cons]
Proof state after:
no goals
Theorem: BitTree.sub_toNat
Proof state before:
H : List Unit
x y : BitTree
inst✝¹ : Perfect H x
inst✝ : Perfect H y
⊢ ∀ {a b c d : ℕ}, a + b + c + d = a + (d + b + c)
Tactic:
intro _ _ _ _
Proof state after:
H : List Unit
x y : BitTree
inst✝¹ : Perfect H x
inst✝ : Perfect H y
a✝ b✝ c✝ d✝ : ℕ
⊢ a✝ + b✝ + c✝ + d✝ = a✝ + (d✝ + b✝ + c✝)
Theorem: BitTree.sub_toNat
Proof state before:
H : List Unit
x y : BitTree
inst✝¹ : Perfect H x
inst✝ : Perfect H y
a✝ b✝ c✝ d✝ : ℕ
⊢ a✝ + b✝ + c✝ + d✝ = a✝ + (d✝ + b✝ + c✝)
Tactic:
ring
Proof state after:
no goals
Theorem: BitTree.lshift2_toNat
Proof state before:
H : List Unit
left✝¹ right✝¹ left✝ right✝ : BitTree
lhs✝¹ : Perfect H left✝¹
rhs✝¹ : Perfect H right✝¹
lhs✝ : Perfect H left✝
rhs✝ : Perfect H right✝
⊢ toNat (() :: () :: H) (lshift2 H (node (node left✝¹ right✝¹) (node left✝ right✝))) % bound (() :: () :: H) =
    toNat (() :: () :: H) (node (node left✝¹ right✝¹) (node left✝ right✝)) * bound H % bound (() :: () :: H)
Tactic:
simp only [
toNat_node, lo, hi, lshift2, bound_cons,
left_distrib, right_distrib, ← mul_assoc,
mul_right_comm _ _ (bound H), mul_comm (toNat _ _) (bound H),
Nat.add_assoc, Nat.mul_add_mod,
toNat_zero, add_zero]
Proof state after:
no goals
Theorem: BitTree.karatsubaHelper₃_toNat
Proof state before:
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)
Tactic:
have h₀: ∀ {x y: Fin 2} {H: List Unit}, x.val * y.val % (bound H * bound H) = x.val * y.val :=
  Nat.mod_eq_of_lt (Nat.mul_lt_mul_for_real
    (lt_of_lt_of_le (Fin.isLt _) (two_le_bound _))
    (lt_of_lt_of_le (Fin.isLt _) (two_le_bound _)))
Proof state after:
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
h₀ : ∀ {x y : Fin 2} {H : List Unit}, ↑x * ↑y % (bound H * bound H) = ↑x * ↑y
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)
Theorem: BitTree.karatsubaHelper₃_toNat
Proof state before:
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
h₀ : ∀ {x y : Fin 2} {H : List Unit}, ↑x * ↑y % (bound H * bound H) = ↑x * ↑y
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)
Tactic:
have h₁: ∀ {x: Fin 2} {H: List Unit} {y: BitTree} [Perfect H y], x.val * y.toNat H % bound H = x.val * y.toNat H
  | 0, _, _, _ => Nat.mod_eq_of_lt (lt_of_eq_of_lt (zero_mul _) (bound_pos _))
  | 1, _, _, _ => Nat.mod_eq_of_lt (lt_of_eq_of_lt (one_mul _) (toNat_lt _))
Proof state after:
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
h₀ : ∀ {x y : Fin 2} {H : List Unit}, ↑x * ↑y % (bound H * bound H) = ↑x * ↑y
h₁ : ∀ {x : Fin 2} {H : List Unit} {y : BitTree} [inst : Perfect H y], ↑x * toNat H y % bound H = ↑x * toNat H y
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)
Theorem: BitTree.karatsubaHelper₃_toNat
Proof state before:
H : List Unit
xy : BitTree
xc : Fin 2
x : BitTree
yc : Fin 2
y : BitTree
x✝² : Perfect (() :: H) xy
x✝¹ : Perfect H (xc, x).2
x✝ : Perfect H (yc, y).2
h : toNat (() :: H) xy = toNat H (xc, x).2 * toNat H (yc, y).2
h₀ : ∀ {x y : Fin 2} {H : List Unit}, ↑x * ↑y % (bound H * bound H) = ↑x * ↑y
h₁ : ∀ {x : Fin 2} {H : List Unit} {y : BitTree} [inst : Perfect H y], ↑x * toNat H y % bound H = ↑x * toNat H y
⊢ toNat (() :: () :: H) (karatsubaHelper₃ H xy (xc, x) (yc, y)) =
    (bound H * ↑(xc, x).1 + toNat H (xc, x).2) * (bound H * ↑(yc, y).1 + toNat H (yc, y).2)
Tactic:
simpa only [karatsubaHelper₃,
  add_toNat (()::()::H), mulBit_ofNat, mulBit'_ofNat,
  bound_cons, ← mul_assoc, mul_zero,
  mul_right_comm _ _ (bound H),
  mul_right_comm _ (toNat _ _) (Fin.val _),
  mul_comm (toNat _ _) (bound H),
  Nat.add_right_comm _ (_ * toNat H y) (_ * toNat H x),
  Nat.add_right_comm _ (toNat _ _ * toNat _ _),
  left_distrib, right_distrib,
  toNat_ofNat, toNat_node, h, toNat_zero,
  add_zero, zero_add, Nat.mod_add_mod, ← Nat.add_assoc,
  h₀, h₁] using Nat.mod_eq_of_lt (lt_of_eq_of_lt
  (Nat.add_assoc _ _ _)
  (add_lt_mul_bound
    (add_le_mul_bound
      (le_trans
        (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _)))
        (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _))))
      (Nat.mul_le_mul
        (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _)))
        (le_of_lt (toNat_lt _))))
    (add_lt_mul_bound
      (Nat.mul_le_mul (mul_le_of_le_one_right' (Nat.le_of_lt_succ (Fin.isLt _))) (le_of_lt (toNat_lt _)))
      (Nat.mul_lt_mul_for_real (toNat_lt _) (toNat_lt _)))))
Proof state after:
no goals
Theorem: BitTree.karatsubaHelper₁_toNat
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
⊢ toNat (() :: H) z₀ = toNat H xlo * toNat H ylo →
    toNat (() :: H) z₂ = toNat H xhi * toNat H yhi →
      toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo) →
        toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) =
          toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Tactic:
intro h₀ h₂ h₃
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Theorem: BitTree.karatsubaHelper₁_toNat
Proof state before:
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi
Tactic:
have h: ∀ {H: List Unit} {a b c d e f: BitTree} [Perfect H a] [Perfect H a] [Perfect H b] [Perfect H c] [Perfect H d] [Perfect H e] [Perfect H f],
    (a.toNat H * b.toNat H + c.toNat H * d.toNat H + e.toNat H * f.toNat H) % (bound H * bound H * bound H * bound H) =
    a.toNat H * b.toNat H + c.toNat H * d.toNat H + e.toNat H * f.toNat H :=
  Nat.mod_eq_of_lt (add_lt_mul_bound
    (add_le_mul_bound
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _)))
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _))))
     (add_lt_mul_bound
      (Nat.mul_le_mul
        (le_of_lt (toNat_lt _))
        (le_of_lt (toNat_lt _)))
      (Nat.mul_lt_mul_for_real
        (bound_pos _)
        (bound_pos _))))
Proof state after:
H : List Unit
xhi xlo yhi ylo : BitTree
inst✝⁶ : Perfect H xhi
inst✝⁵ : Perfect H xlo
inst✝⁴ : Perfect H yhi
inst✝³ : Perfect H ylo
z₀ z₂ z₃ : BitTree
inst✝² : Perfect (() :: H) z₀
inst✝¹ : Perfect (() :: H) z₂
inst✝ : Perfect (() :: () :: H) z₃
h₀ : toNat (() :: H) z₀ = toNat H xlo * toNat H ylo
h₂ : toNat (() :: H) z₂ = toNat H xhi * toNat H yhi
h₃ : toNat (() :: () :: H) z₃ = (toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo)
h :
  ∀ {H : List Unit} {a b c d e f : BitTree} [inst : Perfect H a] [inst : Perfect H a] [inst : Perfect H b]
    [inst : Perfect H c] [inst : Perfect H d] [inst : Perfect H e] [inst : Perfect H f],
    (toNat H a * toNat H b + toNat H c * toNat H d + toNat H e * toNat H f) % (bound H * bound H * bound H * bound H) =
      toNat H a * toNat H b + toNat H c * toNat H d + toNat H e * toNat H f
⊢ toNat (() :: () :: H) (karatsubaHelper₁ (() :: H) z₀ z₂ z₃) = toNat H xhi * toNat H ylo + toNat H xlo * toNat H yhi