Theorem: HMem.Program.splitTimeCost (HMem/Trace/Cost.lean)

State before:
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
⊢ timeCost' p h ≤ subroutineTimeCost h + recurseTimeCost h + localTimeCost h
Tactic:
intro a
State after:
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a

State before:
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a
Tactic:
apply le_trans
State after:
case a
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ ?b

case a
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ?b ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a

case b
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ℕ

State before:
case a
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ timeCost' p h a ≤ ?b

case a
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ?b ≤ (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a

case b
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ ℕ
Tactic:
exact (Stack.timeCost_le_iff _ (Program.halts_of_sound h _)).mp (p.costedMatches ▸ p.costed.splitTimeCost (costed_sound h) (costed_sound' h) a _ (Option.mem_some_iff.mpr rfl))
State after:
case a
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ (Trace.CostedProgram.subroutineTimeCost
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
          Trace.CostedProgram.recurseTimeCost
            (_ : sound (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p))) f sz)
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
        Trace.CostedProgram.localTimeCost
          (_ :
            Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
              (some ∘ Complexity.encode)))
      a ≤
    (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a

State before:
case a
TracedProgram : Sort ?u.211566
α : 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
sz : α → ℕ
p : Program
inst✝ : Trace.HasCostedProgram p
h : sound p f sz
a : α
⊢ (Trace.CostedProgram.subroutineTimeCost
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
          Trace.CostedProgram.recurseTimeCost
            (_ : sound (Trace.TracedProgram.toProgram (Trace.CostedProgram.toTracedProgram (costed p))) f sz)
            (_ :
              Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
                (some ∘ Complexity.encode)) +
        Trace.CostedProgram.localTimeCost
          (_ :
            Trace.TracedProgram.sound' f sz (Trace.CostedProgram.toTracedProgram (costed p))
              (some ∘ Complexity.encode)))
      a ≤
    (subroutineTimeCost h + recurseTimeCost h + localTimeCost h) a
Tactic:
exact le_refl _
State after:
no goals