Imports
Boolean flag extraction from a SUBSET-SUM mask certificate
noncomputable sectionnamespace CLRS.Chapter34.Turing.SubsetSumVerifier.MaskFlagsopen _root_.Turingopen PolyBuilderabbrev RawInput := List SubsetSumSym × List SubsetSumSymdef rawEncoding (input : RawInput) : List (Option SubsetSumSym) :=
pairEncoding input.1 input.2def extractSymbol : SubsetSumSym → List Bool
| .bit flag => [flag]
| _ => []def extract (certificate : List SubsetSumSym) : List Bool :=
certificate.flatMap extractSymboldef flags (input : RawInput) : List Bool := extract input.1private def spec : StatefulFlatMapSpec Unit SubsetSumSym Bool where
initial := ()
action _ symbol := (extractSymbol symbol, ())
finish _ := []
private theorem rewriteFrom_eq (input : List SubsetSumSym) :
rewriteStatefulFlatMapFrom spec () input = extract input := by
induction input with
| nil => rfl
| cons symbol rest ih =>
rw [rewriteStatefulFlatMapFrom.eq_def]
simpa [spec, extract] using congrArg (extractSymbol symbol ++ ·) ihprivate theorem rewrite_eq (input : List SubsetSumSym) :
rewriteStatefulFlatMap spec input = extract input := rewriteFrom_eq inputprivate theorem flatMap_bits (mask : List Bool) :
(mask.map TSPSym.bit).flatMap extractSymbol = mask := by
induction mask with
| nil => rfl
| cons flag mask ih => simp [extractSymbol, ih]@[simp] theorem flags_encode (mask : List Bool) (data : SubsetSumData) :
flags (encodeSubsetSumMask mask, encodeSubsetSumData data) = mask := by
simp [flags, extract, encodeSubsetSumMask, extractSymbol, flatMap_bits]
private noncomputable def extractComputableInPolyTime :
TM2ComputableInPolyTime id id extract := by
have machine := statefulFlatMap_computableInPolyTime spec
exact
{ tm := machine.tm
inputAlphabet := machine.inputAlphabet
outputAlphabet := machine.outputAlphabet
time := machine.time
outputsFun := fun input => by
have output := machine.outputsFun input
rw [rewrite_eq] at output
exact output }noncomputable def flagsComputableInPolyTime :
TM2ComputableInPolyTime rawEncoding id flags := by
let composed := TM2Comp.TM2ComputableInPolyTime.comp_scratch
TSPVerifier.StructuralChecks.certificateProjection
extractComputableInPolyTime
change TM2ComputableInPolyTime
TSPVerifier.StructuralChecks.rawEncoding id (fun input => extract input.1)
simpa only [Function.comp_def] using Classical.choice composedend CLRS.Chapter34.Turing.SubsetSumVerifier.MaskFlags