def
definition
def or abbrev
buildPeelingResult
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Definition body.
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 }
168 · -- Inductive case: U is nonempty
169 have hne : U.Nonempty := Finset.card_pos.mp (by omega)
170 let ⟨⟨K, v⟩, _, hvmem, hment, honly, hdet⟩ := extractFromPC inputs aRef φ H hPC U hU hne
171 let U' := U.erase v
172 have hU' : U' ⊆ inputs := fun w hw => hU (Finset.mem_erase.mp hw).2
173 have hcard' : U'.card = k := by rw [Finset.card_erase_of_mem hvmem]; omega
174 let rec_result := ih U' hU' hcard'
175 exact {
176 vars := v :: rec_result.vars
177 constrs := K :: rec_result.constrs
178 len_eq := by simp only [List.length_cons, rec_result.len_eq]
179 nodup := by
180 refine List.Nodup.cons ?_ rec_result.nodup
181 intro hv_in_vs
182 have hv_in_U' := (rec_result.cover v).mp hv_in_vs
183 exact (Finset.not_mem_erase v U) hv_in_U'
184 cover := by
185 intro w
186 simp only [List.mem_cons]
187 constructor
188 · intro hw
189 rcases hw with rfl | hw'
190 · exact hvmem
191 · exact Finset.mem_of_mem_erase ((rec_result.cover w).mp hw')
192 · intro hw
193 by_cases hwv : w = v
194 · left; exact hwv
195 · right; exact (rec_result.cover w).mpr (Finset.mem_erase.mpr ⟨hwv, hw⟩)
196 step := by
197 intro idx hidx
198 simp only [List.length_cons] at hidx
199 cases idx with
200 | zero =>
201 simp only [List.drop_succ_cons, List.drop_zero]
202 constructor
203 · exact hment
204 constructor
205 · intro w hw
206 have hw_in_U' := (rec_result.cover w).mp hw
207 have hw_in_U := Finset.mem_of_mem_erase hw_in_U'
208 have hw_ne_v : w ≠ v := fun heq => by
209 rw [heq] at hw_in_U'
210 exact (Finset.not_mem_erase v U) hw_in_U'
211 exact honly w hw_in_U hw_ne_v
212 · exact hdet
213 | succ idx' =>
214 simp only [List.drop_succ_cons]
215 have hidx' : idx' < rec_result.vars.length := by simp at hidx; omega
216 exact rec_result.step idx' hidx'
217 }
218
219/-- **PROVED**: PC ⇒ peeling.
220 If the PC condition holds for inputs, we can construct a peeling witness.
221
222 **Proof**: Classical Finset induction via `buildPeelingResult`. At each step:
223 1. Given nonempty U ⊆ inputs, PC gives constraint K and variable v ∈ U
224 2. K mentions only v from U, and determines v
225 3. Recursively peel U \ {v} to get (vs, cs)
226 4. Return (v :: vs, K :: cs)
227
228 Base case: empty U gives ([], []). -/