From f0dc2e04a4618fa7ac94219e6a449227959ccbed Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Tue, 14 Jun 2022 00:02:08 +0200
Subject: [PATCH] Continued work on theory DSL
---
.../lisa/kernel/proof/RunningTheory.scala | 91 ++++++++++++-------
src/main/scala/utilities/KernelHelpers.scala | 2 +
.../scala/utilities/TheoriesHelpers.scala | 2 +
3 files changed, 61 insertions(+), 34 deletions(-)
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index dd307f14..4e1625ff 100644
--- a/src/main/scala/lisa/kernel/proof/RunningTheory.scala
+++ b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
@@ -29,12 +29,12 @@ 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] (name: String, 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] (name: String, 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.
@@ -43,28 +43,33 @@ class RunningTheory {
/**
* Define a predicate symbol as a shortcut for a formula. Example : P(x,y) := ∃!z. (x=y+z)
+ *
* @param label The name and arity of the new symbol
- * @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.
*/
- final case class PredicateDefinition private[RunningTheory] (label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula) extends Definition
+ final case class PredicateDefinition private[RunningTheory](label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula) extends Definition
/**
* Define a function symbol as the unique element that has some property. The existence and uniqueness
* of that elements must have been proven before obtaining such a definition. Example
* f(x,y) := the "z" s.t. x=y+z
+ *
* @param label The name and arity of the new symbol
- * @param args The variables representing the arguments of the predicate in the formula phi.
- * @param out The variable representing the result of the function in phi
- * @param phi The formula defining the function.
+ * @param args The variables representing the arguments of the predicate in the formula phi.
+ * @param out The variable representing the result of the function in phi
+ * @param phi The formula defining the function.
*/
- final case class FunctionDefinition private[RunningTheory] (label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
+ final case class FunctionDefinition private[RunningTheory](label: ConstantFunctionLabel, args: Seq[VariableLabel], out: VariableLabel, phi: Formula) extends Definition
private[proof] val theoryAxioms: mMap[String, Axiom] = mMap.empty
private[proof] val theorems: mMap[String, Theorem] = mMap.empty
+
private[proof] val funDefinitions: mMap[ConstantFunctionLabel, Option[FunctionDefinition]] = mMap.empty
private[proof] val predDefinitions: mMap[ConstantPredicateLabel, Option[PredicateDefinition]] = mMap(equality -> None)
+ private[proof] val knownSymbols: mMap[String, ConstantLabel] = mMap(equality.id -> equality)
+
/**
* Check if a label is a symbol of the theory
*/
@@ -73,15 +78,17 @@ class RunningTheory {
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 isAvailable(label: ConstantLabel): Boolean = !knownSymbols.contains(label.id)
+
+ /**
+ * 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)
@@ -96,7 +103,7 @@ class RunningTheory {
val thm = Theorem(name, proof.conclusion)
theorems.update(name, thm)
ValidJustification(thm)
- case r @ SCProofCheckerJudgement.SCInvalidProof(_, _, 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)
@@ -113,13 +120,14 @@ class RunningTheory {
*/
def makePredicateDefinition(label: ConstantPredicateLabel, args: Seq[VariableLabel], phi: Formula): RunningTheoryJudgement[this.PredicateDefinition] = {
if (belongsToTheory(phi))
- if (!isSymbol(label))
+ if (isAvailable(label))
if (phi.freeVariables.subsetOf(args.toSet) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
val newDef = PredicateDefinition(label, args, phi)
predDefinitions.update(label, Some(newDef))
+ knownSymbols.update(label.id, label)
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("The specified symbol id 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)
}
@@ -139,15 +147,15 @@ class RunningTheory {
* @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
- ): RunningTheoryJudgement[this.FunctionDefinition] = {
+ proof: SCProof,
+ justifications: Seq[Justification],
+ label: ConstantFunctionLabel,
+ args: Seq[VariableLabel],
+ out: VariableLabel,
+ phi: Formula
+ ): RunningTheoryJudgement[this.FunctionDefinition] = {
if (belongsToTheory(phi))
- if (!isSymbol(label))
+ if (isAvailable(label))
if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j)))))
val r = SCProofChecker.checkSCProof(proof)
@@ -160,15 +168,16 @@ class RunningTheory {
if (isSame(r.head, subst) || isSame(r.head, subst2)) {
val newDef = FunctionDefinition(label, args, out, phi)
funDefinitions.update(label, Some(newDef))
+ knownSymbols.update(label.id, label)
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)
- else InvalidJustification("The specified symbol is already part of the theory and can't be redefined.", None)
+ else InvalidJustification("The specified symbol id 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)
}
@@ -272,9 +281,14 @@ class RunningTheory {
* the it is empty can be introduced as well.
*/
- def addSymbol(s: ConstantLabel): Unit = s match
- case c: ConstantFunctionLabel => funDefinitions.update(c, None)
- case c: ConstantPredicateLabel => predDefinitions.update(c, None)
+ def addSymbol(s: ConstantLabel): Unit = {
+ if (isAvailable(s)){
+ knownSymbols.update(s.id, s)
+ s match
+ case c: ConstantFunctionLabel => funDefinitions.update(c, None)
+ case c: ConstantPredicateLabel => predDefinitions.update(c, None)
+ } else {}
+ }
/**
* Public accessor to the set of symbol currently in the theory's language.
@@ -301,10 +315,19 @@ class RunningTheory {
def getAxiom(f: Formula): Option[Axiom] = theoryAxioms.find(a => isSame(a._2.ax, f)).map(_._2)
+ def getDefinition(label: ConstantPredicateLabel): Option[PredicateDefinition] = predDefinitions.get(label).flatten
+
+ def getDefinition(label: ConstantFunctionLabel): Option[FunctionDefinition] = funDefinitions.get(label).flatten
+
def getAxiom(name: String): Option[Axiom] = theoryAxioms.get(name)
def getTheorem(name: String): Option[Theorem] = theorems.get(name)
+ def getDefinition(name: String): Option[Definition] = knownSymbols.get(name).flatMap {
+ case f: ConstantPredicateLabel => getDefinition(f)
+ case f: ConstantFunctionLabel => getDefinition(f)
+ }
+
}
object RunningTheory {
diff --git a/src/main/scala/utilities/KernelHelpers.scala b/src/main/scala/utilities/KernelHelpers.scala
index f9967ba8..4af7f63a 100644
--- a/src/main/scala/utilities/KernelHelpers.scala
+++ b/src/main/scala/utilities/KernelHelpers.scala
@@ -88,6 +88,8 @@ trait KernelHelpers {
given Conversion[FunctionTerm, FunctionLabel] = _.label
+ given Conversion[SchematicFunctionLabel, Term] = _.apply()
+
// given Conversion[Tuple, List[Union[_.type]]] = _.toList
given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3)
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index 9d6c32d2..fdcb6650 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -16,6 +16,8 @@ trait TheoriesHelpers extends KernelHelpers {
else if (isSameSequent(expected, proof.conclusion)) theory.makeTheorem(name, expected, proof.appended(Rewrite(expected, proof.length - 1)), justifications)
else InvalidJustification("The proof does not prove the claimed statement", None)
}
+
+ def getJustification(name:String) : Option[theory.Justification] = theory.getAxiom(name).orElse(theory.getTheorem(name)).orElse(theory.getDefinition(name))
extension (just: RunningTheory#Justification)
def show(output: String => Unit = println): just.type = {
--
GitLab