internlm/Lean-Github huggingface dataset:
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.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)
⊢ (bound H * bound H * toNat H xhi * toNat H yhi + bound H * (toNat H xlo * toNat H yhi + toNat H xhi * toNat H ylo)) %
      (bound H * bound H * bound H * bound H) =
    bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
      bound H * toNat H xhi * toNat H ylo
Tactic:
simp only [left_distrib, ← add_assoc, ← mul_assoc]
Proof state after:
case h₂.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)
⊢ (bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
        bound H * toNat H xhi * toNat H ylo) %
      (bound H * bound H * bound H * bound H) =
    bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
      bound H * toNat H xhi * toNat H ylo
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.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)
⊢ (bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
        bound H * toNat H xhi * toNat H ylo) %
      (bound H * bound H * bound H * bound H) =
    bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
      bound H * toNat H xhi * toNat H ylo
Tactic:
apply Nat.mod_eq_of_lt
Proof state after:
case h₂.h.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)
⊢ bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
      bound H * toNat H xhi * toNat H ylo <
    bound H * bound H * bound H * bound H
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.h.h₂.h₂.h.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)
⊢ toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo) < bound H * bound H * bound H * bound H
Tactic:
apply lt_of_lt_of_eq _ (mul_assoc _ _ _).symm
Proof state after:
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 xhi xlo) * toNat (() :: H) (node yhi ylo) < bound H * bound H * (bound H * bound H)
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
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 xhi xlo) * toNat (() :: H) (node yhi ylo) < bound H * bound H * (bound H * bound H)
Tactic:
apply Nat.mul_lt_mul_for_real
Proof state after:
case hax
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 xhi xlo) < bound H * bound H

case hby
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 yhi ylo) < bound H * bound H
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case hax
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 xhi xlo) < bound H * bound H

case hby
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 yhi ylo) < bound H * bound H
Tactic:
apply lt_of_lt_of_eq (toNat_lt _) (bound_cons _)
Proof state after:
case hby
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 yhi ylo) < bound H * bound H
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case hby
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 yhi ylo) < bound H * bound H
Tactic:
apply lt_of_lt_of_eq (toNat_lt _) (bound_cons _)
Proof state after:
no goals
Theorem: BitTree.karatsuba_eq_mul
Proof state before:
case h₂.h.h₂.h₂.h.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)
⊢ bound H * bound H * toNat H xhi * toNat H yhi + bound H * toNat H xlo * toNat H yhi +
      bound H * toNat H xhi * toNat H ylo ≤
    toNat (() :: H) (node xhi xlo) * toNat (() :: H) (node yhi ylo)
Tactic:
simp [toNat_node, left_distrib, right_distrib, add_assoc, ← mul_assoc, mul_right_comm _ (toNat _ _) (bound _), mul_comm (toNat _ _) (bound _)]
Proof state after:
no goals
Theorem: HMem.Memory.setm_setm
Proof state before:
m : Memory
b : Bool
ma₀ ma₁ : Memory
⊢ setm (setm m b ma₀) b ma₁ = setm m b ma₁
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: HMem.Memory.getv_setv
Proof state before:
m : Memory
v : Bool
⊢ getv (setv m v) = v
Tactic:
simp
Proof state after:
no goals
Theorem: HMem.Memory.getm_setv
Proof state before:
m : Memory
v : Bool
⊢ getm (setv m v) = getm m
Tactic:
funext b
Proof state after:
case h
m : Memory
v b : Bool
⊢ getm (setv m v) b = getm m b
Theorem: HMem.Memory.getm_setv
Proof state before:
case h
m : Memory
v b : Bool
⊢ getm (setv m v) b = getm m b
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: HMem.Memory.getv_setm
Proof state before:
m : Memory
b : Bool
ma : Memory
⊢ getv (setm m b ma) = getv m
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: HMem.Memory.getm_setm_eq
Proof state before:
m : Memory
b : Bool
ma : Memory
⊢ getm (setm m b ma) b = ma
Tactic:
cases b <;> simp
Proof state after:
no goals
Theorem: HMem.Memory.setmp_setmp
Proof state before:
ma₀ ma₁ m : Memory
b : Bool
bs : List Bool
⊢ setmp (setmp m (b :: bs) ma₀) (b :: bs) ma₁ = setmp m (b :: bs) ma₁
Tactic:
simp [setmp_setmp (bs := bs)]
Proof state after:
no goals
Theorem: HMem.Stack.exit_of_step_result
Proof state before:
m : Memory
is p : Program
cs : List (Thunk × List Bool)
r : Memory
⊢ step (execution { state := m, current := is, function := p } cs) = result r → m = r ∧ is = Program.exit ∧ cs = []
Tactic:
cases is <;> cases cs <;> simp
Proof state after:
no goals
Theorem: HMem.Stack.exit_of_step_result'
Proof state before:
cs : List (Thunk × List Bool)
r state✝ : Memory
current✝ function✝ : Program
h : step (execution { state := state✝, current := current✝, function := function✝ } cs) = result r
⊢ execution { state := state✝, current := current✝, function := function✝ } cs =
    execution
      { state := r, current := Program.exit,
        function := { state := state✝, current := current✝, function := function✝ }.function }
      []
Tactic:
simp [exit_of_step_result h]
Proof state after:
no goals
Theorem: HMem.Stack.step_eq_execution
Proof state before:
s : Stack
t : Thunk
cs : List (Thunk × List Bool)
⊢ step s = execution t cs → ∃ t' cs', s = execution t' cs'
Tactic:
cases s <;> simp
Proof state after:
no goals
Theorem: HMem.Stack.step_execution_append
Proof state before:
t₀ : Thunk
cs₀ : List (Thunk × List Bool)
t₁ : Thunk
cs₁ cs : List (Thunk × List Bool)
⊢ step (execution t₀ cs₀) = execution t₁ cs₁ → step (execution t₀ (cs₀ ++ cs)) = execution t₁ (cs₁ ++ cs)
Tactic:
cases t₀ with | _ m c p => cases c <;> cases cs₀ <;> simp [List.append_left_inj]
Proof state after:
no goals
Theorem: HMem.Stack.step_execution_append
Proof state before:
case mk
cs₀ : List (Thunk × List Bool)
t₁ : Thunk
cs₁ cs : List (Thunk × List Bool)
m : Memory
c p : Program
⊢ step (execution { state := m, current := c, function := p } cs₀) = execution t₁ cs₁ →
    step (execution { state := m, current := c, function := p } (cs₀ ++ cs)) = execution t₁ (cs₁ ++ cs)
Tactic:
cases c <;> cases cs₀ <;> simp [List.append_left_inj]
Proof state after:
no goals
Theorem: HMem.Stack.istep_execution_append
Proof state before:
cs : List (Thunk × List Bool)
x✝³ x✝² : Thunk
x✝¹ x✝ : List (Thunk × List Bool)
⊢ step^[0] (execution x✝³ x✝¹) = execution x✝² x✝ → step^[0] (execution x✝³ (x✝¹ ++ cs)) = execution x✝² (x✝ ++ cs)
Tactic:
simp
Proof state after:
no goals
Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
case h₂
α : Type u_1
inst✝⁷ : Complexity.Coding α Memory
β : Type u_2
inst✝⁶ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁵ : Complexity.Coding γ Memory
inst✝⁴ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝³ : Complexity.Computable Encoding.Model fs
inst✝² : Complexity Encoding.Model fs cs
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
γ✝ δ✝ : Type
inst✝¹ : Complexity.Coding γ✝ Memory
inst✝ : Complexity.Encoding δ✝ Memory
fs✝ : γ✝ → δ✝
cs✝ : Complexity.CostFunction γ✝ ℕ
hcost : Complexity Encoding.Model fs✝ cs✝
next : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (subroutine' dst✝ src✝ inst✝¹ inst✝ fs✝ cs✝ hcost next)) fm
a : α
m : Memory
hm : m ∈ fm a
⊢ subroutineTimeCost
        (_ :
          TracedProgram.sound' f size (toTracedProgram next)
            ((flip Option.bind fun m =>
                Option.map (Memory.setms m dst✝ ∘ Complexity.encode ∘ fs✝)
                  (Complexity.decode γ✝ (Memory.getms m src✝))) ∘
              fm))
        a +
      Complexity.ALE.bound Complexity.cost_ale
        (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
          (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) ≤
    subroutineTimeCost h a
Tactic:
apply add_le_add (le_refl _)
Proof state after:
case h₂
α : Type u_1
inst✝⁷ : Complexity.Coding α Memory
β : Type u_2
inst✝⁶ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁵ : Complexity.Coding γ Memory
inst✝⁴ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝³ : Complexity.Computable Encoding.Model fs
inst✝² : Complexity Encoding.Model fs cs
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
γ✝ δ✝ : Type
inst✝¹ : Complexity.Coding γ✝ Memory
inst✝ : Complexity.Encoding δ✝ Memory
fs✝ : γ✝ → δ✝
cs✝ : Complexity.CostFunction γ✝ ℕ
hcost : Complexity Encoding.Model fs✝ cs✝
next : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (subroutine' dst✝ src✝ inst✝¹ inst✝ fs✝ cs✝ hcost next)) fm
a : α
m : Memory
hm : m ∈ fm a
⊢ Complexity.ALE.bound Complexity.cost_ale
      (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
        (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) ≤
    Complexity.CostFunction.flatMap (TracedProgram.sound'_subroutine_arg h) (Encoding.getBound hcost) a
Theorem: HMem.Trace.CostedProgram.splitTimeCost
Proof state before:
α : Type u_1
inst✝⁷ : Complexity.Coding α Memory
β : Type u_2
inst✝⁶ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
γ δ : Type
inst✝⁵ : Complexity.Coding γ Memory
inst✝⁴ : Complexity.Encoding δ Memory
fs : γ → δ
cs : Complexity.CostFunction γ ℕ
inst✝³ : Complexity.Computable Encoding.Model fs
inst✝² : Complexity Encoding.Model fs cs
size : α → ℕ
fm : α → Option Memory
fcp : CostedProgram
hf : Program.sound (TracedProgram.toProgram (toTracedProgram fcp)) f size
dst✝ src✝ : Source
γ✝ δ✝ : Type
inst✝¹ : Complexity.Coding γ✝ Memory
inst✝ : Complexity.Encoding δ✝ Memory
fs✝ : γ✝ → δ✝
cs✝ : Complexity.CostFunction γ✝ ℕ
hcost : Complexity Encoding.Model fs✝ cs✝
next : CostedProgram
h : TracedProgram.sound' f size (toTracedProgram (subroutine' dst✝ src✝ inst✝¹ inst✝ fs✝ cs✝ hcost next)) fm
a : α
m : Memory
hm : m ∈ fm a
⊢ Complexity.ALE.bound Complexity.cost_ale
      (Option.get (Complexity.decode γ✝ (Memory.getms m src✝))
        (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true)) ≤
    Encoding.getBound hcost
      (Option.get ((Complexity.decode γ✝ ∘ flip Memory.getms src✝) m)
        (_ : Option.isSome (Complexity.decode γ✝ (Memory.getms m src✝)) = true))
Tactic:
apply le_refl
Proof state after:
no goals