Skip to content
  1. CLRS-Lean
  2. Chapter 34. NP-Completeness
  3. 34.5. NP-Complete Problems
  4. 34.5. SUBSET-SUM
  5. 34.5. Reduction Machine
  6. 34.5. Choice fields: generated payload semantics
Browse chapters
Imports
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.ReductionMachine.ChoiceFieldFamily import Mathlib.Tactic

Choice fields: generated payload semantics

This file gives the block formatter a total, source-level input family. The family is defined from the finite choice digits for every raw CNF word; on the three-CNF branch it is proved equal to the textbook packed item payloads.

noncomputable sectionnamespace CLRS.Chapter34.Turing.SubsetSumReductionopen _root_.CLRS.Chapter34.SubsetSumReduction

Boolean payload contributed by one finite choice digit.

def choiceCountBits (positions : List SmallDigitPosition) : ChoiceCountSym → List Bool | .digit digit => positions.map fun position => smallDigitBit (choiceBlockDigitTag digit).toSmallDigit position | .itemEnd => []

The payload family generated by the finite choice source, before numeric field canonicalization.

def choiceGeneratedBitItems (truth : Bool) (input : List CNFSym) : List (List Bool) := let formula := decodeCNF input let positions := smallDigitPositions (reductionBlockWidthTicks input) (List.range (reductionVariableCount formula)).map fun index => (choiceVariableDigits formula index ++ choiceOccurrenceDigits formula index truth).flatMap (choiceCountBits positions)
private theorem choicePayload_noEnd (formula : CNF) (index : Nat) (truth : Bool) : ∀ symbol ∈ choiceVariableDigits formula index ++ choiceOccurrenceDigits formula index truth, symbol ≠ .itemEnd := by intro symbol hsymbol simp [choiceVariableDigits, choiceOccurrenceDigits] at hsymbol rcases hsymbol with h | h | h | h · rw [h.2] simp · rw [h] simp · rw [h.2] simp · rcases h with ⟨clause, hclause, heq⟩ rw [← heq] simp private theorem choiceBlockExpand_payload (positions : List SmallDigitPosition) (symbols : List ChoiceCountSym) (hnoEnd : ∀ symbol ∈ symbols, symbol ≠ .itemEnd) : symbols.flatMap (choiceBlockExpand positions) = (symbols.flatMap (choiceCountBits positions)).map ChoiceBlockSym.bit := by induction symbols with | nil => rfl | cons symbol symbols ih => have hhead := hnoEnd symbol (by simp) have htail : ∀ current ∈ symbols, current ≠ .itemEnd := by intro current hcurrent exact hnoEnd current (by simp [hcurrent]) cases symbol with | digit digit => simp only [List.flatMap_cons, choiceBlockExpand, choiceCountBits, List.map_append, ih htail, List.map_map, Function.comp_def] | itemEnd => contradictionprivate theorem map_choiceBlockBit_injective {left right : List Bool} (h : left.map ChoiceBlockSym.bit = right.map ChoiceBlockSym.bit) : left = right := by induction left generalizing right with | nil => cases right <;> simp_all | cons bit left ih => cases right with | nil => simp at h | cons other right => simp only [List.map_cons, List.cons.injEq, ChoiceBlockSym.bit.injEq] at h exact congrArg₂ List.cons h.1 (ih h.2)

The concrete nested-loop block stream is exactly the delimiter encoding of the generated payload family, for every raw CNF word.

theorem choiceBlockStream_eq_items (truth : Bool) (input : List CNFSym) : choiceBlockStream truth input = choiceBlockItemsInput (choiceGeneratedBitItems truth input) := by rw [choiceBlockStream_eq] simp only [choiceDigitStream, choiceGeneratedBitItems, choiceBlockItemsInput, List.flatMap_map] rw [List.flatMap_assoc] apply List.flatMap_congr intro index hindex let positions := smallDigitPositions (reductionBlockWidthTicks input) have hpayload := choiceBlockExpand_payload positions (choiceVariableDigits (decodeCNF input) index ++ choiceOccurrenceDigits (decodeCNF input) index truth) (choicePayload_noEnd (decodeCNF input) index truth) simpa [positions, List.flatMap_append, choiceBlockExpand, List.append_assoc] using congrArg (fun row => row ++ [.itemEnd]) hpayload

On a three-CNF source, every generated payload is byte-for-byte the textbook little-endian packed choice item.

theorem choiceGeneratedBitItems_eq_packed {input : List CNFSym} (hthree : IsThreeCNF (decodeCNF input)) (truth : Bool) : choiceGeneratedBitItems truth input = (List.range (reductionVariableCount (decodeCNF input))).map (fun index => choicePackedBitsLE (decodeCNF input) index truth) := by unfold choiceGeneratedBitItems apply List.map_congr_left intro index hindex let positions := smallDigitPositions (reductionBlockWidthTicks input) have hgenerated := choiceBlockExpand_payload positions (choiceVariableDigits (decodeCNF input) index ++ choiceOccurrenceDigits (decodeCNF input) index truth) (choicePayload_noEnd (decodeCNF input) index truth) have htextbook := choiceItemBlock_eq hthree index (List.mem_range.mp hindex) truth (reductionBlockWidthTicks input) (by rw [reductionBlockWidthTicks_eq]; simp) apply map_choiceBlockBit_injective exact hgenerated.symm.trans htextbook

Public compact fields emitted for one generated truth family.

def choiceGeneratedFields (truth : Bool) (input : List CNFSym) : List SubsetSumSym := choiceBitFields (choiceGeneratedBitItems truth input)

Semantic field boundary used in the final item-family assembly.

theorem choiceGeneratedFields_eq_items {input : List CNFSym} (hthree : IsThreeCNF (decodeCNF input)) (truth : Bool) : choiceGeneratedFields truth input = (List.range (reductionVariableCount (decodeCNF input))).flatMap (fun index => encodeCanonicalBitField (reductionItemBits (decodeCNF input) (.choice index truth))) := by rw [choiceGeneratedFields, choiceGeneratedBitItems_eq_packed hthree, choiceBitFields, List.flatMap_map] apply List.flatMap_congr intro index hindex rw [choiceBitField, binaryCanonicalizer_eq] change encodeCanonicalBitField (choiceItemBits (decodeCNF input) index truth) = _ rw [choiceItemBits_eq]
end CLRS.Chapter34.Turing.SubsetSumReduction