Partial fixes for leanprover/lean4#4154

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,23 +164,23 @@ 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) :
   hasAssignment b assignment ↔ hasAssignment b (addAssignment (¬b) assignment) := by
   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

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 α) :

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]

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

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

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 =>

lean-toolchain

@@ -1,2 +1 @@
-leanprover/lean4:nightly-2024-05-21
-
+leanprover/lean4-pr-releases:pr-release-4154