Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.h.h₁.hx
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ toNat (() :: () :: H)
      (node (karatsuba H xhi yhi) (zero (() :: H)) +
        lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo))) =
    ?h₂.h.h₁.x'

case h₂.h.h₁.hy
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ toNat (() :: () :: H) (node (zero (() :: H)) (karatsuba H xlo ylo)) = ?h₂.h.h₁.y'

case h₂.h.h₁.x'
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ ℕ

case h₂.h.h₁.y'
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ ℕ

case h₂.h.h₂
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ ?h₂.h.h₁.x' + ?h₂.h.h₁.y' = toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)
Tactic:
apply congrArg
Proof state after:
case h₂.h.h₁.hx.h
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ node (karatsuba H xhi yhi) (zero (() :: H)) +
      lshift2 H (ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)) =
    ?h₂.h.h₁.hx.a₂

case h₂.h.h₁.hx.a₂
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ BitTree

case h₂.h.h₁.hy
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ toNat (() :: () :: H) (node (zero (() :: H)) (karatsuba H xlo ylo)) = ?h₂.h.h₁.y'

case h₂.h.h₁.y'
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ ℕ

case h₂.h.h₂
H : List Unit
xhi xlo yhi ylo : BitTree
lhs✝¹ : Perfect H xhi
rhs✝¹ : Perfect H xlo
lhs✝ : Perfect H yhi
rhs✝ : Perfect H ylo
h :
  ∀ {H : List Unit} {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y],
    toNat H x * toNat H y % bound (() :: H) = toNat H x * toNat H y
karatsuba_toNat :
  ∀ {x y : BitTree} [inst : Perfect H x] [inst : Perfect H y], toNat (() :: H) (karatsuba H x y) = toNat H x * toNat H y
h₃ :
  karatsubaHelper₃ H (karatsuba H (addWithCarry xhi xlo 0).2 (addWithCarry yhi ylo 0).2) (addWithCarry xhi xlo 0)
      (addWithCarry yhi ylo 0) =
    ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))
h₁ :
  karatsubaHelper₁ (() :: H) (karatsuba H xlo ylo) (karatsuba H xhi yhi)
      (ofNat (() :: () :: H) ((toNat H xhi + toNat H xlo) * (toNat H yhi + toNat H ylo))) =
    ofNat (() :: () :: H) (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)
⊢ toNat (() :: () :: H) ?h₂.h.h₁.hx.a₂ + ?h₂.h.h₁.y' = toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)