diff --git a/src/main/scala/Example.scala b/src/main/scala/Example.scala
index 49a5bf92ffff0b5f1e26d4bb7bea2468b88e3c87..a207d70a21196821ae8c6b4cea45c4817e3f18f8 100644
--- a/src/main/scala/Example.scala
+++ b/src/main/scala/Example.scala
@@ -1,11 +1,11 @@
-import lisa.kernel.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SCProofChecker.*
import lisa.kernel.proof.SequentCalculus.*
import proven.tactics.SimplePropositionalSolver.solveSequent
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Printer.*
import utilities.tptp.KernelParser.*
import utilities.tptp.ProblemGatherer.*
import utilities.tptp.*
@@ -140,10 +140,6 @@ object Example {
println("SPC: " + p.spc.mkString(", "))
p.formulas.foreach(printAnnotatedFormula)
}
- private def checkProof(proof: SCProof): Unit = {
- val error = SCProofChecker.checkSCProof(proof)
- println(prettySCProof(proof, error))
- }
val P = SchematicPredicateLabel("P", 1)
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
deleted file mode 100644
index 044c181af93298f6b417766f488985bdd860a746..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ /dev/null
@@ -1,333 +0,0 @@
-package lisa.kernel
-
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SCProofCheckerJudgement
-import lisa.kernel.proof.SCProofCheckerJudgement.*
-import lisa.kernel.proof.SequentCalculus.*
-
-/**
- * A set of methods to pretty-print kernel trees.
- */
-object Printer {
-
- private def spaceSeparator(compact: Boolean): String = if (compact) "" else " "
- private def commaSeparator(compact: Boolean, symbol: String = ","): String = s"$symbol${spaceSeparator(compact)}"
-
- private def prettyParentheses(content: String): String = s"(${content})"
-
- private def prettyFunction(name: String, args: Seq[String], compact: Boolean, dropParentheses: Boolean = true): String = {
- if (dropParentheses && args.isEmpty) name else s"$name(${args.mkString(commaSeparator(compact))})"
- }
-
- private def prettyInfix(operator: String, left: String, right: String, compact: Boolean): String =
- Seq(left, operator, right).mkString(spaceSeparator(compact))
-
- // Special symbols that aren't defined in this theory
- private val (membership, subsetOf, sameCardinality) = (
- ConstantPredicateLabel("set_membership", 2),
- ConstantPredicateLabel("subset_of", 2),
- ConstantPredicateLabel("same_cardinality", 2)
- )
- private val (emptySet, unorderedPair, orderedPair, singleton, powerSet, unionSet) = (
- ConstantFunctionLabel("empty_set", 0),
- ConstantFunctionLabel("unordered_pair", 2),
- ConstantFunctionLabel("ordered_pair", 2),
- ConstantFunctionLabel("singleton", 1),
- ConstantFunctionLabel("power_set", 1),
- ConstantFunctionLabel("union", 1)
- )
- private val nonAtomicPredicates: Set[PredicateLabel] = Set(equality, membership, subsetOf, sameCardinality) // Predicates which require parentheses (for readability)
-
- private def prettyFormulaInternal(formula: Formula, isRightMost: Boolean, compact: Boolean): String = formula match {
- case PredicateFormula(label, args) =>
- label match {
- case `equality` =>
- args match {
- case Seq(l, r) => prettyInfix(label.id, prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case `membership` =>
- args match {
- case Seq(l, r) => prettyInfix("∈", prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case `subsetOf` =>
- args match {
- case Seq(l, r) => prettyInfix("⊆", prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case `sameCardinality` =>
- args match {
- case Seq(l, r) => prettyInfix("~", prettyTerm(l), prettyTerm(r), compact)
- case _ => throw new Exception
- }
- case _ =>
- val labelString = label match {
- case ConstantPredicateLabel(id, _) => id
- case SchematicPredicateLabel(id, _) => s"?$id"
- }
- prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
- }
- case ConnectorFormula(label, args) =>
- (label, args) match {
- case (Neg, Seq(arg)) =>
- val isAtomic = arg match {
- case PredicateFormula(label, _) => !nonAtomicPredicates.contains(label)
- case ConnectorFormula(Neg, _) => true
- case _ => false
- }
- val bodyString = prettyFormulaInternal(arg, isRightMost, compact)
- val bodyParenthesized = if (isAtomic) bodyString else prettyParentheses(bodyString)
- s"${label.id}${bodyParenthesized}"
- case (binary @ (Implies | Iff | And | Or), Seq(l, r)) =>
- val precedences: Map[ConnectorLabel, Int] = Map(
- And -> 1,
- Or -> 2,
- Implies -> 3,
- Iff -> 4
- )
- val precedence = precedences(binary)
- val isLeftParentheses = l match {
- case _: BinderFormula => true
- case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
- case ConnectorFormula(leftLabel, _) => precedences.get(leftLabel).exists(_ >= precedence)
- }
- val isRightParentheses = r match {
- case _: BinderFormula => !isRightMost
- case PredicateFormula(leftLabel, _) => nonAtomicPredicates.contains(leftLabel)
- case ConnectorFormula(rightLabel, _) => precedences.get(rightLabel).exists(_ > precedence)
- }
- val (leftString, rightString) = (prettyFormulaInternal(l, isLeftParentheses, compact), prettyFormulaInternal(r, isRightMost || isRightParentheses, compact))
- val leftParenthesized = if (isLeftParentheses) prettyParentheses(leftString) else leftString
- val rightParenthesized = if (isRightParentheses) prettyParentheses(rightString) else rightString
- prettyInfix(label.id, leftParenthesized, rightParenthesized, compact)
- case (nary @ (And | Or), args) if args.nonEmpty =>
- // Rewriting to match the above case; namely op(a) --> a, and op(a, ...rest) --> op(a, op(...rest))
- // Empty args aren't allowed here
- // Invariant: args.size > 2
- if (args.sizeIs == 1) {
- prettyFormulaInternal(args.head, isRightMost, compact)
- } else {
- prettyFormulaInternal(ConnectorFormula(nary, Seq(args.head, ConnectorFormula(nary, args.tail))), isRightMost, compact)
- }
- case _ => prettyFunction(label.id, args.map(a => prettyFormulaInternal(a, isRightMost, compact)), compact)
- }
- case BinderFormula(label, bound, inner) =>
- def accumulateNested(f: Formula, acc: Seq[VariableLabel]): (Seq[VariableLabel], Formula) = f match {
- case BinderFormula(`label`, nestBound, nestInner) => accumulateNested(nestInner, nestBound +: acc)
- case _ => (acc, f)
- }
- val (bounds, innerNested) = accumulateNested(inner, Seq(bound))
- Seq(s"${label.id}${bounds.reverse.map(_.id).mkString(commaSeparator(compact))}.", prettyFormulaInternal(innerNested, true, compact)).mkString(spaceSeparator(compact))
- }
-
- /**
- * Returns a string representation of this formula. See also [[prettyTerm]].
- * Example output:
- * <pre>
- * ∀x, y. (∀z. (z ∈ x) ↔ (z ∈ y)) ↔ (x = y)
- * </pre>
- * @param formula the formula
- * @param compact whether spaces should be omitted between tokens
- * @return the string representation of this formula
- */
- def prettyFormula(formula: Formula, compact: Boolean = false): String = prettyFormulaInternal(formula, true, compact)
-
- /**
- * Returns a string representation of this term. See also [[prettyFormula]].
- * Example output:
- * <pre>
- * f({w, (x, y)}, z)
- * </pre>
- * @param term the term
- * @param compact whether spaces should be omitted between tokens
- * @return the string representation of this term
- */
- def prettyTerm(term: Term, compact: Boolean = false): String = term match {
- case VariableTerm(label) => label.id
- case FunctionTerm(label, args) =>
- label match {
- case `emptySet` =>
- args match {
- case Seq() => prettyFunction("∅", Seq.empty, compact, dropParentheses = true)
- case _ => throw new Exception
- }
- case `unorderedPair` =>
- args match {
- case Seq(l, r) => s"{${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))}}"
- case _ => throw new Exception
- }
- case `orderedPair` =>
- args match {
- case Seq(l, r) => s"(${Seq(l, r).map(prettyTerm(_, compact)).mkString(commaSeparator(compact))})"
- case _ => throw new Exception
- }
- case `singleton` =>
- args match {
- case Seq(s) => s"{${prettyTerm(s)}}"
- case _ => throw new Exception
- }
- case `powerSet` =>
- args match {
- case Seq(s) => prettyFunction("P", Seq(prettyTerm(s)), compact)
- case _ => throw new Exception
- }
- case `unionSet` =>
- args match {
- case Seq(s) => prettyFunction("U", Seq(prettyTerm(s)), compact)
- case _ => throw new Exception
- }
- case _ =>
- val labelString = label match {
- case ConstantFunctionLabel(id, _) => id
- case SchematicFunctionLabel(id, _) => s"?$id"
- }
- prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact)
- }
- }
-
- /**
- * Returns a string representation of this sequent.
- * Example output:
- * <pre>
- * ⊢ ∀x, y. (∀z. (z ∈ x) ↔ (z ∈ y)) ↔ (x = y)
- * </pre>
- * @param sequent the sequent
- * @param compact whether spaces should be omitted between tokens
- * @return the string representation of this sequent
- */
- def prettySequent(sequent: Sequent, compact: Boolean = false): String = {
- def prettyFormulas(set: Set[Formula]): String = set.toSeq.map(prettyFormula(_, compact)).sorted.mkString(commaSeparator(compact, ";"))
- Seq(prettyFormulas(sequent.left), "⊢", prettyFormulas(sequent.right)).filter(_.nonEmpty).mkString(spaceSeparator(compact))
- }
-
- /**
- * Returns a string representation of the line number in a proof.
- * Example output:
- * <pre>
- * 0:2:1
- * </pre>
- * @param line the line number
- * @return the string representation of this line number
- */
- def prettyLineNumber(line: Seq[Int]): String = line.mkString(":")
-
- /**
- * Returns a string representation of this proof.
- * @param proof the proof
- * @param judgement optionally provide a proof checking judgement that will mark a particular step in the proof
- * (`->`) as an error. The proof is considered to be valid by default
- * @return a string where each indented line corresponds to a step in the proof
- */
- def prettySCProof(proof: SCProof, judgement: SCProofCheckerJudgement = SCValidProof, forceDisplaySubproofs: Boolean = false): String = {
- def computeMaxNumberingLengths(proof: SCProof, level: Int, result: IndexedSeq[Int]): IndexedSeq[Int] = {
- val resultWithCurrent = result.updated(
- level,
- (Seq((proof.steps.size - 1).toString.length, result(level)) ++ (if (proof.imports.nonEmpty) Seq((-proof.imports.size).toString.length) else Seq.empty)).max
- )
- proof.steps.collect { case sp: SCSubproof => sp }.foldLeft(resultWithCurrent)((acc, sp) => computeMaxNumberingLengths(sp.sp, level + 1, if (acc.size <= level + 1) acc :+ 0 else acc))
- }
- val maxNumberingLengths = computeMaxNumberingLengths(proof, 0, IndexedSeq(0)) // The maximum value for each number column
- val maxLevel = maxNumberingLengths.size - 1
-
- def leftPadSpaces(v: Any, n: Int): String = {
- val s = String.valueOf(v)
- if (s.length < n) (" " * (n - s.length)) + s else s
- }
- def rightPadSpaces(v: Any, n: Int): String = {
- val s = String.valueOf(v)
- if (s.length < n) s + (" " * (n - s.length)) else s
- }
- def prettySCProofRecursive(proof: SCProof, level: Int, tree: IndexedSeq[Int], topMostIndices: IndexedSeq[Int]): Seq[(Boolean, String, String, String)] = {
- val printedImports = proof.imports.zipWithIndex.reverse.flatMap { case (imp, i) =>
- val currentTree = tree :+ (-i - 1)
- val showErrorForLine = judgement match {
- case SCValidProof => false
- case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
- }
- val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(-i - 1)) ++ Seq.fill(maxLevel - level)(None)
- val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
- def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
- (
- showErrorForLine,
- prefixString,
- Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "),
- prettySequent(imp)
- )
-
- Seq(pretty("Import", 0))
- }
- printedImports ++ proof.steps.zipWithIndex.flatMap { case (step, i) =>
- val currentTree = tree :+ i
- val showErrorForLine = judgement match {
- case SCValidProof => false
- case SCInvalidProof(position, _) => currentTree.startsWith(position) && currentTree.drop(position.size).forall(_ == 0)
- }
- val prefix = (Seq.fill(level - topMostIndices.size)(None) ++ Seq.fill(topMostIndices.size)(None) :+ Some(i)) ++ Seq.fill(maxLevel - level)(None)
- val prefixString = prefix.map(_.map(_.toString).getOrElse("")).zipWithIndex.map { case (v, i1) => leftPadSpaces(v, maxNumberingLengths(i1)) }.mkString(" ")
- def pretty(stepName: String, topSteps: Int*): (Boolean, String, String, String) =
- (
- showErrorForLine,
- prefixString,
- Seq(stepName, topSteps.mkString(commaSeparator(compact = false))).filter(_.nonEmpty).mkString(" "),
- prettySequent(step.bot)
- )
- step match {
- case sp @ SCSubproof(_, _, display) if display || forceDisplaySubproofs =>
- pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if (i == 0) topMostIndices else IndexedSeq.empty) :+ i)
- case other =>
- val line = other match {
- case Rewrite(_, t1) => pretty("Rewrite", t1)
- case Hypothesis(_, _) => pretty("Hypo.")
- case Cut(_, t1, t2, _) => pretty("Cut", t1, t2)
- case LeftAnd(_, t1, _, _) => pretty("Left ∧", t1)
- case LeftNot(_, t1, _) => pretty("Left ¬", t1)
- case RightOr(_, t1, _, _) => pretty("Right ∨", t1)
- case RightNot(_, t1, _) => pretty("Right ¬", t1)
- case LeftExists(_, t1, _, _) => pretty("Left ∃", t1)
- case LeftForall(_, t1, _, _, _) => pretty("Left ∀", t1)
- case LeftExistsOne(_, t1, _, _) => pretty("Left ∃!", t1)
- case LeftOr(_, l, _) => pretty("Left ∨", l*)
- case RightExists(_, t1, _, _, _) => pretty("Right ∃", t1)
- case RightForall(_, t1, _, _) => pretty("Right ∀", t1)
- case RightExistsOne(_, t1, _, _) => pretty("Right ∃!", t1)
- case RightAnd(_, l, _) => pretty("Right ∧", l*)
- case RightIff(_, t1, t2, _, _) => pretty("Right ↔", t1, t2)
- case RightImplies(_, t1, _, _) => pretty("Right →", t1)
- case Weakening(_, t1) => pretty("Weakening", t1)
- case LeftImplies(_, t1, t2, _, _) => pretty("Left →", t1, t2)
- case LeftIff(_, t1, _, _) => pretty("Left ↔", t1)
- case LeftRefl(_, t1, _) => pretty("L. Refl", t1)
- case RightRefl(_, _) => pretty("R. Refl")
- case LeftSubstEq(_, t1, _, _) => pretty("L. SubstEq", t1)
- case RightSubstEq(_, t1, _, _) => pretty("R. SubstEq", t1)
- case LeftSubstIff(_, t1, _, _) => pretty("L. SubstIff", t1)
- case RightSubstIff(_, t1, _, _) => pretty("R. SubstIff", t1)
- case InstFunSchema(_, t1, _) => pretty("?Fun Instantiation", t1)
- case InstPredSchema(_, t1, _) => pretty("?Pred Instantiation", t1)
- case SCSubproof(_, _, false) => pretty("Subproof (hidden)")
- case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
- }
- Seq(line)
- }
- }
- }
-
- val marker = "->"
-
- val lines = prettySCProofRecursive(proof, 0, IndexedSeq.empty, IndexedSeq.empty)
- val maxStepNameLength = lines.map { case (_, _, stepName, _) => stepName.length }.maxOption.getOrElse(0)
- lines
- .map { case (isMarked, indices, stepName, sequent) =>
- val suffix = Seq(indices, rightPadSpaces(stepName, maxStepNameLength), sequent)
- val full = if (!judgement.isValid) (if (isMarked) marker else leftPadSpaces("", marker.length)) +: suffix else suffix
- full.mkString(" ")
- }
- .mkString("\n") + (judgement match {
- case SCValidProof => ""
- case SCInvalidProof(path, message) => s"\nProof checker has reported an error at line ${path.mkString(".")}: $message"
- })
- }
-
-}
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index 680d70b42f6d504076b1481848d6f308136d20c7..56137f419ed9924e3593bc26f538c0c07ff42c2a 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -8,6 +8,7 @@ import lisa.kernel.proof.RunningTheory
*/
sealed abstract class SCProofCheckerJudgement {
import SCProofCheckerJudgement.*
+ val proof: SCProof
/**
* Whether this judgement is positive -- the proof is concluded to be valid;
@@ -15,7 +16,7 @@ sealed abstract class SCProofCheckerJudgement {
* @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
*/
def isValid: Boolean = this match {
- case SCValidProof => true
+ case _: SCValidProof => true
case _: SCInvalidProof => false
}
}
@@ -25,14 +26,14 @@ object SCProofCheckerJudgement {
/**
* A positive judgement.
*/
- case object SCValidProof extends SCProofCheckerJudgement
+ case class SCValidProof(proof: SCProof) extends SCProofCheckerJudgement
/**
* A negative judgement.
* @param path The path of the error, expressed as indices
* @param message The error message that hints about the first error encountered
*/
- case class SCInvalidProof(path: Seq[Int], message: String) extends SCProofCheckerJudgement
+ case class SCInvalidProof(proof: SCProof, path: Seq[Int], message: String) extends SCProofCheckerJudgement
}
/**
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 70f54f3c8ef1bf39d828f65d0bc4d082229503c3..dd307f14d42d81a0dcbba30c28c4dca355ea9d90 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -62,21 +62,26 @@ class RunningTheory {
private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
- private[proof] val definitions: mMap[ConstantLabel, Option[Definition]] = mMap(equality -> None)
+ private[proof] val funDefinitions: mMap[ConstantFunctionLabel, Option[FunctionDefinition]] = mMap.empty
+ private[proof] val predDefinitions: mMap[ConstantPredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
/**
* Check if a label is a symbol of the theory
*/
- def isSymbol(label: ConstantLabel): Boolean = definitions.contains(label)
- /**
- * From a given proof, if it is true in the Running theory, add that theorem to the theory and returns it.
- * The proof's imports must be justified by the list of justification, and the conclusion of the theorem
- * can't contain symbols that do not belong to the theory.
- * @param justifications The list of justifications of the proof's imports.
- * @param proof The proof of the desired Theorem.
- * @return A Theorem if the proof is correct, None else
- */
+ def isSymbol(label: ConstantLabel): Boolean = label match
+ case c: ConstantFunctionLabel => funDefinitions.contains(c)
+ case c: ConstantPredicateLabel => predDefinitions.contains(c)
+
+ /**
+ * From a given proof, if it is true in the Running theory, add that theorem to the theory and returns it.
+ * The proof's imports must be justified by the list of justification, and the conclusion of the theorem
+ * can't contain symbols that do not belong to the theory.
+ *
+ * @param justifications The list of justifications of the proof's imports.
+ * @param proof The proof of the desired Theorem.
+ * @return A Theorem if the proof is correct, None else
+ */
def makeTheorem(name: String, statement: Sequent, proof: SCProof, justifications: Seq[Justification]): RunningTheoryJudgement[this.Theorem] = {
if (proof.conclusion == statement) proofToTheorem(name, proof, justifications)
else InvalidJustification("The proof does not prove the claimed statement", None)
@@ -87,11 +92,11 @@ class RunningTheory {
if (belongsToTheory(proof.conclusion))
val r = SCProofChecker.checkSCProof(proof)
r match {
- case SCProofCheckerJudgement.SCValidProof =>
+ case SCProofCheckerJudgement.SCValidProof(_) =>
val thm = Theorem(name, proof.conclusion)
theorems.update(name, thm)
ValidJustification(thm)
- case r @ SCProofCheckerJudgement.SCInvalidProof(path, message) =>
+ case r @ SCProofCheckerJudgement.SCInvalidProof(_, _, message) =>
InvalidJustification("The given proof is incorrect: " + message, Some(r))
}
else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None)
@@ -100,9 +105,10 @@ class RunningTheory {
/**
* Introduce a new definition of a predicate in the theory. The symbol must not already exist in the theory
* and the formula can't contain symbols that are not in the theory.
+ *
* @param label The desired label.
- * @param args The variables representing the arguments of the predicate in the formula phi.
- * @param phi The formula defining the predicate.
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param phi The formula defining the predicate.
* @return A definition object if the parameters are correct,
*/
def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
@@ -110,7 +116,7 @@ class RunningTheory {
if (!isSymbol(label))
if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
val newDef = PredicateDefinition(label, args, phi)
- definitions.update(label, Some(newDef))
+ predDefinitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
else InvalidJustification("The specified symbol is already part of the theory and can't be redefined.", None)
@@ -123,12 +129,13 @@ class RunningTheory {
* satisfying the definition's formula must first be proven. This is easy if the formula behaves as a shortcut,
* for example f(x,y) = 3x+2y
* but is much more general. The proof's conclusion must be of the form: |- ∀args. ∃!out. phi
- * @param proof The proof of existence and uniqueness
+ *
+ * @param proof The proof of existence and uniqueness
* @param justifications The justifications of the proof.
- * @param label The desired label.
- * @param args The variables representing the arguments of the predicate in the formula phi.
- * @param out The variable representing the function's result in the formula
- * @param phi The formula defining the predicate.
+ * @param label The desired label.
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param out The variable representing the function's result in the formula
+ * @param phi The formula defining the predicate.
* @return A definition object if the parameters are correct,
*/
def makeFunctionDefinition(
@@ -145,19 +152,19 @@ class RunningTheory {
if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
val r = SCProofChecker.checkSCProof(proof)
r match {
- case SCProofCheckerJudgement.SCValidProof =>
+ case SCProofCheckerJudgement.SCValidProof(_) =>
proof.conclusion match {
case Sequent(l, r) if l.isEmpty && r.size == 1 =>
val subst = bindAll(Forall, args, BinderFormula(ExistsOne, out, phi))
val subst2 = bindAll(Forall, args.reverse, BinderFormula(ExistsOne, out, phi))
if (isSame(r.head, subst) || isSame(r.head, subst2)) {
val newDef = FunctionDefinition(label, args, out, phi)
- definitions.update(label, Some(newDef))
+ funDefinitions.update(label, Some(newDef))
RunningTheoryJudgement.ValidJustification(newDef)
} else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for the formula phi.", None)
case _ => InvalidJustification("The conclusion of the proof must have an empty left hand side, and a single formula on the right hand side.", None)
}
- case r @ SCProofCheckerJudgement.SCInvalidProof(path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
+ case r @ SCProofCheckerJudgement.SCInvalidProof(_, path, message) => InvalidJustification("The given proof is incorrect: " + message, Some(r))
}
else InvalidJustification("Not all imports of the proof are correctly justified.", None)
else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None)
@@ -194,6 +201,7 @@ class RunningTheory {
/**
* Verify if a given formula belongs to some language
+ *
* @param phi The formula to check
* @return Weather phi belongs to the specified language
*/
@@ -214,6 +222,7 @@ class RunningTheory {
/**
* Verify if a given term belongs to some language
+ *
* @param t The term to check
* @return Weather t belongs to the specified language
*/
@@ -229,6 +238,7 @@ class RunningTheory {
/**
* Verify if a given sequent belongs to some language
+ *
* @param s The sequent to check
* @return Weather s belongs to the specified language
*/
@@ -244,6 +254,7 @@ class RunningTheory {
* Add a new axiom to the Theory. For example, if the theory contains the language and theorems
* of Zermelo-Fraenkel Set Theory, this function can add the axiom of choice to it.
* If the axiom belongs to the language of the theory, adds it and return true. Else, returns false.
+ *
* @param f the new axiom to be added.
* @return true if the axiom was added to the theory, false else.
*/
@@ -260,28 +271,38 @@ class RunningTheory {
* For example, This function can add the empty set symbol to a theory, and then an axiom asserting
* the it is empty can be introduced as well.
*/
- def addSymbol(s: ConstantLabel): Unit = definitions.update(s, None)
+
+ def addSymbol(s: ConstantLabel): Unit = s match
+ case c: ConstantFunctionLabel => funDefinitions.update(c, None)
+ case c: ConstantPredicateLabel => predDefinitions.update(c, None)
/**
* Public accessor to the set of symbol currently in the theory's language.
+ *
* @return the set of symbol currently in the theory's language.
*/
- def language: List[(ConstantLabel, Option[Definition])] = definitions.toList
+
+ def language: List[(ConstantLabel, Option[Definition])] = funDefinitions.toList ++ predDefinitions.toList
/**
* Public accessor to the current set of axioms of the theory
+ *
* @return the current set of axioms of the theory
*/
def axiomsList: Iterable[Axiom] = theoryAxioms.values
/**
* Verify if a given formula is an axiom of the theory
+ *
* @param f the candidate axiom
* @return wether f is an axiom of the theory
*/
def isAxiom(f: Formula): Boolean = theoryAxioms.exists(a => isSame(a._2.ax, f))
+
def getAxiom(f: Formula): Option[Axiom] = theoryAxioms.find(a => isSame(a._2.ax, f)).map(_._2)
+
def getAxiom(name: String): Option[Axiom] = theoryAxioms.get(name)
+
def getTheorem(name: String): Option[Theorem] = theorems.get(name)
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index ad72abfe303ef53d79351c0b4422f30b2f96961a..1ae79196707b059f70495a60d36ca7831c4e60ad 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -1,9 +1,9 @@
package lisa.kernel.proof
-import lisa.kernel.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProofCheckerJudgement.*
import lisa.kernel.proof.SequentCalculus.*
+import utilities.Printer
object SCProofChecker {
@@ -28,9 +28,9 @@ object SCProofChecker {
val r: SCProofCheckerJudgement =
if (false_premise.nonEmpty)
- SCInvalidProof(Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
+ SCInvalidProof(SCProof(step), Nil, s"Step no $no can't refer to higher number ${false_premise.get} as a premise.")
else if (false_premise2.nonEmpty)
- SCInvalidProof(Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
+ SCInvalidProof(SCProof(step), Nil, s"A step can't refer to step ${false_premise2.get}, imports only contains ${importsSize.get} elements.")
else
step match {
/*
@@ -39,7 +39,7 @@ object SCProofChecker {
* Γ |- Δ
*/
case Rewrite(s, t1) =>
- if (isSameSequent(s, ref(t1))) SCValidProof else SCInvalidProof(Nil, s"The premise and the conclusion are not trivially equivalent.")
+ if (isSameSequent(s, ref(t1))) SCValidProof(SCProof(step)) else SCInvalidProof(SCProof(step), Nil, s"The premise and the conclusion are not trivially equivalent.")
/*
*
* --------------
@@ -47,9 +47,9 @@ object SCProofChecker {
*/
case Hypothesis(Sequent(left, right), phi) =>
if (contains(left, phi))
- if (contains(right, phi)) SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side does not contain formula φ")
- else SCInvalidProof(Nil, s"Left-hand side does not contain formula φ")
+ if (contains(right, phi)) SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side does not contain formula φ")
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side does not contain formula φ")
/*
* Γ |- Δ, φ φ, Σ |- Π
* ------------------------
@@ -60,11 +60,11 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t2).right union ref(t1).right.filterNot(isSame(_, phi))))
if (contains(ref(t2).left, phi))
if (contains(ref(t1).right, phi))
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of first premise does not contain φ as claimed.")
- else SCInvalidProof(Nil, s"Left-hand side of second premise does not contain φ as claimed.")
- else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
- else SCInvalidProof(Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of first premise does not contain φ as claimed.")
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of second premise does not contain φ as claimed.")
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
// Left rules
/*
@@ -80,9 +80,9 @@ object SCProofChecker {
isSameSet(b.left + psi, ref(t1).left + phiAndPsi) ||
isSameSet(b.left + phi + psi, ref(t1).left + phiAndPsi)
)
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
- else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion must be the same.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ∧ψ must be same as left-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- Δ Σ, ψ |- Π
* ------------------------
@@ -92,9 +92,9 @@ object SCProofChecker {
if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)))
val phiOrPsi = ConnectorFormula(Or, disjuncts)
if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
- SCValidProof
- else SCInvalidProof(Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
- else SCInvalidProof(Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + disjuncts is not the same as the union of the left-hand sides of the premises + φ∨ψ.")
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion is not the union of the right-hand sides of the premises.")
/*
* Γ |- φ, Δ Σ, ψ |- Π
* ------------------------
@@ -104,9 +104,9 @@ object SCProofChecker {
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(b.right + phi, ref(t1).right union ref(t2).right))
if (isSameSet(b.left + psi, ref(t1).left union ref(t2).left + phiImpPsi))
- SCValidProof
- else SCInvalidProof(Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
- else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion + ψ must be identical to union of left-hand sides of premisces + φ→ψ.")
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ must be identical to union of right-hand sides of premisces.")
/*
* Γ, φ→ψ |- Δ Γ, φ→ψ, ψ→φ |- Δ
* -------------- or ---------------
@@ -122,9 +122,9 @@ object SCProofChecker {
isSameSet(b.left + psiImpPhi, ref(t1).left + phiIffPsi) ||
isSameSet(b.left + phiImpPsi + psiImpPhi, ref(t1).left + phiIffPsi)
)
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
- else SCInvalidProof(Nil, "Right-hand sides of premise and conclusion must be the same.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of premise and conclusion must be the same.")
/*
* Γ |- φ, Δ
@@ -135,9 +135,9 @@ object SCProofChecker {
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.left, ref(t1).left + nPhi))
if (isSameSet(b.right + phi, ref(t1).right))
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
- else SCInvalidProof(Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion must be the same as left-hand side of premise + ¬φ")
/*
* Γ, φ[t/x] |- Δ
@@ -147,9 +147,9 @@ object SCProofChecker {
case LeftForall(b, t1, phi, x, t) =>
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + substituteVariables(phi, Map(x -> t)), ref(t1).left + BinderFormula(Forall, x, phi)))
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
- else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
/*
* Γ, φ |- Δ
@@ -160,10 +160,10 @@ object SCProofChecker {
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left + BinderFormula(Exists, x, phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
- SCValidProof
- else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
- else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
- else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "The variable x must not be free in the resulting sequent.")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise + ∃x. φ")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
/*
* Γ, ∃y.∀x. (x=y) ↔ φ |- Δ
@@ -175,9 +175,9 @@ object SCProofChecker {
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + temp, ref(t1).left + BinderFormula(ExistsOne, x, phi)))
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
- else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as left-hand side of premise + ∃!x. φ")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
// Right rules
/*
@@ -189,9 +189,9 @@ object SCProofChecker {
val phiAndPsi = ConnectorFormula(And, cunjuncts)
if (isSameSet(b.left, t.map(ref(_).left).reduce(_ union _)))
if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).reduce(_ union _) + phiAndPsi))
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
- else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
* Γ |- φ, Δ Γ |- φ, ψ, Δ
* -------------- or ---------------
@@ -205,9 +205,9 @@ object SCProofChecker {
isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi)
)
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
- else SCInvalidProof(Nil, "Left-hand sides of the premise and the conclusion must be the same.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- ψ, Δ
* --------------
@@ -217,9 +217,9 @@ object SCProofChecker {
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(ref(t1).left, b.left + phi))
if (isSameSet(b.right + psi, ref(t1).right + phiImpPsi))
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
- else SCInvalidProof(Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + ψ must be same as right-hand side of premise + φ→ψ.")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + psi must be same as left-hand side of premise.")
/*
* Γ |- a→ψ, Δ Σ |- ψ→φ, Π
* ----------------------------
@@ -231,9 +231,9 @@ object SCProofChecker {
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
if (isSameSet(b.left, ref(t1).left union ref(t2).left))
if (isSameSet(b.right + phiImpPsi + psiImpPhi, ref(t1).right union ref(t2).right + phiIffPsi))
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
- else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand side of conclusion + a→ψ + ψ→φ is not the same as the union of the right-hand sides of the premises φ↔b.")
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
* Γ, φ |- Δ
* --------------
@@ -243,9 +243,9 @@ object SCProofChecker {
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.right, ref(t1).right + nPhi))
if (isSameSet(b.left + phi, ref(t1).left))
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
- else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of conclusion + φ must be the same as left-hand side of premise")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion must be the same as right-hand side of premise + ¬φ")
/*
* Γ |- φ, Δ
* ------------------- if x is not free in the resulting sequent
@@ -255,10 +255,10 @@ object SCProofChecker {
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x, phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
- SCValidProof
- else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
- else SCInvalidProof(Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
- else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "The variable x must not be free in the resulting sequent.")
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + φ must be the same as right-hand side of premise + ∀x. φ")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of conclusion and premise must be the same.")
/*
* Γ |- φ[t/x], Δ
* -------------------
@@ -267,9 +267,9 @@ object SCProofChecker {
case RightExists(b, t1, phi, x, t) =>
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + substituteVariables(phi, Map(x -> t)), ref(t1).right + BinderFormula(Exists, x, phi)))
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
- else SCInvalidProof(Nil, "Left-hand sides or conclusion and premise must be the same.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand sides or conclusion and premise must be the same.")
/**
* <pre>
@@ -283,9 +283,9 @@ object SCProofChecker {
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + temp, ref(t1).right + BinderFormula(ExistsOne, x, phi)))
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
- else SCInvalidProof(Nil, "Left-hand sides of conclusion and premise must be the same")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of conclusion + ∃y.∀x. (x=y) ↔ φ must be the same as right-hand side of premise + ∃!x. φ")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of conclusion and premise must be the same")
// Structural rules
/*
@@ -296,9 +296,9 @@ object SCProofChecker {
case Weakening(b, t1) =>
if (isSubset(ref(t1).left, b.left))
if (isSubset(ref(t1).right, b.right))
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
- else SCInvalidProof(Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise must be a subset of right-hand side of conclusion")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise must be a subset of left-hand side of conclusion")
// Equality Rules
/*
@@ -312,11 +312,11 @@ object SCProofChecker {
if (isSame(left, right))
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left))
- SCValidProof
- else SCInvalidProof(Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
- else SCInvalidProof(Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
- else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
- case _ => SCInvalidProof(Nil, "φ is not an equality")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Left-hand sides of the conclusion + φ must be the same as left-hand side of the premise.")
+ else SCInvalidProof(SCProof(step), Nil, s"Right-hand sides of the premise and the conclusion aren't the same.")
+ else SCInvalidProof(SCProof(step), Nil, s"φ is not an instance of reflexivity.")
+ case _ => SCInvalidProof(SCProof(step), Nil, "φ is not an equality")
}
/*
@@ -329,10 +329,10 @@ object SCProofChecker {
case PredicateFormula(`equality`, Seq(left, right)) =>
if (isSame(left, right))
if (contains(b.right, phi))
- SCValidProof
- else SCInvalidProof(Nil, s"Right-Hand side of conclusion does not contain φ")
- else SCInvalidProof(Nil, s"φ is not an instance of reflexivity.")
- case _ => SCInvalidProof(Nil, s"φ is not an equality.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, s"Right-Hand side of conclusion does not contain φ")
+ else SCInvalidProof(SCProof(step), Nil, s"φ is not an instance of reflexivity.")
+ case _ => SCInvalidProof(SCProof(step), Nil, s"φ is not an equality.")
}
/*
@@ -351,9 +351,14 @@ object SCProofChecker {
isSameSet(b.left + phi_t_for_f, ref(t1).left ++ sEqT_es + phi_s_for_f) ||
isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f)
)
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
- else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped)."
+ )
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
/*
* Γ |- φ(s_), Δ
@@ -370,9 +375,14 @@ object SCProofChecker {
isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f)
)
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case.")
- else SCInvalidProof(Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case."
+ )
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
/*
* Γ, φ(ψ_) |- Δ
* ---------------------
@@ -388,9 +398,14 @@ object SCProofChecker {
isSameSet(ref(t1).left ++ psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
isSameSet(ref(t1).left ++ psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q)
)
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ↔τ)_ + φ(τ_) (or with ψ and τ swapped).")
- else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ↔τ)_ + φ(τ_) (or with ψ and τ swapped)."
+ )
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
/*
* Γ |- φ[ψ/?p], Δ
@@ -407,9 +422,14 @@ object SCProofChecker {
isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q)
)
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case.")
- else SCInvalidProof(Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case."
+ )
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
/**
* <pre>
@@ -422,9 +442,9 @@ object SCProofChecker {
val expected = (ref(t1).left.map(phi => instantiateFunctionSchemas(phi, insts)), ref(t1).right.map(phi => instantiateFunctionSchemas(phi, insts)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
- SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
- else SCInvalidProof(Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
+ SCValidProof(SCProof(step))
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
/**
* <pre>
@@ -437,18 +457,23 @@ object SCProofChecker {
val expected = (ref(t1).left.map(phi => instantiatePredicateSchemas(phi, insts)), ref(t1).right.map(phi => instantiatePredicateSchemas(phi, insts)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
- SCValidProof
+ SCValidProof(SCProof(step))
else
- SCInvalidProof(Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
- else SCInvalidProof(Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
+ SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
case SCSubproof(sp, premises, _) =>
if (premises.size == sp.imports.size) {
val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)))
if (invalid.isEmpty) {
checkSCProof(sp)
- } else SCInvalidProof(Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
- } else SCInvalidProof(Nil, "Number of premises and imports don't match: " + premises.size + " " + sp.imports.size)
+ } else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof."
+ )
+ } else SCInvalidProof(SCProof(step), Nil, "Number of premises and imports don't match: " + premises.size + " " + sp.imports.size)
}
r
@@ -459,19 +484,19 @@ object SCProofChecker {
* If the proof is not correct, the functrion will report the faulty line and a brief explanation.
*
* @param proof A SC proof to check
- * @return SCValidProof if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
+ * @return SCValidProof(SCProof(step)) if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
* and an explanation.
*/
def checkSCProof(proof: SCProof): SCProofCheckerJudgement = {
val possibleError = proof.steps.view.zipWithIndex
.map((step, no) =>
checkSingleSCStep(no, step, (i: Int) => proof.getSequent(i), Some(proof.imports.size)) match {
- case SCInvalidProof(path, message) => SCInvalidProof(no +: path, message)
- case SCValidProof => SCValidProof
+ case SCInvalidProof(_, path, message) => SCInvalidProof(proof, no +: path, message)
+ case SCValidProof(_) => SCValidProof(proof)
}
)
.find(j => !j.isValid)
- if (possibleError.isEmpty) SCValidProof
+ if (possibleError.isEmpty) SCValidProof(proof)
else possibleError.get
}
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index cb030de9e9c2c4b51b05155aa472ebd5571ad3dc..0bb0cbc8a3a781d573ecc08194284e2be414ba5e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -2,7 +2,7 @@ package lisa.settheory
import lisa.kernel.fol.FOL._
import lisa.kernel.proof.RunningTheory
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
/**
* Base trait for set theoretical axiom systems.
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index 6bd499c09a36a31806a92614699e05dea8ee4db0..81b81922de16ce5817a0add565bcf61d31477fe3 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -1,6 +1,7 @@
package lisa.settheory
+
import lisa.kernel.fol.FOL._
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
/**
* Axioms for the Tarski-Grothendieck theory (TG)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 5a47aad939e8c2afd84ad1f154820f7b308990b1..11fde4e4eb4e2dd94f99511f88123fd1a7394ed2 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -2,7 +2,7 @@ package lisa.settheory
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
/**
* Axioms for the Zermelo theory (Z)
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 13221cc12f60f84b53fae1d358bb3d602919001a..e89ea065be30ad3354e1b7bbfa1049f754e52d3e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -1,7 +1,7 @@
package lisa.settheory
import lisa.kernel.fol.FOL._
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
/**
* Axioms for the Zermelo-Fraenkel theory (ZF)
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index 3d674ce858f4fd76b1d2005003dffcb54e1052a1..331916cc558db0ac818f310f44a056b95a79cf1f 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -1,8 +1,5 @@
package proven.DSetTheory
-import lisa.kernel.Printer
-import lisa.kernel.Printer.prettyFormula
-import lisa.kernel.Printer.prettySCProof
-import lisa.kernel.Printer.prettySequent
+
import lisa.kernel.fol.FOL
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
@@ -14,8 +11,11 @@ import proven.ElementsOfSetTheory.oPair
import proven.ElementsOfSetTheory.orderedPairDefinition
import proven.tactics.Destructors.*
import proven.tactics.ProofTactics.*
-import utilities.KernelHelpers.{_, given}
-import utilities.TheoriesHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Printer
+import utilities.Printer.prettyFormula
+import utilities.Printer.prettySCProof
+import utilities.Printer.prettySequent
import scala.collection.immutable
import scala.collection.immutable.SortedSet
@@ -397,8 +397,6 @@ object Part1 {
/*
val lemma2 = SCProof({
-
-
// goal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!Z. ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
// redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃Z1. ∀Z. Z=Z1 <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
// redGoal ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀Z. Z=UX <=> ∃X. Z=UX /\ ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
@@ -572,13 +570,10 @@ object Part1 {
}
/*
val thm_lemmaCartesianProduct = theory.proofToTheorem("lemmaCartesianProduct", lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
-
val vA = VariableLabel("A")
val vB = VariableLabel("B")
val cart_product = ConstantFunctionLabel("cart_cross", 2)
val def_oPair = theory.makeFunctionDefinition(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments), cart_product, Seq(vA, vB), VariableLabel("z"), innerOfDefinition(lemmaCartesianProduct.conclusion.right.head)).get
-
-
*/
def innerOfDefinition(f: Formula): Formula = f match {
@@ -600,10 +595,7 @@ object Part1 {
}
def main(args: Array[String]): Unit = {
- def checkProof(proof: SCProof): Unit = {
- val error = SCProofChecker.checkSCProof(proof)
- println(prettySCProof(proof, error))
- }
+
println("\nthmMapFunctional")
checkProof(thmMapFunctional)
println("\nlemma1")
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index c1fd97c4000bee26b07bb7cd885d3a5a41d2396f..e5c83222a4a9f693bd518f27ea6646a8f2e74f2f 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -1,20 +1,17 @@
package proven
-import lisa.kernel.Printer
-import lisa.kernel.Printer.*
+
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import lisa.settheory.AxiomaticSetTheory
import lisa.settheory.AxiomaticSetTheory.*
-import lisa.settheory.AxiomaticSetTheory.*
import proven.ElementsOfSetTheory.theory
import proven.tactics.Destructors.*
-import proven.tactics.Destructors.*
import proven.tactics.ProofTactics.*
-import proven.tactics.ProofTactics.*
-import utilities.KernelHelpers.{_, given}
-import utilities.TheoriesHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Printer
+import utilities.Printer.*
import scala.collection.immutable
import scala.collection.immutable.SortedSet
@@ -72,7 +69,7 @@ object ElementsOfSetTheory {
val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
fin4.copy(imports = imps)
} // |- ∀∀({x$1,y$2}={y$2,x$1})
- println(prettySequent(proofUnorderedPairSymmetry.conclusion))
+
val thm_proofUnorderedPairSymmetry: theory.Theorem =
theory.theorem("proofUnorderedPairSymmetry", "⊢ ∀y, x. {x, y} = {y, x}", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
@@ -324,7 +321,7 @@ object ElementsOfSetTheory {
val p2 = RightImplies(emptySeq +> (p1.bot.left.head ==> p1.bot.right.head), 1, p1.bot.left.head, p1.bot.right.head) // |- ({x,y}={x',y'}) ==> (x=x' /\ y=y')\/(x=y' /\ y=x')
generalizeToForall(SCProof(IndexedSeq(p0, p1, p2), IndexedSeq(() |- pairAxiom)), x, y, x1, y1)
} // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
- println(prettySequent(proofUnorderedPairDeconstruction.conclusion))
+
val thm_proofUnorderedPairDeconstruction = theory
.theorem(
"proofUnorderedPairDeconstruction",
@@ -342,7 +339,6 @@ object ElementsOfSetTheory {
/*
val proofOrderedPairDeconstruction: SCProof = {
-
val opairxy = pair(pair(x, y), pair(x, x))
val opairxx = pair(pair(x, x), pair(x, x))
val opairxy1 = pair(pair(x1, y1), pair(x1, x1))
@@ -351,11 +347,8 @@ object ElementsOfSetTheory {
val pairxx = pair(x, x)
val pairxy1 = pair(x1, y1)
val pairxx1 = pair(x1, x1)
-
-
val p0 = SCSubproof(orderedPairDefinition, display = false)
val p1 = SCSubproof(proofUnorderedPairDeconstruction) // |- ∀∀∀∀(({x$4,y$3}={x'$2,y'$1})⇒(((y'$1=y$3)∧(x'$2=x$4))∨((x$4=y'$1)∧(y$3=x'$2))))
-
val p2: SCSubproof = SCSubproof(SCProof(byCase(x === y)(
{
val p2_0 = SCSubproof(SCProof({
@@ -388,7 +381,6 @@ object ElementsOfSetTheory {
}, IndexedSeq(-2)) // {x',y'}={x,x}, x=y |- x=x' /\ x=y'
val p2_2 = Cut(emptySeq ++< p2_0.bot ++> p2_1.bot, 0, 1, p2_0.bot.right.head) // ((x,y)=(x',y')), x=y |- x=x' /\ x=y'
val p2_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (x === y) +> ((x === x1) /\ (y === y1)), 2, x, y, (x === x1) /\ (z === y1), z)
-
SCSubproof(SCProof(IndexedSeq(p2_0, p2_1, p2_2, p2_3), IndexedSeq(p0, p1)), IndexedSeq(-1, -2))
} // ((x,y)=(x',y')), x=y |- x=x' /\ y=y'
,
@@ -398,10 +390,8 @@ object ElementsOfSetTheory {
val p2_0_1 = UseFunctionDefinition(emptySeq +> (oPair(x1, y1) === opairxy1), oPair, Seq(x1, y1)) // |- (x1, y1) === {{x1,y1}, {x1,x1}}
val p2_0_2 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (oPair(x1, y1) === pair(pair(x, y), pair(x, x))),
0, oPair(x, y), oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) // (x1,y1)=(x,y) |- ((x1,y1)={{x,y},{x,x}})
-
val p2_0_3 = RightSubstEq(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +< (opairxy1 === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
2, opairxy1, oPair(x1, y1), z === pair(pair(x, y), pair(x, x)), z) // (x1,y1)=(x,y), (x1,y1)={{x1,y1}, {x1,x1}} |- {{x1,y1}, {x1,x1}}={{x,y},{x,x}})
-
val p2_0_4 = Cut(emptySeq +< (oPair(x, y) === oPair(x1, y1)) +> (pair(pair(x, y), pair(x, x)) === pair(pair(x1, y1), pair(x1, x1))),
1, 3, opairxy1 === oPair(x1, y1))
SCProof(IndexedSeq(p2_0_0, p2_0_1, p2_0_2, p2_0_3, p2_0_4), IndexedSeq(p0))
@@ -414,7 +404,6 @@ object ElementsOfSetTheory {
case BinaryConnectorFormula(`or`, l, r) => (l, r)
}
val pr2_1: SCProof = destructRightOr(pr2_0, f, g) // ((x,y)=(x',y')) |- (({x',x'}={x,y})∧({x',y'}={x,x})), (({x,x}={x',x'})∧({x,y}={x',y'}))
-
val pb2_0 = SCSubproof({
val prb2_0_0 = instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, x1) // |- (({x,y}={x',x'}) ⇒ (((x'=y)∧(x'=x))∨((x=x')∧(y=x'))))
val f = (x1 === y) /\ (x1 === x)
@@ -427,10 +416,8 @@ object ElementsOfSetTheory {
SCProof(IndexedSeq(pb3_0_0, pb3_0_1, pb3_0_2, pb3_0_3, pb3_0_4), IndexedSeq(p1))
}, IndexedSeq(-2)) // {x',x'}={x,y} |- x=y
val pb2_1 = SCSubproof(destructRightAnd(pr2_1, pairxx1 === pairxy, pairxx === pairxy1), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- (({x',x'}={x,y}), (({x,x}={x',x'})∧({x,y}={x',y'}))
-
val pb2_2 = Cut(pb2_1.bot -> pb2_0.bot.left.head +> (x === y), 1, 0, pb2_0.bot.left.head) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
val pc2_0 = SCSubproof(SCProof(IndexedSeq(pb2_0, pb2_1, pb2_2), IndexedSeq(p0, p1)), IndexedSeq(-1, -2)) // ((x,y)=(x',y')) |- x=y, (({x,x}={x',x'})∧({x,y}={x',y'}))
-
val pc2_1 = SCSubproof({
val pc2_1_0 = SCSubproof(destructRightAnd(SCProof(IndexedSeq(), IndexedSeq(pc2_0)), pairxy === pairxy1, pairxx === pairxx1), IndexedSeq(-2)) // ((x,y)=(x',y')) |- x=y, {x,y}={x',y'}
val pc2_1_1 = SCSubproof(instantiateForall(SCProof(IndexedSeq(), IndexedSeq(p1)), x, y, x1, y1), IndexedSeq(-1)) // (({x,y}={x',y'})⇒(((y'=y)∧(x'=x))∨((x=y')∧(y=x'))))
@@ -450,7 +437,6 @@ object ElementsOfSetTheory {
val prc2_2_4 = destructRightAnd(prc2_2_3, x === x1, x === x1) // ((x,y)=(x',y')) |- x=y, x'=x
SCProof(prc2_2_4.steps, IndexedSeq(p1, pc2_0))
}, IndexedSeq(-2, 0)) // ((x,y)=(x',y')) |- x=y, x'=x
-
val pc2_3 = RightSubstEq(pc2_1.bot -> (x1 === y) +> (x === y) +< (x1 === x), 1, x, x1, z === y, z) // ((x,y)=(x',y')), x=x' |- x=y, ((y=y')∧(x=x')))
val pc2_4 = Cut(pc2_3.bot -< (x === x1), 2, 3, x === x1) // ((x,y)=(x',y')) |- x=y, ((y=y')∧(x=x')))
val pc2_5 = LeftNot(pc2_4.bot +< !(x === y) -> (x === y), 4, x === y) // ((x,y)=(x',y')), !x=y |- ((y=y')∧(x=x')))
@@ -458,16 +444,12 @@ object ElementsOfSetTheory {
} // ((x,y)=(x',y')), !x=y |- x=x' /\ y=y'
).steps, IndexedSeq(p0, p1)), IndexedSeq(0, 1)) // ((x,y)=(x',y')) |- x=x' /\ y=y'
SCProof(p0, p1, p2)
-
???
} // |- (x,y)=(x', y') ===> x=x' /\ y=y'
*/
def main(args: Array[String]): Unit = {
- def checkProof(proof: SCProof): Unit = {
- val error = SCProofChecker.checkSCProof(proof)
- println(prettySCProof(proof, error))
- }
+
println("\nproofUnorderedPairSymmetry")
checkProof(proofUnorderedPairSymmetry)
println("\nproofUnorderedPairDeconstruction")
diff --git a/src/main/scala/proven/tactics/Destructors.scala b/src/main/scala/proven/tactics/Destructors.scala
index 86fdd967d7c9383e43e1cb964f79f90e6b8cbdb2..39f2c6cd06d1dec8647e96ae3a19c5726ae52963 100644
--- a/src/main/scala/proven/tactics/Destructors.scala
+++ b/src/main/scala/proven/tactics/Destructors.scala
@@ -5,7 +5,7 @@ import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.SequentCalculus.*
import proven.tactics.ProofTactics.hypothesis
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
object Destructors {
def destructRightOr(p: SCProof, a: Formula, b: Formula): SCProof = {
diff --git a/src/main/scala/proven/tactics/ProofTactics.scala b/src/main/scala/proven/tactics/ProofTactics.scala
index 50b4d61a962826d74b41eec90a03b8e13be4e080..5ac98af434b313e80c47228e53f150a98b4c187d 100644
--- a/src/main/scala/proven/tactics/ProofTactics.scala
+++ b/src/main/scala/proven/tactics/ProofTactics.scala
@@ -1,10 +1,10 @@
package proven.tactics
-import lisa.kernel.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Printer.*
import scala.collection.immutable.Set
diff --git a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
index a48c558fed8dbe7f1c7de0ba64bdad2d2fc8f3ea..69e75d73ac08756a9c2c05181bdcd0a4d780fdb4 100644
--- a/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
+++ b/src/main/scala/proven/tactics/SimplePropositionalSolver.scala
@@ -3,7 +3,7 @@ package proven.tactics
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
import scala.collection.mutable.Set as mSet
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index 2e7ac7364a3e23b52d8f79683a01cf8f5cbb7bdd..f9967ba8727b4a433214976450b49f62c15ccb8b 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -14,7 +14,7 @@ import lisa.kernel.proof.SequentCalculus.isSameSequent
* import lisa.KernelHelpers.*
* </pre>
*/
-object KernelHelpers {
+trait KernelHelpers {
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SequentCalculus.Sequent
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index e0f9864e76803c937d3dd528cc121170203bc497..9d6c32d2dec5f6db0ca7f1e0ce103a0f80c3b2f0 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -1,13 +1,12 @@
package utilities
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
-import lisa.kernel.proof.SCProof
-import lisa.kernel.proof.SequentCalculus.Rewrite
-import lisa.kernel.proof.SequentCalculus.isSameSequent
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.kernel.proof.*
+import utilities.Printer
-object TheoriesHelpers {
+trait TheoriesHelpers extends KernelHelpers {
// for when the kernel will have a dedicated parser
extension (theory: RunningTheory)
@@ -18,4 +17,39 @@ object TheoriesHelpers {
else InvalidJustification("The proof does not prove the claimed statement", None)
}
+ extension (just: RunningTheory#Justification)
+ def show(output: String => Unit = println): just.type = {
+ just match
+ case thm: RunningTheory#Theorem => output(s"Theorem ${thm.name} := ${Printer.prettySequent(thm.proposition)}")
+ case axiom: RunningTheory#Axiom => output(s"Axiom ${axiom.name} := ${Printer.prettyFormula(axiom.ax)}")
+ case d: RunningTheory#Definition =>
+ d match
+ case pd: RunningTheory#PredicateDefinition =>
+ output(s"Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.args.map(VariableTerm(_))*) <=> pd.phi)}") // (label, args, phi)
+ case fd: RunningTheory#FunctionDefinition =>
+ output(s"Definition of function symbol ${fd.label.id} := ${Printer.prettyFormula((fd.label(fd.args.map(VariableTerm(_))*) === fd.out) <=> fd.phi)})")
+ // output(Printer.prettySequent(thm.proposition))
+ // thm
+ just
+ }
+
+ extension [J <: RunningTheory#Justification](theoryJudgement: RunningTheoryJudgement[J]) {
+
+ def showAndGet(output: String => Unit = println): J = {
+ theoryJudgement match
+ case RunningTheoryJudgement.ValidJustification(just) =>
+ just.show(output)
+ case InvalidJustification(message, error) =>
+ output(s"$message\n${error match
+ case Some(judgement) => Printer.prettySCProof(judgement)
+ case None => ""
+ }")
+ theoryJudgement.get
+ }
+ }
+
+ def checkProof(proof: SCProof, output: String => Unit = println): Unit = {
+ val judgement = SCProofChecker.checkSCProof(proof)
+ output(Printer.prettySCProof(judgement))
+ }
}
diff --git a/src/main/scala/utilities/tptp/KernelParser.scala b/src/main/scala/utilities/tptp/KernelParser.scala
index 3f7d2fe05c1c40c482291212c7bb75cf2c6d9f35..215e85d79f370b762bea599561a3a5354b5f9378 100644
--- a/src/main/scala/utilities/tptp/KernelParser.scala
+++ b/src/main/scala/utilities/tptp/KernelParser.scala
@@ -6,7 +6,7 @@ import leo.datastructures.TPTP.FOF
import leo.modules.input.TPTPParser as Parser
import lisa.kernel.fol.FOL as K
import lisa.kernel.proof.SequentCalculus as LK
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
import utilities.tptp.*
import java.io.File
diff --git a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
index 2576c9c9a4863c35b97ee62760b0ff958ea14bf2..c499619ec8712709280d0e31206fcc5ca0dbb748 100644
--- a/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
+++ b/src/test/scala/lisa/kernel/EquivalenceCheckerTests.scala
@@ -1,10 +1,10 @@
package lisa.kernel
-import lisa.kernel.Printer
+import utilities.Printer
import lisa.kernel.fol.FOL
import lisa.kernel.fol.FOL.*
import org.scalatest.funsuite.AnyFunSuite
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
import scala.collection.MapView
import scala.collection.mutable.ArrayBuffer
diff --git a/src/test/scala/lisa/kernel/FolTests.scala b/src/test/scala/lisa/kernel/FolTests.scala
index 7ebe445cc788ee09fb913207d4f049260dede3ba..42e6caed9f3a9dd861be9db59162238fee6484d7 100644
--- a/src/test/scala/lisa/kernel/FolTests.scala
+++ b/src/test/scala/lisa/kernel/FolTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import lisa.kernel.Printer
+import utilities.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +8,7 @@ import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import org.scalatest.funsuite.AnyFunSuite
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
import scala.collection.immutable.SortedSet
import scala.util.Random
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 840dbd5d3082f434a50fb957b5231781afc2de46..3d7aa18bf839e0e322f083663d889198d303b746 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -5,7 +5,7 @@ import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.*
import test.ProofCheckerSuite
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
import scala.collection.immutable.SortedSet
import scala.language.implicitConversions
diff --git a/src/test/scala/lisa/kernel/PrinterTest.scala b/src/test/scala/lisa/kernel/PrinterTest.scala
index cf6a4899b65440498135e5996e7a7547791543eb..67e91f29c1ca1820f2804de870b44f3359ca0dce 100644
--- a/src/test/scala/lisa/kernel/PrinterTest.scala
+++ b/src/test/scala/lisa/kernel/PrinterTest.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import lisa.kernel.Printer._
+import utilities.Printer._
import lisa.kernel.fol.FOL._
import org.scalatest.funsuite.AnyFunSuite
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index fc559c9a75105307136b7fd0b6d6620da60589f1..d5704b084af2fccf9bf8fd0f39e8a7d009cab378 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -1,6 +1,6 @@
package lisa.kernel
-import lisa.kernel.Printer
+import utilities.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
@@ -8,7 +8,7 @@ import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
import lisa.kernel.proof.SequentCalculus.*
import org.scalatest.funsuite.AnyFunSuite
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
import scala.util.Random
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index b9e09182ecdb26f35689f42134711a4ef1ae6798..36a3fb11e37022c4827d795d20d53fefddc173a2 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -1,6 +1,6 @@
-package proven
+package lisa.proven
-import lisa.kernel.Printer
+import utilities.Printer
import lisa.kernel.fol.FOL.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
@@ -10,8 +10,8 @@ import lisa.settheory.AxiomaticSetTheory.*
import proven.ElementsOfSetTheory.*
import proven.tactics.ProofTactics
import test.ProofCheckerSuite
-import utilities.KernelHelpers.{_, given}
-import utilities.KernelHelpers.{_, given}
+import utilities.Helpers.{_, given}
+import utilities.Helpers.{_, given}
class ElementsOfSetTheoryTests extends ProofCheckerSuite {
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index e0b99c734ee9091a7e5daad84562aabfe017f3a3..8598562aa8dd742ca7fee37d2314905d9f47c1ba 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -1,14 +1,14 @@
-package proven
+package lisa.proven
-import lisa.kernel.Printer
-import lisa.kernel.Printer.*
+import utilities.Printer
+import utilities.Printer.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.PredicateLogic
import lisa.kernel.proof.SCProofChecker
import org.scalatest.funsuite.AnyFunSuite
import proven.tactics.SimplePropositionalSolver as SPS
-import utilities.KernelHelpers.*
+import utilities.Helpers.*
import utilities.tptp.KernelParser.*
import utilities.tptp.ProblemGatherer.getPRPproblems
diff --git a/src/test/scala/test/ProofCheckerSuite.scala b/src/test/scala/test/ProofCheckerSuite.scala
index 8a6011d729cf0cdd1a0409d4028a9555a82327fe..caaee39fda0749d07d6b38c21e122b36cdd2c422 100644
--- a/src/test/scala/test/ProofCheckerSuite.scala
+++ b/src/test/scala/test/ProofCheckerSuite.scala
@@ -1,14 +1,14 @@
package test
-import lisa.kernel.Printer
+import utilities.Printer
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker._
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.proof.SequentCalculus.isSameSequent
import lisa.settheory.AxiomaticSetTheory
import org.scalatest.funsuite.AnyFunSuite
-import utilities.KernelHelpers._
-import utilities.KernelHelpers.given_Conversion_Boolean_List_String_Option
+import utilities.Helpers._
+import utilities.Helpers.given_Conversion_Boolean_List_String_Option
abstract class ProofCheckerSuite extends AnyFunSuite {
import lisa.kernel.fol.FOL.*
@@ -39,14 +39,14 @@ abstract class ProofCheckerSuite extends AnyFunSuite {
val axioms = AxiomaticSetTheory.axioms
def checkProof(proof: SCProof): Unit = {
- val error = checkSCProof(proof)
- println(Printer.prettySCProof(proof, error))
+ val judgement = checkSCProof(proof)
+ println(Printer.prettySCProof(judgement))
println(s"\n(${proof.totalLength} proof steps in total)")
}
def checkProof(proof: SCProof, expected: Sequent): Unit = {
val judgement = checkSCProof(proof)
- assert(judgement.isValid, "\n" + Printer.prettySCProof(proof, judgement))
+ assert(judgement.isValid, "\n" + Printer.prettySCProof( judgement))
assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
}