Types (#166)

* Starting a layer of abstraction.

* swrdgv

* sedgf

* ONgoing work. FOL structure mostly implemented, substitutions ongoing.

* continued

* further changes

* LisaObject has a self type being self

* More improvements on substitution

* More work

* multivar substitution

* improvements to MapProofTest

* finished fol, need to do prooflib

* started work on prooflib, cut plenty unused code in Library.scala

* more work on substitutions

* updated WithTheorems

* finished BasicSteptactics and substitutions

* more corrections of tactics using unifier

* fixed F and K imports

* finished PrrofHelpers and definitions. Definitions possibly not final

* Done most of the simpleDeducedSteps

* ongoing work on types

* added doc in Common.scala

* more doc, some simplification

* more doc and simplification of unneeded parts

* fixed some export issues. Commented some tests. translation left for the future.

* remove some debug code

* add missing files

* continue F integration. FInished with Set theory library files, now doing CommonTactics.scala (part is Dario's work).

* simplifier remaining

* renaming and mroe compatibility

* more adaptations

* merge build.sbt

* fixing

* transforming unification to Front

* weird issues with match types and dotty

* Compiles..? Need to simplify use of Arity in formula labels now. Finger crossed.

* add missing files

* still compiles

* Term**0 |-> Term

* Does not compile (dotty crash). Possibly due to covariant schematic labels.

* Labels are contravariant

* Weird "inherits conflicting instances of non-variant base trait LisaObject"

* structure seems to work; Constant extends ConstantFunctionSymbol[0], issue with case class (has to reimplement).

* back to the "common super type with case classes" structure

* finished predicates, compiles. Connector left

* Finished datastructure. TODO: Underlyings, Arity, uncomment asFront

* Compiles, checked arity and underlyings (mostly)

* Rehabilited asFront. Next stop, Substitution.

* porting unificationUtils

* half of unificationUtils done. Need to make Common even closer structure to kernel (variableFormula extends PredicateFormula)

* progress through unification

* compiles, progressing

* safe for reset

* only applySubst remaining.
Note: given
```scala
val s: Seq[(Variable, Term)]
```
`s.toMap` crashes dotty. Instead, do `Map(s*)`.

* Substitution done, everything compiles.

* rehabilited commented function

* utils tests compiles and pass.

* Finished setTheorzLibrary, close to finish OLPropositionalSolver

* Quantifiers.scala work, completed BasicProofTactic, implemented printing of terms and formulas

* progress on compilation and run of SetTheory.scala

* ordinals1 works

* Everything works, even example package. Some tests are still commentated. Simplified a couple proofs.

* Small improvements

* Ready for demo

* scalafix, scalafmt

* git add

* Removed unused option in build.sbt, run scalafixAll and scalafmtAll on lisa-examples, add a newline in build.properties

.gitignore

@@ -11,3 +11,8 @@ target
 *.scala.semanticdb
 
 *.iml
+
+# silex and scallion
+
+silex/*
+scallion/*

build.sbt

@@ -17,6 +17,15 @@ inThisBuild(
   )
 )
 
+
+val commonSettings = Seq(
+  version            := "0.9",
+  crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
+  organization       := "ch.epfl.lara",
+  scalacOptions     ++= Seq("-Ximport-suggestion-timeout", "0")
+)
+
+
 val scala2 = "2.13.8"
 val scala3 = "3.2.2"
 
@@ -49,9 +58,9 @@ lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.gi
 lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18")
 
 lazy val root = Project(
-  id = "lisa",
-  base = file(".")
-)
+    id = "lisa",
+    base = file(".")
+  )
   .settings(commonSettings3)
   .settings(
     version := "0.1"
@@ -86,6 +95,6 @@ lazy val examples = Project(
   id = "lisa-examples",
   base = file("lisa-examples")
 )
+  .settings(commonSettings)
   .settings(commonSettings3)
-  .dependsOn(root)
-
+  .dependsOn(root)

lisa-examples/src/main/scala/Example.scala

@@ -1,86 +1,67 @@
 import lisa.automation.kernel.OLPropositionalSolver.*
-import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheory
-import lisa.kernel.proof.SCProofChecker.*
-import lisa.kernel.proof.SequentCalculus.*
-import lisa.mathematics.settheory.SetTheory.*
-import lisa.prooflib.BasicStepTactic.*
-import lisa.prooflib.ProofTacticLib.*
-import lisa.prooflib.Substitution
-import lisa.prooflib.Substitution.ApplyRules
-import lisa.utils.FOLPrinter.*
-import lisa.utils.KernelHelpers.checkProof
-import lisa.utils.unification.UnificationUtils.*
-
-/**
- * Discover some of the elements of LISA to get started.
- */
-object Example {
-
-  import lisa.kernel.proof.SequentCalculus.*
-
-  def main(args: Array[String]): Unit = {
-    val phi = formulaVariable()
-    val psi = formulaVariable()
-    val PierceLaw = SCProof(
-      Hypothesis(phi |- phi, phi),
-      Weakening(phi |- (phi, psi), 0),
-      RightImplies(() |- (phi, phi ==> psi), 1, phi, psi),
-      LeftImplies((phi ==> psi) ==> phi |- phi, 2, 0, (phi ==> psi), phi),
-      RightImplies(() |- ((phi ==> psi) ==> phi) ==> phi, 3, (phi ==> psi) ==> phi, phi)
-    )
-    val PierceLaw2 = SCProof(
-      RestateTrue(() |- ((phi ==> psi) ==> phi) ==> phi)
-    )
-
-    checkProof(PierceLaw)
-    checkProof(PierceLaw2)
-
-    val theory = new RunningTheory
-    val pierceThm: theory.Theorem = theory.makeTheorem("Pierce's Law", () |- ((phi ==> psi) ==> phi) ==> phi, PierceLaw, Seq.empty).get
-  }
-
-}
+import lisa.prooflib.Substitution.{ApplyRules as Substitute}
 
-object ExampleDSL extends lisa.Main {
+object Example extends lisa.Main {
 
-  // Simple Theorem with LISA's DSL
   val x = variable
-  val P = predicate(1)
-  val f = function(1)
+  val y = variable
+  val P = predicate[1]
+  val f = function[1]
+
+  // Simple proof with LISA's DSL
   val fixedPointDoubleApplication = Theorem(∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))) {
     assume(∀(x, P(x) ==> P(f(x))))
     assume(P(x))
     val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
     val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
     have(thesis) by Tautology.from(step1, step2)
   }
-  show
 
-  // More complicated example of a proof with LISA DSL
-  val y = variable
-  val z = variable
-  val unionOfSingleton = Theorem(union(singleton(x)) === x) {
-    val X = singleton(x)
-    val forward = have(in(z, x) ==> in(z, union(X))) subproof {
-      have(in(z, x) |- in(z, x) /\ in(x, X)) by Tautology.from(pairAxiom of (y -> x, z -> x))
-      val step2 = thenHave(in(z, x) |- ∃(y, in(z, y) /\ in(y, X))) by RightExists
-      have(thesis) by Tautology.from(step2, unionAxiom of (x -> X))
-    }
-
-    val backward = have(in(z, union(X)) ==> in(z, x)) subproof {
-      have(in(z, y) |- in(z, y)) by Restate
-      val step2 = thenHave((y === x, in(z, y)) |- in(z, x)) by ApplyRules(y === x)
-      have(in(z, y) /\ in(y, X) |- in(z, x)) by Tautology.from(pairAxiom of (y -> x, z -> y), step2)
-      val step4 = thenHave(∃(y, in(z, y) /\ in(y, X)) |- in(z, x)) by LeftExists
-      have(in(z, union(X)) ==> in(z, x)) by Tautology.from(unionAxiom of (x -> X), step4)
-    }
-
-    have(in(z, union(X)) <=> in(z, x)) by RightIff(forward, backward)
-    thenHave(forall(z, in(z, union(X)) <=> in(z, x))) by RightForall
-    andThen(Substitution.applySubst(extensionalityAxiom of (x -> union(X), y -> x)))
+  // Example of set theoretic development
+
+  /**
+   * Theorem --- The empty set is a subset of every set.
+   *
+   *    `|- ∅ ⊆ x`
+   */
+  val emptySetIsASubset = Theorem(
+    ∅ ⊆ x
+  ) {
+    have((y ∈ ∅) ==> (y ∈ x)) by Weakening(emptySetAxiom of (x := y))
+    val rhs = thenHave(∀(y, (y ∈ ∅) ==> (y ∈ x))) by RightForall
+    have(thesis) by Tautology.from(subsetAxiom of (x := ∅, y := x), rhs)
   }
-  show
+
+  /**
+   * Theorem --- If a set has an element, then it is not the empty set.
+   *
+   *    `y ∈ x ⊢ ! x = ∅`
+   */
+  val setWithElementNonEmpty = Theorem(
+    (y ∈ x) |- x =/= ∅
+  ) {
+    have((x === ∅) |- !(y ∈ x)) by Substitute(x === ∅)(emptySetAxiom of (x := y))
+  }
+
+  /**
+   * Theorem --- A power set is never empty.
+   *
+   *   `|- !powerAxiom(x) = ∅`
+   */
+  val powerSetNonEmpty = Theorem(
+    powerSet(x) =/= ∅
+  ) {
+    have(thesis) by Tautology.from(
+      setWithElementNonEmpty of (y := ∅, x := powerSet(x)),
+      powerAxiom of (x := ∅, y := x),
+      emptySetIsASubset
+    )
+  }
+
+  /*
+
+  import lisa.mathematics.settheory.SetTheory.*
+
 
   // Examples of definitions
   val succ = DEF(x) --> union(unorderedPair(x, singleton(x)))
@@ -89,53 +70,46 @@ object ExampleDSL extends lisa.Main {
   val inductiveSet = DEF(x) --> in(∅, x) /\ forall(y, in(y, x) ==> in(succ(y), x))
   show
 
-  val defineNonEmptySet = Lemma(∃!(x, !(x === ∅) /\ (x === unorderedPair(∅, ∅)))) {
-    val subst = have(False <=> in(∅, ∅)) by Rewrite(emptySetAxiom of (x -> ∅()))
-    have(in(∅, unorderedPair(∅, ∅)) <=> False |- ()) by Rewrite(pairAxiom of (x -> ∅(), y -> ∅(), z -> ∅()))
-    andThen(Substitution.applySubst(subst))
-    thenHave(∀(z, in(z, unorderedPair(∅, ∅)) <=> in(z, ∅)) |- ()) by LeftForall
-    andThen(Substitution.applySubst(extensionalityAxiom of (x -> unorderedPair(∅(), ∅()), y -> ∅())))
-    andThen(Substitution.applySubst(x === unorderedPair(∅(), ∅())))
-    thenHave((!(x === ∅) /\ (x === unorderedPair(∅, ∅))) <=> (x === unorderedPair(∅, ∅))) by Tautology
-    thenHave(∀(x, (x === unorderedPair(∅, ∅)) <=> (!(x === ∅) /\ (x === unorderedPair(∅, ∅))))) by RightForall
-    thenHave(∃(y, ∀(x, (x === y) <=> (!(x === ∅) /\ (x === unorderedPair(∅, ∅)))))) by RightExists
-  }
-  show
 
-  // This definition is underspecified
-  val nonEmpty = DEF() --> The(x, !(x === ∅))(defineNonEmptySet)
-  show
 
-  // Simple tactic definition for LISA DSL
-  import lisa.automation.kernel.OLPropositionalSolver.*
-
-  // object SimpleTautology extends ProofTactic {
-  //   def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = {
-  //     val redF = reducedForm(f)
-  //     if (redF == ⊤) {
-  //       Restate(decisionsPos |- f :: decisionsNeg)
-  //     } else if (redF == ⊥) {
-  //       proof.InvalidProofTactic("Sequent is not a propositional tautology")
-  //     } else {
-  //       val atom = findBestAtom(redF).get
-  //       def substInRedF(f: Formula) = redF.substituted(atom -> f)
-  //       TacticSubproof {
-  //         have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg))
-  //         val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom)
-  //         have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg))
-  //         val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom)
-  //         have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2)
-  //         thenHave(decisionsPos |- f :: decisionsNeg) by Restate
-  //       }
-  //     }
-  //   }
-  //   def solveSequent(using proof: library.Proof)(bot: Sequent) =
-  //     TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula
-  //       have(solveFormula(sequentToFormula(bot), Nil, Nil))
-  //       thenHave(bot) by Restate.from
-  //     }
-  // }
 
+
+   */
+
+  /*
+
+
+
+// Simple tactic definition for LISA DSL
+import lisa.automation.kernel.OLPropositionalSolver.*
+
+// object SimpleTautology extends ProofTactic {
+//   def solveFormula(using proof: library.Proof)(f: Formula, decisionsPos: List[Formula], decisionsNeg: List[Formula]): proof.ProofTacticJudgement = {
+//     val redF = reducedForm(f)
+//     if (redF == ⊤) {
+//       Restate(decisionsPos |- f :: decisionsNeg)
+//     } else if (redF == ⊥) {
+//       proof.InvalidProofTactic("Sequent is not a propositional tautology")
+//     } else {
+//       val atom = findBestAtom(redF).get
+//       def substInRedF(f: Formula) = redF.substituted(atom -> f)
+//       TacticSubproof {
+//         have(solveFormula(substInRedF(⊤), atom :: decisionsPos, decisionsNeg))
+//         val step2 = thenHave(atom :: decisionsPos |- redF :: decisionsNeg) by Substitution2(⊤ <=> atom)
+//         have(solveFormula(substInRedF(⊥), decisionsPos, atom :: decisionsNeg))
+//         val step4 = thenHave(decisionsPos |- redF :: atom :: decisionsNeg) by Substitution2(⊥ <=> atom)
+//         have(decisionsPos |- redF :: decisionsNeg) by Cut(step4, step2)
+//         thenHave(decisionsPos |- f :: decisionsNeg) by Restate
+//       }
+//     }
+//   }
+//   def solveSequent(using proof: library.Proof)(bot: Sequent) =
+//     TacticSubproof { // Since the tactic above works on formulas, we need an extra step to convert an arbitrary sequent to an equivalent formula
+//       have(solveFormula(sequentToFormula(bot), Nil, Nil))
+//       thenHave(bot) by Restate.from
+//     }
+// }
+   */
   // val a = formulaVariable()
   // val b = formulaVariable()
   // val c = formulaVariable()

lisa-examples/src/main/scala/ExampleKernel.scala

@@ -0,0 +1,33 @@
+import lisa.utils.K
+
+import K.*
+
+/**
+ * Discover some of the elements of the logical kernel of LISA.
+ */
+object ExampleKernel {
+
+  import lisa.kernel.proof.SequentCalculus.*
+
+  def main(args: Array[String]): Unit = {
+    val phi = formulaVariable()
+    val psi = formulaVariable()
+    val PierceLaw = SCProof(
+      Hypothesis(phi |- phi, phi),
+      Weakening(phi |- (phi, psi), 0),
+      RightImplies(() |- (phi, phi ==> psi), 1, phi, psi),
+      LeftImplies((phi ==> psi) ==> phi |- phi, 2, 0, (phi ==> psi), phi),
+      RightImplies(() |- ((phi ==> psi) ==> phi) ==> phi, 3, (phi ==> psi) ==> phi, phi)
+    )
+    val PierceLaw2 = SCProof(
+      RestateTrue(() |- ((phi ==> psi) ==> phi) ==> phi)
+    )
+
+    checkProof(PierceLaw, println)
+    checkProof(PierceLaw2, println)
+
+    val theory = new RunningTheory
+    val pierceThm: theory.Theorem = theory.makeTheorem("Pierce's Law", () |- ((phi ==> psi) ==> phi) ==> phi, PierceLaw, Seq.empty).get
+  }
+
+}