continued work on theories presentation

src/main/scala/proven/dev/Library.scala

+package proven.dev
+
+import lisa.kernel.fol.FOL
+import lisa.kernel.proof.*
+import utilities.TheoriesHelpers.{*, given}
+import utilities.KernelHelpers.{*, given}
+import lisa.kernel.fol.FOL.*
+
+trait Library {
+    implicit val theory:RunningTheory
+
+    def theorem(name: String, statement:String, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = theory.theorem(name, statement, proof, justifications)
+
+    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)
+    }
+
+    //given Conversion[FunctionTerm, FunctionLabel] = _.label
+
+    def ?(s:String) = SchematicFLabel(s)
+    def &(s:String) = SchematicPLabel(s)
+
+    given Conversion[String, VariableLabel] = VariableLabel(_)
+    given Conversion[String, VariableTerm] = s => VariableTerm(VariableLabel(s))
+
+    ?("x")
+}

src/main/scala/proven/dev/MainLibrary.scala

@@ -3,9 +3,9 @@ package proven.dev
 import lisa.kernel.proof.RunningTheory
 import lisa.settheory.AxiomaticSetTheory
 
-trait MainLibrary {
-
-  given RunningTheory = AxiomaticSetTheory.runningSetTheory
+trait MainLibrary extends Library {
+  implicit val theory: RunningTheory = AxiomaticSetTheory.runningSetTheory
+  
   import AxiomaticSetTheory.runningSetTheory.*
 
 }

src/main/scala/proven/dev/SetTheory.scala

@@ -7,9 +7,10 @@ import lisa.settheory.AxiomaticSetTheory
 import lisa.settheory.AxiomaticSetTheory.*
 import proven.DSetTheory.Part1.{russelParadox, theory}
 import utilities.KernelHelpers.{*, given}
-import utilities.TheoriesHelpers.{*, given}
+import lisa.kernel.proof.RunningTheory
 
 trait SetTheory extends MainLibrary{
+  /*
   private val x = SchematicFunctionLabel("x", 0)
   private val y = SchematicFunctionLabel("y", 0)
   private val z = SchematicFunctionLabel("z", 0)
@@ -19,19 +20,22 @@ trait SetTheory extends MainLibrary{
   private val f = SchematicFunctionLabel("f", 0)
   private val g = SchematicFunctionLabel("g", 0)
   private val h = SchematicPredicateLabel("h", 0)
+  */
+
+  private val `s?` = "sd"
 
   given Conversion[SchematicFunctionLabel, Term] with
-    def apply(s: SchematicFunctionLabel): Term = s()
+    def apply(s: SchematicFunctionLabel): Term = s.apply()
+
+
 
-  /**
-   */
   val russelParadox: SCProof = {
-    val contra = (in(y, y)) <=> !(in(y, y))
+    val contra = (in(?y, ?y)) <=> !(in(?y, ?y))
     val s0 = Hypothesis(contra |- contra, contra)
-    val s1 = LeftForall(forall(x1, in(x1, y) <=> !in(x1, x1)) |- contra, 0, in(x1, y) <=> !in(x1, x1), x1, y)
-    val s2 = Rewrite(forall(x1, in(x1, y) <=> !in(x1, x1)) |- (), 1)
+    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)
   }
-  import AxiomaticSetTheory.runningSetTheory.*
-  theorem(AxiomaticSetTheory.runningSetTheory)("russelParadox", "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢", russelParadox, Nil).get
+  theorem("russelParadox", "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢", russelParadox, Nil).get
+
 }

src/main/scala/utilities/TheoriesHelpers.scala

@@ -18,4 +18,5 @@ object TheoriesHelpers {
 
 
 
+
 }