internlm/Lean-Github huggingface dataset:
Theorem: Nat.size_le_self
Proof state before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ bit false n ≠ 0

case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0
Tactic:
simpa using λ h ↦ absurd (hb h) Bool.noConfusion
Proof state after:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0
Theorem: Nat.size_le_self
Proof state before:
case f.true
n : ℕ
ih : size n ≤ n
hb : n = 0 → true = true
⊢ bit true n ≠ 0
Tactic:
simp
Proof state after:
no goals
Theorem: Nat.size_le_self
Proof state before:
case f.false
n : ℕ
ih : size n ≤ n
hb : n = 0 → false = true
⊢ 1 ≤ n
Tactic:
cases n
Proof state after:
case f.false.zero
ih : size zero ≤ zero
hb : zero = 0 → false = true
⊢ 1 ≤ zero

case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝
Theorem: Nat.size_le_self
Proof state before:
case f.false.zero
ih : size zero ≤ zero
hb : zero = 0 → false = true
⊢ 1 ≤ zero

case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝
Tactic:
exact absurd (hb rfl) Bool.noConfusion
Proof state after:
case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝
Theorem: Nat.size_le_self
Proof state before:
case f.false.succ
n✝ : ℕ
ih : size (succ n✝) ≤ succ n✝
hb : succ n✝ = 0 → false = true
⊢ 1 ≤ succ n✝
Tactic:
exact Nat.succ_le_succ (Nat.zero_le _)
Proof state after:
no goals
Theorem: blah
Proof state before:
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a
Tactic:
ring_nf
Proof state after:
a x : ℕ
⊢ x * x ^ a + (1 + x) ^ a ≤ x * (1 + x) ^ a + x ^ a + (1 + x) ^ a
Theorem: blah
Proof state before:
a x : ℕ
⊢ x * x ^ a + (1 + x) ^ a ≤ x * (1 + x) ^ a + x ^ a + (1 + x) ^ a
Tactic:
apply add_le_add_right
Proof state after:
case bc
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a + x ^ a
Theorem: blah
Proof state before:
case bc
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a + x ^ a
Tactic:
apply le_add_right
Proof state after:
case bc.h
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a
Theorem: blah
Proof state before:
case bc.h
a x : ℕ
⊢ x * x ^ a ≤ x * (1 + x) ^ a
Tactic:
apply Nat.mul_le_mul_left
Proof state after:
case bc.h.h
a x : ℕ
⊢ x ^ a ≤ (1 + x) ^ a
Theorem: blah
Proof state before:
case bc.h.h
a x : ℕ
⊢ x ^ a ≤ (1 + x) ^ a
Tactic:
apply Nat.pow_le_pow_left
Proof state after:
case bc.h.h.h
a x : ℕ
⊢ x ≤ 1 + x
Theorem: blah
Proof state before:
case bc.h.h.h
a x : ℕ
⊢ x ≤ 1 + x
Tactic:
apply Nat.le_add_left
Proof state after:
no goals
Theorem: blah2
Proof state before:
a x : ℕ
⊢ (x + 1) ^ a - x ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1)
Tactic:
apply Nat.sub_le_of_le_add
Proof state after:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1) + x ^ a
Theorem: blah2
Proof state before:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) - x ^ (a + 1) + x ^ a
Tactic:
rw [← Nat.sub_add_comm]
Proof state after:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) + x ^ a - x ^ (a + 1)

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Theorem: blah2
Proof state before:
case h
a x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + 1) + x ^ a - x ^ (a + 1)

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Tactic:
apply Nat.le_sub_of_add_le
Proof state after:
case h.h
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Theorem: blah2
Proof state before:
case h.h
a x : ℕ
⊢ (x + 1) ^ a + x ^ (a + 1) ≤ (x + 1) ^ (a + 1) + x ^ a

case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Tactic:
apply blah
Proof state after:
case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Theorem: blah2
Proof state before:
case h
a x : ℕ
⊢ x ^ (a + 1) ≤ (x + 1) ^ (a + 1)
Tactic:
apply Nat.pow_le_pow_left
Proof state after:
case h.h
a x : ℕ
⊢ x ≤ x + 1
Theorem: blah2
Proof state before:
case h.h
a x : ℕ
⊢ x ≤ x + 1
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: blah4
Proof state before:
a b : ℕ
⊢ 0 ^ (a + b) - 0 ^ a ≤ (0 + 1) ^ (a + b) - (0 + 1) ^ a
Tactic:
cases a <;> cases b <;> simp
Proof state after:
no goals
Theorem: blah4
Proof state before:
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a ≤ (x + 1 + 1) ^ (a + b) - (x + 1 + 1) ^ a
Tactic:
apply Nat.le_sub_of_add_le
Proof state after:
case h
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + 1) ^ a ≤ (x + 1 + 1) ^ (a + b)
Theorem: blah4
Proof state before:
case h
a b x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + 1) ^ a ≤ (x + 1 + 1) ^ (a + b)
Tactic:
rw [← Nat.sub_add_comm, add_comm, Nat.sub_add_comm]
Proof state after:
case h
a b x : ℕ
⊢ (x + 1 + 1) ^ a - (x + 1) ^ a + (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Theorem: blah4
Proof state before:
case h
a b x : ℕ
⊢ (x + 1 + 1) ^ a - (x + 1) ^ a + (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.add_le_of_le_sub _ blah3
Proof state after:
a b x : ℕ
⊢ (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Theorem: blah4
Proof state before:
a b x : ℕ
⊢ (x + 1) ^ (a + b) ≤ (x + 1 + 1) ^ (a + b)

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.pow_le_pow_left (Nat.le_succ _)
Proof state after:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Theorem: blah4
Proof state before:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + 1) ^ a

case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.pow_le_pow_left (Nat.le_succ _)
Proof state after:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Theorem: blah4
Proof state before:
case h
a b x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)
Tactic:
apply Nat.pow_le_pow_right (Nat.zero_lt_succ _)
Proof state after:
case h
a b x : ℕ
⊢ a ≤ a + b
Theorem: blah4
Proof state before:
case h
a b x : ℕ
⊢ a ≤ a + b
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: blah5
Proof state before:
a b x : ℕ
⊢ x ^ (a + b) - x ^ a ≤ (x + 0) ^ (a + b) - (x + 0) ^ a
Tactic:
simp
Proof state after:
no goals
Theorem: blah6
Proof state before:
a b y : ℕ
⊢ (0 + y) ^ a - 0 ^ a ≤ (0 + y) ^ (a + b) - 0 ^ (a + b)
Tactic:
cases a <;> cases b <;> cases y <;>
simp [Nat.pow_add]
Proof state after:
case succ.succ.succ
n✝² n✝¹ n✝ : ℕ
⊢ 1 ≤ Nat.succ n✝ ^ Nat.succ n✝¹
Theorem: blah6
Proof state before:
case succ.succ.succ
n✝² n✝¹ n✝ : ℕ
⊢ 1 ≤ Nat.succ n✝ ^ Nat.succ n✝¹
Tactic:
exact le_trans (Nat.pow_le_pow_right (Nat.zero_lt_succ 0) (Nat.succ_le_succ (Nat.zero_le _))) (Nat.pow_le_pow_left (Nat.succ_le_succ (Nat.zero_le _)) _)
Proof state after:
no goals
Theorem: blah6
Proof state before:
a b y x : ℕ
⊢ (x + 1 + y) ^ a - (x + 1) ^ a ≤ (x + 1 + y) ^ (a + b) - (x + 1) ^ (a + b)
Tactic:
apply Nat.le_sub_of_add_le
Proof state after:
case h
a b y x : ℕ
⊢ (x + 1 + y) ^ a - (x + 1) ^ a + (x + 1) ^ (a + b) ≤ (x + 1 + y) ^ (a + b)
Theorem: blah6
Proof state before:
case h
a b y x : ℕ
⊢ (x + 1 + y) ^ a - (x + 1) ^ a + (x + 1) ^ (a + b) ≤ (x + 1 + y) ^ (a + b)
Tactic:
rw [← Nat.sub_add_comm, add_comm (_ ^ _), Nat.sub_add_comm]
Proof state after:
case h
a b y x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + y) ^ a ≤ (x + 1 + y) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case h
a b y x : ℕ
⊢ (x + 1) ^ (a + b) - (x + 1) ^ a + (x + 1 + y) ^ a ≤ (x + 1 + y) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.add_le_of_le_sub _ blah5
Proof state after:
a b y x : ℕ
⊢ (x + 1 + y) ^ a ≤ (x + 1 + y) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
a b y x : ℕ
⊢ (x + 1 + y) ^ a ≤ (x + 1 + y) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.pow_le_pow_right
Proof state after:
case hx
a b y x : ℕ
⊢ x + 1 + y > 0

case a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case hx
a b y x : ℕ
⊢ x + 1 + y > 0

case a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.lt_add_right _ (Nat.zero_lt_succ _)
Proof state after:
case a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.le_add_right
Proof state after:
case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1) ^ (a + b)

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.pow_le_pow_right
Proof state after:
case h.hx
a b y x : ℕ
⊢ x + 1 > 0

case h.a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case h.hx
a b y x : ℕ
⊢ x + 1 > 0

case h.a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.zero_lt_succ _
Proof state after:
case h.a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case h.a
a b y x : ℕ
⊢ a ≤ a + b

case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.le_add_right
Proof state after:
case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Theorem: blah6
Proof state before:
case h
a b y x : ℕ
⊢ (x + 1) ^ a ≤ (x + 1 + y) ^ a
Tactic:
apply Nat.pow_le_pow_left
Proof state after:
case h.h
a b y x : ℕ
⊢ x + 1 ≤ x + 1 + y
Theorem: blah6
Proof state before:
case h.h
a b y x : ℕ
⊢ x + 1 ≤ x + 1 + y
Tactic:
apply Nat.le_add_right
Proof state after:
no goals
Theorem: blah7
Proof state before:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
apply (Nat.exists_eq_add_of_le hab).elim
Proof state after:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), b = a + a_1 → y ^ a - x ^ a ≤ y ^ b - x ^ b
Theorem: blah7
Proof state before:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), b = a + a_1 → y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
apply (Nat.exists_eq_add_of_le hxy).elim
Proof state after:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), y = x + a_1 → ∀ (a_3 : ℕ), b = a + a_3 → y ^ a - x ^ a ≤ y ^ b - x ^ b
Theorem: blah7
Proof state before:
a b x y : ℕ
hab : a ≤ b
hxy : x ≤ y
⊢ ∀ (a_1 : ℕ), y = x + a_1 → ∀ (a_3 : ℕ), b = a + a_3 → y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
intro _ hxy _ hab
Proof state after:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b
Theorem: blah7
Proof state before:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ y ^ a - x ^ a ≤ y ^ b - x ^ b
Tactic:
rw [hxy, hab]
Proof state after:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ (x + a✝¹) ^ a - x ^ a ≤ (x + a✝¹) ^ (a + a✝) - x ^ (a + a✝)
Theorem: blah7
Proof state before:
a b x y : ℕ
hab✝ : a ≤ b
hxy✝ : x ≤ y
a✝¹ : ℕ
hxy : y = x + a✝¹
a✝ : ℕ
hab : b = a + a✝
⊢ (x + a✝¹) ^ a - x ^ a ≤ (x + a✝¹) ^ (a + a✝) - x ^ (a + a✝)
Tactic:
exact blah6
Proof state after:
no goals
Theorem: HMem.Program.simpleLoopCost
Proof state before:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n : ℕ
⊢ ∀ (a : α), sz a = n → timeCost' p h a ≤ x * n + x
Tactic:
induction n using Nat.case_strong_induction_on with
| hi n₀ ih =>
  intro a hsz
  apply le_trans (splitTimeCost _ _)
  apply le_of_eq_of_le
  apply Eq.trans
  apply Nat.add_right_comm _ _ _
  apply Nat.add_comm
  apply add_le_add _
  apply hsi
  apply le_trans
  apply Trace.CostedProgram.recurseTimeCostBound (x := x * n₀ + x)
  intro arg harg
  apply le_trans _ (add_le_add_right (mul_le_mul (le_refl _ ) _ (zero_le _) (zero_le _)) _)
  use sz arg
  specialize ih (sz arg) _
  apply Nat.succ_le_succ_iff.mp
  apply le_of_le_of_eq _ hsz
  apply Nat.succ_le_of_lt harg
  specialize ih _ rfl
  simp only [p.costedMatches']
  apply ih
  apply Nat.succ_le_succ_iff.mp
  apply le_of_le_of_eq _ hsz
  apply Nat.succ_le_of_lt harg
  simp only [p.costedMatches, hr, one_mul, Nat.mul_succ]
  apply le_refl
| hz =>
  intro a hsz
  apply le_trans (splitTimeCost _ _)
  apply le_of_eq_of_le
  apply Eq.trans
  apply Nat.add_right_comm _ _ _
  apply Nat.add_comm
  apply add_le_add _
  apply hsi
  apply le_of_eq_of_le _ (zero_le _)
  apply Trace.CostedProgram.recurseTimeCost_leaf (costed_sound h) _ hsz
Proof state after:
no goals
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
⊢ ∀ (a : α), sz a = Nat.succ n₀ → timeCost' p h a ≤ x * Nat.succ n₀ + x
Tactic:
intro a hsz
Proof state after:
case hi
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ timeCost' p h a ≤ x * Nat.succ n₀ + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ timeCost' p h a ≤ x * Nat.succ n₀ + x
Tactic:
apply le_trans (splitTimeCost _ _)
Proof state after:
case hi
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a ≤ x * Nat.succ n₀ + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a ≤ x * Nat.succ n₀ + x
Tactic:
apply le_of_eq_of_le
Proof state after:
case hi.h₁
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a = ?hi.b

case hi.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ ?hi.b ≤ x * Nat.succ n₀ + x

case hi.b
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ ℕ
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi.h₁.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ subroutineTimeCost h a + localTimeCost h a + recurseTimeCost h a = ?hi.b

case hi.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ ?hi.b ≤ x * Nat.succ n₀ + x

case hi.b
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ ℕ
Tactic:
apply Nat.add_comm
Proof state after:
case hi.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ recurseTimeCost h a + (subroutineTimeCost h a + localTimeCost h a) ≤ x * Nat.succ n₀ + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ recurseTimeCost h a + (subroutineTimeCost h a + localTimeCost h a) ≤ x * Nat.succ n₀ + x
Tactic:
apply add_le_add _
Proof state after:
case hi.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ subroutineTimeCost h a + localTimeCost h a ≤ x

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ recurseTimeCost h a ≤ x * Nat.succ n₀
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hi.h₂
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ subroutineTimeCost h a + localTimeCost h a ≤ x

TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ recurseTimeCost h a ≤ x * Nat.succ n₀
Tactic:
apply hsi
Proof state after:
TracedProgram : Sort ?u.75510
α : Type u_1
inst✝² : Complexity.Coding α Memory
β : Type u_2
inst✝¹ : Complexity.Encoding β Memory
f : α → β
tp : TracedProgram
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
x : ℕ
hsi : subroutineTimeCost h + localTimeCost h ≤ fun x_1 => x
hr : maxRecurse p = 1
n₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
⊢ recurseTimeCost h a ≤ x * Nat.succ n₀