Updated the LISA submodule

project/plugins.sbt

@@ -0,0 +1 @@
+addSbtPlugin("ch.epfl.scala" % "sbt-scalafix" % "0.9.34")

src/main/scala/me/cassayre/florian/masterproject/examples/proofOptimization.scala

@@ -1,7 +1,7 @@
 package me.cassayre.florian.masterproject.examples
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
+import utilities.Helpers.*
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.{SCProof, SCProofChecker}
 import me.cassayre.florian.masterproject.front.printer.KernelPrinter
@@ -17,15 +17,15 @@ import me.cassayre.florian.masterproject.util.SCUtils
   def testProofOptimization(proof: SCProof): Unit = {
     val originalChecked = SCProofChecker.checkSCProof(proof)
     println("Original proof:")
-    println(KernelPrinter.prettyProof(proof, judgement = originalChecked))
+    println(KernelPrinter.prettyJudgedProof(originalChecked))
 
     assert(originalChecked.isValid)
 
     val optimized = SCUtils.optimizeProofIteratively(proof)
     val optimizedChecked = SCProofChecker.checkSCProof(optimized)
     println()
     println("Simplified proof:")
-    println(KernelPrinter.prettyProof(optimized, judgement = optimizedChecked))
+    println(KernelPrinter.prettyJudgedProof(optimizedChecked))
 
     assert(proof.conclusion == optimized.conclusion) // The conclusion must remain the same
     assert(optimizedChecked.isValid) // The proof must still be valid

src/main/scala/me/cassayre/florian/masterproject/front/printer/KernelPrinter.scala

@@ -1,5 +1,6 @@
 package me.cassayre.florian.masterproject.front.printer
 
+import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SCProofCheckerJudgement.*
 import lisa.kernel.proof.{SCProofCheckerJudgement, SequentCalculus as SC}
 import lisa.kernel.fol.FOL
@@ -30,7 +31,11 @@ object KernelPrinter {
     Sequent(sorted(s.left.toIndexedSeq.map(fromKernel)), sorted(s.right.toIndexedSeq.map(fromKernel)))
   }
 
-  def prettyProof(scProof: lisa.kernel.proof.SCProof, style: FrontPrintStyle = FrontPrintStyle.Unicode, compact: Boolean = false, explicit: Boolean = false, judgement: SCProofCheckerJudgement = SCValidProof): String = {
+  def prettyProof(scProof: SCProof, style: FrontPrintStyle = FrontPrintStyle.Unicode, compact: Boolean = false, explicit: Boolean = false): String =
+    prettyJudgedProof(SCValidProof(scProof), style, compact, explicit)
+
+  def prettyJudgedProof(judgement: SCProofCheckerJudgement, style: FrontPrintStyle = FrontPrintStyle.Unicode, compact: Boolean = false, explicit: Boolean = false): String = {
+    val scProof = judgement.proof
     val p = FrontPrintParameters(style, compact)
     val r = KernelRuleIdentifiers(p.s)
     def prettyName(name: String): String = style match {
@@ -162,8 +167,8 @@ object KernelPrinter {
         val fullPath = i +: path
 
         val prefix = judgement match {
-          case SCValidProof => ""
-          case SCInvalidProof(errorPath, _) => if(errorPath.reverse == fullPath) proofStepIndicator else proofStepNoIndicator
+          case SCValidProof(_) => ""
+          case SCInvalidProof(_, errorPath, _) => if(errorPath.reverse == fullPath) proofStepIndicator else proofStepNoIndicator
         }
 
         prefix +
@@ -188,8 +193,8 @@ object KernelPrinter {
     }
 
     val errorSeq = judgement match {
-      case SCValidProof => Seq.empty
-      case SCInvalidProof(path, message) => Seq(s"Proof checker has reported an error at line ${path.mkString(".")}: $message")
+      case SCValidProof(_) => Seq.empty
+      case SCInvalidProof(_, path, message) => Seq(s"Proof checker has reported an error at line ${path.mkString(".")}: $message")
     }
 
     val allLinesPairs = recursivePrint(proof, Seq.empty)

src/main/scala/me/cassayre/florian/masterproject/front/proof/sequent/SequentDefinitions.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.front.proof.sequent
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 
 trait SequentDefinitions {

src/main/scala/me/cassayre/florian/masterproject/front/proof/state/ProofEnvironmentDefinitions.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.front.proof.state
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.{RunningTheory, SCProof, SCProofChecker}
 import lisa.kernel.proof.RunningTheoryJudgement.*
 import lisa.kernel.proof.SequentCalculus.{SCSubproof, sequentToFormula}
@@ -31,8 +31,8 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
 
     override def contains(sequent: Sequent): Boolean = proven.contains(sequent)
 
-    def belongsToTheory(label: ConstantFunctionLabel[?]): Boolean = runningTheory.isAcceptedFunctionLabel(toKernel(label))
-    def belongsToTheory(label: ConstantPredicateLabel[?]): Boolean = runningTheory.isAcceptedPredicateLabel(toKernel(label))
+    def belongsToTheory(label: ConstantFunctionLabel[?]): Boolean = runningTheory.isSymbol(toKernel(label))
+    def belongsToTheory(label: ConstantPredicateLabel[?]): Boolean = runningTheory.isSymbol(toKernel(label))
     def belongsToTheory(term: Term): Boolean =
       functionsOf(term).collect { case f: ConstantFunctionLabel[?] => f }.forall(belongsToTheory)
     def belongsToTheory(formula: Formula): Boolean =
@@ -53,7 +53,7 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
           Seq(
             "Error: the theorem was found to produce an invalid proof; this could indicate a problem with a tactic or a bug in the implementation",
             "The produced proof is shown below for reference:",
-            Printer.prettySCProof(scProof, judgement)
+            Printer.prettySCProof(judgement)
           ).mkString("\n")
         )
       }
@@ -62,7 +62,7 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
       val justifications = justificationPairs.map { case (justification, _) => justification }
 
       val kernelJustifications = justificationPairs.map { case (_, kernelJustification) => kernelJustification }
-      val kernelTheorem = runningTheory.proofToTheorem(s"t${proven.size}", scProof, kernelJustifications) match {
+      val kernelTheorem = runningTheory.makeTheorem(s"t${proven.size}", scProof.conclusion, scProof, kernelJustifications) match {
         case ValidJustification(result) => result
         case InvalidJustification(_, _) => throw new Error // Should have been caught before
       }
@@ -169,7 +169,7 @@ trait ProofEnvironmentDefinitions extends ProofStateDefinitions {
         Seq(
           "Error: the reconstructed proof was found to be invalid; this could indicate a bug in the implementation of this very method",
           "The reconstructed proof is shown below for reference:",
-          Printer.prettySCProof(scProof, judgement)
+          Printer.prettySCProof(judgement)
         ).mkString("\n")
       )
     }

src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystem.scala

@@ -1,9 +1,9 @@
 package me.cassayre.florian.masterproject.legacy
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
-import lisa.kernel.Printer
-import lisa.kernel.Printer.*
+import utilities.Helpers.*
+import utilities.Printer
+import utilities.Printer.*
 import lisa.kernel.proof.SequentCalculus.{Hypothesis, Sequent, Weakening, sequentToFormula}
 import lisa.kernel.proof.{RunningTheory, SCProof, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory

src/main/scala/me/cassayre/florian/masterproject/legacy/GoalBasedProofSystemREPL.scala

@@ -6,7 +6,7 @@ import me.cassayre.florian.masterproject.legacy.GoalBasedProofSystem.*
 import java.util.Scanner
 import scala.util.{Failure, Success, Try}
 import lisa.kernel.fol.FOL.*
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.{RunningTheory, SCProofChecker}
 import lisa.settheory.AxiomaticSetTheory
 
@@ -126,7 +126,7 @@ object GoalBasedProofSystemREPL {
                             .println(prettyFrame(prettyProofState(newState.proofState)))
                             .println()
                             .println("All goals have been proven, the proof will now be reconstructed below:")
-                            .println(Printer.prettySCProof(proof, judgement))
+                            .println(Printer.prettySCProof(judgement))
                             .println()
                             .println(
                               if(judgement.isValid)

src/main/scala/me/cassayre/florian/masterproject/legacy/meta/Meta.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.meta
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.{SCProof, SCProofChecker, SequentCalculus}
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 import me.cassayre.florian.masterproject.legacy.parser.SCReader.*

src/main/scala/me/cassayre/florian/masterproject/legacy/parser/SCResolver.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.parser
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.legacy.parser.SCParsed.*
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SCProof

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/demo.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 
 import scala.util.chaining.*
 import me.cassayre.florian.masterproject.front.{*, given}

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests.scala

@@ -1,7 +1,7 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
 import me.cassayre.florian.masterproject.front.{*, given}
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 
 @main def tests(): Unit = {
@@ -37,7 +37,7 @@ import lisa.kernel.proof.SCProofChecker
     case Some((proof, theorems)) =>
       val judgement = SCProofChecker.checkSCProof(proof)
 
-      println(Printer.prettySCProof(proof, judgement))
+      println(Printer.prettySCProof(judgement))
 
       println()
       if(theorems.nonEmpty) {

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests2.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import me.cassayre.florian.masterproject.front.{*, given}
 

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests4.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import me.cassayre.florian.masterproject.front.{*, given}
 import me.cassayre.florian.masterproject.front.theory.SetTheory.*

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests5.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.front.{*, given}
 import me.cassayre.florian.masterproject.front.theory.SetTheory.*
 

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tests6.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.test.front
 
-import lisa.kernel.Printer
+import utilities.Printer
 
 import scala.util.chaining.*
 import me.cassayre.florian.masterproject.front.fol.FOL.{*, given}

src/main/scala/me/cassayre/florian/masterproject/legacy/test/front/tmp.scala.old

@@ -0,0 +1,103 @@
+package me.cassayre.florian.masterproject.legacy.test.front
+
+import lisa.kernel.Printer
+
+import scala.util.chaining.*
+import me.cassayre.florian.masterproject.front.{*, given}
+
+@main def tmp(): Unit = {}
+/*val (a, b, c) = (SchematicPredicateLabel[0]("a"), SchematicPredicateLabel[0]("b"), SchematicPredicateLabel[0]("c"))
+
+@main def tmp(): Unit = {
+  import me.cassayre.florian.masterproject.front.theory.SetTheory.*
+
+  val (s, t, u) = (SchematicFunctionLabel[0]("s"), SchematicFunctionLabel[0]("t"), SchematicFunctionLabel[0]("u"))
+  val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z"))
+
+  given ProofEnvironment = newSetTheoryEnvironment()
+
+  val axExt: Axiom = axiomExtensionality.asJustified.display()
+  val axEmpty: Axiom = axiomEmpty.asJustified.display()
+  val axUnion: Axiom = axiomUnion.asJustified.display()
+
+  // 1. Generalize universal quantifiers
+
+  val thmExtSchema: Theorem = {
+    val t0 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, x => forall(y, forall(z, (z in x) <=> (z in y)) <=> (x === y)))
+        .withFunction(Notations.t, s())
+    )(axExt).get
+
+    val t1 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, y => forall(z, (z in s) <=> (z in y)) <=> (s === y))
+        .withFunction(Notations.t, t())
+    )(t0).get
+
+    t1
+  }.display()
+
+  val thmEmptySchema: Theorem = elimRForallS(
+    RuleParameters()
+      .withPredicate(Notations.p, x => !(x in emptySet))
+      .withFunction(Notations.t, s())
+  )(axEmpty).get.display()
+
+  val thmUnionSchema: Theorem = {
+    val t0 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, x => forall(z, (x in unionSet(z)) <=> exists(y, (x in y) /\ (y in z))))
+        .withFunction(Notations.t, s())
+    )(axUnion).get
+    val t1 = elimRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, z => (s in unionSet(z)) <=> exists(y, (s in y) /\ (y in z)))
+        .withFunction(Notations.t, t())
+    )(t0).get
+    t1
+  }.display()
+
+  val _ = {
+    val p = ProofMode(() |- unionSet(emptySet) === emptySet)
+    import p.*
+
+    apply(elimRSubstIff(
+      RuleParameters()
+        .withConnector(Notations.f, identity)
+        .withPredicate(Notations.a, formula"forall z. (z in U({})) <=> (z in {})")
+    ))
+
+    focus(1)
+    val _ = thmExtSchema(Notations.s, unionSet(emptySet))(Notations.t, emptySet)
+
+    apply(justification) // Uses the previously proved theorem
+
+    apply(introRForallS(
+      RuleParameters()
+        .withPredicate(Notations.p, z => formula"\ $z. ($z in U({})) <=> ($z in {})")
+        .withFunction(Notations.t, s())
+    ))
+
+    apply(RuleSubstituteRightIff(
+      RuleParameters()
+        .withConnector(Notations.f, x => x <=> (s in emptySet))
+        .withPredicate(Notations.a, formula"exists y. (?s in y) /\ (y in {})")
+    ))
+
+    focus(1)
+    val _ = thmUnionSchema(t, emptySet).rewrite(state.goals.head).get.display()
+    apply(justification)
+
+    apply(introRIff)
+    apply(introRImp)
+    apply(introLExists(
+      RuleParameters()
+        .withPredicate(Notations.p, y => (s in y) /\ (y in emptySet))
+    ))
+
+    apply(introLAnd)
+
+  }
+
+}*/

src/main/scala/me/cassayre/florian/masterproject/legacy/test/tests.scala

@@ -1,9 +1,9 @@
 package me.cassayre.florian.masterproject.legacy.test
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
+import utilities.Helpers.*
 import me.cassayre.florian.masterproject.legacy.GoalBasedProofSystem.*
-import lisa.kernel.Printer
+import utilities.Printer
 import lisa.kernel.proof.SCProofChecker
 import lisa.settheory.AxiomaticSetTheory
 

src/main/scala/me/cassayre/florian/masterproject/legacy/unification/Unifier.scala

@@ -1,6 +1,6 @@
 package me.cassayre.florian.masterproject.legacy.unification
 
-import lisa.kernel.Printer
+import utilities.Printer
 import me.cassayre.florian.masterproject.front.fol.FOL.*
 
 import scala.annotation.tailrec

src/main/scala/me/cassayre/florian/masterproject/util/MonadicSCProofBuilder.scala

@@ -1,7 +1,7 @@
 package me.cassayre.florian.masterproject.util
 
 import lisa.kernel.fol.FOL.*
-import lisa.KernelHelpers.*
+import utilities.Helpers.*
 import lisa.kernel.proof.SCProof
 import lisa.kernel.proof.SequentCalculus.*
 import me.cassayre.florian.masterproject.util.SCProofBuilder.{*, given}

src/main/scala/me/cassayre/florian/masterproject/util/SCProofBuilder.scala

@@ -1,8 +1,8 @@
 package me.cassayre.florian.masterproject.util
 
+import lisa.kernel.fol.FOL
 import lisa.kernel.proof.{SCProof, SequentCalculus}
 import lisa.kernel.proof.SequentCalculus.*
-import lisa.settheory.AxiomaticSetTheory.Axiom
 
 /**
  * The proof builder API, a helper to build kernel proofs.
@@ -38,7 +38,7 @@ object SCProofBuilder {
     infix def by(premises: Int*): SCImplicitProofStep = SCImplicitProofStep(s, premises, Seq.empty)
     infix def by(step: SCProofStep): SCExplicitProofStep = SCExplicitProofStep(step)
     infix def justifiedBy(sequents: Sequent*): SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, sequents)
-    infix def justifiedBy(axiom: Axiom): SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, Seq(Sequent(Set.empty, Set(axiom))))
+    infix def justifiedBy(axiom: FOL.Formula): SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, Seq(Sequent(Set.empty, Set(axiom))))
     def justified: SCImplicitProofStep = SCImplicitProofStep(s, Seq.empty, Seq(s))
   }
 

src/main/scala/me/cassayre/florian/masterproject/util/SCProofStepFinder.scala

@@ -3,7 +3,7 @@ package me.cassayre.florian.masterproject.util
 import lisa.kernel.fol.FOL.*
 import lisa.kernel.proof.SequentCalculus.*
 import lisa.kernel.proof.{SCProof, SCProofChecker}
-import lisa.kernel.Printer
+import utilities.Printer
 
 import scala.collection.View