diff --git a/Saturn/Clause.lean b/Saturn/Clause.lean index 874949c..fbc8826 100644 --- a/Saturn/Clause.lean +++ b/Saturn/Clause.lean @@ -123,7 +123,7 @@ structure IsUnitClause{n: Nat}(clause: Clause (n +1)) where parity: Bool equality : clause = unitClause n parity index bound -def clauseUnit{n: Nat}(clause: Clause (n + 1))(parity: Bool) : Option (IsUnitClause clause) := +def unitClause?{n: Nat}(clause: Clause (n + 1))(parity: Bool) : Option (IsUnitClause clause) := let f : Fin (n + 1) → (Option (IsUnitClause clause)) := fun ⟨k, w⟩ => match deqSeq _ clause.coords ((unitClause n parity k w).coords) with @@ -134,17 +134,17 @@ def clauseUnit{n: Nat}(clause: Clause (n + 1))(parity: Bool) : Option (IsUnitCla let seq : FinSeq (n + 1) (Fin (n + 1)) := fun k w => ⟨k, w⟩ findSome? f seq -structure SomeUnitClause{n : Nat}(clauses : Array (Clause (n + 1))) where +structure SomeUnitClause{n : Nat}(clauses : List (Clause (n + 1))) where pos: Nat - posBound : pos < clauses.size + posBound : pos < clauses.length index: Nat bound : index < n + 1 parity: Bool equality : clauses.get ⟨pos, posBound⟩ = unitClause n parity index bound -def someUnitClauseAux {n : Nat}: (clauses : Array (Clause (n + 1))) → - Vector Nat clauses.size → Vector Nat clauses.size → - (cb: Nat) → (cbBound : cb ≤ clauses.size) → Option (SomeUnitClause clauses) → +def someUnitClauseAux {n : Nat}: (clauses : List (Clause (n + 1))) → + Vector Nat clauses.length → Vector Nat clauses.length → + (cb: Nat) → (cbBound : cb ≤ clauses.length) → Option (SomeUnitClause clauses) → Option (SomeUnitClause clauses) := fun clauses posCount negCount cb => match cb with @@ -156,7 +156,7 @@ def someUnitClauseAux {n : Nat}: (clauses : Array (Clause (n + 1))) → | none => if (posCount.coords m cbBound) + (negCount.coords m cbBound) = 1 then let parity := (posCount.coords m cbBound) == 1 - match clauseUnit (clauses.get ⟨m, cbBound⟩) parity with + match unitClause? (clauses.get ⟨m, cbBound⟩) parity with | some u => some ⟨m, cbBound, u.index, u.bound, u.parity, u.equality⟩ | none => someUnitClauseAux clauses @@ -164,13 +164,13 @@ def someUnitClauseAux {n : Nat}: (clauses : Array (Clause (n + 1))) → else none -def someUnitClause {n : Nat}: (clauses : Array (Clause (n + 1))) → - Vector Nat clauses.size → - Vector Nat clauses.size → +def someUnitClause {n : Nat}: (clauses : List (Clause (n + 1))) → + Vector Nat clauses.length → + Vector Nat clauses.length → Option (SomeUnitClause clauses) := fun clauses posCount negCount => - someUnitClauseAux clauses posCount negCount clauses.size - (Nat.le_refl clauses.size) none + someUnitClauseAux clauses posCount negCount clauses.length + (Nat.le_refl clauses.length) none /- Pure variables: definitions and finding with proofs diff --git a/Saturn/Core.lean b/Saturn/Core.lean index b11a769..fdd11df 100644 --- a/Saturn/Core.lean +++ b/Saturn/Core.lean @@ -22,6 +22,11 @@ def Vector.coords {α : Type}{n : Nat}(v: Vector α n) : FinSeq n α := | m + 1, cons head tail, zero, lt => head | m + 1, cons head tail, j + 1, w => tail.coords j (Nat.le_of_succ_le_succ w) +def Vector.toList {α : Type}{n : Nat}(v: Vector α n) : List α := + match n, v with + | .(zero), nil => [] + | _ + 1, cons head tail => head :: tail.toList + abbrev Clause(n : Nat) : Type := Vector (Option Bool) n abbrev Valuation(n: Nat) : Type := Vector Bool n diff --git a/Saturn/DPLL.lean b/Saturn/DPLL.lean index 2d1e74e..ce98e35 100644 --- a/Saturn/DPLL.lean +++ b/Saturn/DPLL.lean @@ -1,7 +1,7 @@ import Saturn.Prover import Saturn.FinSeq import Saturn.Vector -import Saturn.Clause +import Saturn.Clause import Saturn.Containment import Saturn.Solverstep import Saturn.Resolution @@ -20,7 +20,7 @@ The DPLL algorithm with proofs. Here we implement: - lifting of proofs from branches and combining them if necessary -/ -instance {n: Nat} : DecidableEq (Clause n) := +instance {n: Nat} : DecidableEq (Clause n) := fun c1 c2 => match decEq c1.coords c2.coords with | isTrue pf => isTrue (coords_eq_implies_vec_eq pf) @@ -33,11 +33,11 @@ instance {n: Nat} : DecidableEq (Clause n) := We map to branches inductively. The main work is done earlier. -/ def prependResData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1) - (clauses: Vector (Clause (n + 1)) dom): - (rd : ReductionData branch focus focusLt clauses) → - (head : Clause (n + 1)) → - ReductionData branch focus focusLt (head +: clauses) := - fun rd head => + (clauses: Vector (Clause (n + 1)) dom): + (rd : ReductionData branch focus focusLt clauses) → + (head : Clause (n + 1)) → + ReductionData branch focus focusLt (head +: clauses) := + fun rd head => if c : head.coords focus focusLt = some branch then PosResClause.prependResData branch focus focusLt clauses head c rd else @@ -45,52 +45,52 @@ def prependResData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1 def restrictionDataAux{domHead domAccum dom n: Nat}(branch: Bool) (focus: Nat)(focusLt : focus < n + 1): - (clausesHead: Vector (Clause (n + 1)) domHead) → - (clausesAccum: Vector (Clause (n + 1)) domAccum) → - (s : domHead + domAccum = dom) → - (restAcum : ReductionData branch focus focusLt clausesAccum) → + (clausesHead: Vector (Clause (n + 1)) domHead) → + (clausesAccum: Vector (Clause (n + 1)) domAccum) → + (s : domHead + domAccum = dom) → + (restAcum : ReductionData branch focus focusLt clausesAccum) → (clauses: Vector (Clause (n + 1)) dom) → - (clsEq : concatSeqAux s clausesHead.coords clausesAccum.coords = clauses.coords) → - ReductionData branch focus focusLt clauses := + (clsEq : concatSeqAux s clausesHead.coords clausesAccum.coords = clauses.coords) → + ReductionData branch focus focusLt clauses := match domHead with - | zero => + | zero => by intro clausesHead clausesAccum s restAccum clauses clsEq - have ss : dom = domAccum := by + have ss : dom = domAccum := by rw [← s] apply Nat.zero_add done have sf : FinSeq dom (Clause (n + 1)) = FinSeq domAccum (Clause (n + 1)):= by rw [ss] - have clSeq : clauses = clauses.coords.vec := by + have clSeq : clauses = clauses.coords.vec := by apply coords_eq_implies_vec_eq rw [seq_to_vec_coords] - have resolve : concatSeqAux s clausesHead.coords clausesAccum.coords = - Eq.mpr sf clausesAccum.coords := by rfl + have resolve : concatSeqAux s clausesHead.coords clausesAccum.coords = + Eq.mpr sf clausesAccum.coords := by rfl rw [clSeq] rw [← clsEq] - rw [resolve] + rw [resolve] match dom , domAccum, ss, sf, clausesAccum, restAccum with - | d, .(d), rfl, rfl, cls, ra => - have sm : FinSeq.vec (cls.coords) = cls := by + | d, .(d), rfl, rfl, cls, ra => + have sm : FinSeq.vec (cls.coords) = cls := by apply coords_eq_implies_vec_eq rw [seq_to_vec_coords] rw [← sm] at ra exact ra - | k + 1 => fun clausesHead clausesAccum s restAccum clauses clsEq => - let ss : k + (domAccum + 1) = dom := + | k + 1 => fun clausesHead clausesAccum s restAccum clauses clsEq => + let ss : k + (domAccum + 1) = dom := by rw [← s] rw [(Nat.add_comm domAccum 1)] rw [(Nat.add_assoc k 1 domAccum)] done - let resolve : concatSeqAux s clausesHead.coords clausesAccum.coords = + let resolve : concatSeqAux s clausesHead.coords clausesAccum.coords = concatSeqAux ss (clausesHead.coords.init) ((clausesHead.coords.last) +| clausesAccum.coords) := rfl - let recRestAccum := + let recRestAccum := prependResData branch focus focusLt clausesAccum restAccum (last clausesHead.coords) - restrictionDataAux branch focus focusLt (FinSeq.vec (init clausesHead.coords)) - ((last clausesHead.coords) +: clausesAccum) ss recRestAccum clauses - (by + restrictionDataAux branch focus focusLt (FinSeq.vec (init clausesHead.coords)) + ((last clausesHead.coords) +: clausesAccum) ss recRestAccum clauses + (by have sm : (FinSeq.vec (init clausesHead.coords)).coords = init (clausesHead.coords) := by rw [seq_to_vec_coords] rw [sm, @@ -98,20 +98,20 @@ def restrictionDataAux{domHead domAccum dom n: Nat}(branch: Bool) ← resolve, clsEq] done) - + def restrictionData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + 1): - (clauses: Vector (Clause (n + 1)) dom) → - ReductionData branch focus focusLt clauses := + (clauses: Vector (Clause (n + 1)) dom) → + ReductionData branch focus focusLt clauses := fun clauses => - let rc : ReductionClauses branch focus focusLt Vector.nil := + let rc : ReductionClauses branch focus focusLt Vector.nil := ⟨0, Vector.nil, Vector.nil, - fun k w => nomatch w, + fun k w => nomatch w, Vector.nil, fun k w => nomatch w⟩ let rd : ReductionData branch focus focusLt Vector.nil := ⟨rc, ⟨fun k w => nomatch w⟩, ⟨fun k w => nomatch w⟩, - ⟨fun k w => nomatch w⟩, + ⟨fun k w => nomatch w⟩, ⟨(by intro k kw have eq0 : rc.codom = 0 := by rfl @@ -119,7 +119,7 @@ def restrictionData{dom n: Nat}(branch: Bool)(focus: Nat)(focusLt : focus < n + have contra := not_lt_zero _ kw exact False.elim contra )⟩⟩ - restrictionDataAux branch focus focusLt clauses Vector.nil + restrictionDataAux branch focus focusLt clauses Vector.nil (Nat.add_zero dom) rd clauses (concat_empty_seq_id clauses.coords) /- @@ -128,17 +128,17 @@ The simple cases: having a contradiction or having no clauses. def contraSol{n dom: Nat}{clauses : Vector (Clause (n + 1)) dom}{j : Nat}{jw : j < dom} (eqn : clauses.coords j jw = contradiction (n + 1)): SatSolution clauses := - SatSolution.unsat (ResolutionTree.assumption j jw _ eqn) - + SatSolution.unsat (ResolutionTree.assumption j jw _ eqn) + def emptySol{n: Nat}(clauses : Vector (Clause (n + 1)) zero) : SatSolution clauses := SatSolution.sat (FinSeq.vec (fun _ _=> true)) (fun _ kw => nomatch kw) /- Solution for length one clauses -/ -def lengthOneEqual{cl1 cl2 : Clause 1}(eql : cl1.coords zero (zero_lt_succ zero) = cl2.coords zero (zero_lt_succ zero)) : +def lengthOneEqual{cl1 cl2 : Clause 1}(eql : cl1.coords zero (zero_lt_succ zero) = cl2.coords zero (zero_lt_succ zero)) : cl1 = cl2 := - coords_eq_implies_vec_eq + coords_eq_implies_vec_eq (funext (fun j => match j with | zero => funext (fun _ => eql) @@ -146,20 +146,20 @@ def lengthOneEqual{cl1 cl2 : Clause 1}(eql : cl1.coords zero (zero_lt_succ zero) )) def lengthOneUnit{cl: Clause 1}{b : Bool}(eql : cl.coords zero (zero_lt_succ zero) = some b): - cl = unitClause zero b zero (zero_lt_succ zero) := - let lem1 : - (unitClause zero b zero (zero_lt_succ zero)).coords zero (zero_lt_succ zero) = + cl = unitClause zero b zero (zero_lt_succ zero) := + let lem1 : + (unitClause zero b zero (zero_lt_succ zero)).coords zero (zero_lt_succ zero) = some b := by apply unitDiag - let lem2 : cl.coords zero (zero_lt_succ zero) = - (unitClause zero b zero (zero_lt_succ zero)).coords - zero (zero_lt_succ zero) - := + let lem2 : cl.coords zero (zero_lt_succ zero) = + (unitClause zero b zero (zero_lt_succ zero)).coords + zero (zero_lt_succ zero) + := by rw [eql] exact Eq.symm lem1 - done + done lengthOneEqual lem2 def lengthOneContra{cl: Clause 1}(eql : cl.coords zero (zero_lt_succ zero) = none): @@ -173,22 +173,22 @@ def lengthOneSolution{dom : Nat}: (clauses : Vector (Clause 1) dom) → SatSolu match searchElem cls.coords (contradiction 1) with | ExistsElem.exsts _ _ eqn => contraSol eqn | ExistsElem.notExst noContra => - let head := cls.coords (zero) (zero_lt_succ l) - if c : head.coords zero (zero_lt_succ zero) = none then - let eqn := lengthOneContra c + let head := cls.coords (zero) (zero_lt_succ l) + if c : head.coords zero (zero_lt_succ zero) = none then + let eqn := lengthOneContra c contraSol eqn - else + else if ct : head.coords zero (zero_lt_succ zero) = some true then match searchElem cls.coords (unitClause zero false zero (zero_lt_succ zero)) with - | ExistsElem.exsts _ _ eqn => - let treePf2 := unitProof eqn - let treePf1 : + | ExistsElem.exsts _ _ eqn => + let treePf2 := unitProof eqn + let treePf1 : ResolutionTree cls (unitClause zero true zero (zero_lt_succ zero)) := ResolutionTree.assumption zero (zero_lt_succ l) _ (lengthOneUnit ct) let tree := mergeAlignUnitTrees treePf1 treePf2 SatSolution.unsat tree - | ExistsElem.notExst noNeg => - SatSolution.sat (FinSeq.vec (fun _ _ => true)) + | ExistsElem.notExst noNeg => + SatSolution.sat (FinSeq.vec (fun _ _ => true)) fun k kw => let lem1 : Not ((cls.coords k kw).coords zero (zero_lt_succ zero) = some false) := fun hyp => noNeg k kw (lengthOneUnit hyp) @@ -198,20 +198,20 @@ def lengthOneSolution{dom : Nat}: (clauses : Vector (Clause 1) dom) → SatSolu match (cls.coords k kw).coords zero (zero_lt_succ zero), lem1, lem2 with | some true, _, _ => rfl | some false, l1, _ => absurd (l1 rfl) id - | none, _, l2 => absurd (l2 rfl) id - ⟨zero, zero_lt_succ _, lem⟩ - else + | none, _, l2 => absurd (l2 rfl) id + ⟨zero, zero_lt_succ _, lem⟩ + else if cf : head.coords zero (zero_lt_succ zero) = some false then match searchElem cls.coords (unitClause zero true zero (zero_lt_succ zero)) with - | ExistsElem.exsts _ _ eqn => - let treePf2 := unitProof eqn - let treePf1 : + | ExistsElem.exsts _ _ eqn => + let treePf2 := unitProof eqn + let treePf1 : ResolutionTree cls (unitClause zero false zero (zero_lt_succ zero)) := ResolutionTree.assumption zero (zero_lt_succ l) _ (lengthOneUnit cf) let tree := mergeAlignUnitTrees treePf1 treePf2 SatSolution.unsat tree - | ExistsElem.notExst noNeg => - SatSolution.sat (FinSeq.vec (fun _ _ => false)) + | ExistsElem.notExst noNeg => + SatSolution.sat (FinSeq.vec (fun _ _ => false)) fun k kw => let lem1 : Not ((cls.coords k kw).coords zero (zero_lt_succ zero) = some true) := fun hyp => noNeg k kw (lengthOneUnit hyp) @@ -220,41 +220,41 @@ def lengthOneSolution{dom : Nat}: (clauses : Vector (Clause 1) dom) → SatSolu let lem : (cls.coords k kw).coords zero (zero_lt_succ zero) = some false := match (cls.coords k kw).coords zero (zero_lt_succ zero), lem1, lem2 with | some false, _, _ => rfl - | some true, l1, _ => False.elim (l1 rfl) - | none, _, l2 => False.elim (l2 rfl) + | some true, l1, _ => False.elim (l1 rfl) + | none, _, l2 => False.elim (l2 rfl) ⟨zero, zero_lt_succ _, lem⟩ - else + else match head.coords zero (zero_lt_succ zero), c, ct, cf with | some true, _, l2, _ => False.elim (l2 rfl) | some false, _, _, l3 => False.elim (l3 rfl) | none, l1, _, _ => False.elim (l1 rfl) -- a helper -theorem notpure_cases(b: Bool): (x : Option Bool) → x = none ∨ x = some b → +theorem notpure_cases(b: Bool): (x : Option Bool) → x = none ∨ x = some b → Not (x = some (not b)) := fun x eqn => match b, eqn with - | true, Or.inr pf => + | true, Or.inr pf => fun hyp => let lem1 : some true = some false := by rw [← pf] rw [hyp] rfl done - let lem2 : true = false := by + let lem2 : true = false := by injection lem1 - + Bool.noConfusion lem2 - | false, Or.inr pf => + | false, Or.inr pf => fun hyp => let lem1 : some true = some false := by rw [← pf] rw [hyp] rfl done - let lem2 : true = false := by + let lem2 : true = false := by injection lem1 - + Bool.noConfusion lem2 | _ , Or.inl pf => fun hyp => let w := Eq.trans (Eq.symm pf) hyp @@ -265,22 +265,22 @@ Lifting under containment and from branches and putting together lifts -/ def containmentLift{dom n: Nat}(clauses : Vector (Clause (n + 1)) dom) (cntn : Containment clauses): - SatSolution (cntn.imageSeq) → SatSolution clauses := + SatSolution (cntn.imageSeq) → SatSolution clauses := fun sol => match sol with - | SatSolution.sat val pf => + | SatSolution.sat val pf => SatSolution.sat val ( - fun k kw => + fun k kw => let ⟨ind, bd, w⟩ := cntn.forward k kw let ev := pf ind bd let lem := containsSat (clauses.coords k kw) (cntn.imageSeq.coords ind bd) w val lem ev) - - | SatSolution.unsat tree => - let tree := + + | SatSolution.unsat tree => + let tree := transportResTree cntn.imageSeq clauses cntn.reverse (contradiction (n + 1)) - tree - SatSolution.unsat tree + tree + SatSolution.unsat tree def solveSAT{n dom : Nat}: (clauses : Vector (Clause (n + 1)) dom) → SatSolution clauses := @@ -291,109 +291,109 @@ def solveSAT{n dom : Nat}: (clauses : Vector (Clause (n + 1)) dom) → SatSolut let posCount := clauses.map (parityCount true) let negCount := clauses.map (parityCount false) match findElem? clauses.coords (contradiction (m + 2)) with - | some z => contraSol z.equation - | none => + | some z => contraSol z.equation + | none => let cntn := simplifiedContainment clauses posCount negCount let cls := cntn.imageSeq let posCount := cls.map (parityCount true) let negCount := cls.map (parityCount false) let solution : SatSolution cls := match someUnitClause cls.coords posCount negCount with - | some ⟨i, iw, index, bd, par, eql⟩ => + | some ⟨i, iw, index, bd, par, eql⟩ => let rd := restrictionData par index bd cls let subCls := rd.restrictionClauses.restClauses let subSol := solveSAT subCls match subSol with - | SatSolution.sat valuation pf => - let pb := pullBackSolution par index bd cls + | SatSolution.sat valuation pf => + let pb := pullBackSolution par index bd cls rd.restrictionClauses rd.droppedProof rd.forwardRelation valuation pf let valuationN := insert par _ index bd valuation.coords SatSolution.sat valuationN.vec pb | SatSolution.unsat tree => by let liftedProof := - pullBackResTree par index bd cls - rd.restrictionClauses rd.nonPosReverse rd.reverseRelation + pullBackResTree par index bd cls + rd.restrictionClauses rd.nonPosReverse rd.reverseRelation tree - - cases liftedProof - case contra pf => + + cases liftedProof + case contra pf => exact SatSolution.unsat pf case unit tree => let tree1 := unitProof eql let merged := mergeAlignUnitTrees tree1 tree - exact SatSolution.unsat merged - | none => - match hasPure cls with - | some ⟨index, bd, par, evid⟩=> + exact SatSolution.unsat merged + | none => + match hasPure cls with + | some ⟨index, bd, par, evid⟩=> let rd := restrictionData par index bd cls let subCls := rd.restrictionClauses.restClauses let subSol := solveSAT subCls match subSol with - | SatSolution.sat valuation pf => - let pb := pullBackSolution par index bd cls + | SatSolution.sat valuation pf => + let pb := pullBackSolution par index bd cls rd.restrictionClauses rd.droppedProof rd.forwardRelation valuation pf let valuationN := insert par _ index bd valuation.coords SatSolution.sat valuationN.vec pb | SatSolution.unsat tree => by let liftedProof := - pullBackResTree par index bd cls - rd.restrictionClauses rd.nonPosReverse rd.reverseRelation + pullBackResTree par index bd cls + rd.restrictionClauses rd.nonPosReverse rd.reverseRelation tree cases liftedProof - case contra pf => + case contra pf => exact SatSolution.unsat pf - case unit tree => - let base : (j : Nat) → (lt : j < cntn.codom) → - Not ((cls.coords j lt).coords index bd = some (not par)) := - fun j jw => + case unit tree => + let base : (j : Nat) → (lt : j < cntn.codom) → + Not ((cls.coords j lt).coords index bd = some (not par)) := + fun j jw => notpure_cases par ((cls.coords j jw).coords index bd) (evid j jw) let pure := trees_preserve_notsomebranch (not par) index bd base (unitClause (m + 1) (!par) index bd) tree - let impure := unitDiag (m + 1) (not par) index bd + let impure := unitDiag (m + 1) (not par) index bd exact absurd impure pure - | none => + | none => let index := zero let bd := zero_lt_succ (m + 1) - let rd : ReductionData false zero bd cls := + let rd : ReductionData false zero bd cls := restrictionData false index bd cls let subCls := rd.restrictionClauses.restClauses let subSol: SatSolution subCls := solveSAT subCls match subSol with - | SatSolution.sat valuation pf => - let pb := pullBackSolution false index bd cls + | SatSolution.sat valuation pf => + let pb := pullBackSolution false index bd cls rd.restrictionClauses rd.droppedProof rd.forwardRelation valuation pf let valuationN := insert false _ index bd valuation.coords SatSolution.sat valuationN.vec pb | SatSolution.unsat tree => by let liftedProof : LiftedResTree false zero bd cls := - pullBackResTree false index bd cls - rd.restrictionClauses rd.nonPosReverse rd.reverseRelation + pullBackResTree false index bd cls + rd.restrictionClauses rd.nonPosReverse rd.reverseRelation tree - cases liftedProof - case contra pf => + cases liftedProof + case contra pf => exact SatSolution.unsat pf - case unit tree1 => - let rd : ReductionData true zero bd cls + case unit tree1 => + let rd : ReductionData true zero bd cls := restrictionData true index bd cls let subCls := rd.restrictionClauses.restClauses let subSol := solveSAT subCls match subSol with - | SatSolution.sat valuation pf => - let pb := pullBackSolution true index bd cls + | SatSolution.sat valuation pf => + let pb := pullBackSolution true index bd cls rd.restrictionClauses rd.droppedProof rd.forwardRelation valuation pf let valuationN := insert true _ index bd valuation.coords exact SatSolution.sat valuationN.vec pb - | SatSolution.unsat tree => + | SatSolution.unsat tree => let liftedProof := - pullBackResTree true index bd cls - rd.restrictionClauses rd.nonPosReverse rd.reverseRelation + pullBackResTree true index bd cls + rd.restrictionClauses rd.nonPosReverse rd.reverseRelation tree - cases liftedProof - case contra pf => + cases liftedProof + case contra pf => exact SatSolution.unsat pf - case unit tree2 => + case unit tree2 => let merged := mergeUnitTrees index bd tree2 tree1 exact SatSolution.unsat merged containmentLift clauses cntn solution @@ -403,24 +403,24 @@ Decidability and convenience functions. -/ instance {dom n: Nat}{clauses : Vector (Clause (n + 1)) dom} : Prover (SatSolution clauses) where - statement := fun sol => solutionProp sol + statement := fun sol => solutionProp sol proof := fun sol => solutionProof sol def proveOrDisprove{n dom : Nat}(clauses : Vector (Clause (n + 1)) dom) := getProof (solveSAT clauses) instance {n dom : Nat}{clauses : Vector (Clause (n + 1)) dom} : - Decidable (isSat clauses) := + Decidable (isSat clauses) := match solveSAT clauses with | SatSolution.sat valuation evidence => isTrue ⟨valuation, evidence⟩ - | SatSolution.unsat tree => isFalse $ fun hyp => + | SatSolution.unsat tree => isFalse $ fun hyp => not_sat_and_unsat clauses hyp $ tree_unsat clauses tree instance {n dom : Nat}{clauses : Vector (Clause (n + 1)) dom} : - Decidable (isUnSat clauses) := + Decidable (isUnSat clauses) := match solveSAT clauses with - | SatSolution.sat valuation evidence => isFalse $ fun hyp => - not_sat_and_unsat clauses ⟨valuation, evidence⟩ hyp + | SatSolution.sat valuation evidence => isFalse $ fun hyp => + not_sat_and_unsat clauses ⟨valuation, evidence⟩ hyp | SatSolution.unsat tree => isTrue $ tree_unsat clauses tree