chore: cleanup non terminal simps in LRAT (#7243)
This PR cleans up non terminal simps in the LRAT checking module.
This commit is contained in:
Henrik Böving
GitHub
parent
56a3ac1814
commit
e801dc96ca
3 changed files with 19 additions and 19 deletions
|
|
@ -32,17 +32,13 @@ theorem mem_of_necessary_assignment {n : Nat} {p : (PosFin n) → Bool} {c : Def
|
|||
simp only [Entails.eval, Bool.not_eq_false] at h
|
||||
split at h
|
||||
· next heq => simp [Literal.negate, ← heq, h, v_in_c]
|
||||
· next hne =>
|
||||
exfalso
|
||||
simp [(· ⊨ ·), h] at pv
|
||||
· next hne => simp [(· ⊨ ·), h] at pv
|
||||
· specialize p'_not_entails_c v
|
||||
have h := p'_not_entails_c.2 v_in_c
|
||||
simp only [(· ⊨ ·), Bool.not_eq_false] at h
|
||||
split at h
|
||||
· next heq => simp [Literal.negate, ← heq, h, v_in_c]
|
||||
· next hne =>
|
||||
exfalso
|
||||
simp [(· ⊨ ·), h] at pv
|
||||
· next hne => simp [(· ⊨ ·), h] at pv
|
||||
|
||||
theorem entails_of_irrelevant_assignment {n : Nat} {p : (PosFin n) → Bool} {c : DefaultClause n}
|
||||
{l : Literal (PosFin n)} (p_entails_cl : p ⊨ c.delete (Literal.negate l)) :
|
||||
|
|
@ -199,7 +195,8 @@ theorem sat_of_confirmRupHint_of_insertRat_fold {n : Nat} (f : DefaultFormula n)
|
|||
intro fc confirmRupHint_fold_res confirmRupHint_success
|
||||
let motive := ConfirmRupHintFoldEntailsMotive fc.1
|
||||
have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
|
||||
simp [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRatUnits, hf.2.1, fc, motive]
|
||||
simp only [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRatUnits, hf.2.1,
|
||||
Bool.false_eq_true, false_implies, and_true, true_and, motive, fc]
|
||||
have fc_satisfies_AssignmentsInvariant : AssignmentsInvariant fc.1 :=
|
||||
assignmentsInvariant_insertRatUnits f hf (negate c)
|
||||
exact limplies_of_assignmentsInvariant fc.1 fc_satisfies_AssignmentsInvariant
|
||||
|
|
|
|||
|
|
@ -177,7 +177,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
|
|||
let mostRecentUnitIdx : Fin (insertUnit (units, assignments, foundContradiction) l).1.size :=
|
||||
⟨units.size, units_size_lt_updatedUnits_size⟩
|
||||
have j_lt_updatedUnits_size : j.1 < (insertUnit (units, assignments, foundContradiction) l).1.size := by
|
||||
simp [insertUnit, h5, ite_false, Array.size_push]
|
||||
simp only [insertUnit, h5, Bool.false_eq_true, ↓reduceIte, Array.size_push]
|
||||
exact Nat.lt_trans j.2 (Nat.lt_succ_self units.size)
|
||||
match hb : b, hl : l.2 with
|
||||
| true, true =>
|
||||
|
|
@ -225,7 +225,7 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
|
|||
exact k_ne_l rfl
|
||||
| false, true =>
|
||||
refine ⟨mostRecentUnitIdx, ⟨j.1, j_lt_updatedUnits_size⟩, i_gt_zero, ?_⟩
|
||||
simp [insertUnit, h5, ite_false, Array.getElem_push_eq, ne_eq]
|
||||
simp only [insertUnit, h5, Bool.false_eq_true, ↓reduceIte, mostRecentUnitIdx]
|
||||
constructor
|
||||
· simp +zetaDelta [i_eq_l, ← hl]
|
||||
rfl
|
||||
|
|
@ -259,7 +259,6 @@ theorem insertUnitInvariant_insertUnit {n : Nat} (assignments0 : Array Assignmen
|
|||
rcases Nat.lt_or_eq_of_le <| Nat.le_of_lt_succ k_property with k_lt_units_size | k_eq_units_size
|
||||
· exact h k_lt_units_size
|
||||
· simp only [← k_eq_units_size, not_true, mostRecentUnitIdx] at k_ne_l
|
||||
exact k_ne_l rfl
|
||||
| false, false =>
|
||||
exfalso
|
||||
have assignments_i_rw : assignments[i.1]! = assignments[i.1] := by
|
||||
|
|
|
|||
|
|
@ -42,11 +42,11 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
|
|||
apply Exists.intro i
|
||||
by_cases l.1.1 = i.1
|
||||
· next l_eq_i =>
|
||||
simp [l_eq_i, Array.getElem_modify_self, h]
|
||||
simp only [Bool.false_eq_true, ↓reduceIte, l_eq_i, Array.getElem_modify_self, h,
|
||||
insertUnit_res]
|
||||
exact add_both_eq_both l.2
|
||||
· next l_ne_i =>
|
||||
simp [Array.getElem_modify_of_ne l_ne_i]
|
||||
exact h
|
||||
simpa [Array.getElem_modify_of_ne l_ne_i] using h
|
||||
· apply Exists.intro l.1
|
||||
simp only [insertUnit, hl, ite_false, Array.getElem_modify_self, reduceCtorEq]
|
||||
simp only [getElem!_def, l_in_bounds, Array.getElem?_eq_getElem,
|
||||
|
|
@ -60,8 +60,9 @@ theorem contradiction_of_insertUnit_success {n : Nat} (assignments : Array Assig
|
|||
· next l_eq_false =>
|
||||
simp only [Bool.not_eq_true] at l_eq_false
|
||||
simp only [l_eq_false]
|
||||
simp [hasAssignment, l_eq_false, hasNegAssignment, getElem!_def, l_in_bounds,
|
||||
Array.getElem?_eq_getElem] at hl
|
||||
simp only [hasAssignment, l_eq_false, Bool.false_eq_true, ↓reduceIte, hasNegAssignment,
|
||||
getElem!_def, l_in_bounds, Array.getElem?_eq_getElem, Bool.not_eq_true,
|
||||
insertUnit_res] at hl
|
||||
split at hl <;> simp_all +decide
|
||||
|
||||
theorem contradiction_of_insertUnit_fold_success {n : Nat} (assignments : Array Assignment) (assignments_size : assignments.size = n)
|
||||
|
|
@ -350,7 +351,10 @@ theorem assignmentsInvariant_insertRupUnits_of_assignmentsInvariant {n : Nat} (f
|
|||
rcases hp2 with ⟨i2, hp2⟩
|
||||
simp only [Fin.getElem_fin] at h1
|
||||
simp only [Fin.getElem_fin] at h2
|
||||
simp [h1, Clause.toList, unit_eq, List.mem_singleton, h2] at hp1 hp2
|
||||
simp only [Clause.toList, h1, unit_eq, List.mem_cons, Prod.mk.injEq, Bool.false_eq_true,
|
||||
and_false, List.not_mem_nil, or_self, Bool.decide_eq_false, Bool.not_eq_eq_eq_not,
|
||||
Bool.not_true, false_and, and_true, or_false, false_or, h2, Bool.true_eq_false, j2_unit,
|
||||
j1_unit] at hp1 hp2
|
||||
simp only [hp2.1, ← hp1.1, decide_eq_true_eq, true_and] at hp2
|
||||
simp [hp1.2] at hp2
|
||||
|
||||
|
|
@ -693,8 +697,7 @@ theorem confirmRupHint_preserves_motive {n : Nat} (f : DefaultFormula n) (rupHin
|
|||
simp only [Bool.true_eq_false, decide_false, Bool.false_eq_true, ↓reduceIte,
|
||||
hasNeg_addPos]
|
||||
exact pacc
|
||||
· exfalso -- hb, pi, l_eq_i, and plb are incompatible
|
||||
simp only [Bool.not_eq_true] at hb
|
||||
· simp only [Bool.not_eq_true] at hb
|
||||
simp [(· ⊨ ·), hb, Subtype.ext l_eq_i, pi] at plb
|
||||
· simp only [Bool.not_eq_true] at pi
|
||||
simp only [pi, decide_true]
|
||||
|
|
@ -726,7 +729,8 @@ theorem sat_of_confirmRupHint_insertRup_fold {n : Nat} (f : DefaultFormula n)
|
|||
intro fc confirmRupHint_fold_res confirmRupHint_success
|
||||
let motive := ConfirmRupHintFoldEntailsMotive fc.1
|
||||
have h_base : motive 0 (fc.fst.assignments, [], false, false) := by
|
||||
simp [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRupUnits, f_readyForRupAdd.2.1, motive, fc]
|
||||
simp only [ConfirmRupHintFoldEntailsMotive, size_assignments_insertRupUnits,
|
||||
f_readyForRupAdd.2.1, Bool.false_eq_true, false_implies, and_true, true_and, motive, fc]
|
||||
have fc_satisfies_AssignmentsInvariant :=
|
||||
assignmentsInvariant_insertRupUnits_of_assignmentsInvariant f f_readyForRupAdd (negate c)
|
||||
exact limplies_of_assignmentsInvariant fc.1 fc_satisfies_AssignmentsInvariant
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue