PeelingResult

formal source

 134  exact ⟨(K, v), hK.1, hv.1, hv.2.1, hv.2.2.1, hv.2.2.2⟩
 135
 136/-- Bundled result type for peeling construction. -/
 137structure PeelingResult {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
 138    (φ : CNF n) (H : XORSystem n) (U : Finset (Var n)) where
 139  vars : List (Var n)
 140  constrs : List (Constraint n)
 141  len_eq : vars.length = constrs.length
 142  nodup : vars.Nodup
 143  cover : ∀ v, v ∈ vars ↔ v ∈ U
 144  step : ∀ k (hk : k < vars.length),
 145    let v := vars.get ⟨k, hk⟩
 146    let K := constrs.get ⟨k, by omega⟩
 147    mentionsVar K v = true ∧
 148    (∀ w ∈ vars.drop k.succ, mentionsVar K w = false) ∧
 149    determinesVar aRef K v
 150
 151/-- **PROVED**: Build the peeling order via Finset induction.
 152    At each step, PC gives constraint K and variable v ∈ U that K uniquely determines.
 153    Recursively peel U \ {v} to get (vs, cs), then return (v :: vs, K :: cs). -/
 154noncomputable def buildPeelingResult {n : Nat} (inputs : InputSet n) (aRef : Assignment n)
 155    (φ : CNF n) (H : XORSystem n) (hPC : PC inputs aRef φ H)
 156    (U : Finset (Var n)) (hU : U ⊆ inputs) :
 157    PeelingResult inputs aRef φ H U := by
 158  induction' hcard : U.card with k ih generalizing U
 159  · -- Base case: U is empty
 160    exact {
 161      vars := []
 162      constrs := []
 163      len_eq := rfl
 164      nodup := List.nodup_nil
 165      cover := by intro v; simp; rw [Finset.card_eq_zero.mp hcard]; exact Finset.not_mem_empty v
 166      step := by intro k hk; simp at hk
 167    }