sgl_provision

import Definitions.Def_sgl_elim_solution
import Definitions.Def_sgl_merge_solution

/-!
# Scratch tapes, provisioned locally

The provisioning chain is proved on the platform, but a submission compiles
against published definitions, and whether platform-proved theorems join the
environment is not a fact to build on.  Both children exist locally — the
merge and the last elimination — so the induction that strings them together
might as well exist locally too.
-/

namespace SipserGacsLautemann

variable {tapes : Nat}

/-- One scratch tape fewer. -/
theorem eliminate_one_scratch_tape_local (scratch : Nat)
    (predicate : (Fin tapes → List Bool) → Prop)
    (hdecides : DecidesInPolynomialTimeWithScratch (scratch + 1) predicate) :
    DecidesInPolynomialTimeWithScratch scratch predicate := by
  cases scratch with
  | zero =>
      exact (decidesInPolynomialTimeWithScratch_zero predicate).mpr
        ((decidesInPolynomialTimeWithScratch_zero predicate).mp
          (eliminate_last_scratch_tape predicate hdecides))
  | succ s =>
      exact merge_empty_scratch_tapes s predicate hdecides

/-- **Scratch tapes are free.** -/
theorem scratch_tape_provisioning_local (scratch : Nat)
    (predicate : (Fin tapes → List Bool) → Prop)
    (hdecides : DecidesInPolynomialTimeWithScratch scratch predicate) :
    DecidesInPolynomialTime predicate := by
  induction scratch with
  | zero =>
      exact (decidesInPolynomialTimeWithScratch_zero predicate).mp hdecides
  | succ s ih =>
      exact ih (eliminate_one_scratch_tape_local s predicate hdecides)

end SipserGacsLautemann