From a200b634c2b407efa1ac9a378d275e31fcdc6b8b Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Mon, 3 Jun 2024 18:03:08 +0200 Subject: [PATCH] Partial fixes for https://github.com/leanprover/lean4/pull/4154 --- LeanSAT/LRAT/Assignment.lean | 20 +++++++++---------- LeanSAT/LRAT/CNF.lean | 4 ++-- LeanSAT/LRAT/Formula/Basic.lean | 5 +++-- LeanSAT/LRAT/Formula/RatAddSound.lean | 14 ++++++++----- LeanSAT/LRAT/Formula/RupAddSound.lean | 6 +++--- .../Reflect/BVExpr/BitBlast/Lemmas/Add.lean | 4 +++- lean-toolchain | 3 +-- 7 files changed, 31 insertions(+), 25 deletions(-) diff --git a/LeanSAT/LRAT/Assignment.lean b/LeanSAT/LRAT/Assignment.lean index de62ea8d..fe688b94 100644 --- a/LeanSAT/LRAT/Assignment.lean +++ b/LeanSAT/LRAT/Assignment.lean @@ -98,14 +98,14 @@ def hasAssignment (b : Bool) : Assignment → Bool := theorem removePos_addPos_cancel {assignment : Assignment} (h : ¬(hasPosAssignment assignment)) : removePosAssignment (addPosAssignment assignment) = assignment := by - rw [removePosAssignment, addPosAssignment] - rw [hasPosAssignment] at h + rw [removePosAssignment.eq_def, addPosAssignment.eq_def] + rw [hasPosAssignment.eq_def] at h cases assignment <;> simp_all theorem removeNeg_addNeg_cancel {assignment : Assignment} (h : ¬(hasNegAssignment assignment)) : removeNegAssignment (addNegAssignment assignment) = assignment := by - rw [removeNegAssignment, addNegAssignment] - rw [hasNegAssignment] at h + rw [removeNegAssignment.eq_def, addNegAssignment.eq_def] + rw [hasNegAssignment.eq_def] at h cases assignment <;> simp_all theorem remove_add_cancel {assignment : Assignment} {b : Bool} (h : ¬(hasAssignment b assignment)) : @@ -129,9 +129,9 @@ theorem has_of_both (b : Bool) : hasAssignment b both = true := by theorem has_of_add (assignment : Assignment) (b : Bool) : hasAssignment b (addAssignment b assignment) := by rw [addAssignment, hasAssignment] split - . rw [hasPosAssignment, addPosAssignment] + . rw [hasPosAssignment.eq_def, addPosAssignment.eq_def] cases assignment <;> simp - . rw [hasNegAssignment, addNegAssignment] + . rw [hasNegAssignment.eq_def, addNegAssignment.eq_def] cases assignment <;> simp theorem not_hasPos_of_removePos (assignment : Assignment) : ¬hasPosAssignment (removePosAssignment assignment) := by @@ -164,11 +164,11 @@ theorem unassigned_of_has_neither (assignment : Assignment) (lacks_pos : ¬(hasP split at lacks_pos <;> simp_all (config := { decide := true }) theorem hasPos_of_addNeg (assignment : Assignment) : hasPosAssignment (addNegAssignment assignment) = hasPosAssignment assignment := by - rw [hasPosAssignment, addNegAssignment] + rw [hasPosAssignment.eq_def, addNegAssignment.eq_def] cases assignment <;> simp (config := { decide := true }) theorem hasNeg_of_addPos (assignment : Assignment) : hasNegAssignment (addPosAssignment assignment) = hasNegAssignment assignment := by - rw [hasNegAssignment, addPosAssignment] + rw [hasNegAssignment.eq_def, addPosAssignment.eq_def] cases assignment <;> simp (config := { decide := true }) theorem has_iff_has_of_add_complement (assignment : Assignment) (b : Bool) : @@ -176,11 +176,11 @@ theorem has_iff_has_of_add_complement (assignment : Assignment) (b : Bool) : by_cases hb : b <;> simp [hb, hasAssignment, addAssignment, hasPos_of_addNeg, hasNeg_of_addPos] theorem addPos_of_addNeg_eq_both (assignment : Assignment) : addPosAssignment (addNegAssignment assignment) = both := by - rw [addPosAssignment, addNegAssignment] + rw [addPosAssignment.eq_def, addNegAssignment.eq_def] cases assignment <;> simp theorem addNeg_of_addPos_eq_both (assignment : Assignment) : addNegAssignment (addPosAssignment assignment) = both := by - rw [addNegAssignment, addPosAssignment] + rw [addNegAssignment.eq_def, addPosAssignment.eq_def] cases assignment <;> simp instance {n : Nat} : HSat (PosFin n) (Array Assignment) where diff --git a/LeanSAT/LRAT/CNF.lean b/LeanSAT/LRAT/CNF.lean index 60e5bae3..df793995 100644 --- a/LeanSAT/LRAT/CNF.lean +++ b/LeanSAT/LRAT/CNF.lean @@ -18,11 +18,11 @@ theorem sat_negate_iff_not_sat {p : α → Bool} {l : Literal α} : p ⊨ negate simp only [negateLiteral, sat_iff] constructor . intro h pl - rw [sat_iff, h, not] at pl + rw [sat_iff, h, not.eq_def] at pl split at pl <;> simp_all . intro h rw [sat_iff] at h - rw [not] + rw [not.eq_def] split <;> simp_all theorem unsat_of_limplies_complement [HSat α t] (x : t) (l : Literal α) : diff --git a/LeanSAT/LRAT/Formula/Basic.lean b/LeanSAT/LRAT/Formula/Basic.lean index 6eaa79f5..9baf3c0f 100644 --- a/LeanSAT/LRAT/Formula/Basic.lean +++ b/LeanSAT/LRAT/Formula/Basic.lean @@ -44,7 +44,8 @@ theorem assignments_invariant_of_strong_assignments_invariant {n : Nat} (f : Def Bool.decide_coe, List.all_eq_true] at pf specialize pf (unit (i, b)) h simp [Clause.instHSat, unit_eq, Clause.toList] at pf - exact pf + -- exact pf + sorry -- TODO theorem assignments_invariant_entails_limplies {n : Nat} (f : DefaultFormula n) (f_assignments_invariant : assignments_invariant f) : limplies (PosFin n) f f.assignments := by @@ -79,7 +80,7 @@ theorem insert_preserves_ratUnits {n : Nat} (f : DefaultFormula n) (c : DefaultC theorem ofArray_fold_fn_preserves_assignments_size {n : Nat} (assignments : Array Assignment) (cOpt : Option (DefaultClause n)) : (ofArray_fold_fn assignments cOpt).size = assignments.size := by - rw [ofArray_fold_fn] + rw [ofArray_fold_fn.eq_def] split . rfl . split <;> simp [Array.modify_preserves_size] diff --git a/LeanSAT/LRAT/Formula/RatAddSound.lean b/LeanSAT/LRAT/Formula/RatAddSound.lean index 7b2934fb..5d23397c 100644 --- a/LeanSAT/LRAT/Formula/RatAddSound.lean +++ b/LeanSAT/LRAT/Formula/RatAddSound.lean @@ -399,7 +399,7 @@ theorem performRatCheck_success_entails_c_without_negPivot {n : Nat} (f : Defaul (negPivot : Literal (PosFin n)) (ratHint : Nat × Array Nat) (performRatCheck_success : (performRatCheck f negPivot ratHint).2) (c : DefaultClause n) : f.clauses[ratHint.1]! = some c → limplies (PosFin n) f (c.delete negPivot) := by intro hc p pf - simp only [performRatCheck, hc, Bool.or_eq_true, Bool.not_eq_true'] at performRatCheck_success + simp only [performRatCheck.eq_def, hc, Bool.or_eq_true, Bool.not_eq_true'] at performRatCheck_success split at performRatCheck_success . next h => exact insertRat_entails_hsat f hf (DefaultClause.delete c negPivot) p pf h @@ -413,7 +413,8 @@ theorem performRatCheck_success_entails_c_without_negPivot {n : Nat} (f : Defaul have c_negPivot_in_fc : (DefaultClause.delete c negPivot) ∈ toList (insert f (DefaultClause.delete c negPivot)) := by rw [insert_iff] exact Or.inl rfl - exact of_decide_eq_true $ pfc (DefaultClause.delete c negPivot) c_negPivot_in_fc + --exact of_decide_eq_true $ pfc (DefaultClause.delete c negPivot) c_negPivot_in_fc + sorry theorem existsRatHint_of_ratHintsExhaustive {n : Nat} (f : DefaultFormula n) (f_readyForRatAdd : readyForRatAdd f) (pivot : Literal (PosFin n)) (ratHints : Array (Nat × Array Nat)) @@ -524,10 +525,12 @@ theorem performRatCheck_fold_success_entails_safe_insert {n : Nat} (f : DefaultF rw [insert_iff] at c'_in_fc rcases c'_in_fc with c'_eq_c | c'_in_f . simp only [c'_eq_c, decide_eq_true_eq] at pc' - exact pc' pc + -- exact pc' pc + sorry . simp only [(· ⊨ ·), List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, List.all_eq_true] at pf - exact pc' $ pf c' c'_in_f + -- exact pc' $ pf c' c'_in_f + sorry . rw [← Clause.limplies_iff_mem] at pivot_in_c let p' : (PosFin n) → Bool := fun a => if a = pivot.1 then pivot.2 else p a have p'_rw : p' = (fun a => if a = pivot.1 then pivot.2 else p a) := rfl @@ -545,7 +548,8 @@ theorem performRatCheck_fold_success_entails_safe_insert {n : Nat} (f : DefaultF . have pc' : p ⊨ c' := by simp only [(· ⊨ ·), List.any_eq_true, Prod.exists, Bool.exists_bool, Bool.decide_coe, List.all_eq_true] at pf - exact of_decide_eq_true $ pf c' c'_in_f + -- exact of_decide_eq_true $ pf c' c'_in_f + sorry have negPivot_in_c' : negateLiteral pivot ∈ Clause.toList c' := mem_of_necessary_assignment pc' p'_not_entails_c' have h : p ⊨ (c'.delete (negateLiteral pivot)) := by rcases existsRatHint_of_ratHintsExhaustive f f_readyForRatAdd pivot ratHints diff --git a/LeanSAT/LRAT/Formula/RupAddSound.lean b/LeanSAT/LRAT/Formula/RupAddSound.lean index ad590458..372e2580 100644 --- a/LeanSAT/LRAT/Formula/RupAddSound.lean +++ b/LeanSAT/LRAT/Formula/RupAddSound.lean @@ -359,7 +359,7 @@ theorem encounteredBoth_entails_unsat {n : Nat} (c : DefaultClause n) (assignmen (l : Literal (PosFin n)) (_ : l ∈ c.clause) : (reduce_fold_fn assignment res l) = encounteredBoth → unsatisfiable (PosFin n) assignment := by intro h - rw [reduce_fold_fn] at h + rw [reduce_fold_fn.eq_def] at h split at h <;> [ exact ih rfl; @@ -391,7 +391,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi simp only [reduce_postcondition_induction_motive, Fin.getElem_fin, forall_exists_index, and_imp, Prod.forall] constructor . intro h p - rw [reduce_fold_fn] at h + rw [reduce_fold_fn.eq_def] at h split at h . simp only at h . split at h @@ -443,7 +443,7 @@ theorem reduce_fold_fn_preserves_induction_motive {c_arr : Array (Literal (PosFi . simp only at h . simp only at h . intro i b h p hp j j_lt_idx_add_one p_entails_c_arr_j - rw [reduce_fold_fn] at h + rw [reduce_fold_fn.eq_def] at h split at h . simp only at h . split at h diff --git a/LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean b/LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean index 7cffe30b..4a82b4fd 100644 --- a/LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean +++ b/LeanSAT/Reflect/BVExpr/BitBlast/Lemmas/Add.lean @@ -21,6 +21,8 @@ theorem denote_mkFullAdderOut (assign : Assignment) (aig : AIG BVBit) (input : F Bool.bne_left_inj] rw [LawfulOperator.denote_mem_prefix (f := mkXorCached)] +-- deterministic timeout: #check mkFullAdderCarry.eq_1 + @[simp] theorem denote_mkFullAdderCarry (assign : Assignment) (aig : AIG BVBit) (input : FullAdderInput aig) : ⟦mkFullAdderCarry aig input, assign.toAIGAssignment⟧ @@ -35,7 +37,7 @@ theorem denote_mkFullAdderCarry (assign : Assignment) (aig : AIG BVBit) (input : ⟦aig, input.lhs, assign.toAIGAssignment⟧ ⟦aig, input.rhs, assign.toAIGAssignment⟧) := by - simp only [mkFullAdderCarry, Ref_cast', Int.reduceNeg, denote_mkOrCached, + simp only [mkFullAdderCarry.eq_def, Ref_cast', Int.reduceNeg, denote_mkOrCached, LawfulOperator.denote_input_entry, denote_mkAndCached, denote_projected_entry', denote_mkXorCached, denote_projected_entry] conv => diff --git a/lean-toolchain b/lean-toolchain index 1c8a9b7a..04fed034 100644 --- a/lean-toolchain +++ b/lean-toolchain @@ -1,2 +1 @@ -leanprover/lean4:nightly-2024-05-21 - +leanprover/lean4-pr-releases:pr-release-4154