From 023f1364590fef9215f8f80d1f3ebb025c52b445 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Wed, 15 Jun 2022 01:17:05 +0200
Subject: [PATCH] Tests and experimentation of theory files structure, more
work on dsl.
---
build.sbt | 2 +-
src/main/scala/dev/A.scala | 5 +
src/main/scala/dev/WithMain.scala | 8 ++
.../lisa/kernel/proof/RunningTheory.scala | 28 ++--
.../lisa/settheory/SetTheoryDefinitions.scala | 14 +-
.../lisa/settheory/SetTheoryTGAxioms.scala | 8 +-
.../lisa/settheory/SetTheoryZAxioms.scala | 24 ++--
.../lisa/settheory/SetTheoryZFAxioms.scala | 9 +-
src/main/scala/proven/DSetTheory/Part1.scala | 8 +-
src/main/scala/proven/MainLibrary.scala | 12 ++
src/main/scala/proven/SetTheory.scala | 31 +++++
src/main/scala/utilities/Library.scala | 124 ++++++++++++++++++
.../scala/utilities/TheoriesHelpers.scala | 4 +-
13 files changed, 235 insertions(+), 42 deletions(-)
create mode 100644 src/main/scala/dev/A.scala
create mode 100644 src/main/scala/dev/WithMain.scala
create mode 100644 src/main/scala/proven/MainLibrary.scala
create mode 100644 src/main/scala/proven/SetTheory.scala
create mode 100644 src/main/scala/utilities/Library.scala
diff --git a/build.sbt b/build.sbt
index 70c4dbe4..1699b485 100644
--- a/build.sbt
+++ b/build.sbt
@@ -4,7 +4,7 @@ licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0
version := "0.1"
-scalaVersion := "3.0.2"
+scalaVersion := "3.1.3"
scalacOptions ++= Seq("-deprecation", "-feature")
scalacOptions ++= Seq(
diff --git a/src/main/scala/dev/A.scala b/src/main/scala/dev/A.scala
new file mode 100644
index 00000000..e9ddcd24
--- /dev/null
+++ b/src/main/scala/dev/A.scala
@@ -0,0 +1,5 @@
+package dev
+
+trait A extends WithMain {}
+
+object A extends A
diff --git a/src/main/scala/dev/WithMain.scala b/src/main/scala/dev/WithMain.scala
new file mode 100644
index 00000000..72454a97
--- /dev/null
+++ b/src/main/scala/dev/WithMain.scala
@@ -0,0 +1,8 @@
+package dev
+
+abstract class WithMain {
+ def main(args: Array[String]): Unit = {
+ println("Bonjour")
+ }
+
+}
diff --git a/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/src/main/scala/lisa/kernel/proof/RunningTheory.scala
index 4e1625ff..95280f5e 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.
@@ -48,7 +48,7 @@ class RunningTheory {
* @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
@@ -60,7 +60,7 @@ class RunningTheory {
* @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
@@ -103,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)
@@ -147,13 +147,13 @@ 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 (isAvailable(label))
if (phi.freeVariables.subsetOf(args.toSet + out) && phi.schematicFunctions.isEmpty && phi.schematicPredicates.isEmpty)
@@ -173,7 +173,7 @@ class RunningTheory {
} 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)
@@ -282,7 +282,7 @@ class RunningTheory {
*/
def addSymbol(s: ConstantLabel): Unit = {
- if (isAvailable(s)){
+ if (isAvailable(s)) {
knownSymbols.update(s.id, s)
s match
case c: ConstantFunctionLabel => funDefinitions.update(c, None)
diff --git a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
index 0bb0cbc8..d4f35c04 100644
--- a/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryDefinitions.scala
@@ -8,13 +8,11 @@ import utilities.Helpers.{_, given}
* Base trait for set theoretical axiom systems.
* Defines the symbols used in set theory.
*/
-private[settheory] trait SetTheoryDefinitions {
- type Axiom = Formula
- 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)
- final val sPsi = SchematicPredicateLabel("P", 3)
+trait SetTheoryDefinitions {
+
+ private val tete = "tete"
+ def axioms: Set[(String, Formula)] = Set.empty
+
// Predicates
final val in = ConstantPredicateLabel("set_membership", 2)
final val subset = ConstantPredicateLabel("subset_of", 2)
@@ -33,7 +31,7 @@ private[settheory] trait SetTheoryDefinitions {
final val functions = Set(emptySet, pair, singleton, powerSet, union, universe)
val runningSetTheory: RunningTheory = new RunningTheory()
- given RunningTheory = runningSetTheory
+ // given RunningTheory = runningSetTheory
predicates.foreach(s => runningSetTheory.addSymbol(s))
functions.foreach(s => runningSetTheory.addSymbol(s))
diff --git a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
index 81b81922..53e837d1 100644
--- a/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryTGAxioms.scala
@@ -6,9 +6,11 @@ import utilities.Helpers.{_, given}
/**
* Axioms for the Tarski-Grothendieck theory (TG)
*/
-private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
+trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
+ private val (x, y, z) =
+ (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
- final val tarskiAxiom: Axiom = forall(
+ final val tarskiAxiom: Formula = forall(
x,
in(x, universe(x)) /\
forall(
@@ -20,6 +22,6 @@ private[settheory] trait SetTheoryTGAxioms extends SetTheoryZFAxioms {
runningSetTheory.addAxiom("TarskiAxiom", tarskiAxiom)
- override def axioms: Set[(String, Axiom)] = super.axioms + (("TarskiAxiom", tarskiAxiom))
+ override def axioms: Set[(String, Formula)] = super.axioms + (("TarskiAxiom", tarskiAxiom))
}
diff --git a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
index 11fde4e4..3e59d388 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala
@@ -7,18 +7,22 @@ import utilities.Helpers.{_, given}
/**
* Axioms for the Zermelo theory (Z)
*/
-private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
+trait SetTheoryZAxioms extends SetTheoryDefinitions {
- final val emptySetAxiom: Axiom = forall(x, !in(x, emptySet()))
- final val extensionalityAxiom: Axiom = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
- final val pairAxiom: Axiom = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
- final val unionAxiom: Axiom = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
- final val powerAxiom: Axiom = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
- final val foundationAxiom: Axiom = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
+ private val (x, y, z) =
+ (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+ private final val sPhi = SchematicPredicateLabel("P", 2)
- final val comprehensionSchema: Axiom = forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ sPhi(x, z)))))
+ final val emptySetAxiom: Formula = forall(x, !in(x, emptySet()))
+ final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y)))
+ final val pairAxiom: Formula = forall(x, forall(y, forall(z, in(z, pair(x, y)) <=> (x === z) \/ (y === z))))
+ final val unionAxiom: Formula = forall(x, forall(z, in(x, union(z)) <=> exists(y, in(x, y) /\ in(y, z))))
+ final val powerAxiom: Formula = forall(x, forall(y, in(x, powerSet(y)) <=> subset(x, y)))
+ final val foundationAxiom: Formula = forall(x, !(x === emptySet()) ==> exists(y, in(y, x) /\ forall(z, in(z, x) ==> !in(z, y))))
- private val zAxioms: Set[(String, Axiom)] = Set(
+ final val comprehensionSchema: Formula = forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ sPhi(x, z)))))
+
+ private val zAxioms: Set[(String, Formula)] = Set(
("EmptySet", emptySetAxiom),
("extensionalityAxiom", extensionalityAxiom),
("pairAxiom", pairAxiom),
@@ -30,6 +34,6 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions {
zAxioms.foreach(a => runningSetTheory.addAxiom(a._1, a._2))
- override def axioms: Set[(String, Axiom)] = super.axioms ++ zAxioms
+ override def axioms: Set[(String, Formula)] = super.axioms ++ zAxioms
}
diff --git a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
index e89ea065..50eaf462 100644
--- a/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
+++ b/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala
@@ -6,15 +6,18 @@ import utilities.Helpers.{_, given}
/**
* Axioms for the Zermelo-Fraenkel theory (ZF)
*/
-private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms {
+trait SetTheoryZFAxioms extends SetTheoryZAxioms {
+ private val (x, y, a, b) =
+ (VariableLabel("x"), VariableLabel("y"), VariableLabel("A"), VariableLabel("B"))
+ private final val sPsi = SchematicPredicateLabel("P", 3)
- final val replacementSchema: Axiom = forall(
+ final val replacementSchema: Formula = forall(
a,
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", replacementSchema)
- override def axioms: Set[(String, Axiom)] = super.axioms + (("replacementSchema", replacementSchema))
+ override def axioms: Set[(String, Formula)] = super.axioms + (("replacementSchema", replacementSchema))
}
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index 331916cc..8b69a2b4 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -19,7 +19,7 @@ import utilities.Printer.prettySequent
import scala.collection.immutable
import scala.collection.immutable.SortedSet
-object Part1 {
+trait Part1 {
val theory = AxiomaticSetTheory.runningSetTheory
def axiom(f: Formula): theory.Axiom = theory.getAxiom(f).get
@@ -33,6 +33,9 @@ object Part1 {
private val g = SchematicFunctionLabel("g", 0)
private val h = SchematicPredicateLabel("h", 0)
+ val sPhi = SchematicPredicateLabel("P", 2)
+ val sPsi = SchematicPredicateLabel("P", 3)
+
given Conversion[SchematicFunctionLabel, Term] with
def apply(s: SchematicFunctionLabel): Term = s()
@@ -92,6 +95,9 @@ object Part1 {
val B = VariableLabel("B")
val B1 = VariableLabel("B1")
val phi = SchematicPredicateLabel("phi", 2)
+ val sPhi = SchematicPredicateLabel("P", 2)
+ val sPsi = SchematicPredicateLabel("P", 3)
+
val H = existsOne(x, phi(x, a))
val H1 = forall(a, in(a, A) ==> H)
val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
diff --git a/src/main/scala/proven/MainLibrary.scala b/src/main/scala/proven/MainLibrary.scala
new file mode 100644
index 00000000..c0c1c45a
--- /dev/null
+++ b/src/main/scala/proven/MainLibrary.scala
@@ -0,0 +1,12 @@
+package proven
+
+import lisa.kernel.proof.RunningTheory
+import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.SetTheoryTGAxioms
+import utilities.Library
+
+abstract class MainLibrary extends Library(AxiomaticSetTheory.runningSetTheory) with SetTheoryTGAxioms {
+ import AxiomaticSetTheory.*
+ override val output: String => Unit = println
+
+}
diff --git a/src/main/scala/proven/SetTheory.scala b/src/main/scala/proven/SetTheory.scala
new file mode 100644
index 00000000..84fae876
--- /dev/null
+++ b/src/main/scala/proven/SetTheory.scala
@@ -0,0 +1,31 @@
+package proven
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.settheory.AxiomaticSetTheory
+import lisa.settheory.AxiomaticSetTheory.*
+import utilities.Helpers.{_, given}
+
+trait SetTheory extends MainLibrary {
+ private val x = SchematicFunctionLabel("x", 0)
+ private val y = SchematicFunctionLabel("y", 0)
+ private val z = SchematicFunctionLabel("z", 0)
+ private val x_ = VariableLabel("x")
+ private val y_ = VariableLabel("y")
+ private val z_ = VariableLabel("z")
+
+ THEOREM("russelParadox") of ("∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢") PROOF {
+ val contra = in(y, y) <=> !in(y, y)
+ val s0 = Hypothesis(contra |- contra, contra)
+ val s1 = LeftForall(forall(x_, in(x_, y) <=> !in(x_, x_)) |- contra, 0, in(x_, y) <=> !in(x_, x_), x_, y)
+ val s2 = Rewrite(forall(x_, in(x_, y) <=> !in(x_, x_)) |- (), 1)
+ SCProof(s0, s1, s2)
+ } using ()
+
+ thm"russelParadox".show()
+}
+
+object SetTheory extends SetTheory {}
diff --git a/src/main/scala/utilities/Library.scala b/src/main/scala/utilities/Library.scala
new file mode 100644
index 00000000..6f505e44
--- /dev/null
+++ b/src/main/scala/utilities/Library.scala
@@ -0,0 +1,124 @@
+package utilities
+
+import lisa.kernel.proof.RunningTheory
+import lisa.kernel.proof.RunningTheoryJudgement
+import lisa.kernel.proof.SCProof
+
+import Helpers.{given, *}
+
+abstract class Library(val theory: RunningTheory) {
+ val output: String => Unit
+ type Justification = theory.Justification
+ type Theorem = theory.Theorem
+ val Theorem = theory.Theorem
+ type Definition = theory.Definition
+ type Axiom = theory.Axiom
+ val Axiom = theory.Axiom
+ type PredicateDefinition = theory.PredicateDefinition
+ val PredicateDefinition = theory.PredicateDefinition
+ type FunctionDefinition = theory.FunctionDefinition
+ val FunctionDefinition = theory.FunctionDefinition
+ type Judgement[J <: Justification] = RunningTheoryJudgement[J]
+
+ type Proof = SCProof
+ val Proof = SCProof
+ Proof.apply()
+
+ // extension (s:String) def apply():Unit = ()
+
+ def makeTheorem(name: String, statement: String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] =
+ theory.theorem(name, statement, proof, justifications)
+
+ case class TheoremNameWithStatement(name: String, statement: String) {
+ def PROOF(proof: SCProof): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof)
+ }
+
+ case class TheoremName(name: String) {
+ def of(statement: String): TheoremNameWithStatement = TheoremNameWithStatement(name, statement)
+ }
+
+ def THEOREM(name: String): TheoremName = TheoremName(name)
+
+ case class TheoremNameWithProof(name: String, statement: String, proof: SCProof) {
+ def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match
+ case RunningTheoryJudgement.ValidJustification(just) => just
+ case wrongJudgement: RunningTheoryJudgement.InvalidJustification[_] => wrongJudgement.showAndGet(output)
+
+ def using(u: Unit): theory.Theorem = using()
+ }
+
+ given Conversion[TheoremNameWithProof, theory.Theorem] = _.using()
+
+ implicit class JsonHelper(val sc: StringContext) {
+
+ def thm(args: Any*): theory.Theorem = getTheorem(sc.parts.mkString(""))
+
+ def ax(args: Any*): theory.Axiom = getAxiom(sc.parts.mkString(""))
+
+ def defi(args: Any*): theory.Definition = getDefinition(sc.parts.mkString(""))
+ }
+
+ def getTheorem(name: String): theory.Theorem =
+ theory.getTheorem(name) match
+ case Some(value) => value
+ case None => throw java.util.NoSuchElementException(s"No theorem with name \"$name\" was found.")
+
+ def getAxiom(name: String): theory.Axiom =
+ theory.getAxiom(name) match
+ case Some(value) => value
+ case None => throw java.util.NoSuchElementException(s"No axiom with name \"$name\" was found.")
+
+ def getDefinition(name: String): theory.Definition =
+ theory.getDefinition(name) match
+ case Some(value) => value
+ case None => throw java.util.NoSuchElementException(s"No definition for symbol \"$name\" was found.")
+
+ given Conversion[String, theory.Justification] = name => theory.getJustification(name).get
+
+ def main(args: Array[String]): Unit = { println("bonjour") }
+ /*
+ val a:String = "a"
+ val b:String = "b"
+ val c:String = "c"
+ val d:String = "d"
+ val e:String = "e"
+ val f:String = "f"
+ val g:String = "g"
+ val h:String = "h"
+ val i:String = "i"
+ val j:String = "j"
+ val k:String = "k"
+ val l:String = "l"
+ val m:String = "m"
+ val n:String = "n"
+ val o:String = "o"
+ val p:String = "p"
+ val q:String = "q"
+ val r:String = "r"
+ val s:String = "s"
+ val t:String = "t"
+ val u:String = "u"
+ val v:String = "v"
+ val w:String = "w"
+ val x:String = "x"
+ val y:String = "y"
+ val z:String = "z"
+
+ case class SchematicFLabel(s:String){
+ def apply(ts:Term*): FunctionTerm = FunctionTerm(SchematicFunctionLabel(s, ts.length), ts)
+ def apply(n:Int): SchematicFunctionLabel = SchematicFunctionLabel(s, n)
+ }
+
+ case class SchematicPLabel(s:String){
+ def apply(fs:Term*): PredicateFormula = PredicateFormula(SchematicPredicateLabel(s, fs.length), fs)
+ def apply(n:Int): SchematicPredicateLabel = SchematicPredicateLabel(s, n)
+ }
+
+ def ?(s:String) = SchematicFLabel(s)
+ def &(s:String) = SchematicPLabel(s)
+
+ given Conversion[String, VariableLabel] = VariableLabel(_)
+ given Conversion[String, VariableTerm] = s => VariableTerm(VariableLabel(s))
+
+ */
+}
diff --git a/src/main/scala/utilities/TheoriesHelpers.scala b/src/main/scala/utilities/TheoriesHelpers.scala
index fdcb6650..0199ba73 100644
--- a/src/main/scala/utilities/TheoriesHelpers.scala
+++ b/src/main/scala/utilities/TheoriesHelpers.scala
@@ -16,8 +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))
+
+ 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