diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index d9561a39722ccfb5b7bdea4ca185f19066b98484..053be248ab164361b41091eea38be6c92da538ef 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -11,9 +11,12 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* A formula is a tree whose nodes are either terms or labeled by predicates or logical connectors.
*/
sealed abstract class Formula extends TreeWithLabel[FormulaLabel] {
- def predicates: Set[ConstantPredicateLabel]
- def functions: Set[ConstantFunctionLabel]
- //def predicatesSchemas: Set[PredicateLabel] = predicates filter { case _: ConstantPredicateLabel => false; case _: SchematicPredicateLabel => true }
+
+ def constantFunctions: Set[ConstantFunctionLabel]
+ def schematicFunctions: Set[SchematicFunctionLabel]
+
+ def constantPredicates: Set[ConstantPredicateLabel]
+ def schematicPredicates: Set[SchematicPredicateLabel]
}
/**
@@ -22,12 +25,17 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
final case class PredicateFormula(label: PredicateLabel, args: Seq[Term]) extends Formula {
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
- override def predicates: Set[ConstantPredicateLabel] = label match {
+ override def constantPredicates: Set[ConstantPredicateLabel] = label match {
case l: ConstantPredicateLabel => Set(l)
case l: SchematicPredicateLabel => Set()
}
+ override def schematicPredicates: Set[SchematicPredicateLabel] = label match {
+ case l: ConstantPredicateLabel => Set()
+ case l: SchematicPredicateLabel => Set(l)
+ }
- override def functions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions)
+ override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
+ override def schematicFunctions: Set[SchematicFunctionLabel] = args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions)
}
@@ -37,9 +45,12 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
final case class ConnectorFormula(label: ConnectorLabel, args: Seq[Formula]) extends Formula {
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
- override def predicates: Set[ConstantPredicateLabel] = args.foldLeft(Set.empty[ConstantPredicateLabel])((prev, next) => prev union next.predicates)
- override def functions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions)
+ override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
+ override def schematicFunctions: Set[SchematicFunctionLabel] = args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions)
+
+ override def constantPredicates: Set[ConstantPredicateLabel] = args.foldLeft(Set.empty[ConstantPredicateLabel])((prev, next) => prev union next.constantPredicates)
+ override def schematicPredicates: Set[SchematicPredicateLabel] = args.foldLeft(Set.empty[SchematicPredicateLabel])((prev, next) => prev union next.schematicPredicates)
}
/**
@@ -48,9 +59,11 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
final case class BinderFormula(label: BinderLabel, bound: VariableLabel, inner: Formula) extends Formula {
override def freeVariables: Set[VariableLabel] = inner.freeVariables - bound
- override def predicates: Set[ConstantPredicateLabel] = inner.predicates
+ override def constantFunctions: Set[ConstantFunctionLabel] = inner.constantFunctions
+ override def schematicFunctions: Set[SchematicFunctionLabel] = inner.schematicFunctions
- override def functions: Set[ConstantFunctionLabel] = inner.functions
+ override def constantPredicates: Set[ConstantPredicateLabel] = inner.constantPredicates
+ override def schematicPredicates: Set[SchematicPredicateLabel] = inner.schematicPredicates
}
/**
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 25c23e0e72aab95c21e93f1c7d0f1121d958388b..33a9d54e8457a89b49a195e29f052953a0b8ddf3 100644
--- a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -10,7 +10,8 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
def freeVariables: Set[VariableLabel]
- def functions: Set[ConstantFunctionLabel]
+ def constantFunctions: Set[ConstantFunctionLabel]
+ def schematicFunctions: Set[SchematicFunctionLabel]
}
@@ -30,7 +31,8 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
final case class VariableTerm(label: VariableLabel) extends Term {
override def freeVariables: Set[VariableLabel] = Set(label)
- override def functions: Set[ConstantFunctionLabel] = Set.empty
+ override def constantFunctions: Set[ConstantFunctionLabel] = Set.empty
+ override def schematicFunctions: Set[SchematicFunctionLabel] = Set.empty
}
/**
@@ -44,9 +46,13 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables)
- override def functions: Set[ConstantFunctionLabel] = label match {
- case l:ConstantFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions) + l
- case l:SchematicFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.functions)
+ override def constantFunctions: Set[ConstantFunctionLabel] = label match {
+ case l:ConstantFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions) + l
+ case l:SchematicFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions)
+ }
+ override def schematicFunctions: Set[SchematicFunctionLabel] = label match {
+ case l:ConstantFunctionLabel => args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions)
+ case l:SchematicFunctionLabel => args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions) + l
}
val arity: Int = args.size
diff --git a/src/main/scala/lisa/kernel/proof/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
new file mode 100644
index 0000000000000000000000000000000000000000..20f6740f21583ab0cc9e52ca229b8ce9713360c9
--- /dev/null
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -0,0 +1,71 @@
+package lisa.kernel.proof
+
+import lisa.kernel.proof.RunningTheory
+
+/**
+ * The judgement (or verdict) of a proof checking procedure.
+ * Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
+ */
+sealed abstract class SCProofCheckerJudgement {
+ import SCProofCheckerJudgement.*
+
+ /**
+ * Whether this judgement is positive -- the proof is concluded to be valid;
+ * or negative -- the proof checker couldn't certify the validity of this proof.
+ * @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
+ */
+ def isValid: Boolean = this match {
+ case SCValidProof => true
+ case _: SCInvalidProof => false
+ }
+}
+
+object SCProofCheckerJudgement {
+ /**
+ * A positive judgement.
+ */
+ case object SCValidProof 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
+}
+
+
+/**
+ * The judgement (or verdict) of a running theory.
+ */
+sealed abstract class RunningTheoryJudgement[J<:RunningTheory#Justification] {
+ import RunningTheoryJudgement.*
+
+ /**
+ * Whether this judgement is positive -- the justification could be imported into the running theory;
+ * or negative -- the justification is not suitable to be imported in the theory.
+ * @return An instance of either [[ValidJustification]] or [[InvalidJustification]]
+ */
+ def isValid: Boolean = this match {
+ case _: ValidJustification[?] => true
+ case _: InvalidJustification[?] => false
+ }
+ def get:J = this match {
+ case ValidJustification(just) => just
+ case InvalidJustification(message, error) => None.get
+ }
+}
+
+object RunningTheoryJudgement {
+ /**
+ * A positive judgement.
+ */
+ case class ValidJustification[J<:RunningTheory#Justification](just:J) extends RunningTheoryJudgement[J]
+
+ /**
+ * A negative judgement.
+ * @param error If the justification is rejected because the proof is wrong, will contain the error in the proof.
+ * @param message The error message that hints about the first error encountered
+ */
+ case class InvalidJustification[J<:RunningTheory#Justification](message: String, error: Option[SCProofCheckerJudgement.SCInvalidProof]) extends RunningTheoryJudgement[J]
+}
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 9c87f3aff0c755478a3d53c729e65942fb15eea0..a67c56156fce6623033c917b3d545e0a35176c7e 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -7,6 +7,7 @@ import lisa.kernel.fol.FOL.*
import scala.collection.mutable.Map as mMap
import scala.collection.mutable.Set as mSet
import scala.collection.immutable.Set
+import lisa.kernel.proof.RunningTheoryJudgement.*
/**
* This class describes the theory, i.e. the context and language, in which theorems are proven.
@@ -26,11 +27,11 @@ class RunningTheory {
/**
* A theorem encapsulate a sequent and assert that this sequent has been correctly proven and may be used safely in further proofs.
*/
- final case class Theorem private[RunningTheory](proposition: Sequent) extends Justification
+ final case class Theorem private[RunningTheory](name:String, proposition: Sequent) extends Justification
/**
* An axiom is any formula that is assumed and considered true within the theory. It can freely be used later in any proof.
*/
- final case class Axiom private[RunningTheory](ax: Formula) extends Justification
+ final case class Axiom private[RunningTheory](name:String, ax: Formula) extends Justification
/**
* A definition can be either a PredicateDefinition or a FunctionDefinition.
@@ -57,7 +58,8 @@ class RunningTheory {
final case class FunctionDefinition private[RunningTheory](label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
- private[proof] val theoryAxioms : mSet[Axiom] = mSet.empty
+ private[proof] val theoryAxioms : mMap[String, Axiom] = mMap.empty
+ private[proof] val theorems : mMap[String, Theorem] = mMap.empty
private[proof] val funDefinitions: mMap[FunctionLabel, Option[FunctionDefinition]] = mMap.empty
private[proof] val predDefinitions: mMap[PredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
@@ -71,17 +73,27 @@ class RunningTheory {
def isAcceptedPredicateLabel(label:PredicateLabel): Boolean = predDefinitions.contains(label)
/**
- * From a given proof, if it is true in the Running theory, returns a theorem that is valid in the given theory.
+ * 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 p The proof of the desired Theorem.
* @return A Theorem if the proof is correct, None else
*/
- def proofToTheorem(p: SCProof, justifications:Seq[Justification]): Option[this.Theorem] =
- if (checkProofWithinTheory(p, justifications) && belongsToTheory(p.conclusion))
- Some(Theorem(p.conclusion))
- else None
+ def proofToTheorem(name:String, proof: SCProof, justifications:Seq[Justification]): RunningTheoryJudgement[this.Theorem] =
+ if (proof.imports.forall(i => justifications.exists( j => isSameSequent(i, sequentFromJustification(j)))))
+ if (belongsToTheory(proof.conclusion))
+ val r = SCProofChecker.checkSCProof(proof)
+ r match {
+ case SCProofCheckerJudgement.SCValidProof =>
+ val thm = Theorem(name, proof.conclusion)
+ theorems.update(name, thm)
+ RunningTheoryJudgement.ValidJustification(thm)
+ case r @ SCProofCheckerJudgement.SCInvalidProof(path, 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)
+ else InvalidJustification("Not all imports of the proof are correctly justified.", None)
/**
@@ -92,14 +104,16 @@ class RunningTheory {
* @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): Option[this.PredicateDefinition] = {
- if (belongsToTheory(phi) && !isAcceptedPredicateLabel(label)) {
- val newDef = PredicateDefinition(label, args, phi)
- predDefinitions.update(label, Some(newDef))
- Some(newDef)
- } else {
- None
- }
+ def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
+ if (belongsToTheory(phi))
+ if (!isAcceptedPredicateLabel(label))
+ if (phi.freeVariables.isEmpty && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+ val newDef = PredicateDefinition(label, args, phi)
+ 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)
+ 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)
}
/**
@@ -116,49 +130,38 @@ class RunningTheory {
* @param phi The formula defining the predicate.
* @return A definition object if the parameters are correct,
*/
- def makeFunctionDefinition(proof: SCProof, justifications:Seq[Justification], label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula): Option[this.FunctionDefinition] = {
- if (belongsToTheory(phi) && !isAcceptedFunctionLabel(label) && checkProofWithinTheory(proof, justifications)) {
-
- 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)
- funDefinitions.update(label, Some(newDef))
- Some(newDef)
- }
- else None
-
- case _ => None
- }
- } else {
- None
- }
+ def makeFunctionDefinition(proof: SCProof, justifications:Seq[Justification], label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula): RunningTheoryJudgement[this.FunctionDefinition] = {
+ if (belongsToTheory(phi))
+ if (!isAcceptedFunctionLabel(label))
+ if (phi.freeVariables.isEmpty && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
+ if (proof.imports.forall(i => justifications.exists( j => isSameSequent(i, sequentFromJustification(j)))))
+ val r = SCProofChecker.checkSCProof(proof)
+ r match {
+ 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)
+ funDefinitions.update(label, Some(newDef))
+ RunningTheoryJudgement.ValidJustification(newDef)
+ }
+ else InvalidJustification("The proof is correct but its conclusion does not correspond to a definition for 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))
+ }
+ 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)
+ else InvalidJustification("The specified symbol is already part of the theory and can't be redefined.", None)
+ 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)
}
-
- /**
- * Verify is a proof is correct withing a given Theory. It separately verifies if the proof is correct from
- * a pure sequent calculus point of view, and if definitions and theorem imported into the proof are indeed
- * part of the theory.
- *
- */
- def checkProofWithinTheory(proof: SCProof, justifications: Seq[Justification]): Boolean = {
-
- if (belongsToTheory(proof.conclusion)){
- if (proof.imports.forall(i => justifications.exists( j => isSameSequent(i, sequentFromJustification(j))) ))
- true
- else
- false
- }
- else false
- }
-
private def sequentFromJustification(j:Justification): Sequent = j match {
- case Theorem(proposition) => proposition
- case Axiom(ax) => Sequent(Set.empty, Set(ax))
+ case Theorem(name, proposition) => proposition
+ case Axiom(name, ax) => Sequent(Set.empty, Set(ax))
case PredicateDefinition(label, args, phi) =>
val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, args.map(VariableTerm.apply)), phi))
Sequent(Set(), Set(bindAll(Forall, args, inner)))
@@ -194,8 +197,8 @@ class RunningTheory {
}
def makeFormulaBelongToTheory(phi:Formula) : Unit = {
- phi.predicates.foreach(addSymbol)
- phi.functions.foreach(addSymbol)
+ phi.constantPredicates.foreach(addSymbol)
+ phi.constantFunctions.foreach(addSymbol)
}
/**
* Verify if a given term belongs to some language
@@ -232,9 +235,9 @@ class RunningTheory {
* @param f the new axiom to be added.
* @return true if the axiom was added to the theory, false else.
*/
- def addAxiom(f:Formula):Boolean = {
+ def addAxiom(name:String, f:Formula):Boolean = {
if (belongsToTheory(f)){
- theoryAxioms.add(Axiom(f))
+ theoryAxioms.update(name, Axiom(name, f))
true
}
else false
@@ -258,14 +261,17 @@ class RunningTheory {
* Public accessor to the current set of axioms of the theory
* @return the current set of axioms of the theory
*/
- def getAxioms: List[Axiom] = theoryAxioms.toList
+ 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.ax,f))
+ 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)
}
object RunningTheory {
diff --git a/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala b/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
deleted file mode 100644
index bf81d106f20b8587e6cd263bdefa6e6256f5e6b0..0000000000000000000000000000000000000000
--- a/src/main/scala/lisa/kernel/proof/SCProofCheckerJudgement.scala
+++ /dev/null
@@ -1,33 +0,0 @@
-package lisa.kernel.proof
-
-/**
- * The judgement (or verdict) of a proof checking procedure.
- * Typically, see [[SCProofChecker.checkSingleSCStep]] and [[SCProofChecker.checkSCProof]].
- */
-sealed abstract class SCProofCheckerJudgement {
- import SCProofCheckerJudgement.*
-
- /**
- * Whether this judgement is positive -- the proof is concluded to be valid;
- * or negative -- the proof checker couldn't certify the validity of this proof.
- * @return An instance of either [[SCValidProof]] or [[SCInvalidProof]]
- */
- def isValid: Boolean = this match {
- case SCValidProof => true
- case _: SCInvalidProof => false
- }
-}
-
-object SCProofCheckerJudgement {
- /**
- * A positive judgement.
- */
- case object SCValidProof 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
-}
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 6b6d1de060e2cb0c40a0521f3077dea7ec4561f0..5df53d836163af787707961fad9bbf40042e4032 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -9,7 +9,7 @@ import lisa.KernelHelpers.{given, _}
*/
private[settheory] trait SetTheoryDefinitions{
type Axiom = Formula
- def axioms: Set[Axiom] = Set.empty
+ def axioms: Set[(String, Axiom)] = Set.empty
private[settheory] final val (x, y, z, a, b) =
(VariableLabel("x"), VariableLabel("y"), VariableLabel("z"), VariableLabel("A"), VariableLabel("B"))
final val sPhi = SchematicPredicateLabel("P", 2)
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index c1a92a892a5097b1dac2357d11123da93acff40d..cc8cf2e5f028532fffcdf9b8aaca7540317a627c 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -12,8 +12,8 @@ private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
)
)
- runningSetTheory.addAxiom(tarskiAxiom)
+ runningSetTheory.addAxiom("TarskiAxiom", tarskiAxiom)
- override def axioms: Set[Axiom] = super.axioms + tarskiAxiom
+ override def axioms: Set[(String, Axiom)] = super.axioms + (("TarskiAxiom", tarskiAxiom))
}
\ No newline at end of file
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 46071edaa86050f87444b5b555215699209f666e..5ccf623b9844b7ecdd18e5f85c11c909f58e4f05 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -18,12 +18,20 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
final val comprehensionSchema: Axiom = forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
- private val zAxioms: Set[Axiom] = Set(emptySetAxiom, extensionalityAxiom, pairAxiom, unionAxiom, powerAxiom, foundationAxiom, comprehensionSchema)
+ private val zAxioms: Set[(String, Axiom)] = Set(
+ ("EmptySet", emptySetAxiom),
+ ("extensionalityAxiom", extensionalityAxiom),
+ ("pairAxiom", pairAxiom),
+ ("unionAxiom", unionAxiom),
+ ("powerAxiom", powerAxiom),
+ ("foundationAxiom", foundationAxiom),
+ ("comprehensionSchema", comprehensionSchema)
+ )
- zAxioms.foreach(a => runningSetTheory.addAxiom(a))
+ zAxioms.foreach(a => runningSetTheory.addAxiom(a._1, a._2))
- override def axioms: Set[Axiom] = super.axioms ++ zAxioms
+ override def axioms: Set[(String, Axiom)] = super.axioms ++ zAxioms
}
\ No newline at end of file
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index 6ea73c22866260ea2152894f499ab443430498a9..d211beb2ce67cb0d060bdcb2b9dfe7e35258550e 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -11,9 +11,9 @@ private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
forall(x, (in(x, a)) ==> existsOne(y, sPsi(a,x,y))) ==>
exists(b, forall(x, in(x, a) ==> exists(y, in(y, b) /\ sPsi(a,x,y))))
)
- runningSetTheory.addAxiom(replacementSchema)
+ runningSetTheory.addAxiom("replacementSchema", replacementSchema)
- override def axioms: Set[Axiom] = super.axioms + replacementSchema
+ override def axioms: Set[(String, Axiom)] = super.axioms + (("replacementSchema", replacementSchema))
}
\ No newline at end of file
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index dbdd6a43583fcfe8a511190aaf2fbd9162133d6c..c3dd6d3c2265a3e8c0486605f4bb321aa1dc0ae5 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -16,7 +16,7 @@ import lisa.settheory.AxiomaticSetTheory
import scala.collection.immutable
object Part1 {
val theory = AxiomaticSetTheory.runningSetTheory
- def axiom(f:Formula) = theory.getAxioms.find(c => c.ax == f).get
+ def axiom(f:Formula):theory.Axiom = theory.getAxiom(f).get
private val x = SchematicFunctionLabel("x", 0)()
@@ -42,7 +42,7 @@ object Part1 {
//val s4 = Rewrite(() |- !exists(y1, forall(x1, in(x1,y1) <=> !in(x1, x1))), 3)
SCProof(s0, s1, s2)
}
- val thm_russelParadox = theory.proofToTheorem(russelParadox, Nil).get
+ val thm_russelParadox = theory.proofToTheorem("russelParadox", russelParadox, Nil).get
val thm4:SCProof = {
//forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
@@ -62,7 +62,7 @@ object Part1 {
val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) )
SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), Vector(i1, i2))
}
- val thm_thm4 = theory.proofToTheorem(thm4, Seq(axiom(comprehensionSchema), thm_russelParadox)).get
+ val thm_thm4 = theory.proofToTheorem("thm4", thm4, Seq(axiom(comprehensionSchema), thm_russelParadox)).get
val thmMapFunctional: SCProof = {
val a = VariableLabel("a")
@@ -209,7 +209,7 @@ object Part1 {
val steps = Vector(s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15,s16,s17,s18,s19,s20,s21,s22)
SCProof(steps, Vector(i1, i2, i3))
}
- val thm_thmMapFunctional = theory.proofToTheorem(thmMapFunctional, Seq(axiom(replacementSchema), axiom(comprehensionSchema),axiom(extensionalityAxiom))).get
+ val thm_thmMapFunctional = theory.proofToTheorem("thmMapFunctional", thmMapFunctional, Seq(axiom(replacementSchema), axiom(comprehensionSchema),axiom(extensionalityAxiom))).get
/**
* ∀ b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b)
@@ -251,7 +251,7 @@ object Part1 {
// by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s6
// have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s7
}
- val thm_lemma1 = theory.proofToTheorem(lemma1, Seq(thm_thmMapFunctional)).get
+ val thm_lemma1 = theory.proofToTheorem("lemma1", lemma1, Seq(thm_thmMapFunctional)).get
/*
val lemma2 = SCProof({
@@ -326,7 +326,7 @@ object Part1 {
// redGoal2 x=x1 <=> phi(x), z=F(x), x=x1 ⊢ F(x1)=z g2.s1
// redGoal2 x=x1 <=> phi(x), z=F(x1), x=x1 ⊢ F(x1)=z TRUE g2.s0
}
- val thm_lemmaApplyFToObject = theory.proofToTheorem(lemmaApplyFToObject, Nil).get
+ val thm_lemmaApplyFToObject = theory.proofToTheorem("lemmaApplyFToObject", lemmaApplyFToObject, Nil).get
/**
* ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)
@@ -353,7 +353,7 @@ object Part1 {
val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
SCProof(Vector(s0,s1,s2), Vector(i1, i2))
}
- val thm_lemmaMapTwoArguments = theory.proofToTheorem(lemmaMapTwoArguments, Seq(thm_lemma1, thm_lemmaApplyFToObject)).get
+ val thm_lemmaMapTwoArguments = theory.proofToTheorem("lemmaMapTwoArguments", lemmaMapTwoArguments, Seq(thm_lemma1, thm_lemmaApplyFToObject)).get
/**
* ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ (x1 = (a, b))
@@ -394,7 +394,7 @@ object Part1 {
}
println("cartesian")
- val thm_lemmaCartesianProduct = theory.proofToTheorem(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
+ val thm_lemmaCartesianProduct = theory.proofToTheorem("lemmaCartesianProduct", lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
val vA = VariableLabel("A")
val vB = VariableLabel("B")
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index a103dbe012cb0c87d5bf4dfe44dc9027716c8009..36e7e30809d24659faef2a77df30f500ba398360 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -19,7 +19,7 @@ import scala.collection.immutable
object ElementsOfSetTheory {
val theory = AxiomaticSetTheory.runningSetTheory
- def axiom(f:Formula) = theory.getAxioms.find(c => c.ax == f).get
+ def axiom(f:Formula): theory.Axiom = theory.getAxiom(f).get
private val x = VariableLabel("x")
private val y = VariableLabel("y")
@@ -65,7 +65,7 @@ object ElementsOfSetTheory {
val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
fin4.copy(imports = imps)
} // |- ∀∀({x$1,y$2}={y$2,x$1})
- val thm_proofUnorderedPairSymmetry = theory.proofToTheorem(proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
+ val thm_proofUnorderedPairSymmetry = theory.proofToTheorem("proofUnorderedPairSymmetry", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
val proofUnorderedPairDeconstruction: SCProof = {
@@ -223,13 +223,12 @@ 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))))
- val thm_proofUnorderedPairDeconstruction = theory.proofToTheorem(proofUnorderedPairDeconstruction, Seq(axiom(pairAxiom))).get
+ val thm_proofUnorderedPairDeconstruction = theory.proofToTheorem("proofUnorderedPairDeconstruction", proofUnorderedPairDeconstruction, Seq(axiom(pairAxiom))).get
// i2, i1, p0, p1, p2, p3
val orderedPairDefinition: SCProof = simpleFunctionDefinition(pair(pair(x, y), pair(x, x)), Seq(x, y))
- println("def_oPair")
val def_oPair = theory.makeFunctionDefinition(orderedPairDefinition, Nil, oPair, Seq(x, y), x1, x1 === pair(pair(x, y), pair(x, x)))
/*
diff --git a/src/test/scala/lisa/proven/SimpleProverTests.scala b/src/test/scala/lisa/proven/SimpleProverTests.scala
index 5eb2269e58a8b82afeb609df11377f521cd7bf3e..3538752262928c4d671eb135a12f51ef2ec1242c 100644
--- a/src/test/scala/lisa/proven/SimpleProverTests.scala
+++ b/src/test/scala/lisa/proven/SimpleProverTests.scala
@@ -14,9 +14,9 @@ import proven.tactics.SimplePropositionalSolver as SPS
class SimpleProverTests extends AnyFunSuite {
+ /*
test("Simple propositional logic proofs") {
val problems = getPRPproblems.take(1)
-
problems.foreach( pr => {
println("--- Problem "+pr.file)
val sq = problemToSequent(pr)
@@ -29,4 +29,5 @@ class SimpleProverTests extends AnyFunSuite {
})
}
+ */
}