some cleanup

Saturn/Containment.lean

@@ -40,6 +40,7 @@ def varDomDecide : (v1 : Option Bool) → (v2 : Option Bool) → Decidable (v1 
                       assumption
                   c (lem2) 
             )
+
 def contains{n: Nat} (cl1 cl2 : Clause n) : Prop :=
   ∀ k : Nat, ∀ kw : k < n, ∀ b : Bool, cl2.coords k kw = some b → cl1.coords k kw = some b
 
@@ -86,7 +87,7 @@ theorem contains_beyond_zero_implies_contains {n: Nat} (cl1 cl2 : Clause n) :
     intro h k kw b
     exact h k kw (Nat.zero_le _) b
 
-def containsSat{n: Nat} (cl1 cl2 : Clause n) :
+theorem containsSat{n: Nat} (cl1 cl2 : Clause n) :
   cl1 ⊇  cl2 → (valuation : Valuation n) → clauseSat cl2 valuation → clauseSat cl1 valuation := by
     intro dom valuation  
     intro ⟨j, jw, vs⟩ 

Saturn/DPLL.lean

@@ -408,24 +408,18 @@ instance {dom n: Nat}{clauses : Vector (Clause (n + 1)) dom}
 def proveOrDisprove{n dom : Nat}(clauses : Vector (Clause (n + 1)) dom) :=
             getProof (solveSAT clauses)
 
-def decideSat{n dom : Nat}(clauses : Vector (Clause (n + 1)) dom) :
+instance {n dom : Nat}{clauses : Vector (Clause (n + 1)) dom} :
     Decidable (isSat clauses) := 
-      match solveSAT clauses with
+    match solveSAT clauses with
       | SatSolution.sat valuation evidence =>
           isTrue ⟨valuation, evidence⟩
-      | SatSolution.unsat tree =>
-          isFalse $ fun hyp => not_sat_and_unsat clauses hyp $ tree_unsat clauses tree
+      | SatSolution.unsat tree => isFalse $ fun hyp => 
+            not_sat_and_unsat clauses hyp $ tree_unsat clauses tree
 
-def decideUnSat{n dom : Nat}(clauses : Vector (Clause (n + 1)) dom) :
+instance {n dom : Nat}{clauses : Vector (Clause (n + 1)) dom} :
     Decidable (isUnSat clauses) := 
-      match solveSAT clauses with
-      | SatSolution.sat valuation evidence =>
-          isFalse $ fun hyp => not_sat_and_unsat clauses ⟨valuation, evidence⟩ hyp    
+    match solveSAT clauses with
+      | SatSolution.sat valuation evidence => isFalse $ fun hyp => 
+        not_sat_and_unsat clauses ⟨valuation, evidence⟩ hyp    
       | SatSolution.unsat tree =>
-          isTrue $ tree_unsat clauses tree
-
-instance {n dom : Nat}{clauses : Vector (Clause (n + 1)) dom} :
-    Decidable (isSat clauses) := decideSat clauses
-
-instance {n dom : Nat}{clauses : Vector (Clause (n + 1)) dom} :
-    Decidable (isUnSat clauses) := decideUnSat clauses
+        isTrue $ tree_unsat clauses tree

Saturn/Examples.lean

@@ -15,7 +15,7 @@ def cl2 : Clause 2 := (some false) +: (none) +: Vector.nil -- ¬P
 
 def cl3 : Clause 2 := (none) +: (some false) +: Vector.nil -- ¬Q
 
-def eg1Statement : Vector (Clause 2) 3 := cl1 +: cl2 +: cl3 +: Vector.nil -- all three clauses
+def eg1Statement := cl1 +: cl2 +: cl3 +: Vector.nil -- all three clauses
 def eg2Statement := cl1 +: cl3 +: Vector.nil -- clauses 1 and 3 only
 
 #eval decide (isSat eg2Statement)  -- true

Saturn/Resolution.lean

@@ -166,7 +166,7 @@ def unitTriple(n : Nat)(k: Nat)(lt : k < n + 1) :
                       ⟩
 
 -- if a valuation satisfies the bottom two clauses, it satisfies the top clause as a proposition
-theorem triple_step_proof{n: Nat}(left right top : Clause (n + 1))
+theorem triple_step{n: Nat}(left right top : Clause (n + 1))
   (triple : ResolutionTriple left right top) :
         (valuation: Valuation (n + 1))  → (clauseSat left valuation) → 
         (clauseSat right valuation) → (clauseSat top valuation) := 
@@ -308,20 +308,17 @@ theorem resolutionToProof{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom)(top
                 resolutionToProof clauses left leftTree valuation base 
               let rightBase : clauseSat right valuation := 
                 resolutionToProof clauses right rightTree  valuation base 
-              let lemStep := triple_step_proof left right top triple valuation leftBase rightBase
+              let lemStep := triple_step left right top triple valuation leftBase rightBase
             by
               exact lemStep
               done
 
 -- unsat from a resolution tree
 theorem tree_unsat{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom):
       ResolutionTree clauses (contradiction (n + 1)) → isUnSat clauses := 
-        fun tree => 
-          fun valuation =>
-            fun hyp : ∀ p : Nat, ∀ pw : p < dom, clauseSat (clauses.coords p pw) valuation =>
-              let lem := resolutionToProof clauses (contradiction (n + 1))
-                            tree valuation hyp
-              contradiction_is_false _ valuation lem
+  fun tree valuation hyp =>
+    contradiction_is_false _ valuation $ 
+      resolutionToProof clauses (contradiction (n + 1)) tree valuation hyp
 
 /-
 Pieces for building trees.
@@ -421,6 +418,3 @@ theorem trees_preserve_notsomebranch{dom n : Nat}{clauses : Vector (Clause (n +
                         (left.coords k kw) (right.coords k kw) (top.coords k kw) join
                           leftLem rightLem
                     lem hyp               
-
-
-

Saturn/SatSolution.lean

@@ -15,23 +15,16 @@ inductive SatSolution{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom) where
         → clauseSat (clauses.coords k kw) valuation) → SatSolution clauses 
 
 def SatSolution.toString{dom n: Nat}{clauses : Vector (Clause (n + 1)) dom}:
-        (sol: SatSolution clauses) →  String := 
-      fun sol =>
-      match sol with
+        (sol: SatSolution clauses) →  String 
       | unsat tree => "unsat: " ++ tree.toString 
       | sat valuation _ => "sat: " ++ (valuation.coords.list).toString
 
-def solutionProp{dom n: Nat}{clauses : Vector (Clause (n + 1)) dom}
-                  (sol : SatSolution clauses) : Prop :=
-  match sol with
-  | SatSolution.unsat _  => isUnSat clauses
-  | SatSolution.sat _ _ => isSat clauses
+def solutionProp{dom n: Nat}{clauses : Vector (Clause (n + 1)) dom}:
+                  (sol : SatSolution clauses) →  Prop 
+| SatSolution.unsat _  => isUnSat clauses
+| SatSolution.sat _ _ => isSat clauses
 
 def solutionProof{dom n: Nat}{clauses : Vector (Clause (n + 1)) dom}
-                  (sol : SatSolution clauses) :
-                    solutionProp sol :=
-  match sol with
-  | SatSolution.unsat tree   => 
-          tree_unsat clauses tree
-  | SatSolution.sat valuation evidence =>
-          ⟨valuation, evidence⟩
+                  :(sol : SatSolution clauses) → solutionProp sol 
+| SatSolution.unsat tree  => tree_unsat clauses tree
+| SatSolution.sat valuation evidence => ⟨valuation, evidence⟩