style: proof style in LRAT.LRATCheckerSOund

LeanSAT/LRAT/LRATCheckerSound.lean

@@ -9,7 +9,7 @@ import LeanSAT.LRAT.CNF
 open LRAT Result Formula Clause Sat
 
 theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (f_readyForRupAdd : readyForRupAdd f)
-  (rupHints: Array Nat) (rupAddSuccess : (Formula.performRupAdd f Clause.empty rupHints).snd = true) : unsatisfiable α f := by
+    (rupHints: Array Nat) (rupAddSuccess : (Formula.performRupAdd f Clause.empty rupHints).snd = true) : unsatisfiable α f := by
   let f' := (performRupAdd f empty rupHints).1
   have f'_def := rupAdd_result f empty rupHints f' f_readyForRupAdd
   rw [← rupAddSuccess] at f'_def
@@ -29,12 +29,12 @@ theorem addEmptyCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f
     empty_eq, List.any_nil] at pf
 
 theorem addRupCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (f_readyForRupAdd : readyForRupAdd f)
-  (f_readyForRatAdd : readyForRatAdd f) (c : β) (f' : σ) (rupHints : Array Nat) (heq : performRupAdd f c rupHints = (f', true))
-  (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a)
-  (ih : ∀ (f : σ),
-    readyForRupAdd f → readyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) →
-    lratChecker f restPrf = success → unsatisfiable α f)
-  (f'_success : lratChecker f' restPrf = success) : unsatisfiable α f := by
+    (f_readyForRatAdd : readyForRatAdd f) (c : β) (f' : σ) (rupHints : Array Nat) (heq : performRupAdd f c rupHints = (f', true))
+    (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a)
+    (ih : ∀ (f : σ),
+      readyForRupAdd f → readyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) →
+      lratChecker f restPrf = success → unsatisfiable α f)
+    (f'_success : lratChecker f' restPrf = success) : unsatisfiable α f := by
   have f'_def := rupAdd_result f c rupHints f' f_readyForRupAdd heq
   have f'_readyForRupAdd : readyForRupAdd f' := by
     rw [f'_def]
@@ -49,14 +49,14 @@ theorem addRupCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f :
   exact ih p pf
 
 theorem addRatCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (f_readyForRupAdd : readyForRupAdd f)
-  (f_readyForRatAdd : readyForRatAdd f) (c : β) (pivot : Literal α) (f' : σ) (rupHints : Array Nat)
-  (ratHints : Array (Nat × Array Nat)) (pivot_limplies_c : limplies α pivot c)
-  (heq : performRatAdd f c pivot rupHints ratHints = (f', true))
-  (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a)
-  (ih : ∀ (f : σ),
-    readyForRupAdd f → readyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) →
-    lratChecker f restPrf = success → unsatisfiable α f)
-  (f'_success : lratChecker f' restPrf = success) : unsatisfiable α f := by
+    (f_readyForRatAdd : readyForRatAdd f) (c : β) (pivot : Literal α) (f' : σ) (rupHints : Array Nat)
+    (ratHints : Array (Nat × Array Nat)) (pivot_limplies_c : limplies α pivot c)
+    (heq : performRatAdd f c pivot rupHints ratHints = (f', true))
+    (restPrf : List (Action β α)) (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a)
+    (ih : ∀ (f : σ),
+      readyForRupAdd f → readyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) →
+      lratChecker f restPrf = success → unsatisfiable α f)
+    (f'_success : lratChecker f' restPrf = success) : unsatisfiable α f := by
   rw [limplies_iff_mem] at pivot_limplies_c
   have f'_def := ratAdd_result f c pivot rupHints ratHints f' f_readyForRatAdd pivot_limplies_c heq
   have f'_readyForRupAdd : readyForRupAdd f' := by
@@ -73,20 +73,20 @@ theorem addRatCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f :
   exact ih p pf
 
 theorem delCaseSound [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (f_readyForRupAdd : readyForRupAdd f)
-  (f_readyForRatAdd : readyForRatAdd f) (ids : Array Nat) (restPrf : List (Action β α))
-  (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a)
-  (ih : ∀ (f : σ),
-    readyForRupAdd f → readyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) →
-    lratChecker f restPrf = success → unsatisfiable α f)
-  (h : lratChecker (Formula.delete f ids) restPrf = success) : unsatisfiable α f := by
+    (f_readyForRatAdd : readyForRatAdd f) (ids : Array Nat) (restPrf : List (Action β α))
+    (restPrfWellFormed : ∀ (a : Action β α), a ∈ restPrf → wellFormedAction a)
+    (ih : ∀ (f : σ),
+      readyForRupAdd f → readyForRatAdd f → (∀ (a : Action β α), a ∈ restPrf → wellFormedAction a) →
+      lratChecker f restPrf = success → unsatisfiable α f)
+    (h : lratChecker (Formula.delete f ids) restPrf = success) : unsatisfiable α f := by
   intro p pf
   have f_del_readyForRupAdd : readyForRupAdd (Formula.delete f ids) := delete_readyForRupAdd f ids f_readyForRupAdd
   have f_del_readyForRatAdd : readyForRatAdd (Formula.delete f ids) := delete_readyForRatAdd f ids f_readyForRatAdd
   exact ih (delete f ids) f_del_readyForRupAdd f_del_readyForRatAdd restPrfWellFormed h p (limplies_delete p pf)
 
 theorem lratCheckerSound [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (f_readyForRupAdd : readyForRupAdd f)
-  (f_readyForRatAdd : readyForRatAdd f) (prf : List (Action β α)) (prfWellFormed : ∀ a : Action β α, a ∈ prf → wellFormedAction a) :
-  lratChecker f prf = success → unsatisfiable α f := by
+    (f_readyForRatAdd : readyForRatAdd f) (prf : List (Action β α)) (prfWellFormed : ∀ a : Action β α, a ∈ prf → wellFormedAction a) :
+      lratChecker f prf = success → unsatisfiable α f := by
   induction prf generalizing f
   . unfold lratChecker
     simp only [false_implies]
@@ -134,9 +134,9 @@ theorem lratCheckerSound [DecidableEq α] [Clause α β] [Formula α β σ] (f :
       exact delCaseSound f f_readyForRupAdd f_readyForRatAdd ids restPrf restPrfWellFormed ih h
 
 theorem incrementalLRATCheckerSound [DecidableEq α] [Clause α β] [Formula α β σ] (f : σ) (f_readyForRupAdd : readyForRupAdd f)
-  (f_readyForRatAdd : readyForRatAdd f) (a : Action β α) (aWellFormed : wellFormedAction a) :
-  ((incrementalLRATChecker f a).2 = success → unsatisfiable α f) ∧
-  ((incrementalLRATChecker f a).2 = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).1 → unsatisfiable α f) := by
+    (f_readyForRatAdd : readyForRatAdd f) (a : Action β α) (aWellFormed : wellFormedAction a) :
+      ((incrementalLRATChecker f a).2 = success → unsatisfiable α f) ∧
+      ((incrementalLRATChecker f a).2 = out_of_proof → unsatisfiable α (incrementalLRATChecker f a).1 → unsatisfiable α f) := by
   constructor
   . intro incrementalChecker_success p pf
     unfold incrementalLRATChecker at incrementalChecker_success