Save proofs (#187)

    -Add ids to terms like for formulas
    -Add serialization of proofs. Theorems can be serialized to binary files and loaded back on later run.
    -On my machine, running everything up to Recursion.scala takes 19s instead of 24s.
    -Does no hash consing, but simple optimizations to proof size (remove consecutive rewrites, flatten subproofs)
    -Cleans up the distinction between fullName (with the whole path, should be unique) and name (just the last part, possibly duplicate across different files/domains).
    -Good completion of documentation in WithTheorems
    -checkProofs does not print proofs of more thant 100 steps now.
    -fixed an indexing bug in ShrinkProof.flattenProof
    -Suite of tests for serialization, export then load a collection of theorems.
    -Push suite of tests for Tableaux tactic that were missing.

lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala

@@ -26,7 +26,7 @@ private[fol] trait CommonDefinitions {
 
     val counterSeparator: Char = '_'
     val delimiter: Char = '`'
-    val forbiddenChars: Set[Char] = ("()[]{}?" + delimiter + counterSeparator).toSet
+    val forbiddenChars: Set[Char] = ("()[]{}?,;" + delimiter + counterSeparator).toSet
     def isValidIdentifier(s: String): Boolean = s.forall(c => !forbiddenChars.contains(c) && !c.isWhitespace)
   }
 

lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala

@@ -38,6 +38,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
    */
   sealed case class Term(label: TermLabel, args: Seq[Term]) extends TreeWithLabel[TermLabel] {
     require(label.arity == args.size)
+    val uniqueNumber: Long = TermCounters.getNewId
     val arity: Int = label.arity
 
     override def freeVariables: Set[VariableLabel] = label match {
@@ -55,6 +56,13 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
     }
     override def freeSchematicTermLabels: Set[SchematicTermLabel] = schematicTermLabels
   }
+  private object TermCounters {
+    var totalNumberOfTerms: Long = 0
+    def getNewId: Long = {
+      totalNumberOfTerms += 1
+      totalNumberOfTerms
+    }
+  }
 
   /**
    * A VariableTerm is exactly an arity-0 term whose label is a variable label, but we provide specific constructors and destructors.

lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala

@@ -1,6 +1,10 @@
 package lisa.prooflib
 
+import lisa.utils.Serialization.*
+
 trait BasicMain {
+  val library: Library
+
   private val realOutput: String => Unit = println
 
   given om: OutputManager = new OutputManager {

lisa-utils/src/main/scala/lisa/prooflib/Library.scala

@@ -30,6 +30,8 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
 
   var last: Option[JUSTIFICATION] = None
 
+  var _withCache: Boolean = false
+
   val knownDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
 
   def addSymbol(s: F.ConstantFunctionLabel[?] | F.ConstantPredicateLabel[?] | F.Constant): Unit = {

lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala

@@ -148,17 +148,17 @@ trait ProofsHelpers {
   )
   class definitionWithVars[N <: Arity](val args: Variable *** N) {
 
-    // inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(t: Term) = simpleDefinition(lambda(args, t, args.length))
-    // inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(f: Formula) = predicateDefinition(lambda(args, f, args.length))
+    // inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: Term) = simpleDefinition(lambda(args, t, args.length))
+    // inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(f: Formula) = predicateDefinition(lambda(args, f, args.length))
 
-    inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(t: The): ConstantFunctionLabelOfArity[N] =
-      FunctionDefinition[N](name.value, name.value, line.value, file.value)(args.toSeq, t.out, t.f, t.just).label
+    inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(t: The): ConstantFunctionLabelOfArity[N] =
+      FunctionDefinition[N](name.value, line.value, file.value)(args.toSeq, t.out, t.f, t.just).label
 
-    inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(term: Term): ConstantFunctionLabelOfArity[N] =
-      SimpleFunctionDefinition[N](name.value, name.value, line.value, file.value)(lambda(args.toSeq, term).asInstanceOf).label
+    inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term: Term): ConstantFunctionLabelOfArity[N] =
+      SimpleFunctionDefinition[N](name.value, line.value, file.value)(lambda(args.toSeq, term).asInstanceOf).label
 
-    inline infix def -->(using om: OutputManager, name: sourcecode.Name, line: sourcecode.Line, file: sourcecode.File)(formula: Formula): ConstantPredicateLabelOfArity[N] =
-      PredicateDefinition[N](name.value, name.value, line.value, file.value)(lambda(args.toSeq, formula).asInstanceOf).label
+    inline infix def -->(using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(formula: Formula): ConstantPredicateLabelOfArity[N] =
+      PredicateDefinition[N](name.value, line.value, file.value)(lambda(args.toSeq, formula).asInstanceOf).label
 
   }
 
@@ -172,13 +172,13 @@ trait ProofsHelpers {
   /**
    * Allows to make definitions "by unique existance" of a function symbol
    */
-  class FunctionDefinition[N <: F.Arity](using om: OutputManager)(val name: String, val fullName: String, line: Int, file: String)(
+  class FunctionDefinition[N <: F.Arity](using om: OutputManager)(val fullName: String, line: Int, file: String)(
       val vars: Seq[F.Variable],
       val out: F.Variable,
       val f: F.Formula,
       j: JUSTIFICATION
   ) extends DEFINITION(line, file) {
-    def repr: String =
+    override def repr: String =
       s" ${if (withSorry) " Sorry" else ""} Definition of function symbol ${label(vars)} := the ${out} such that ${(out === label(vars)) <=> f})\n"
 
     // val expr = LambdaExpression[Term, Formula, N](vars, f, valueOf[N])
@@ -284,33 +284,25 @@ trait ProofsHelpers {
   /**
    * Allows to make definitions "by equality" of a function symbol
    */
-  class SimpleFunctionDefinition[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(
+  class SimpleFunctionDefinition[N <: F.Arity](using om: OutputManager)(fullName: String, line: Int, file: String)(
       val lambda: LambdaExpression[Term, Term, N],
       out: F.Variable,
       j: JUSTIFICATION
-  ) extends FunctionDefinition[N](name, fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {
-    override def repr: String =
-      s" Definition of function symbol ${label(lambda.bounds.asInstanceOf)} := ${lambda.body}${if (j.withSorry) " (!! Relies on Sorry)" else ""}\n"
-
-  }
+  ) extends FunctionDefinition[N](fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {}
 
   object SimpleFunctionDefinition {
-    def apply[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(lambda: LambdaExpression[Term, Term, N]): SimpleFunctionDefinition[N] = {
-
-      // THM(using om: OutputManager)(val statement: F.Sequent, val fullName: String, line: Int, file: String, val kind: TheoremKind)(computeProof: Proof ?=> Unit)
+    def apply[N <: F.Arity](using om: OutputManager)(fullName: String, line: Int, file: String)(lambda: LambdaExpression[Term, Term, N]): SimpleFunctionDefinition[N] = {
       val intName = "definition_" + fullName
       val out = Variable(freshId(lambda.allSchematicLabels.map(_.id), "y"))
-      val defThm = new THM(F.ExistsOne(out, out === lambda.body), intName, line, file, InternalStatement)({
+      val defThm = THM(F.ExistsOne(out, out === lambda.body), intName, line, file, InternalStatement)({
         have(SimpleDeducedSteps.simpleFunctionDefinition(lambda, out))
       })
-      new SimpleFunctionDefinition[N](name, fullName, line, file)(lambda, out, defThm)
+      new SimpleFunctionDefinition[N](fullName, line, file)(lambda, out, defThm)
     }
   }
 
-  class PredicateDefinition[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(val lambda: LambdaExpression[Term, Formula, N])
-      extends DEFINITION(line, file) {
-    override def repr: String =
-      s" Definition of predicate symbol ${label(lambda.bounds.asInstanceOf)} := ${lambda.body}"
+  class PredicateDefinition[N <: F.Arity](using om: OutputManager)(val fullName: String, line: Int, file: String)(val lambda: LambdaExpression[Term, Formula, N]) extends DEFINITION(line, file) {
+
     lazy val vars: Seq[F.Variable] = lambda.bounds.asInstanceOf
     val arity = lambda.arity