internlm/Lean-Github huggingface dataset:
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₀ : ℕ
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 le_trans
Proof state after:
case a
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 ≤ ?b

case a
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₀
⊢ ?b ≤ x * Nat.succ n₀

case 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 a
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 ≤ ?b

case a
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₀
⊢ ?b ≤ x * Nat.succ n₀

case 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 Trace.CostedProgram.recurseTimeCostBound (x := x * n₀ + x)
Proof state after:
case a.hsz
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₀
⊢ ∀ (arg : α),
    sz arg < sz a →
      timeCost (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
          (_ :
            haltsOn (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
              (Complexity.encode arg)) ≤
        x * n₀ + x

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case a.hsz
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₀
⊢ ∀ (arg : α),
    sz arg < sz a →
      timeCost (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
          (_ :
            haltsOn (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
              (Complexity.encode arg)) ≤
        x * n₀ + x

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
intro arg harg
Proof state after:
case a.hsz
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₀
arg : α
harg : sz arg < sz a
⊢ timeCost (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
      (_ :
        haltsOn (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p)))
          (Complexity.encode arg)) ≤
    x * n₀ + x

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
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 : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
ih : timeCost' p h arg ≤ x * sz arg + x
⊢ timeCost p (_ : haltsOn p (Complexity.encode arg)) ≤ x * sz arg + 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₀
arg : α
harg : sz arg < sz a
⊢ sz arg ≤ n₀

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
apply ih
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₀
arg : α
harg : sz arg < sz a
⊢ sz arg ≤ n₀

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
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₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ sz arg ≤ n₀

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
apply Nat.succ_le_succ_iff.mp
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₀
arg : α
harg : sz arg < sz a
⊢ Nat.succ (sz arg) ≤ Nat.succ n₀

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
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₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ Nat.succ (sz arg) ≤ Nat.succ n₀

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
apply le_of_le_of_eq _ hsz
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₀
arg : α
harg : sz arg < sz a
⊢ Nat.succ (sz arg) ≤ sz a

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
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₀ : ℕ
ih : ∀ m ≤ n₀, ∀ (a : α), sz a = m → timeCost' p h a ≤ x * m + x
a : α
hsz : sz a = Nat.succ n₀
arg : α
harg : sz arg < sz a
⊢ Nat.succ (sz arg) ≤ sz a

case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
apply Nat.succ_le_of_lt harg
Proof state after:
case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case a
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₀
⊢ maxRecurse (Trace.CostedProgram.toProgram (costed p)) * (x * n₀ + x) ≤ x * Nat.succ n₀
Tactic:
simp only [p.costedMatches, hr, one_mul, Nat.mul_succ]
Proof state after:
case a
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₀
⊢ x * n₀ + x ≤ x * n₀ + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case a
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₀
⊢ x * n₀ + x ≤ x * n₀ + x
Tactic:
apply le_refl
Proof state after:
no goals
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz
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
⊢ ∀ (a : α), sz a = 0 → timeCost' p h a ≤ x * 0 + x
Tactic:
intro a hsz
Proof state after:
case hz
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
a : α
hsz : sz a = 0
⊢ timeCost' p h a ≤ x * 0 + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz
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
a : α
hsz : sz a = 0
⊢ timeCost' p h a ≤ x * 0 + x
Tactic:
apply le_trans (splitTimeCost _ _)
Proof state after:
case hz
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
a : α
hsz : sz a = 0
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a ≤ x * 0 + x
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz
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
a : α
hsz : sz a = 0
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a ≤ x * 0 + x
Tactic:
apply le_of_eq_of_le
Proof state after:
case hz.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
a : α
hsz : sz a = 0
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a = ?hz.b

case hz.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
a : α
hsz : sz a = 0
⊢ ?hz.b ≤ x * 0 + x

case hz.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
a : α
hsz : sz a = 0
⊢ ℕ
Theorem: HMem.Program.simpleLoopCost
Proof state before:
case hz.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
a : α
hsz : sz a = 0
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a = ?hz.b

case hz.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
a : α
hsz : sz a = 0
⊢ ?hz.b ≤ x * 0 + x

case hz.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
a : α
hsz : sz a = 0
⊢ ℕ
Tactic:
apply Eq.trans
Proof state after:
case hz.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
a : α
hsz : sz a = 0
⊢ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a = ?hz.h₁.b

case hz.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
a : α
hsz : sz a = 0
⊢ ?hz.h₁.b = ?hz.b

case hz.h₁.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
a : α
hsz : sz a = 0
⊢ ℕ

case hz.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
a : α
hsz : sz a = 0
⊢ ?hz.b ≤ x * 0 + x

case hz.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
a : α
hsz : sz a = 0
⊢ ℕ