Add support for egg and egg executable for windows.

lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala

@@ -39,7 +39,8 @@ object SequentCalculus {
       else if (s.right.size == 1) s.right.head
       else s.right.reduce(or(_)(_))
     }
-    implies(left)(right)
+    if (s.left.isEmpty) right
+    else implies(left)(right)
   }
 
   /**

lisa-sets2/src/main/scala/lisa/automation/atp/Egg.scala

@@ -25,7 +25,8 @@ import sys.process._
 object Egg extends ProofTactic with ProofSequentTactic {
   private var i : Int = 0
 
-  val goelandExec = "../bin/egg-sc-tptp"
+  val eggExec_linux = "../bin/egg-sc-tptp"
+  val eggExec_windows = "..\\bin\\egg-sc-tptp.exe"
 
   class OsNotSupportedException(msg: String) extends Exception(msg)
 
@@ -91,12 +92,21 @@ object Egg extends ProofTactic with ProofSequentTactic {
     }
     val r = problemToFile(foldername, filename, "question"+i, axioms, sequent, source)
     i += 1
-
     if generateProofs then
       val OS = System.getProperty("os.name")
       if OS.contains("nix") || OS.contains("nux") || OS.contains("aix") then
-        val ret = s"chmod u+x \"$goelandExec\"".!
-        val cmd = (s"$goelandExec $foldername$filename.p $foldername$outputname.p") // TODO
+        val ret = s"chmod u+x \"$eggExec_linux\"".!
+        val cmd = (s"$eggExec_linux $foldername$filename.p $foldername$outputname.p") // TODO
+        val res = try {
+          cmd.!!
+        } catch {
+          case e: Exception => 
+            throw e
+        }
+        val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+        Success(proof)
+      else if OS.contains("win") || OS.contains("Win") then
+        val cmd = (s"$eggExec_windows $foldername$filename.p $foldername$outputname.p --level1") // TODO
         val res = try {
           cmd.!!
         } catch {
@@ -105,8 +115,6 @@ object Egg extends ProofTactic with ProofSequentTactic {
         }
         val proof = reconstructProof(new File(foldername+outputname+".p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
         Success(proof)
-      else if OS.contains("win") then
-        Failure(OsNotSupportedException("The Egg automated theorem prover is not yet supported on Windows."))
       else 
         Failure(OsNotSupportedException("The Egg automated theorem prover is only supported on Linux for now."))
     else 

lisa-sets2/src/main/scala/lisa/maths/Tests.scala

@@ -1,10 +1,8 @@
 package lisa.maths
-import lisa.automation.atp.Goeland
+import lisa.automation.atp.*
 import lisa.utils.KernelHelpers.checkProof
 import lisa.utils.tptp.*
-import java.io.*
-import lisa.kernel.proof.SCProofCheckerJudgement.SCInvalidProof
-import lisa.kernel.proof.SCProofCheckerJudgement.SCValidProof
+
 
 object Tests extends lisa.Main {
   draft()
@@ -13,10 +11,18 @@ object Tests extends lisa.Main {
   val y = variable[Term]
   val z = variable[Term]
   val P = variable[Term >>: Formula]
+  val f = variable[Term >>: Term]
+
+
+  //val ppp = ProofParser.reconstructProof(new File("goeland/testEgg.p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+
+  //checkProof(ppp)
 
-  val ppp = ProofParser.reconstructProof(new File("goeland/testEgg.p"))(using ProofParser.mapAtom, ProofParser.mapTerm, ProofParser.mapVariable)
+  val rule8 = Axiom(forall(x, x === f(f(f(f(f(f(f(f(x))))))))) )
+  val rule5 = Axiom(forall(x, x === f(f(f(f(f(x)))))) )
 
-  checkProof(ppp)
+  val saturation = Theorem(∅ === f(∅)):
+    have(thesis) by Egg.from(rule8, rule5)
 
   /*
   val buveurs = Theorem(exists(x, P(x) ==> forall(y, P(y)))) {