diff --git a/.gitignore b/.gitignore
index b05d0969af134147e63d239ea3e88689adf52071..aaadedc954e6510f795774cc4f14d71ddd3e5b1d 100644
--- a/.gitignore
+++ b/.gitignore
@@ -3,6 +3,8 @@
.metals
.vscode
project/metals.sbt
+project/project/metals.sbt
+sbt-launch.jar
# build-related
.bsp
diff --git a/CHANGES.md b/CHANGES.md
index c8dd41a37eb34d33d7de4ebf132f6e72e54445e8..9e00084aefc0fa88d3b085b37aa98eff324f253b 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,9 @@
# Change List
+## 2024-04-12
+Addition of simply typed lambda calculus with top level polymorphism and inductive poylmorphic algebraic data types.
+Addition of tactics for typechecking and structural induction over ADTs.
+
## 2024-03-02
Support for reconstructing proofs from file in SC-TPTP format. Support and inclusion of Goeland as a tactic. Doc in the manual.
diff --git a/build.sbt b/build.sbt
index 1e58411042d0ddb5eb6f8e4141d1a9149fb0e0c5..bc9c0c1befbdc3d06de8973f9bc22905ba36ad77 100644
--- a/build.sbt
+++ b/build.sbt
@@ -20,7 +20,7 @@ ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports"
val commonSettings = Seq(
- crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
+ crossScalaVersions := Seq("3.3.1"),
run / fork := true
)
@@ -40,10 +40,11 @@ val commonSettings3 = commonSettings ++ Seq(
// "-source:future", re-enable when liancheng/scalafix-organize-imports#221 is fixed
),
+ javaOptions += "-Xmx10G",
libraryDependencies += "org.scalatest" %% "scalatest" % "3.2.10" % "test",
libraryDependencies += "com.lihaoyi" %% "sourcecode" % "0.3.0",
//libraryDependencies += "org.scala-lang.modules" %% "scala-parser-combinators" % "2.1.1",
- libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
+ // libraryDependencies += ("io.github.uuverifiers" %% "princess" % "2023-06-19").cross(CrossVersion.for3Use2_13),
Test / parallelExecution := false
)
diff --git a/lisa-examples/src/main/scala/ADTExample.scala b/lisa-examples/src/main/scala/ADTExample.scala
new file mode 100644
index 0000000000000000000000000000000000000000..8314d18c6262fc5c9ad3ad0c0b1659147044bd8d
--- /dev/null
+++ b/lisa-examples/src/main/scala/ADTExample.scala
@@ -0,0 +1,125 @@
+object ADTExample extends lisa.Main {
+ import lisa.maths.settheory.types.adt.{*, given}
+
+ // variable declarations
+ val A = variable
+
+ val n = variable
+ val l = variable
+ val x = variable
+ val y = variable
+
+ val x0 = variable
+ val x1 = variable
+ val y0 = variable
+ val y1 = variable
+
+ // ***********************
+ // * 1 : Examples of ADT *
+ // ***********************
+
+ // Boolean
+ val define(bool: ADT[0], constructors(tru, fals)) = () | ()
+
+ // Nat
+ val define(nat: ADT[0], constructors(zero, succ)) = () | nat
+
+ // Option
+ val define(option: ADT[1], constructors(none, some)) = A --> () | A
+
+ // List
+ val define(list: ADT[1], constructors(nil, cons)) = A --> () | (A, list)
+
+ // Nothing
+ val define(nothing, constructors()) = |
+
+ // ****************
+ // * 2 : Theorems *
+ // ****************
+
+ // Injectivity
+ show(nil.injectivity)
+ show(cons.injectivity)
+ show(list.injectivity(nil, cons))
+
+ // Introduction rules
+ show(nil.intro)
+ show(cons.intro)
+
+ Lemma(nil(A) :: list(A)){
+ have(thesis) by TypeChecker.prove
+ }
+ Lemma((x :: A, l :: list(A)) |- cons(A) * x * l :: list(A)){
+ have(thesis) by TypeChecker.prove
+ }
+
+ // Induction
+ show(list.induction)
+
+ // Pattern matching
+ show(list.elim)
+
+ // *****************
+ // * 3 : Functions *
+ // *****************
+
+ val not = fun(bool, bool) {
+ Case(tru) { fals }
+ Case(fals) { tru }
+ }
+
+ val pred = fun(nat, nat):
+ Case(zero):
+ zero
+ Case(succ, n):
+ n
+
+
+ // ************************
+ // * 4 : Induction Tactic *
+ // ************************
+
+ Theorem(x :: bool |- not * (not * x) === x) {
+ have(thesis) by Induction() {
+ Case(tru) subproof {
+ val notFals = have(not * fals === tru) by Restate.from((not.elim(fals)))
+ have(fals === not * tru) by Restate.from(not.elim(tru))
+ have(not * (not * tru) === tru) by Substitution.ApplyRules(lastStep)(notFals)
+ }
+ Case(fals) subproof {
+ val notTrue = have(not * tru === fals) by Restate.from((not.elim(tru)))
+ have(tru === not * fals) by Restate.from(not.elim(fals))
+ have(not * (not * fals) === fals) by Substitution.ApplyRules(lastStep)(notTrue)
+ }
+ }
+ }
+
+ // ****************************
+ // * 5: All features together *
+ // ****************************
+
+ val consInj = Theorem((l :: list(A), x :: A) |- !(l === cons(A) * x * l)) {
+
+ val typeNil = have(nil(A) :: list(A)) by TypeChecker.prove
+ val typeCons = have((y :: A, l :: list(A)) |- cons(A) * y * l :: list(A)) by TypeChecker.prove
+
+ have(l :: list(A) |- forall(x, x :: A ==> !(l === cons(A) * x * l))) by Induction(){
+ Case(nil) subproof {
+ have(x :: A ==> !(nil(A) === cons(A) * x * nil(A))) by Tautology.from(list.injectivity(nil, cons) of (y0 := x, y1 := nil(A)), typeNil)
+ thenHave(forall(x, x :: A ==> !(nil(A) === cons(A) * x * nil(A)))) by RightForall
+ }
+ Case(cons, y, l) subproof {
+ have((y :: A ==> !(l === cons(A) * y * l), y :: A, l :: list(A)) |- x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l))) by Tautology.from(
+ cons.injectivity of (x0 := y, x1 := l, y0 := x, y1 := cons(A) * y * l),
+ typeCons
+ )
+ thenHave((y :: A ==> !(l === cons(A) * y * l), y :: A, l :: list(A)) |- forall(x, x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l)))) by RightForall
+ thenHave((forall(x, x :: A ==> !(l === cons(A) * x * l)), y :: A, l :: list(A)) |- forall(x, x :: A ==> !(cons(A) * y * l === cons(A) * x * (cons(A) * y * l)))) by LeftForall
+ }
+ }
+
+ thenHave(l :: list(A) |- x :: A ==> !(l === cons(A) * x * l)) by InstantiateForall(x)
+ thenHave(thesis) by Tautology
+ }
+
+}
\ No newline at end of file
diff --git a/lisa-sets/src/main/scala/lisa/Main.scala b/lisa-sets/src/main/scala/lisa/Main.scala
index 2ce01a39efaa24a8796d52e1887a01e6d76625de..c96ac042bded9608dc0898b3aac8ad9e01765757 100644
--- a/lisa-sets/src/main/scala/lisa/Main.scala
+++ b/lisa-sets/src/main/scala/lisa/Main.scala
@@ -29,6 +29,9 @@ trait Main extends BasicMain {
def definition: JUSTIFICATION = {
getDefinition(symbol).get
}
+ def shortDefinition: JUSTIFICATION = {
+ getShortDefinition(symbol).get
+ }
}
}
diff --git a/lisa-sets/src/main/scala/lisa/automation/Apply.scala b/lisa-sets/src/main/scala/lisa/automation/Apply.scala
index 22b0bc9c1ccb5325a607ac56211592a913bf9305..a0c22d7902b93a43077c45b2cb160993e506eb84 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Apply.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Apply.scala
@@ -6,7 +6,10 @@ import lisa.prooflib.ProofTacticLib.*
import lisa.prooflib.SimpleDeducedSteps.*
import lisa.prooflib.*
import lisa.utils.unification.UnificationUtils.*
-import scala.util.boundary, boundary.break
+
+import scala.util.boundary
+
+import boundary.break
/**
@@ -48,16 +51,21 @@ class Apply(using val lib: Library, val proof: lib.Proof)(thm: proof.Fact) exten
*/
private def normalForm(seq: Sequent): Sequent =
def removeImplies(s: Sequent): Sequent =
- s.right.head match
- case AppliedConnector(Implies, Seq(phi, psi)) => s.left + phi |- psi
- case _ => s
-
+ if s.right.isEmpty then
+ s
+ else
+ s.right.head match
+ case AppliedConnector(Implies, Seq(phi, psi)) => removeImplies(s.left + phi |- psi)
+ case _ => s
+
+
+
def removeConjunctions(s: Sequent): Sequent =
- s.left.flatMap(f =>
- f match
- case AppliedConnector(And, Seq(phi, psi)) => Set(phi, psi)
- case _ => Set(f)
- ) |- s.right
+ def rec(f: Formula): Set[Formula] =
+ f match
+ case AppliedConnector(And, Seq(phi, psi)) => rec(phi) ++ rec(psi)
+ case _ => Set(f)
+ s.left.flatMap(rec) |- s.right
removeConjunctions(removeImplies(seq))
@@ -106,128 +114,140 @@ class Apply(using val lib: Library, val proof: lib.Proof)(thm: proof.Fact) exten
private def substitute(using _proof: lib.Proof)(fact: _proof.Fact, fSubst: FormulaSubstitution, tSubst: TermSubstitution): _proof.Fact =
fact.of(fSubst.toFSubstPair: _*).of(tSubst.toTSubstPair: _*)
-
/**
- * Applies on method with a sequence as an argument instead of a varargs.
- */
- infix def onSeq(premises: Seq[proof.Fact])(bot: Sequent): proof.ProofTacticJudgement = on(premises : _*)(bot)
+ * Applies on method with a varargs instead of a sequence.
+ */
+ infix def on(premises: proof.Fact*)(bot: Sequent): proof.ProofTacticJudgement = on(premises.toSeq)(bot)
+
/**
* Executes the tactic. See class description for use cases.
*
* @param premises the facts that are applied to the theorem
+ * @param excluding the variables that are not to be substituted
* @param bot the sequent the user want to prove
*/
- infix def on(premises: proof.Fact*)(bot: Sequent): proof.ProofTacticJudgement =
-
- boundary:
- TacticSubproof { sp ?=>
-
- // STEP 1: Convert the given theorem, facts and sequent to their normal forms
- val botNormalized: Sequent = normalForm(bot)
- val thmNormalized: sp.Fact = lib.have(normalForm(thm.statement)) by Restate.from(thm)
- val premisesNormalized = premises.map(p => lib.have(normalForm(p.statement)) by Restate.from(p))
-
- // STEP 2: Unify the conclusion of the sequent the user want to prove and the conclusion
- val botCcl: Formula = botNormalized.right.head
- val thmCcl: Formula = thmNormalized.statement.right.head
-
- matchFormula(botCcl, thmCcl) match
- case Some((formulaCclAssignment, termCclAssignment)) =>
-
- //Unification succeeded, subtitution can be performed
- val thmAfterCclUnification: sp.Fact = substitute(thmNormalized, formulaCclAssignment, termCclAssignment)
-
- // STEP 3: Process each fact
- val thmAfterPrems: sp.Fact = {
-
- premisesNormalized.foldLeft(lib.have(thmAfterCclUnification))((updatedThm, premNormalized) => {
-
-
- val premCcl: Formula = premNormalized.statement.right.head
-
- // STEP 3.1: Unify the conclusion of the fact with a premise of the theorem
- // Three possibilities:
- // - the unification succeeded and the variables in the theorem are subtituted to match the conclusion of the fact;
- // - if the unification did not succeeded, try the unification in the other direction, i.e. try to specify the fact
- // instead of the theorem. If this works, make the susbtitution inside the fact;
- // - both unifications do not succeed and the fact is dropped.
- // TODO: add a warning when the fact is dropped
- val conclusionsUnification: Option[(sp.Fact, sp.Fact)] =
- searchPremises(updatedThm.statement, premCcl) match
- case Some((fSubstAfterPrem, tSubstAfterPrem)) => Some((substitute(updatedThm, fSubstAfterPrem, tSubstAfterPrem), premNormalized))
- case None =>
- searchPremisesRev(updatedThm.statement, premCcl) match
- case Some((fSubstAfterPrem, tSubstAfterPrem)) => Some((updatedThm, substitute(premNormalized, fSubstAfterPrem, tSubstAfterPrem)))
- case None => None
-
-
-
-
- conclusionsUnification match
- case Some(updatedThmAfterCclUnification, premAfterCclUnification) =>
-
- // STEP 3.2: For each premise of the fact:
- // - check if it is in the sequent the user want to prove. If yes, add it to the preconditions of the theorem
- // using weakening;
- // - else if it matches one of the premises of the theorem specify the theorem by using the appropriate sustitution.
- // When performing this operation, the conclusion of the fact must be temporarily removed from the premises of the theorem
- // to avoid buggy situations in case the fact is of the form p |- p;
- // - else add the premise to the premises of the theorem using weakening.
- val premCclAfterCclUnification: Formula = premAfterCclUnification.statement.right.head
-
- val updatedThmAfterWeakening: sp.Fact =
- premAfterCclUnification.statement.left.foldLeft(updatedThmAfterCclUnification)((updatedThmDuringWeakening, premPrem) => {
- if botNormalized.left.contains(premPrem) then
- lib.have(updatedThmDuringWeakening.statement +<< premPrem) by Weakening(updatedThmDuringWeakening)
- else
- searchPremises(updatedThmDuringWeakening.statement -<? premCclAfterCclUnification, premPrem) match
- case Some((fSubstDuringWeakening, tSubstDuringWeakening)) =>
- substitute(updatedThmDuringWeakening, fSubstDuringWeakening, tSubstDuringWeakening)
- case None =>
- lib.have(updatedThmDuringWeakening.statement +<< premPrem) by Weakening(updatedThmDuringWeakening)
- })
-
-
- // STEP 3.3 Use cut to apply the conclusion of the fact to the theorem
- // TODO: maybe throw a warning when the fact cannot be applied instead of making the proof crash
- val cutStep: sp.ProofTacticJudgement = Cut(premAfterCclUnification, updatedThmAfterWeakening)(updatedThmAfterWeakening.statement -<? premCclAfterCclUnification)
-
- if cutStep.isValid then
- lib.have(cutStep)
- else
- break(proof.InvalidProofTactic(s"The following argument could not be applied to the theorem\n${premAfterCclUnification.statement}"))
-
-
-
- // STEP 3.1 failed: the fact is dropped
- case None => updatedThm
-
- })
- }
-
- // STEP 4: If some cases, after all these operations, the theorem can remain too general to prove the sequent.
- // To avoid such situation, perform a last unification between the premises of the sequent and those
- // of the theorem.
- val thmAfterLastUnification: sp.Fact = botNormalized.left.foldLeft(thmAfterPrems)((updatedThm, premBot) => {
- searchPremises(updatedThm.statement, premBot) match
- case Some(fSubst, tSubst) => substitute(updatedThm, fSubst, tSubst)
+ infix def on(premises: Seq[proof.Fact], excluding: Iterable[Variable | VariableFormula] = Set())(bot: Sequent): proof.ProofTacticJudgement =
+
+ if thm == null then
+ proof.InvalidProofTactic("The theorem is null. Please check that it has been defined earlier in the proof.")
+ else if premises.exists(_ == null) then
+ proof.InvalidProofTactic("One of the premises is null. Please check that they all have been defined earlier in the proof.")
+ else
+ // STEP 0: Separate the variables and the variable formula in their respective sets
+ val (excludingTVars, excludingFVars) = excluding.foldLeft[(Set[Variable], Set[VariableFormula])](Set(), Set())((acc, v) => v match
+ case v: Variable => (acc._1 + v, acc._2)
+ case v: VariableFormula => (acc._1, acc._2 + v)
+ )
+
+ boundary{
+ TacticSubproof { sp ?=>
+
+ // STEP 1: Convert the given theorem, facts and sequent to their normal forms
+ val botNormalized: Sequent = normalForm(bot)
+ val thmNormalized: sp.Fact = lib.have(normalForm(thm.statement)) by Restate.from(thm)
+ val premisesNormalized = premises.map(p => lib.have(normalForm(p.statement)) by Restate.from(p))
+
+ // STEP 2: Unify the conclusion of the sequent the user want to prove and the conclusion
+ val thmAfterCclUnification: sp.Fact =
+ (botNormalized.right.isEmpty, thmNormalized.statement.right.isEmpty) match
+ case (true, true) => thmNormalized
+ case (true, false) => break(proof.InvalidProofTactic(s"The given theorem could not prove the sequent."))
+ case (false, true) => break(proof.InvalidProofTactic(s"The given theorem could not prove the sequent."))
+ case (false, false) =>
+ val botCcl: Formula = botNormalized.right.head
+ val thmCcl: Formula = thmNormalized.statement.right.head
+
+ matchFormula(botCcl, thmCcl, excludingTVars, excludingFVars) match
+ //Unification succeeded, subtitution can be performed
+ case Some((formulaCclAssignment, termCclAssignment)) => substitute(thmNormalized, formulaCclAssignment, termCclAssignment)
+ // STEP 2 failed
+ case None => break(proof.InvalidProofTactic(s"The conclusion of the goal and the theorem could not be unified."))
+
+ // STEP 3: Process each fact
+ val thmAfterPrems: sp.Fact = {
+
+ premisesNormalized.foldLeft(lib.have(thmAfterCclUnification))((updatedThm, premNormalized) => {
+
+
+ val premCcl: Formula = premNormalized.statement.right.head
+
+ // STEP 3.1: Unify the conclusion of the fact with a premise of the theorem
+ // Three possibilities:
+ // - the unification succeeded and the variables in the theorem are subtituted to match the conclusion of the fact;
+ // - if the unification did not succeeded, try the unification in the other direction, i.e. try to specify the fact
+ // instead of the theorem. If this works, make the susbtitution inside the fact;
+ // - both unifications do not succeed and the fact is dropped.
+ // TODO: add a warning when the fact is dropped
+ val conclusionsUnification: Option[(sp.Fact, sp.Fact)] =
+ searchPremises(updatedThm.statement, premCcl, excludingTVars, excludingFVars) match
+ case Some((fSubstAfterPrem, tSubstAfterPrem)) => Some((substitute(updatedThm, fSubstAfterPrem, tSubstAfterPrem), premNormalized))
+ case None =>
+ searchPremisesRev(updatedThm.statement, premCcl, excludingTVars, excludingFVars) match
+ case Some((fSubstAfterPrem, tSubstAfterPrem)) => Some((updatedThm, substitute(premNormalized, fSubstAfterPrem, tSubstAfterPrem)))
+ case None => None
+
+ conclusionsUnification match
+ case Some(updatedThmAfterCclUnification, premAfterCclUnification) =>
+
+ // STEP 3.2: For each premise of the fact:
+ // - check if it is in the sequent the user want to prove. If yes, add it to the preconditions of the theorem
+ // using weakening;
+ // - else if it matches one of the premises of the theorem specify the theorem by using the appropriate sustitution.
+ // When performing this operation, the conclusion of the fact must be temporarily removed from the premises of the theorem
+ // to avoid buggy situations in case the fact is of the form p |- p;
+ // - else add the premise to the premises of the theorem using weakening.
+ val premCclAfterCclUnification: Formula = premAfterCclUnification.statement.right.head
+
+ val updatedThmAfterWeakening: sp.Fact =
+ premAfterCclUnification.statement.left.foldLeft(updatedThmAfterCclUnification)((updatedThmDuringWeakening, premPrem) => {
+ if botNormalized.left.contains(premPrem) then
+ lib.have(updatedThmDuringWeakening.statement +<< premPrem) by Weakening(updatedThmDuringWeakening)
+ else
+ searchPremises(updatedThmDuringWeakening.statement -<? premCclAfterCclUnification, premPrem, excludingTVars, excludingFVars) match
+ case Some((fSubstDuringWeakening, tSubstDuringWeakening)) =>
+ substitute(updatedThmDuringWeakening, fSubstDuringWeakening, tSubstDuringWeakening)
+ case None =>
+ lib.have(updatedThmDuringWeakening.statement +<< premPrem) by Weakening(updatedThmDuringWeakening)
+ })
+
+
+ // STEP 3.3 Use cut to apply the conclusion of the fact to the theorem
+ // TODO: maybe throw a warning when the fact cannot be applied instead of making the proof crash
+ val cutStep: sp.ProofTacticJudgement = Cut(premAfterCclUnification, updatedThmAfterWeakening)(updatedThmAfterWeakening.statement -<? premCclAfterCclUnification)
+
+ if cutStep.isValid then
+ lib.have(cutStep)
+ else
+ break(proof.InvalidProofTactic(s"The following argument could not be applied to the theorem\n${premAfterCclUnification.statement} \n Deduced theorem: ${updatedThmAfterWeakening.statement}"))
+
+
+ // STEP 3.1 failed: the fact is dropped
case None => updatedThm
+
})
-
- // STEP 5: Prove the sequent using the theorem obtained with the previous steps. Weakening is necessary in case
- // additional preconditions that do not appear in the theorem are present in the sequent.
- val finalStep: sp.ProofTacticJudgement = Weakening(thmAfterLastUnification)(bot)
- if finalStep.isValid then
- lib.have(finalStep)
- else
- break(proof.InvalidProofTactic(s"The given theorem could not prove the sequent\n. Deduced theorem: ${thmAfterLastUnification.statement}"))
-
- // STEP 2 failed
- case None => break(proof.InvalidProofTactic(s"The conclusion of the goal and the theorem could not be unified."))
-
+ }
+
+ // STEP 4: If some cases, after all these operations, the theorem can remain too general to prove the sequent.
+ // To avoid such situation, perform a last unification between the premises of the sequent and those
+ // of the theorem.
+ val thmAfterLastUnification: sp.Fact = botNormalized.left.foldLeft(thmAfterPrems)((updatedThm, premBot) => {
+ searchPremises(updatedThm.statement, premBot, excludingTVars, excludingFVars) match
+ case Some(fSubst, tSubst) => substitute(updatedThm, fSubst, tSubst)
+ case None => updatedThm
+ })
+
+ // STEP 5: Prove the sequent using the theorem obtained with the previous steps. Weakening is necessary in case
+ // additional preconditions that do not appear in the theorem are present in the sequent.
+ val finalStep: sp.ProofTacticJudgement = Weakening(thmAfterLastUnification)(bot)
+ if finalStep.isValid then
+ lib.have(finalStep)
+ else
+ break(proof.InvalidProofTactic(s"The given theorem could not prove the sequent.\n Deduced theorem: ${thmAfterLastUnification.statement}\n Expected: ${bot}"))
+
+
+ }
}
-
}
/**
diff --git a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index 9430195a14705a74d000832a122f3cc707b9e963..c5b8e80a2cd9c2908dddbd36c43a3b6e1699dd5d 100644
--- a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -113,7 +113,7 @@ object CommonTactics {
case F.AppliedPredicate(F.`equality`, Seq(`x`, (y: F.Variable))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
y
- case F.AppliedPredicate(F.`equality`, List(F.AppliedFunction(y: F.Variable, _), F.AppliedFunction(`x`, _))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
+ case F.AppliedPredicate(F.`equality`, List(F.AppliedFunctional(y: F.Variable, _), F.AppliedFunctional(`x`, _))) if x != y && F.contains(uniquenessSeq.left, phi.substitute(x := y)) =>
y
} match {
case Some(y) => ExistenceAndUniqueness.withParameters(phi, x, y)(existence, uniqueness)(bot)
diff --git a/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala b/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
index 568110cd0a5c214913515185cfce390b5e223be9..e8d50cf0bbfc370007d0d5e1dc4a1e6ce865c423 100644
--- a/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/atp/Goeland.scala
@@ -1,18 +1,20 @@
package lisa.automation.atp
-import lisa.utils.tptp.*
-import ProofParser.*
-import KernelParser.*
-
-import lisa.prooflib.ProofTacticLib.*
import lisa.fol.FOL as F
import lisa.prooflib.Library
+import lisa.prooflib.OutputManager
+import lisa.prooflib.ProofTacticLib.*
import lisa.utils.K
+import lisa.utils.tptp.*
import java.io.*
-import sys.process._
import scala.io.Source
-import scala.util.{Try, Success, Failure}
-import lisa.prooflib.OutputManager
+import scala.util.Failure
+import scala.util.Success
+import scala.util.Try
+
+import ProofParser.*
+import KernelParser.*
+import sys.process._
/**
* Goéland is an automated theorem prover. This tactic calls the Goéland prover to solve the current sequent.
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
new file mode 100644
index 0000000000000000000000000000000000000000..850103caa9d80adacaeb8202a08a38684113cb9f
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/TypeSystem.scala
@@ -0,0 +1,535 @@
+package lisa.maths.settheory.types
+
+import lisa.prooflib.ProofTacticLib.*
+import lisa.fol.FOL
+import lisa.automation.Tautology
+import lisa.fol.FOL.{*, given}
+import lisa.prooflib.BasicStepTactic.*
+import lisa.prooflib.SimpleDeducedSteps.*
+import lisa.SetTheoryLibrary.{given, *}
+import lisa.SetTheoryLibrary
+import lisa.kernel.proof.SequentCalculus.SCProofStep
+import lisa.maths.settheory.SetTheory.functional
+import lisa.prooflib.OutputManager
+import lisa.maths.settheory.SetTheory.{singleton, app}
+
+object TypeLib extends lisa.Main {
+
+ import TypeSystem.*
+
+ val |=> : ConstantFunctionLabel[2] = ConstantFunctionLabel.infix("|=>", 2)
+ private inline def temp = |=>
+ extension (t:Term) {
+ def |=>(o:Term): Term = TypeLib.temp(t, o)
+ }
+ val app: ConstantFunctionLabel[2] = lisa.maths.settheory.SetTheory.app
+ addSymbol(|=>)
+
+ val f = variable
+ val x = variable
+ val y = variable
+ val z = variable
+ val A = variable
+ val B = variable
+ val F = function[1]
+ val funcspaceAxiom = Axiom(f ∈ (A |=> B) ==> (x ∈ A ==> app(f, x) ∈ B))
+ val any = DEF(x) --> top
+
+
+ // A |=> B is the set of functions from A to B
+ // C |> D is the functional class of functionals from the class C to the class D
+ // F is C |> D desugars into ∀(x, (x is C) => (F(x) is D))
+
+ val testTheorem = Theorem((x is A, f is (A |=> B), F is (A |=> B) |> (A |=> B) ) |- (F(f)*(x) is B)) {
+ have(thesis) by TypeChecker.prove
+ }
+
+ val 𝔹 = DEF() --> unorderedPair(∅, singleton(∅))
+
+ val empty_in_B = Theorem( (∅ :: 𝔹) ) {
+ have( ∅ :: unorderedPair(∅, singleton(∅))) by Tautology.from(pairAxiom of (z := ∅, x := ∅, y := singleton(∅)))
+ thenHave(thesis ) by Substitution.ApplyRules(𝔹.shortDefinition)
+ }
+
+ val sing_empty_in_B = Theorem( (singleton(∅) :: 𝔹) ) {
+ have( singleton(∅) :: unorderedPair(∅, singleton(∅))) by Tautology.from(pairAxiom of (z := singleton(∅), x := ∅, y := singleton(∅)))
+ thenHave(thesis ) by Substitution.ApplyRules(𝔹.shortDefinition)
+ }
+
+ val Zero = DEF() --> (∅.typedWith(𝔹)(empty_in_B), 𝔹)
+
+ val One = {
+ val One = DEF() --> singleton(∅)
+ val One_in_B = Theorem( (One :: 𝔹) ) {
+ have(thesis) by Substitution.ApplyRules(One.shortDefinition)(sing_empty_in_B)
+ }
+ One.typedWith(𝔹)(One_in_B)
+ }
+
+ val zero_in_B = Theorem( (Zero :: 𝔹) ) {
+ have( Zero :: 𝔹) by TypeChecker.prove
+ }
+
+
+}
+
+object TypeSystem {
+
+ import TypeLib.{
+ |=>, app, f, x, A, B, funcspaceAxiom, any, definition, given
+ }
+
+
+
+ type Class = Term | (Term**1 |-> Formula)
+
+ type SmallClass = Term
+
+ case class FunctionalClass(in: Seq[Class], args: Seq[Variable], out: Class, arity: Int) {
+ def formula[N <: Arity](f: (Term**N |-> Term)): Formula =
+ val inner = (args.zip(in.toSeq).map((term, typ) => (term is typ).asFormula).reduceLeft((a, b) => a /\ b)) ==> (f.applySeq(args) is out)
+ args.foldRight(inner)((v, form) => forall(v, form))
+
+ override def toString(): String = in.map(_.toStringSeparated()).mkString("(", ", ", ")") + " |> " + out.toStringSeparated()
+ }
+ object FunctionalClass {
+ def apply(in: Seq[Class], out: Class, arity: Int): FunctionalClass = FunctionalClass(in, Seq.empty, out, arity)
+ }
+
+ extension [N <: Arity](f: (Term**N |-> Term)) {
+ def is (typ: FunctionalClass): FunctionalTypeAssignment[N] & Formula = FunctionalTypeAssignment[N](f, typ).asInstanceOf
+ }
+
+ extension[A <: Class] (c: Class) {
+ //(1 to arity).map(i => freshVariable(in.toSeq :+ out, "%x" + i))
+ def |>(out: Class): FunctionalClass = FunctionalClass(Seq(c),Seq(freshVariable(Seq(out), "$x")), out, 1)
+ def |>(out: FunctionalClass): FunctionalClass =
+ val newVar = freshVariable(out.in.toSeq :+ out.out, "$x")
+ FunctionalClass(c +: out.in, newVar +: out.args, out.out, out.arity+1)
+ def toStringSeparated(): String = c match
+ case t: Term => t.toStringSeparated()
+ case f: (Term**1 |-> Formula) @unchecked => f.toString()
+ }
+
+ extension [A <: Class](t: Term) {
+ def is(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
+ def ::(clas:A): Formula with TypeAssignment[A] = TypeAssignment(t, clas).asInstanceOf[Formula with TypeAssignment[A]]
+ def @@(t2: Term): AppliedFunction = AppliedFunction(t, t2)
+ def *(t2: Term): AppliedFunction = AppliedFunction(t, t2)
+ }
+
+
+ object * {def unapply(t: Term): Option[(Term, Term)] = t match {
+ case AppliedFunction(f, a) => Some((f, a))
+ case app(f, a) => Some((f, a))
+ case _ => None
+ }}
+
+
+ /**
+ * A type assumption is a pair of a variable and a type.
+ * It is also a formula, equal to the type applied to the variable.
+ */
+ sealed trait TypeAssignment[A <: Class]{
+ this: Formula =>
+ val t: Term
+ val typ: A
+ val asFormula: Formula = this
+
+ override def toString() =
+ t.toStringSeparated() + "::" + typ.toStringSeparated()
+ override def toStringSeparated(): String = "(" + toString() + ")"
+ }
+ object TypeAssignment {
+
+ /**
+ * A type assumption is a pair of a variable and a type.
+ * It is also a formula, equal to the type applied to the variable.
+ */
+ def apply[A <: Class](t: Term, typ:A): TypeAssignment[A] =
+ val form = typ match
+ case f: Term => in(t, f)
+ case f : (Term**1 |-> Formula) @unchecked =>
+ ((f: Term**1 |-> Formula)(t): Formula)
+ form match
+ case f: VariableFormula =>
+ throw new IllegalArgumentException("Class formula cannot be a variable formula, as we require a type to have no free variable.")
+ case f: ConstantFormula => new TypeAssignmentConstant(t, typ, f)
+ case f: AppliedPredicate => new TypeAssignmentPredicate(t, typ, f)
+ case f: AppliedConnector => new TypeAssignmentConnector(t, typ, f)
+ case f: BinderFormula => new TypeAssignmentBinder(t, typ, f)
+
+ def unapply(ta: Formula): Option[(Term, Class)] = ta match
+ case ta: TypeAssignment[?] => Some((ta.t, ta.typ))
+ case in(x, set) => Some((x, set))
+ case AppliedPredicate(label, args) if label.arity == 1 => Some((args.head, label.asInstanceOf[Term**1 |-> Formula]))
+ case _ => None
+
+ }
+ val is = TypeAssignment
+
+ given [A <: Class]: Conversion[TypeAssignment[A], Formula] = _.asInstanceOf[Formula]
+ /*
+ given [A <: Class]: Conversion[TypeAssignment[A], Sequent] = ta => Sequent(Set.empty, Set(ta))
+ given [A <: Class]: FormulaSetConverter[TypeAssignment[A]] with {
+ override def apply(f: TypeAssignment[A]): Set[Formula] = Set(f.asInstanceOf[Formula])
+ }
+*/
+
+
+ private class TypeAssignmentConstant[A <: Class](val t: Term, val typ:A, formula: ConstantFormula) extends ConstantFormula(formula.id) with TypeAssignment[A]
+ private class TypeAssignmentPredicate[A <: Class](val t: Term, val typ:A, formula: AppliedPredicate) extends AppliedPredicate(formula.label, formula.args) with TypeAssignment[A] {
+
+ override def substituteUnsafe(map: Map[FOL.SchematicLabel[?], FOL.LisaObject[?]]): FOL.Formula =
+ if map.keySet.exists(_ == typ) then super.substituteUnsafe(map)
+ else
+ val newArgs = args.map(_.substituteUnsafe(map))
+ if newArgs == args then this else
+ val newTyp = (typ: LisaObject[?]).substituteUnsafe(map).asInstanceOf[A]
+
+ TypeAssignmentPredicate(t.substituteUnsafe(map), newTyp, formula.copy(args = newArgs))
+ }
+ private class TypeAssignmentConnector[A <: Class](val t: Term, val typ:A, formula: AppliedConnector) extends AppliedConnector(formula.label, formula.args) with TypeAssignment[A]
+ private class TypeAssignmentBinder[A <: Class](val t: Term, val typ:A, formula: BinderFormula) extends BinderFormula(formula.f, formula.bound, formula.body) with TypeAssignment[A]
+
+
+ type TypingContext = Iterable[TypeAssignment[?]]
+
+
+ sealed trait FunctionalTypeAssignment[N <: Arity]{
+ this: Formula =>
+ val functional: Term**N |-> Term
+ val typ: FunctionalClass
+ val asFormula: Formula = this
+
+
+ override def toString() = functional.toString() + " : " + typ.toString()
+ override def toStringSeparated(): String = "(" + toString + ")"
+
+ }
+ object FunctionalTypeAssignment {
+ def apply[N <: Arity](functional: Term**N |-> Term, typ: FunctionalClass): FunctionalTypeAssignment[N] =
+ val form = typ.formula(functional)
+ form match
+ case fo: VariableFormula =>
+ throw new IllegalArgumentException("Class formula cannot be a variable formula, as we require a type to have no free variable.")
+ case fo: ConstantFormula => new FunctionalTypeAssignmentConstant(functional, typ, fo)
+ case fo: AppliedPredicate => new FunctionalTypeAssignmentPredicate(functional, typ, fo)
+ case fo: AppliedConnector => new FunctionalTypeAssignmentConnector(functional, typ, fo)
+ case fo: BinderFormula => new FunctionalTypeAssignmentBinder(functional, typ, fo)
+
+ def unapply[N <: Arity](f: Formula): Option[((Term ** N) |-> Term, FunctionalClass)] =
+ f match
+ case ta: FunctionalTypeAssignment[N] => Some((ta.functional, ta.typ))
+ case _ => None
+ }
+ private class FunctionalTypeAssignmentConstant[N <: Arity](val functional: Term**N |-> Term, val typ: FunctionalClass, formula: ConstantFormula) extends ConstantFormula(formula.id) with FunctionalTypeAssignment[N]
+ private class FunctionalTypeAssignmentPredicate[N <: Arity](val functional: Term**N |-> Term, val typ: FunctionalClass, formula: AppliedPredicate) extends AppliedPredicate(formula.label, formula.args) with FunctionalTypeAssignment[N]
+ private class FunctionalTypeAssignmentConnector[N <: Arity](val functional: Term**N |-> Term, val typ: FunctionalClass, formula: AppliedConnector) extends AppliedConnector(formula.label, formula.args) with FunctionalTypeAssignment[N]
+ private class FunctionalTypeAssignmentBinder[N <: Arity](val functional: Term**N |-> Term, val typ: FunctionalClass, formula: BinderFormula) extends BinderFormula(formula.f, formula.bound, formula.body) with FunctionalTypeAssignment[N]
+
+
+
+
+
+ class TypedConstant[A <: Class]
+ (id: Identifier, val typ: A, val justif: JUSTIFICATION) extends Constant(id) with LisaObject[TypedConstant[A]] {
+ val formula = TypeAssignment(this, typ)
+ assert(justif.statement.left.isEmpty && (justif.statement.right.head == formula))
+
+ override def substituteUnsafe(map: Map[lisa.fol.FOL.SchematicLabel[?], lisa.fol.FOL.LisaObject[?]]): TypedConstant[A] = this
+ }
+
+ // Function Labels
+
+
+
+
+
+ class TypedConstantFunctional[N <: Arity](
+ id : Identifier,
+ arity: N,
+ val typ: FunctionalClass,
+ val justif: JUSTIFICATION
+ ) extends ConstantFunctionLabel[N](id, arity) with LisaObject[TypedConstantFunctional[N]] {
+
+ override def substituteUnsafe(map: Map[lisa.fol.FOL.SchematicLabel[?], lisa.fol.FOL.LisaObject[?]]): TypedConstantFunctional[N] = this
+ }
+
+
+
+
+
+ class AppliedFunction(val func: Term, val arg: Term) extends AppliedFunctional(app, Seq(func, arg)) with LisaObject[AppliedFunction] {
+
+ override def substituteUnsafe(map: Map[lisa.fol.FOL.SchematicLabel[?], lisa.fol.FOL.LisaObject[?]]): AppliedFunction = AppliedFunction(func.substituteUnsafe(map), arg.substituteUnsafe(map))
+
+ override def toString(): String =
+ func match
+ case AppliedFunction(af @ AppliedFunctional(label, args), t1) if label.id.name == "=:=" =>
+ s"(${t1.toStringSeparated()} =:=_${args.head.toStringSeparated()} ${arg.toStringSeparated()})"
+ case _ =>
+ func.toStringSeparated() + "*(" + arg.toStringSeparated() + ")"
+ override def toStringSeparated(): String = toString()
+ }
+ object AppliedFunction {
+ def unapply(af: AppliedFunctional): Option[(Term, Term)] = af match
+ case AppliedFunctional(label, Seq(func, arg)) if label == app => Some((func, arg))
+ case _ => None
+ }
+
+
+
+ ///////////////////////
+ ///// Definitions /////
+ ///////////////////////
+
+
+ class TypedSimpleConstantDefinition[A <: Class](using om: OutputManager)(fullName: String, line: Int, file: String)(
+ val expression: Term,
+ out: Variable,
+ j: JUSTIFICATION,
+ val typ:A
+ ) extends SimpleFunctionDefinition[0](fullName, line, file)(lambda[Term, Term](Seq[Variable](), expression).asInstanceOf, out, j) {
+ val typingName = "typing_" + fullName
+ val typingJudgement = THM( label :: typ, typingName, line, file, InternalStatement)({
+ have(expression :: typ) by TypeChecker.prove
+ thenHave(thesis) by lisa.automation.Substitution.ApplyRules(getShortDefinition(label).get)
+ })
+ val typedLabel: TypedConstant[A] = TypedConstant(label.id, typ, typingJudgement)
+
+
+ }
+ object TypedSimpleConstantDefinition {
+ def apply[A <: Class](using om: OutputManager)(fullName: String, line: Int, file: String)(expression: Term, typ:A): TypedSimpleConstantDefinition[A] = {
+ val intName = "definition_" + fullName
+ val out = Variable(freshId(expression.allSchematicLabels.map(_.id), "y"))
+ val defThm = THM(ExistsOne(out, out === expression), intName, line, file, InternalStatement)({
+ have(lisa.prooflib.SimpleDeducedSteps.simpleFunctionDefinition(lambda(Seq[Variable](), expression), out))
+ })
+ new TypedSimpleConstantDefinition(fullName, line, file)(expression, out, defThm, typ)
+ }
+ }
+ extension (d: definitionWithVars[0]) {
+ inline infix def -->[A<:Class](
+ using om: OutputManager, name: sourcecode.FullName, line: sourcecode.Line, file: sourcecode.File)(term:Term, typ: A): TypedConstant[A] =
+ TypedSimpleConstantDefinition[A](name.value, line.value, file.value)(term, typ).typedLabel
+ }
+
+ extension (c: Constant) {
+ def typedWith[A <: Class](typ:A)(justif: JUSTIFICATION) : TypedConstant[A] =
+ if justif.statement.right.size != 1 || justif.statement.left.size != 0 || !K.isSame((c is typ).asFormula.underlying, justif.statement.right.head.underlying) then
+ throw new IllegalArgumentException(s"A proof of typing of $c must be of the form ${c :: typ}, but the given justification shows ${justif.statement}.")
+ else TypedConstant(c.id, typ, justif)
+ }
+
+
+
+
+
+
+
+
+ /////////////////////////
+ ///// Type Checking /////
+ /////////////////////////
+
+ object TypeChecker extends ProofTactic {
+ private val x = variable
+
+ class TypingException(val msg: String) extends Exception(msg)
+
+ def prove(using proof: SetTheoryLibrary.Proof)(bot:lisa.fol.FOL.Sequent): proof.ProofTacticJudgement =
+ val context = bot.left
+ var success: proof.ProofTacticJudgement = null
+ var typingError: proof.ProofTacticJudgement = null
+ bot.right.find(goal =>
+ goal match
+ case (term is typ) =>
+ val ptj = typecheck(using SetTheoryLibrary)(context.toSeq, term, Some(typ))
+ if ptj.isValid then
+ success = ptj
+ true
+ else
+ typingError = ptj
+ false
+ case _ => false
+ )
+ if success != null then success else if typingError != null then typingError else proof.InvalidProofTactic("The right hand side of the goal must be a typing judgement")
+
+ private def fullFlat(context: Seq[Formula]): Seq[Formula] = context.flatMap{
+ case AppliedConnector(And, cunj) => fullFlat(cunj)
+ case f => Seq(f)
+ }
+
+ def typecheck(using lib: SetTheoryLibrary.type, proof: lib.Proof)(context: Seq[Formula], term:Term, typ: Option[Class]): proof.ProofTacticJudgement =
+ val typingAssumptions: Map[Term, Seq[Class]] = fullFlat(context).collect{
+ case TypeAssignment(term, typ) => (term, typ)
+ }.groupBy(_._1).map((t, l) => (t, l.map(_._2)))
+
+ val functionalTypingAssumptions: Map[(? |-> Term), Seq[FunctionalClass]] = context.collect{
+ case FunctionalTypeAssignment(func, typ) => (func, typ)
+ }.groupBy(_._1).map((func, l) => (func, l.map(_._2)))
+
+ TacticSubproof {
+ context.foreach(assume(_))
+ try {
+
+ def innerTypecheck(context2: Map[Term, Seq[Class]], term:Term, typ:Option[Class]): Class= {
+ val possibleTypes = typingAssumptions.getOrElse(term, Nil)
+ if typ == Some(any) then
+ have(term is any) by Restate.from(TypeLib.any.definition of (x := term))
+ any
+ else if typ.isEmpty && possibleTypes.size >=1 then
+ have(term is possibleTypes.head) by Restate
+ possibleTypes.head
+ else if (typ.nonEmpty && possibleTypes.contains(typ.get)) then
+ have(term is typ.get) by Restate
+ typ.get
+ else term match
+ case tc: TypedConstant[?] =>
+ if typ.isEmpty then
+ have(tc is tc.typ) by Restate.from(tc.justif)
+ tc.typ
+ else if K.isSame((tc is typ.get).asFormula.underlying, (tc is tc.typ).asFormula.underlying) then
+ have(tc is typ.get) by Restate.from(tc.justif)
+ typ.get
+ else throw TypingException("Constant " + tc + " expected to be of type " + typ + " but has type " + tc.typ + ".")
+
+ case AppliedFunction(func, arg) =>
+ val funcType = innerTypecheck(context2, func, None)
+ val funcProof = lastStep
+ val argType = innerTypecheck(context2, arg, None)
+ val argProof = lastStep
+ funcType match
+ case inType |=> outType => typ match
+ case None =>
+ if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
+ have(term is outType) by Tautology.from(
+ funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
+ funcProof,
+ argProof
+ )
+ outType
+ else throw
+ TypingException("Function " + func + " found to have type " + funcType + ", but argument " + arg + " has type " + argType + " instead of expected " + inType + ".")
+ case Some(typ) if K.isSame((term is typ).asFormula.underlying, (term is outType).asFormula.underlying) =>
+ if K.isSame((arg is inType).asFormula.underlying, (arg is argType).asFormula.underlying) then
+ have(term is outType) by Tautology.from(
+ funcspaceAxiom of (f := func, x := arg, A:= inType, B:= outType),
+ funcProof,
+ argProof
+ )
+ typ
+ else
+ throw TypingException("Function " + func + " found to have type " + funcType + ", but argument " + arg + " has type " + argType + " instead of expected " + inType + ".")
+
+ case _ =>
+ throw TypingException("Function " + func + " expected to have function type ? |=> " + typ + ", but has type " + funcType + ". ")
+ case _ =>
+ throw TypingException("Function " + func + " expected to have function type ? |=> " + typ + ", but has type " + funcType + ". Note that terms having multiple different types is only partialy supported.")
+
+ case AppliedFunctional(label, args) =>
+ val (argTypes, argTypesProofs) = args.map(arg =>
+ try (innerTypecheck(context2, arg, None), lastStep)
+ catch
+ case e: TypingException => (any, any.definition of (x := arg)) //if no type could be constructed the normal way, we give it "any"
+ ).unzip
+ val labelTypes = label match
+ case label: TypedConstantFunctional[?] =>
+ (label.typ, () => label.justif) +:
+ functionalTypingAssumptions.getOrElse(label, Nil).map(fc => (fc, () => (have( fc.formula(label.asInstanceOf) ) by Restate) ))
+
+ case _ => functionalTypingAssumptions.getOrElse(label, Nil).map(fc => (fc, () => have( fc.formula(label.asInstanceOf) ) by Restate ))
+ functionalTypingAssumptions.get(label)
+ if labelTypes.isEmpty then
+ throw TypingException("Function " + label + " expected to have type (" + argTypes.mkString(", ") + ") |=> ? but is untyped.")
+ else
+ typ match
+ case None =>
+ labelTypes.find((labelType, step) =>
+ labelType.arity == args.size &&
+ (args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) =>
+ K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying) //
+ )
+ ) match
+ case None =>
+ throw TypingException("Function " + label + " expected to have type (" + argTypes.mkString(", ") + ") |=> ? but is assigned " + labelTypes.mkString(" & ") + ". Note that terms having multiple different types is only partialy supported.")
+ case Some(labelType, step) =>
+ val out: Class = labelType.out
+
+ val in: Seq[Class] = labelType.in.toSeq
+ //val labelProp = labelType.formula(label.asInstanceOf)
+ val labelPropStatement = step()
+ val labInst = labelPropStatement.of(args: _*)
+ val subst = (labelType.args zip args).map((v, a) => (v := a))
+ val newOut: Class = out match {
+ case t: Term => t.substitute(subst: _*)
+ case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+ }
+ have(term is newOut) by Tautology.from(
+ (argTypesProofs :+ labInst ) : _*
+ )
+ newOut
+ case Some(typValue) =>
+ labelTypes.find((labelType, step) =>
+ labelType.arity == args.size &&
+ (args zip argTypes).zip(labelType.in.toSeq).forall((argAndTypes, inType) =>
+ K.isSame((argAndTypes._1 is inType).asFormula.underlying, (argAndTypes._1 is argAndTypes._2).asFormula.underlying)
+ ) && {
+ val subst = (labelType.args zip args).map((v, a) => (v := a))
+ val newOut: Class = labelType.out match {
+ case t: Term => t.substitute(subst: _*)
+ case f: (Term**1 |-> Formula) @unchecked => f.substitute(subst: _*)
+ }
+ K.isSame((term is newOut).asFormula.underlying, (term is typValue).asFormula.underlying)
+
+ }
+ ) match
+ case None =>
+ throw TypingException("Function " + label + " expected to have type (" + argTypes.mkString(", ") + ") |=> " + typValue + " but is assigned " + labelTypes.mkString(" & ") + ". Note that terms having multiple different types is only partialy supported.")
+ case Some(labelType, step) =>
+ val out: Class = labelType.out
+ val in: Seq[Class] = labelType.in.toSeq
+ //val labelProp = labelType.formula(label.asInstanceOf)
+ val labelPropStatement = step()
+ have(term is typValue) by Tautology.from(
+ (argTypesProofs :+ labelPropStatement.of(args: _*) ) : _*
+ )
+ typValue
+
+ case v: Variable =>
+ if possibleTypes.isEmpty then
+ throw TypingException("Variable " + v + " expected to be of type " + typ + " but is untyped.")
+ else throw TypingException("Variable " + v + " expected to be of type " + typ + " but is assigned " + possibleTypes.mkString(" & ") + ".")
+
+ case c: Constant =>
+ if possibleTypes.isEmpty then
+ throw TypingException("Constant " + c + " expected to be of type " + typ + " but is untyped.")
+ else throw TypingException("Constant " + c + " expected to be of type " + typ + " but is assigned " + possibleTypes.mkString(" & ") + ".")
+
+ case _: AppliedFunctional =>
+ throw Exception("Why is this not handled by the previous case? Scala reports an incomplete match")
+
+ }
+ innerTypecheck(typingAssumptions, term, typ)
+ }
+ catch {
+ case e: TypingException =>
+ return proof.InvalidProofTactic(e.msg)
+ }
+ }
+
+
+ }
+
+
+
+
+
+
+
+
+
+
+}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
new file mode 100644
index 0000000000000000000000000000000000000000..df6d157e3b4d0ce6cc2ed20d0eda85c935942e7d
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Frontend.scala
@@ -0,0 +1,566 @@
+package lisa.maths.settheory.types.adt
+
+/**
+ * This object provides a DSL for defining algebraic data types (ADTs) and functions over ADT in Lisa.
+ * For usage examples, please refer to the documentation of the package or the reference manual.
+ */
+object ADTSyntax {
+
+ import ADTDefinitions.*
+ import lisa.maths.settheory.SetTheory.{*, given}
+
+ /**
+ * Builder for defining a constructor specification.
+ *
+ * @param param the parameters of the constructor
+ */
+ case class ConstructorBuilder (private val param: Seq[ConstructorArgument]) {
+
+ /**
+ * The number of arguments the constructor takes
+ */
+ def size: Int = param.length
+
+ /**
+ * Merges the parameters of two constructors.
+ *
+ * @param b the other constructor
+ */
+ infix def ++(b: ConstructorBuilder): ConstructorBuilder = ConstructorBuilder(param ++ b.param.toSeq)
+
+ /**
+ * Converts this constructor into an ADT with a single constructor.
+ */
+ def toADTBuilder = ADTBuilder(Seq(this))
+
+ /**
+ * Combines two constructors into an ADT.
+ *
+ * @param b the other constructor
+ */
+ infix def |(b: ConstructorBuilder): ADTBuilder = this | b.toADTBuilder
+
+ /**
+ * Adds this constructor to an ADT.
+ *
+ * @param b the ADT to which the constructor is added
+ */
+ infix def |(b: ADTBuilder): ADTBuilder = toADTBuilder | b
+
+ /**
+ * Outputs the [[UntypedConstructor]] associated with this builder.
+ *
+ * @param name the name of the constructor
+ */
+ def build(variables1: Seq[Variable], variables2: Seq[Variable]): SyntacticConstructor = SyntacticConstructor(param, variables1, variables2)
+ }
+
+ /**
+ * Companion object for the [[ConstructorBuilder]] class.
+ */
+ object ConstructorBuilder {
+
+ /**
+ * Creates an empty [[ConstructorBuilder]].
+ */
+ def empty: ConstructorBuilder = ConstructorBuilder(Seq.empty)
+ }
+
+ trait ConstructorConverter[T] {
+
+ /**
+ * Converts a value into a [[ConstructorBuilder]].
+ */
+ def apply(t: T): ConstructorBuilder
+ }
+
+ /**
+ * Converts a value into a [[ConstructorBuilder]].
+ *
+ * @param any the value to convert
+ * @param c the converter that is used for the conversion
+ */
+ private def any_to_const[T](any: T)(using c: ConstructorConverter[T]): ConstructorBuilder = c(any)
+
+ given unit_to_const: ConstructorConverter[Unit] with {
+
+ /**
+ * Converts a unit value into a constructor taking no arguments.
+ */
+ override def apply(u: Unit): ConstructorBuilder = ConstructorBuilder.empty
+ }
+
+ given empty_to_const: ConstructorConverter[EmptyTuple] with {
+
+ /**
+ * Converts an empty tuple into a constructor taking no arguments.
+ */
+ override def apply(t: EmptyTuple): ConstructorBuilder = ConstructorBuilder.empty
+ }
+
+ given term_to_const[T <: Term]: ConstructorConverter[T] with {
+
+ /**
+ * Converts a term into a constructor taking one non inductive argument.
+ */
+ override def apply(t: T): ConstructorBuilder = ConstructorBuilder(Seq(GroundType(t)))
+ }
+
+ given adt_to_const[N <: Arity]: ConstructorConverter[ADT[N]] with {
+
+ /**
+ * Converts an ADT into a constructor taking one inductive argument.
+ */
+ override def apply(a: ADT[N]): ConstructorBuilder = ConstructorBuilder(Seq(Self))
+ }
+
+ given adt_tuple_to_const[N <: Arity, T <: Tuple](using ConstructorConverter[T]): ConstructorConverter[ADT[N] *: T] with {
+
+ /**
+ * Converts a tuple prepended with a type into a constructor taking an argument and whose other arguments are deduced from
+ * applying recursively the conversion to the tuple.
+ */
+ override def apply(t: ADT[N] *: T): ConstructorBuilder =
+ any_to_const(t.head) ++ any_to_const(t.tail)
+ }
+
+
+ given term_tuple_to_const[H <: Term, T <: Tuple](using ConstructorConverter[T]): ConstructorConverter[H *: T] with {
+
+ /**
+ * Converts a tuple prepended with a type into a constructor taking an argument and whose other arguments are deduced from
+ * applying recursively the conversion to the tuple.
+ */
+ override def apply(t: H *: T): ConstructorBuilder =
+ any_to_const(t.head) ++ any_to_const(t.tail)
+ }
+
+ extension [T1](left: T1)(using c1: ConstructorConverter[T1])
+ /**
+ * Converts two values into constructors and combines them into an ADT.
+ *
+ * @param right the other value to convert
+ * @param c2 the implicit converter for the second value
+ */
+ infix def |[T2](right: T2)(using c2: ConstructorConverter[T2]): ADTBuilder = any_to_const(left) | any_to_const(right)
+
+ /**
+ * Builder for defining ADT specifications.
+ *
+ * @param constructors the builders for each constructor of the ADT.
+ */
+ case class ADTBuilder (private val constructors: Seq[ConstructorBuilder]) {
+
+ /**
+ * The number of constructors in the ADT.
+ */
+ def size: Int = constructors.length
+
+ /**
+ * Combines this ADT with another one.
+ *
+ * @param b the other ADT
+ */
+ infix def |(b: ADTBuilder): ADTBuilder = ADTBuilder(constructors ++ b.constructors)
+
+ /**
+ * Adds a constructor to this ADT.
+ *
+ * @param b the constructor to add
+ */
+ infix def |(b: ConstructorBuilder): ADTBuilder = this | b.toADTBuilder
+
+ /**
+ * Converts a value into a constructor and adds it to this ADT.
+ *
+ * @param t the value to convert
+ * @param c the implicit converter
+ */
+ infix def |[T](t: T)(using c: ConstructorConverter[T]): ADTBuilder = this | any_to_const(t)
+
+ /**
+ * Outputs the corresponding ADT and its constructors.
+ *
+ * @tparam N the number of type variables appearing in the specification of the ADT
+ * @param typeVariables the type variables of the ADT
+ * @param names the names of the constructors and of the ADT
+ */
+ def build[N <: Arity](typeVariables: Variable ** N, names: Seq[String]): (ADT[N], constructors[N]) =
+
+ val trimmedNames = (if size == 0 then names else names.tail).take(size + 1)
+ require(
+ trimmedNames.length == constructors.length + 1,
+ s"The number of new identifiers for constructors must match the given specification.\nNew identifiers: ${names.length - 1}, number of constructors: ${constructors.length}."
+ )
+
+ val typeVarsSet = typeVariables.toSeq.toSet
+ val syntacticCons = constructors.map(c =>
+ c.build(Helpers.chooseVars("x", c.size, typeVarsSet), Helpers.chooseVars("y", c.size, typeVarsSet))
+ )
+ val syntacticADT = SyntacticADT[N](trimmedNames.head, syntacticCons, typeVariables)
+ val semanticCons = trimmedNames.tail.zip(syntacticCons).map(SemanticConstructor(_, _, syntacticADT))
+ val semanticADT = SemanticADT[N](syntacticADT, semanticCons)
+ val cons = semanticCons.map(Constructor(_))
+ (ADT[N](semanticADT, cons), new constructors[N](cons : _*))
+
+ }
+
+ /**
+ * Companion object for the [[ADTBuilder]] class.
+ */
+ object ADTBuilder {
+
+ /**
+ * Creates an empty [[ADTBuilder]].
+ */
+ def empty: ADTBuilder = ADTBuilder(Seq.empty)
+
+ /**
+ * Creates an empty [[ADTBuilder]].
+ */
+ def | = empty
+ }
+
+ /**
+ * Builder for defining polymorphic ADT specifications.
+ *
+ * @tparam N the number of type variables of the ADT
+ * @param typeVariable the type variables of the ADT
+ * @param specification the builder for ADT
+ */
+ case class PolymorphicADTBuilder[N <: Arity](typeVariables: Variable ** N, specification: ADTBuilder) {
+
+ /**
+ * Outputs the corresponding ADT and its constructors.
+ *
+ * @param names the names of the constructors and of the ADT
+ */
+ def build(names: Seq[String]) = specification.build(typeVariables, names)
+
+ /**
+ * Adds a constructor to the ADT specification
+ *
+ * @param b the builder of the constructor
+ */
+ def | (b: ConstructorBuilder): PolymorphicADTBuilder[N] = PolymorphicADTBuilder(typeVariables, specification | b)
+
+ /**
+ * Adds a constructor to the ADT specification
+ *
+ * @param t the value to be converted into a constructor
+ */
+ def |[T] (t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[N] = | (any_to_const(t))
+ }
+
+ // Syntactic sugar for polymorphic ADT Builders
+
+ extension (u: Unit)
+ def --> (builder: ADTBuilder): PolymorphicADTBuilder[0] = PolymorphicADTBuilder[0](**(), builder)
+ def --> (builder: ConstructorBuilder): PolymorphicADTBuilder[0] = --> (builder.toADTBuilder)
+ def -->[T](t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[0] = --> (any_to_const(t))
+
+ extension (v: Variable)
+ def --> (builder: ADTBuilder): PolymorphicADTBuilder[1] = PolymorphicADTBuilder[1](**(v), builder)
+ def --> (builder: ConstructorBuilder): PolymorphicADTBuilder[1] = --> (builder.toADTBuilder)
+ def -->[T](t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[1] = --> (any_to_const(t))
+
+ extension (v: (Variable, Variable))
+ def --> (builder: ADTBuilder): PolymorphicADTBuilder[2] = PolymorphicADTBuilder[2](**(v._1, v._2), builder)
+ def --> (builder: ConstructorBuilder): PolymorphicADTBuilder[2] = --> (builder.toADTBuilder)
+ def -->[T](t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[2] = --> (any_to_const(t))
+
+ extension (v: (Variable, Variable, Variable))
+ def --> (builder: ADTBuilder): PolymorphicADTBuilder[3] = PolymorphicADTBuilder[3](**(v._1, v._2, v._3), builder)
+ def --> (builder: ConstructorBuilder): PolymorphicADTBuilder[3] = --> (builder.toADTBuilder)
+ def -->[T](t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[3] = --> (any_to_const(t))
+
+ extension (v: (Variable, Variable, Variable, Variable))
+ def --> (builder: ADTBuilder): PolymorphicADTBuilder[4] = PolymorphicADTBuilder[4](**(v._1, v._2, v._3, v._4), builder)
+ def --> (builder: ConstructorBuilder): PolymorphicADTBuilder[4] = --> (builder.toADTBuilder)
+ def -->[T](t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[4] = --> (any_to_const(t))
+
+ extension (v: (Variable, Variable, Variable, Variable, Variable))
+ def --> (builder: ADTBuilder): PolymorphicADTBuilder[5] = PolymorphicADTBuilder[5](**(v._1, v._2, v._3, v._4, v._5), builder)
+ def --> (builder: ConstructorBuilder): PolymorphicADTBuilder[5] = --> (builder.toADTBuilder)
+ def -->[T](t: T)(using ConstructorConverter[T]): PolymorphicADTBuilder[5] = --> (any_to_const(t))
+
+
+ /**
+ * Lists all constructors of this ADT.
+ */
+ case class constructors[N <: Arity](cons: Constructor[N]*)
+
+ /**
+ * Companion object for the [[constructors]] class.
+ */
+ object constructors {
+ def unapplySeq[N <: Arity](adt: ADT[N]): Seq[Constructor[N]] = adt.constructors
+ }
+
+ /**
+ * Contains useful macros for ADT UI
+ */
+ object Macro {
+ import scala.quoted._
+
+ /**
+ * Extract all the scala identifiers defined in the same line or after an expression.
+ *
+ * @param e the expression around which the names are extracted
+ */
+ inline def extractNames[T](e: T): Seq[String] = ${extractNames('{e})}
+
+ /**
+ * Macro implementing [[this.extractNames]].
+ *
+ * @param e the quoted expression around which the names are extracted
+ */
+ private def extractNames[T](using Quotes)(e: Expr[T]) : Expr[Seq[String]] =
+
+ import quotes.reflect._
+
+
+ val subscope = Symbol.spliceOwner.owner.owner.owner
+ val scope = subscope.owner
+ val tree = scope.tree
+
+ case class traverser(s: Symbol) extends TreeTraverser {
+ var reachedADT: Boolean = false
+ var constructorNames: Seq[String] = Seq.empty[String]
+
+ override def traverseTree(tree: Tree)(owner: Symbol): Unit = tree match
+ case v : ValDef =>
+ if !reachedADT then
+ if v.symbol == s then
+ constructorNames = constructorNames :+ v.symbol.name
+ reachedADT = true
+ else
+ constructorNames = constructorNames :+ v.symbol.name
+
+ super.traverseTree(tree)(owner)
+ case _ => super.traverseTree(tree)(owner)
+ }
+
+ val trav = traverser(subscope)
+ trav.traverseTree(tree)(scope)
+ Expr(trav.constructorNames)
+ }
+
+ /**
+ * Syntax to define Algebraic Data Types
+ */
+ object define {
+ /**
+ * Extracts the constructors from an ADT.
+ *
+ * @param adt the ADT
+ * @return a tuple containing the ADT and its constructors
+ */
+ private def extractConstructors[N <: Arity](adt: ADT[N]): (ADT[N], constructors[N]) = (adt, constructors(adt.constructors : _*))
+
+ /**
+ * Outputs a polymorphic ADT and constructors from a user specification
+ * Needs to be inline in order to fetch the name of the ADT and the constructor.
+ *
+ * @param builder the builder user for specifying the ADT
+ */
+ inline def unapply[N <: Arity](builder: PolymorphicADTBuilder[N]): (ADT[N], constructors[N]) = builder.build(Macro.extractNames(builder))
+
+ /**
+ * Outputs a (non polymorphic) ADT and constructors from a user specification.
+ * Needs to be inline in order to fetch the name of the ADT and the constructor.
+ *
+ * @param builder the builder user for specifying the ADT
+ */
+ inline def unapply(builder: ADTBuilder): (ADT[0], constructors[0]) = unapply[0](() --> builder)
+
+ /**
+ * Returns an ADT containing only one constructor out of a user specification.
+ * Needs to be inline in order to fetch the name of the ADT and the constructor.
+ *
+ * @param builder the builder of the unique constructor of the ADT
+ */
+ private inline def unapply(builder: ConstructorBuilder): (ADT[0], constructors[0]) = unapply(builder.toADTBuilder)
+
+ /**
+ * Returns an ADT isomorphic to a given type. It has only one constructor taking as only argument an element of
+ * the provided type.
+ * Needs to be inline in order to fetch the name of the ADT and the constructor.
+ *
+ * @param t type given by the user
+ */
+ inline def unapply(t: Term): (ADT[0], constructors[0]) = unapply(term_to_const(t))
+
+ /**
+ * Returns the unit type. This is an ADT containing only one value and hence having only one
+ * constructor (non-inductive and taking no arguments).
+ * Needs to be inline in order to fetch the name of the ADT and the constructor.
+ *
+ * @param u user specification indicating that they want to generate the unit type
+ */
+ inline def unapply(u: Unit): (ADT[0], constructors[0]) = unapply(unit_to_const(u))
+
+ /**
+ * Returns a product type (also known as tuple). This is an ADT containing only one constructor.
+ * Generally its arguments are non inductive as the opposite would lead to the empty type.
+ * Needs to be inline in order to fetch the name of the ADT and the constructor.
+ *
+ * @param t user specification of the tuple
+ */
+ inline def unapply[N <: Arity, T <: Tuple](t: (ADT[N] | Term) *: T)(using ConstructorConverter[T]): (ADT[0], constructors[0]) =
+ t.head match
+ case a: ADT[N] => unapply(adt_tuple_to_const(a *: t.tail))
+ case term: Term => unapply(any_to_const(term *: t.tail))
+ }
+
+ /**
+ * Converts an ADT with no type variables into a term.
+ */
+ given adt_to_term: Conversion[ADT[0], Term] = _.applyUnsafe(**())
+
+ /**
+ * Converts a function over an ADT with no type variables into a term (i.e a set function).
+ */
+ given fun_to_term: Conversion[ADTFunction[0], Term] = _.applyUnsafe(**())
+
+ /**
+ * Converts a constructor with no type variables into a term (i.e a set function).
+ */
+ given constructor_to_term: Conversion[Constructor[0], Term] = _.applyUnsafe(**())
+
+ /**
+ * Mutable data structure that registers the patterns that have been filled inside a pattern matching syntax.
+ *
+ * @tparam N the type variables of the ADT
+ * @param comp the complementary information stored in the builder
+ */
+ class CaseBuilder[N <: Arity, T, R](val comp : R) {
+
+ /**
+ * The underlying mutable map between patterns and the body of the corresponding cases. For each
+ * patterns stores the variables that have been used to represent its arguments.
+ *
+ */
+ private val underlying = scala.collection.mutable.Map[Constructor[N], (Seq[Variable], T)]()
+
+ /**
+ * Adds a case to the pattern matching
+ *
+ * @param cons the pattern / constructor
+ * @param value the value next to the variables that are used for the pattern's arguments
+ */
+ def += (cons: Constructor[N], value: (Seq[Variable], T)) = underlying += (cons -> value)
+
+ /**
+ * Checks if the cases of a pattern matching are valid. Specifically, it checks that:
+ * - All constructors are covered
+ * - There are no extra cases
+ * - The number of variables provided by the user matches the arity of the constructor
+ *
+ * @param adt the ADT over which the pattern matching is performed
+ * @return an error message if the pattern matching is invalid, None otherwise
+ */
+ def isValid(adt: ADT[N]): Option[String] =
+ val constructors = adt.constructors.toSet
+ val casesConstructors = underlying.keySet.toSet
+
+ val constructorsMinusCases = constructors -- casesConstructors
+ val casesMinusConstructors = casesConstructors -- constructors
+
+ // STEP 1: Check that all constructors are covered
+ if !constructorsMinusCases.isEmpty then
+ Some(s"Case for ${constructorsMinusCases.head.name} is missing.")
+ // STEP 2: Check that there are no extra cases
+ else if !casesMinusConstructors.isEmpty then
+ Some(s"${casesMinusConstructors.head.name} is not a constructor of ${adt.name}.")
+ else
+ underlying.keys.foldLeft[Option[String]](None)((acc, c) =>
+ val vars = underlying(c)._1.toSet
+ // STEP 3: Check that for each case the number of variables provided by the user matches the arity of the constructor
+ acc.orElse(Some(s"Case ${c.name}: ${vars.size} variables were provided whereas the arity of ${c.name} is ${c.arity}.").filter(_ => vars.size != c.underlying.arity))
+ )
+
+ /**
+ * Outputs an immutable map out of the underlying mutable one
+ */
+ def build: Map[Constructor[N], (Seq[Variable], T)] = underlying.toMap
+ }
+
+ /**
+ * Case of a a pattern matching syntax
+ *
+ * @param cons the pattern / constructor
+ * @param vars variables that are used to represent the arguments of the constructor
+ */
+ case class Case[N <: Arity](cons: Constructor[N], vars: Variable*) {
+
+ /**
+ * Used in the context of an induction proof. Adds the subproof corresponding to this case into a builder.
+ *
+ * @see [[Induction]]
+ *
+ * @param proof the outer scope of the induction proof
+ * @param line the line at which this case is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which this case is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param builder the builder of the induction proof
+ * @param subproof the proof of the case (possibly using the induction hypothesis)
+ */
+ def subproof (using proof: Proof, line: sourcecode.Line, file: sourcecode.File, builder: CaseBuilder[N, proof.ProofStep, (Sequent, Seq[Term], Variable)])(subproof: proof.InnerProof ?=> Unit): Unit =
+ val (bot, args, adtVar) = builder.comp
+ val prop = bot.right.head
+ val consTerm = appSeq(cons.underlying.term(args))(vars)
+ val subst = adtVar -> consTerm
+
+ val assumptions =
+ (wellTypedSet(cons.underlying.semanticSignature(vars).map(p => (p._1, p._2.substitute(cons.underlying.typeVariablesSeq.zip(args).map(SubstPair(_, _)) : _*))))
+ ++
+ cons.underlying.syntacticSignature(vars).filter(_._2 == Self).map((v, _) => prop.substitute(adtVar -> v)))
+
+ //val botWithAssumptions = bot.substitute(subst) ++ ((assumptions ++ proof.getAssumptions) |- ())
+ val botWithAssumptions = bot.substitute(subst) ++ (assumptions |- ())
+
+
+
+ val iProof: proof.InnerProof = new proof.InnerProof(Some(botWithAssumptions))
+ subproof(using iProof)
+ val proofStep = (new SUBPROOF(using proof)(None)(iProof)).judgement.validate(line, file).asInstanceOf[proof.ProofStep]
+
+ def subproofWithExtraStep: proof.ProofTacticJudgement = TacticSubproof{ ip ?=>
+ val fullSeq = Tautology(using lisa.SetTheoryLibrary, ip)(proofStep)(botWithAssumptions)
+ if fullSeq.isValid then
+ fullSeq.validate(line, file)
+ else
+ return proof.InvalidProofTactic(s"Proof of case ${cons.name} is invalid.\nExpected: ${botWithAssumptions}.")
+ }
+
+ builder += (cons, (vars, subproofWithExtraStep.validate(line, file)))
+
+ /**
+ * Used in the context of a function definition. Adds the body of the case to a builder.
+ *
+ * @param body the body of this case
+ * @param builder the builder for the function definition
+ */
+ def apply(body : Term)(using builder: CaseBuilder[N, Term, Unit]) = builder += (cons, (vars, body))
+ }
+
+ /**
+ * Defines a function over an ADT
+ *
+ * @param adt the domain of this function
+ * @param returnType the return type of this function
+ * @param name the name of this functions
+ * @param cases the definition of the function for each constructor
+ */
+ def fun[N <: Arity](adt: ADT[N], returnType: Term)(using name: sourcecode.Name)(cases: CaseBuilder[N, Term, Unit] ?=> Unit): ADTFunction[N] = {
+ val builder = CaseBuilder[N, Term, Unit](())
+ cases(using builder)
+ builder.isValid(adt) match
+ case None =>
+ ADTFunction(SemanticFunction[N](name.value, adt.underlying, builder.build.map((k, v) => (k.underlying, v)), returnType), adt)
+ case Some(msg) => throw IllegalArgumentException(msg)
+ }
+
+}
\ No newline at end of file
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Functions.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Functions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..0c67f2ea1710a2a2fc9118c35fa516741b988cd1
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Functions.scala
@@ -0,0 +1,134 @@
+/**
+ * Defines set theoretic functions over Algebraic Data Types
+ */
+
+package lisa.maths.settheory.types.adt
+
+import lisa.maths.settheory.SetTheory.{_, given}
+import lisa.maths.settheory.types.TypeLib.|=>
+import lisa.maths.settheory.types.TypeSystem.::
+import lisa.maths.settheory.types.TypeSystem._
+
+import ADTDefinitions.*
+import Helpers.*
+import Helpers.{/\, ===, \/}
+
+/**
+ * Set theoretic interpretation of a function over an ADT.
+ *
+ * @tparam N the number of type variables of the domain of this function
+ * @param name the name of this function
+ * @param adt the domain of this function
+ * @param cases the body of this function for each constructor
+ * @param returnType the codomain of this function
+ * @param line the line at which this function is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which this function is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ */
+class SemanticFunction[N <: Arity](name: String, adt: SemanticADT[N], cases: Map[SemanticConstructor[N], (Seq[Variable], Term)], returnType: Term)(using line: sourcecode.Line, file: sourcecode.File) {
+
+ /**
+ * Map binding each constructor to a theorem stating that the case is well typed.
+ */
+ private val checkReturnType: Map[SemanticConstructor[N], THM] =
+ (for c <- cases.keys yield
+ val (vars, body) = cases(c)
+ c -> Lemma(wellTyped(c.semanticSignature(vars)) |- body :: returnType) {
+ have(thesis) by TypeChecker.prove
+ }
+ ).toMap
+
+ /**
+ * Type variables appearing in this function's domain.
+ */
+ val typeVariables: Variable ** N = adt.typeVariables
+
+ /**
+ * Sequence of type variables appearing in this function's domain.
+ */
+ val typeVariablesSeq: Seq[Variable] = adt.typeVariablesSeq
+
+ /**
+ * Number of type variables appearing in this function.
+ */
+ val typeArity: N = adt.typeArity
+
+ /**
+ * Full name of this function. That is the name of the function prefixed by the name of the ADT.
+ */
+ val fullName = s"$name"
+ // val fullName = s"${adt.name}/$name"
+
+ val typ = adt.term |=> returnType
+
+ /**
+ * Definition of this function.
+ *
+ * Formally it is the only function whose domain is the ADT and such that for each constructor c f * (c * x1 * ... * xn) = case(c, x1, ..., xn)
+ */
+ private val untypedDefinition = (f :: typ) /\ simplify(/\(cases.map((c, caseDef) =>
+ val (vars, body) = caseDef
+ forallSeq(vars, wellTypedFormula(c.semanticSignature(vars)) ==> (f * c.appliedTerm(vars) === body))
+ )))
+
+ /**
+ * Lemma --- Uniqueness of this function.
+ */
+ private val uniqueness = Axiom(existsOne(f, untypedDefinition))
+
+ /**
+ * Set theoretic definition of the constructor.
+ */
+ private val classFunction = FunctionDefinition(fullName, line.value, file.value)(typeVariablesSeq, f, untypedDefinition, uniqueness).label
+
+ /**
+ * Identifier of this function.
+ */
+ val id: Identifier = classFunction.id
+
+
+ /**
+ * Function where type variables are instantiated with schematic symbols.
+ */
+ val term = classFunction.applySeq(typeVariablesSeq)
+
+ /**
+ * Lemma --- The body of this function correpsonds to the cases provided by the user.
+ *
+ * `for each constructor c, ∀x1, ..., xn. f * (c * x1 * ... * xn) = case(c, x1, ..., xn)`
+ */
+ val shortDefinition = cases.map((c, caseDef) =>
+ val (vars, body) = caseDef
+ c -> Lemma(simplify(wellTypedFormula(c.semanticSignature(vars))) ==> (term * c.appliedTerm(vars) === body)) {
+ have(forall(f, (term === f) <=> untypedDefinition)) by Exact(classFunction.definition)
+ thenHave((term === term) <=> (term :: typ) /\ (/\(cases.map((c, caseDef) => {
+ val (vars, body) = caseDef
+ forallSeq(vars, wellTypedFormula(c.semanticSignature(vars)) ==> (term * c.appliedTerm(vars) === body))
+ })))) by InstantiateForall(term)
+ thenHave(forallSeq(vars, wellTypedFormula(c.semanticSignature(vars)) ==> (term * c.appliedTerm(vars) === body))) by Weakening
+ vars.foldLeft(lastStep)((l, _) =>
+ lastStep.statement.right.head match
+ case Forall(v, phi) => thenHave(phi) by InstantiateForall(v)
+ case _ => throw UnreachableException
+ )
+ }
+ )
+
+ /**
+ * Lemma --- Introduction rule
+ *
+ * `f : ADT -> T`
+ *
+ * where `T` is the return type of this function
+ */
+ val intro = Lemma(forallSeq(typeVariablesSeq, term :: typ)) {
+ have(forall(f, (term === f) <=> untypedDefinition)) by Exact(classFunction.definition)
+ thenHave((term === term) <=> (term :: typ) /\ (/\(cases.map((c, caseDef) => {
+ val (vars, body) = caseDef
+ forallSeq(vars, /\(wellTyped(c.semanticSignature(vars))) ==> (term * c.appliedTerm(vars) === body))
+ })))) by InstantiateForall(term)
+ thenHave(term :: typ) by Weakening
+ thenHave(thesis) by QuantifiersIntro(typeVariablesSeq)
+ }
+}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5830f1aab2e5cdf4acd0c20726ff0bae21e083ad
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Helpers.scala
@@ -0,0 +1,1030 @@
+package lisa.maths.settheory.types.adt
+
+/**
+ * Tactic that proves every goal of the form:
+ *
+ * ` ... |- ..., ∀x1, ..., xn. P(x), ...`
+ *
+ * ` ..., ∀x1, ..., xn . P(x), ... |- ...`
+ *
+ * ` ... |- ..., ∃x1, ..., xn. P(x), ...`
+ *
+ * ` ..., ∃x1, ..., xn . P(x), ... |- ...`
+ *
+ * given a proof of the sequents without quantification.
+ */
+object QuantifiersIntro extends lisa.prooflib.ProofTacticLib.ProofTactic {
+
+ import lisa.prooflib.SimpleDeducedSteps.Restate
+ import lisa.prooflib.BasicStepTactic.*
+ import lisa.fol.FOL.*
+
+ /**
+ * Executes the tactic on a specific goal.
+ *
+ * @param lib the library that is currently being used
+ * @param proof the ongoing proof in which the tactic is called
+ * @param vars the variables that needs to be quantified
+ * @param fact the proof of the sequent without quantification
+ * @param bot the statement to prove
+ */
+ def apply(using lib: lisa.prooflib.Library, proof: lib.Proof)(vars: Seq[Variable])(fact: proof.Fact)(bot: Sequent): proof.ProofTacticJudgement =
+ TacticSubproof { sp ?=>
+ if vars.isEmpty then
+ lib.have(bot) by Restate.from(fact)
+ else
+ val diff: Sequent = bot -- fact.statement
+
+ diff match
+ case Sequent(s, _) if s.size == 1 =>
+ val diffRest = bot.left -- s
+ val f = s.head
+ val fWithoutQuant = (fact.statement.left -- diffRest).head
+ f match
+ case BinderFormula(Forall, _, _) =>
+ vars.foldRight[(sp.Fact, Formula)](fact, fWithoutQuant)( (v, acc) =>
+ val (accFact, accFormula) = acc
+ val newFormula = forall(v, accFormula)
+ (lib.have(diffRest + newFormula |- bot.right) by LeftForall(accFact), newFormula)
+ )
+ case BinderFormula(Exists, _, _) =>
+ vars.foldRight[(sp.Fact, Formula)](fact, fWithoutQuant)( (v, acc) =>
+ val (accFact, accFormula) = acc
+ val newFormula = exists(v, accFormula)
+ (lib.have(diffRest + newFormula |- bot.right) by LeftExists(accFact), newFormula)
+ )
+ case _ => return proof.InvalidProofTactic(s"The formula that changed is not quantified: $f.")
+ case Sequent(_, s) if s.size == 1 =>
+ val diffRest = bot.right -- s
+ val f = s.head
+ val fWithoutQuant = (fact.statement.right -- diffRest).head
+ f match
+ case BinderFormula(Forall, _, _) =>
+ vars.foldRight[(sp.Fact, Formula)](fact, fWithoutQuant)( (v, acc) =>
+ val (accFact, accFormula) = acc
+ val newFormula = forall(v, accFormula)
+ (lib.have(bot.left |- diffRest + newFormula) by RightForall(accFact), newFormula)
+ )
+ case BinderFormula(Exists, _, _) =>
+ vars.foldRight[(sp.Fact, Formula)](fact, fWithoutQuant)( (v, acc) =>
+ val (accFact, accFormula) = acc
+ val newFormula = exists(v, accFormula)
+ (lib.have(bot.left |- diffRest + newFormula) by RightExists(accFact), newFormula)
+ )
+ case _ => return proof.InvalidProofTactic(s"The formula that changed is not quantified: $f.")
+ case Sequent(s1, s2) if s1.isEmpty && s2.isEmpty => lib.have(bot) by Restate.from(fact)
+ case _ => return proof.InvalidProofTactic("Two or more formulas in the sequent have changed.")
+
+
+ }
+}
+
+/**
+ * General purpose helpers.
+ */
+private [adt] object Helpers {
+
+ import lisa.fol.FOL.{*, given}
+
+ /**
+ * Benchmarks a block of code.
+ *
+ * @param name the name of the benchmark
+ * @param f the block of code to benchmark
+ * @return the result of the block of code and prints how long it took to execute
+ */
+ def benchmark[T](name: String)(f: => T): T = {
+ val before = System.nanoTime
+
+ val res = f
+
+ val totalTime = (System.nanoTime - before) / 1000000
+
+ println(s"$name time: $totalTime ms")
+
+ res
+ }
+
+ /**
+ * Exception thrown when code that should not be accessed is reached.
+ */
+ object UnreachableException extends Exception("This code should not be accessed. If you see this message, please report it to the library maintainers.")
+
+ // *********************
+ // * FIRST ORDER LOGIC *
+ // *********************
+
+ val a = variable
+ val b = variable
+ val c = variable
+ val d = variable
+
+ val f = variable
+ val g = variable
+ val h = variable
+
+ val n = variable
+ val m = variable
+
+ val p = formulaVariable
+ val p1 = formulaVariable
+ val p2 = formulaVariable
+ val p3 = formulaVariable
+ val p4 = formulaVariable
+
+ val q1 = formulaVariable
+ val q2 = formulaVariable
+
+ val r = variable
+ val s = variable
+ val t = variable
+
+ val x = variable
+ val y = variable
+ val z = variable
+
+ val Q = predicate[1]
+ val P = predicate[1]
+ val P2 = predicate[2]
+ val schemPred = predicate[1]
+
+ /**
+ * Formula representing whether two sequences of terms are pairwise equal.
+ *
+ * @param s2 the sequence to compare with
+ */
+ extension (s1: Seq[Term]) def ===(s2: Seq[Term]): Formula = /\(s1.zip(s2).map(_ === _))
+
+ /**
+ * Disjunction of a sequence of formulas.
+ *
+ * @param s the formulas to which the disjunction is applied
+ */
+ def \/(s: Iterable[Formula]): Formula =
+ if s.isEmpty then False
+ else s.fold(False)(_ \/ _)
+
+ /**
+ * Conjunction of a sequence of formulas.
+ *
+ * @param s the formulas to which the conjunction is applied
+ */
+ def /\(s: Iterable[Formula]): Formula =
+ if s.isEmpty then True
+ else s.fold(True)(_ /\ _)
+
+ /**
+ * Repeats existential quantification over a sequence of variables.
+ *
+ * @param vars the variables to quantify over
+ * @param f the formula to which the quantifiers are applied
+ * @return the quantified formula
+ */
+ def existsSeq(vars: Seq[Variable], f: Formula): Formula =
+ vars.foldRight(f)(exists(_, _))
+
+ /**
+ * Repeats universal quantification over a sequence of variables.
+ *
+ * @param vars the variables to quantify over
+ * @param f the formula to which the quantifiers are applied
+ * @return the quantified formula
+ */
+ def forallSeq(vars: Seq[Variable], f: Formula): Formula =
+ vars.foldRight(f)(forall(_, _))
+
+ /**
+ * Simplifies a formula by removing True and False constants.
+ *
+ * @param f the formula to simplify
+ */
+ def simplify(f: Formula): Formula =
+ f match
+ case Or(False, phi) => simplify(phi)
+ case Or(phi, False) => simplify(phi)
+ case Or(phi, psi) => simplify(phi) \/ simplify(psi)
+ case And(True, phi) => simplify(phi)
+ case And(phi, True) => simplify(phi)
+ case And(phi, psi) => simplify(phi) /\ simplify(psi)
+ case Implies(True, phi) => simplify(phi)
+ case Implies(phi, psi) => Implies(simplify(phi), simplify(psi))
+ case _ => f
+
+
+ /**
+ * Picks fresh variables starting with a given prefix .
+ *
+ * @param prefix the prefix of the fresh variables
+ * @param size the number of fresh variables to output
+ * @param assigned the variables that are already used
+ * @param counter the index to append to the prefix
+ * @param acc the variables that have already been generated by this method
+ *
+ */
+ def chooseVars(prefix: String, size: Int, assigned: Set[Variable] = Set.empty, counter: Int = 0, acc: Seq[Variable] = Seq.empty): Seq[Variable] =
+ if size == 0 then
+ acc
+ else
+ val newVar = Variable(s"${prefix}${counter}")
+ if assigned.contains(newVar) then
+ chooseVars(prefix, size, assigned, counter + 1, acc)
+ else
+ chooseVars(prefix, size - 1, assigned, counter + 1, acc :+ newVar)
+
+
+}
+
+/**
+ * Definitions and helper functions for ADT.
+ */
+private[adt] object ADTDefinitions {
+
+ import lisa.maths.settheory.SetTheory.*
+ import lisa.maths.settheory.types.TypeSystem.*
+ import Helpers.{/\}
+
+ /**
+ * The specification of a constructor can either contain terms or a self reference, i.e. a reference to the ADT itself.
+ */
+ trait ConstructorArgument {
+ /**
+ * Returns the term associated to a constructor argument, or in case it is a self reference, returns the term associated to the ADT.
+ *
+ * @param arg the constructor argument
+ * @param adt the term representing the ADT
+ */
+ def getOrElse(adt: Term): Term =
+ this match {
+ case Self => adt
+ case GroundType(term) => term
+ }
+
+ /**
+ * Substitutes the type variables of a constructor argument.
+ */
+ def substitute(p: SubstPair*): ConstructorArgument =
+ this match
+ case Self => Self
+ case GroundType(t) => GroundType(t.substitute(p : _*))
+ }
+
+ /**
+ * A symbol for self reference
+ */
+ case object Self extends ConstructorArgument
+
+ /**
+ * Syntactic represenation of a term
+ *
+ * @param t the underlying term
+ */
+ case class GroundType(t: Term) extends ConstructorArgument
+
+ /**
+ * Shorthand for the union of the range of a function.
+ *
+ * @param f the function
+ */
+ def unionRange(f: Term) = union(relationRange(f))
+
+ /**
+ * Shorthand for the range of a restricted function.
+ *
+ * @param f the function
+ * @param n the domain to which the function is restricted
+ */
+ def restrRange(f: Term, n: Term) = relationRange(restrictedFunction(f, n))
+
+ /**
+ * Applies a sequence of arguments to a function.
+ *
+ * @param f the function
+ * @param args the arguments to apply
+ */
+ def appSeq(f: Term)(args: Seq[Term]): Term = args.foldLeft(f)(_ * _)
+
+ /**
+ * Converts an integer to the associated ordinal.
+ *
+ * @param n the integer to convert
+ */
+ def toTerm(n: Int): Term =
+ require(n >= 0, "n must be a non-negative integer")
+ if n == 0 then emptySet
+ else successor(toTerm(n - 1))
+
+ /**
+ * Returns a sequence of formulas asserting that all terms of a sequence are well-typed.
+ *
+ * @param s the terms and their respective types
+ */
+ def wellTyped(s: Seq[(Term, Term)]): Seq[Formula] = s.map(_ :: _)
+
+ /**
+ * Returns a sequence of formulas asserting that all terms of a sequence are well-typed with respect to the
+ * specification of a constructor.
+ *
+ * @param s the terms and their respective type
+ * @param orElse the term to use in case of a self reference
+ */
+ def wellTyped(s: Seq[(Term, ConstructorArgument)])(orElse: Term): Seq[Formula] = s.map((t, arg) => t :: arg.getOrElse(orElse))
+
+ /**
+ * Returns a set of formulas asserting that all terms of a sequence are well-typed.
+ *
+ * @param s the terms and their respective types
+ */
+ def wellTypedSet(s: Seq[(Term, Term)]): Set[Formula] = wellTyped(s).toSet
+
+ /**
+ * Returns a set of formulas asserting that all terms of a sequence are well-typed with respect to the
+ * specification of a constructor.
+ *
+ * @param s the terms and their respective type
+ * @param orElse the term to use in case of a self reference
+ */
+ def wellTypedSet(s: Seq[(Term, ConstructorArgument)])(orElse: Term): Set[Formula] = wellTyped(s)(orElse).toSet
+
+ /**
+ * Returns a formula asserting that all terms of a sequence are well-typed.
+ *
+ * @param s the terms and their respective types
+ */
+ def wellTypedFormula(s: Seq[(Term, Term)]): Formula = /\ (wellTyped(s))
+
+ /**
+ * Returns a formula asserting that all terms of a sequence are well-typed with respect to the
+ * specification of a constructor.
+ *
+ * @param s the terms and their respective type
+ * @param orElse the term to use in case of a self reference
+ */
+ def wellTypedFormula(s: Seq[(Term, ConstructorArgument)])(orElse: Term): Formula = /\ (wellTyped(s)(orElse))
+
+}
+
+
+/**
+ * List of external set theoretic theorems needed for proofs about ADT.
+ * Some of these theorems are not yet implemented in the library and
+ * will be added in the future.
+ */
+private [adt] object ADTHelperTheorems {
+
+ import lisa.maths.settheory.SetTheory.{*, given}
+ import lisa.maths.Quantifiers.{existentialEquivalenceDistribution, equalityInExistentialQuantifier,
+ existentialConjunctionWithClosedFormula, equalityTransitivity}
+ import ADTDefinitions.*
+ import Helpers.*
+ //import lisa.maths.Quantifiers.*
+
+ // TODO: Remove
+ val pair = ConstantFunctionLabel("pair", 2)
+ addSymbol(pair)
+
+ val pairExtensionality = Lemma((pair(a, b) === pair(c, d)) <=> ((a === c) /\ (b === d))) {
+ sorry
+ }
+
+ // *********************
+ // * FIRST ORDER LOGIC *
+ // *********************
+
+
+ /**
+ * Lemma --- Alternative statement of transitivity of equality.
+ */
+ val altEqualityTransitivity = Lemma((x === y, y === z) |- x === z) {
+ have(thesis) by Restate.from(equalityTransitivity)
+ }
+
+ /**
+ * Lemma --- Transitivity of equivalence.
+ */
+ val equivalenceRewriting = Lemma((p1 <=> p2, p2 <=> p3) |- p1 <=> p3) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- Modus ponens for equivalence.
+ */
+ val equivalenceApply = Lemma((p1 <=> p2, p1) |- p2) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- Top level existential quantifiers can be swapped.
+ */
+ val existentialSwap = Lemma(∃(x, ∃(y, P2(x, y))) <=> ∃(y, ∃(x, P2(x, y)))) {
+ have(thesis) by Tableau
+ }
+
+ /**
+ * Lemma --- Modus ponens for reversed equivalence.
+ */
+ val equivalenceRevApply = Lemma((p2 <=> p1, p1) |- p2) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- If a statement is equivalent to the conjunction of two other statements, and one of them is true, then it can be removed from the equivalence.
+ */
+ val equivalenceAnd = Lemma((p2, p1 <=> (p2 /\ p3)) |- p1 <=> p3) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- If two formulas are equivalent then adding a disjunction on their right side preserves the equivalence.
+ */
+ val rightAndEquivalence = Lemma(p1 <=> p2 |- (p1 /\ p) <=> (p2 /\ p)) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- If two formulas are equivalent then adding an implication on their left side preserves the equivalence.
+ */
+ val impliesEquivalence = Lemma((p1 <=> p2, p3 <=> p4) |- (p1 ==> p3) <=> (p2 ==> p4)) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- If two formulas are equivalent then adding an implication on their left side preserves the equivalence.
+ */
+ val leftImpliesEquivalenceWeak = Lemma(p1 <=> p2 |- (p ==> p1) <=> (p ==> p2)) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- Implication distributes over equivalence.
+ */
+ val leftImpliesEquivalenceStrong = Lemma(p ==> (p1 <=> p2) |- (p ==> p1) <=> (p ==> p2)) {
+ have(thesis) by Tautology
+ }
+
+ /**
+ * Lemma --- If there exists a unique element satisfying a predicate, then all
+ * other elements satisfying the predicate are equal to it.
+ */
+ val existsOneUniqueness = Lemma((∃!(x, P(x)), P(x), P(y)) |- x === y) {
+ sorry
+ }
+
+ // *******************
+ // * NATURAL NUMBERS *
+ // *******************
+
+ // Natural numbers
+ val N = Constant("N")
+ addSymbol(N)
+
+ /**
+ * Lemma --- 0 is a natural number.
+ *
+ * `0 ∈ N`
+ */
+ val zeroIsNat = Lemma(in(emptySet, N)) {
+ sorry
+ }
+
+ /**
+ * Lemma --- The natural numbers are not empty.
+ *
+ * `N != ∅`
+ */
+ val natNotEmpty = Lemma(!(N === emptySet)) {
+ have(thesis) by Cut(zeroIsNat, setWithElementNonEmpty of (y := emptySet, x := N))
+ }
+
+ /**
+ * Lemma --- There exists a natural number.
+ *
+ * `∃n ∈ N`
+ */
+ val existsNat = Lemma(exists(n, in(n, N))) {
+ have(thesis) by RightExists(zeroIsNat)
+ }
+
+ /**
+ * Lemma --- Successor is an injective function.
+ *
+ * `n = m <=> n + 1 = m + 1`
+ */
+ val successorInjectivity = Lemma((n === m) <=> (successor(n) === successor(m))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- A term is a natural number if and only if its successor is a natural number.
+ *
+ * `n ∈ N <=> n + 1 ∈ N`
+ */
+ val successorIsNat = Lemma(in(n, N) <=> in(successor(n), N)) {
+ sorry
+ }
+
+ /**
+ * Lemma --- Any number is smaller than its successor
+ *
+ * `∀n ∈ N. n < n + 1`
+ */
+ val inSuccessor = Lemma(in(n, successor(n))) {
+ val uniomAxiomForward = have(exists(y, in(y, unorderedPair(n, singleton(n))) /\ in(n, y)) |- in(n, union(unorderedPair(n, singleton(n))))) by Cut(
+ unionAxiom of (x := unorderedPair(n, singleton(n)), z := n),
+ equivalenceRevApply of (p1 := exists(y, in(y, unorderedPair(n, singleton(n))) /\ in(n, y)), p2 := in(n, union(unorderedPair(n, singleton(n)))))
+ )
+ have(in(singleton(n), unorderedPair(n, singleton(n))) /\ in(n, singleton(n))) by RightAnd(
+ secondElemInPair of (x := n, y := singleton(n)),
+ singletonHasNoExtraElements of (x := n, y := n)
+ )
+ thenHave(exists(y, in(y, unorderedPair(n, singleton(n))) /\ in(n, y))) by RightExists
+ have(in(n, union(unorderedPair(n, singleton(n))))) by Cut(lastStep, uniomAxiomForward)
+ thenHave(union(unorderedPair(n, singleton(n))) === successor(n) |- in(n, successor(n))) by RightSubstEq.withParametersSimple(
+ List((union(unorderedPair(n, singleton(n))), successor(n))),
+ lambda(s, in(n, s))
+ )
+ have(thesis) by Cut(successor.shortDefinition of (x := n), lastStep)
+ }
+
+ /**
+ * Lemma --- 0 is not the successor of any natural number.
+ *
+ * `∀n ∈ N. n + 1 != 0`
+ */
+ val zeroIsNotSucc = Lemma(!(successor(n) === emptySet)) {
+ have(thesis) by Cut(inSuccessor, setWithElementNonEmpty of (y := n, x := successor(n)))
+ }
+
+ /**
+ * Lemma --- A number is smaller or equal than another number if and only if it is strictly smaller than its successor.
+ *
+ * `m <= n <=> m < n + 1`
+ */
+ val natSubset = Lemma(in(n, N) |- subset(m, n) <=> in(m, successor(n))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- The intersection of a natural number with the set of natural numbers is the number itself.
+ *
+ * `n ∩ N = n`
+ */
+ val intersectionNat = Lemma(in(n, N) |- setIntersection(n, N) === n) {
+ sorry
+ }
+
+ /**
+ * Lemma --- If a number is smaller or equal than a natural number, then it is also a natural number.
+ *
+ * `m <= n, n ∈ N |- m ∈ N`
+ */
+ val subsetIsNat = Lemma(subset(a, b) |- in(b, N) ==> in(a, N)) {
+ sorry
+ }
+
+ /**
+ * Lemma --- Induction principle for natural numbers
+ *
+ * `P(0), ∀n ∈ N. P(n) => P(n + 1) |- ∀n ∈ N. P(n)`
+ */
+ val natInduction = Lemma((P(emptySet), forall(m, in(m, N) ==> (P(m) ==> P(successor(m))))) |- forall(n, in(n, N) ==> P(n))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- Every number is smaller or equal than its successor.
+ *
+ * `n <= n + 1`
+ */
+ val subsetSuccessor = Lemma(subset(n, successor(n))) {
+ have(setUnion(n, singleton(n)) === union(unorderedPair(n, singleton(n))) |- subset(n, union(unorderedPair(n, singleton(n))))) by RightSubstEq.withParametersSimple(
+ List((setUnion(n, singleton(n)), union(unorderedPair(n, singleton(n))))),
+ lambda(s, subset(n, s))
+ )(unionSubsetFirst of (a := n, b := singleton(n)))
+ have(subset(n, union(unorderedPair(n, singleton(n))))) by Cut(setUnion.shortDefinition of (x := n, y := singleton(n)), lastStep)
+ thenHave(successor(n) === union(unorderedPair(n, singleton(n))) |- subset(n, successor(n))) by RightSubstEq.withParametersSimple(
+ List((successor(n), union(unorderedPair(n, singleton(n))))),
+ lambda(s, subset(n, s))
+ )
+ have(thesis) by Cut(successor.shortDefinition of (x := n), lastStep)
+ }
+
+ // *************
+ // * FUNCTIONS *
+ // *************
+
+ /**
+ * Lemma --- Range introduction and elimination rules. If en element is in the image of a function, then it has a preimage inside its domain.
+ *
+ * `functional(f) |- y ⊆ Im(f) <=> ∃x ∈ Dom(f). f(x) = y`
+ */
+ val functionRangeMembership = Lemma(functional(f) |- in(y, relationRange(f)) <=> ∃(x, in(x, relationDomain(f)) /\ (app(f, x) === y))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- The restriction of a function is still a function.
+ *
+ * `functional(f) |- functional(f|x)`
+ */
+ val functionalRestrictedFunction = Lemma(functional(f) |- functional(restrictedFunction(f, x))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- If an element is in the image of a restricted function, then it has a preimage inside its domain.
+ *
+ * `functional(f) |- y ⊆ Im(f) <=> ∃x ∈ d ∩ Dom(f). f|d(x) = y`
+ */
+ val restrictedFunctionRangeMembership = Lemma(functional(f) |- in(y, relationRange(restrictedFunction(f, d))) <=> ∃(x, in(x, d ∩ relationDomain(f)) /\ (app(restrictedFunction(f, d), x) === y))) {
+ have(functional(f) |- in(y, relationRange(restrictedFunction(f, d))) <=> ∃(x, in(x, relationDomain(restrictedFunction(f, d))) /\ (app(restrictedFunction(f, d), x) === y))) by Cut(
+ functionalRestrictedFunction of (x := d),
+ functionRangeMembership of (f := restrictedFunction(f, d))
+ )
+ thenHave(functional(f) |- in(y, relationRange(restrictedFunction(f, d))) <=> ∃(x, in(x, d ∩ relationDomain(f)) /\ (app(restrictedFunction(f, d), x) === y))) by Substitution.ApplyRules(
+ restrictedFunctionDomain of (x := d)
+ )
+ }
+
+ /**
+ * Lemma --- Characterization of the union of the range of a function.
+ *
+ * `∪ Im(h) = {z | ∃n ∈ Dom(h). z ∈ h(n)}`
+ */
+ val unionRangeMembership = Lemma(functional(h) |- in(z, unionRange(h)) <=> exists(n, in(n, relationDomain(h)) /\ in(z, app(h, n)))) {
+ val iffAfterAnd = have(functional(h) |- (y ∈ relationRange(h) /\ z ∈ y) <=> ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y)) /\ z ∈ y) by Cut(
+ functionRangeMembership of (f := h),
+ rightAndEquivalence of (p1 := y ∈ relationRange(h), p2 := ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y)), p := z ∈ y)
+ )
+ have(functional(h) |- (y ∈ relationRange(h) /\ z ∈ y) <=> ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y)) by Apply(equivalenceRewriting).on(
+ iffAfterAnd,
+ existentialConjunctionWithClosedFormula of (P := lambda(m, m ∈ relationDomain(h) /\ (app(h, m) === y)), p := z ∈ y)
+ )
+
+ thenHave(functional(h) |- ∀(y, (y ∈ relationRange(h) /\ z ∈ y) <=> ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y))) by RightForall
+
+ val beforeExSwap = have(functional(h) |- ∃(y, y ∈ relationRange(h) /\ z ∈ y) <=> ∃(y, ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y))) by Cut(
+ lastStep,
+ existentialEquivalenceDistribution of (
+ P := lambda(y, y ∈ relationRange(h) /\ z ∈ y),
+ Q := lambda(y, ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y))
+ )
+ )
+
+ have(∃(y, ∃(m, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y)) <=> ∃(m, ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)))) subproof {
+
+ have(m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y <=> m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)) by Restate
+ thenHave(forall(y, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y <=> m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y))) by RightForall
+ have(∃(y, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y) <=> ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y))) by Cut(
+ lastStep,
+ existentialEquivalenceDistribution of (
+ P := lambda(y, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y),
+ Q := lambda(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y))
+ )
+ )
+ thenHave(forall(m, ∃(y, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y) <=> ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)))) by RightForall
+ have(∃(m, ∃(y, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y)) <=> ∃(m, ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)))) by Cut(
+ lastStep,
+ existentialEquivalenceDistribution of (
+ P := lambda(y, ∃(y, m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y)),
+ Q := lambda(y, ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)))
+ )
+ )
+ have(thesis) by Apply(equivalenceRewriting).on(lastStep, existentialSwap of (P2 := lambda((y, m), m ∈ relationDomain(h) /\ (app(h, m) === y) /\ z ∈ y)))
+ }
+
+ val introM =
+ have(functional(h) |- ∃(y, y ∈ relationRange(h) /\ z ∈ y) <=> ∃(m, ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)))) by Apply(equivalenceRewriting).on(beforeExSwap, lastStep)
+
+ have(
+ ∀(m, (∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y))) <=> (m ∈ relationDomain(h) /\ z ∈ app(h, m)))
+ ) by RightForall(equalityInExistentialQuantifier of (P := lambda(y, m ∈ relationDomain(h) /\ z ∈ y), y := app(h, m)))
+
+ have(
+ ∃(m, (∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y)))) <=> ∃(m, m ∈ relationDomain(h) /\ z ∈ app(h, m))
+ ) by Cut(
+ lastStep,
+ existentialEquivalenceDistribution of (
+ P := lambda(m, ∃(y, m ∈ relationDomain(h) /\ z ∈ y /\ (app(h, m) === y))),
+ Q := lambda(m, m ∈ relationDomain(h) /\ z ∈ app(h, m))
+ )
+ )
+
+ have(functional(h) |- ∃(y, y ∈ relationRange(h) /\ z ∈ y) <=> ∃(m, m ∈ relationDomain(h) /\ z ∈ app(h, m))) by Apply(equivalenceRewriting).on(
+ introM,
+ lastStep
+ )
+
+ have(thesis) by Apply(equivalenceRewriting).on(
+ lastStep,
+ unionAxiom.asInstanceOf
+ )
+ }
+
+ // *************
+ // * EMPTYNESS *
+ // *************
+
+ /**
+ * Lemma --- The union of the empty set is the empty set.
+ *
+ * `∪ ∅ = ∅`
+ */
+ val unionEmpty = Lemma(union(emptySet) === emptySet) {
+ sorry
+ }
+
+ /**
+ * Lemma --- Restricting the domain of a function to the empty set yields the empty set.
+ *
+ * `h|∅ = ∅`
+ */
+ val restrictedFunctionEmptyDomain = Lemma(restrictedFunction(h, emptySet) === emptySet) {
+ sorry
+ }
+
+ /**
+ * Lemma --- If the domain of a function is non empty, then the function is non empty as well.
+ *
+ * `Dom(h) != ∅ |- h != ∅`
+ */
+ val nonEmptyDomain = Lemma(!(relationDomain(h) === emptySet) |- !(h === emptySet)) {
+ sorry
+ }
+
+ /**
+ * Lemma --- A superset of a non empty set is non empty.
+ *
+ * `x ⊆ y, x != ∅ |- y != ∅`
+ */
+ val subsetNotEmpty = Lemma((subset(x, y), !(x === emptySet)) |- !(y === emptySet)) {
+ val subst = have(y === emptySet |- y === emptySet) by Hypothesis
+ have((subset(x, emptySet), y === emptySet) |- (x === emptySet)) by Apply(equivalenceApply of (p1 := subset(x, emptySet))).on(emptySetIsItsOwnOnlySubset.asInstanceOf)
+ thenHave((subset(x, y), y === emptySet) |- (x === emptySet)) by Substitution.ApplyRules(subst)
+ }
+
+ /**
+ * Theorem --- The range of the empty relation is empty.
+ *
+ * `range(∅) = ∅`
+ *
+ */
+ val rangeEmpty = Theorem(relationRange(emptySet) === emptySet) {
+ import lisa.maths.settheory.SetTheory
+
+ have(!in(SetTheory.pair(a, t), emptySet)) by Exact(emptySetAxiom)
+ thenHave(forall(a, !in(SetTheory.pair(a, t), emptySet))) by RightForall
+ val s0 = thenHave(!exists(a, in(SetTheory.pair(a, t), emptySet))) by Restate
+
+ have(!in(t, emptySet)) by Exact(emptySetAxiom)
+ have(in(t, emptySet) <=> exists(a, in(SetTheory.pair(a, t), emptySet))) by Tautology.from(lastStep, s0)
+ val defRHS = thenHave(forall(t, in(t, emptySet) <=> exists(a, in(SetTheory.pair(a, t), emptySet)))) by RightForall
+
+ have((relationRange(emptySet) === emptySet) <=> forall(t, in(t, emptySet) <=> exists(a, in(SetTheory.pair(a, t), emptySet)))) by InstantiateForall(emptySet)(
+ relationRange.definition of (r := emptySet, z := emptySet)
+ )
+ have(relationRange(emptySet) === emptySet) by Tautology.from(defRHS, lastStep)
+ }
+
+
+ /**
+ * Lemma --- The range of the empty function is empty.
+ *
+ * `Im(∅) = ∅`
+ */
+ val unionRangeEmpty = Lemma(unionRange(emptySet) === emptySet) {
+ have(unionRange(emptySet) === unionRange(emptySet)) by RightRefl
+ thenHave(unionRange(emptySet) === union(emptySet)) by Substitution.ApplyRules(rangeEmpty)
+ thenHave(thesis) by Substitution.ApplyRules(unionEmpty)
+ }
+
+ /**
+ * Lemma --- If a function and a domain are non empty, then restricting this function to this
+ * domain yields a non empty set.
+ *
+ * `h != ∅, d != ∅ |- h|d != ∅`
+ */
+ val restrictedFunctionNotEmpty = Lemma((!(h === emptySet), !(d === emptySet)) |- !(restrictedFunction(h, d) === emptySet)) {
+ sorry
+ }
+
+ // ****************
+ // * MONOTONICITY *
+ // ****************
+
+ /**
+ * Lemma --- Union is a monotonic operation with respect to set inclusion.
+ *
+ * `x ⊆ y |- ∪ x ⊆ ∪ y`
+ */
+ val unionMonotonic = Lemma(subset(x, y) |- subset(union(x), union(y))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- Range is a monotonic operation with respect to set inclusion.
+ *
+ * `f ⊆ g |- Im(f) ⊆ Im(g)`
+ */
+ val rangeMonotonic = Lemma(subset(f, g) |- subset(relationRange(f), relationRange(g))) {
+ sorry
+ }
+
+ /**
+ * Lemma --- The union of the range is a monotonic operation with respect to set inclusion.
+ *
+ * `f ⊆ g |- ∪ Im(f) ⊆ ∪ Im(g)`
+ */
+ val unionRangeMonotonic = Lemma(subset(f, g) |- subset(unionRange(f), unionRange(g))) {
+ have(thesis) by Apply(unionMonotonic).on(rangeMonotonic.asInstanceOf)
+ }
+
+ /**
+ * Lemma --- If two implications are true then disjuncting on both sides is also a valid implication.
+ */
+ val disjunctionsImplies = Lemma((p1 ==> p2, q1 ==> q2) |- (p1 \/ q1) ==> (p2 \/ q2)) {
+
+ val right = have((p1 ==> p2, q1 ==> q2, p1) |- p2 \/ q2) by Restate
+ val left = have((p1 ==> p2, q1 ==> q2, q1) |- p2 \/ q2) by Restate
+
+ have((p1 ==> p2, q1 ==> q2, p1 \/ q1) |- p2 \/ q2) by LeftOr(left, right)
+ }
+
+ /**
+ * Lemma --- If a class function F (whose representation is P) is monotonic then with respect to set inclusion, then S -> F(S) ∪ S is also
+ * a monotonic function.
+ *
+ * `s ⊆ t, F(s) ⊆ F(t) |- F(s) ∪ s ⊆ F(t) ∪ t`
+ */
+ val unionPreimageMonotonic = Lemma((subset(s, t), P(s) ==> P(t)) |- (P(s) \/ in(x, s)) ==> (P(t) \/ in(x, t))) {
+ have(subset(s, t) |- forall(z, in(z, s) ==> in(z, t))) by Cut(
+ subsetAxiom of (x := s, y := t),
+ equivalenceApply of (p1 := subset(s, t), p2 := forall(z, in(z, s) ==> in(z, t)))
+ )
+ thenHave(subset(s, t) |- in(x, s) ==> in(x, t)) by InstantiateForall(x)
+ have(thesis) by Cut(lastStep, disjunctionsImplies of (p1 := in(x, s), p2 := in(x, t), q1 := P(s), q2 := P(t)))
+ }
+
+ /**
+ * Lemma --- Resticting a function to a smaller domain yields a subset of the original function.
+ *
+ * `x ⊆ y |- f|x ⊆ f|y`
+ */
+ val restrictedFunctionDomainMonotonic = Lemma(subset(x, y) |- subset(restrictedFunction(f, x), restrictedFunction(f, y))) {
+ sorry
+ }
+
+ // *******************
+ // * SPECIFIC LEMMAS *
+ // *******************
+
+ /**
+ * Lemma --- Characterization of the union of the range of a cumulative function restricted to the successor of a natural number.
+ *
+ * `cumulative(h) and Dom(h) = N |- ∪ Im(h|n + 1) = h(n)`
+ */
+ val unionRangeCumulativeRestrictedFunction =
+ Lemma((functional(h), relationDomain(h) === N, in(n, N), ∀(m, subset(m, n) ==> subset(app(h, m), app(h, n)))) |- unionRange(restrictedFunction(h, successor(n))) === app(h, n)) {
+
+ val domainSubset = have(in(n, N) |- setIntersection(successor(n), N) === successor(n)) by Apply(intersectionNat).on(equivalenceApply of (p1 := in(n, N)), successorIsNat.asInstanceOf)
+
+ have(functional(h) |- (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ (successor(n) ∩ relationDomain(h)) /\ (app(restrictedFunction(h, successor(n)), m) === y)) /\ z ∈ y) by Cut(
+ restrictedFunctionRangeMembership of (f := h, d := successor(n)),
+ rightAndEquivalence of (p1 := y ∈ restrRange(h, successor(n)), p2 := ∃(m, m ∈ (successor(n) ∩ relationDomain(h)) /\ (app(restrictedFunction(h, successor(n)), m) === y)), p := z ∈ y)
+ )
+
+ thenHave(
+ (functional(h), relationDomain(h) === N) |- (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ (successor(n) ∩ N) /\ (app(restrictedFunction(h, successor(n)), m) === y)) /\ z ∈ y
+ ) by RightSubstEq.withParametersSimple(
+ List((relationDomain(h), N)),
+ lambda(s, (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ (successor(n) ∩ s) /\ (app(restrictedFunction(h, successor(n)), m) === y)) /\ z ∈ y)
+ )
+
+ thenHave(
+ (functional(h), in(n, N), relationDomain(h) === N, successor(n) ∩ N === successor(n)) |- (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(
+ m,
+ m ∈ (successor(n) ∩ N) /\ (app(restrictedFunction(h, successor(n)), m) === y)
+ ) /\ z ∈ y
+ ) by Weakening
+
+ thenHave(
+ (functional(h), in(n, N), relationDomain(h) === N, successor(n) ∩ N === successor(n)) |- (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(
+ m,
+ m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y)
+ ) /\ z ∈ y
+ ) by RightSubstEq.withParametersSimple(
+ List((successor(n) ∩ N, successor(n))),
+ lambda(s, (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ s /\ (app(restrictedFunction(h, successor(n)), m) === y)) /\ z ∈ y)
+ )
+
+ have(
+ (functional(h), in(n, N), relationDomain(h) === N) |- (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y)) /\ z ∈ y
+ ) by Cut(domainSubset, lastStep)
+
+ have(
+ (functional(h), in(n, N), relationDomain(h) === N) |- (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y) /\ z ∈ y)
+ ) by Apply(equivalenceRewriting).on(
+ lastStep,
+ existentialConjunctionWithClosedFormula of (P := lambda(m, m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y)), p := z ∈ y)
+ )
+
+ thenHave(
+ (functional(h), in(n, N), relationDomain(h) === N) |- ∀(
+ y,
+ (y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y) /\ z ∈ y)
+ )
+ ) by RightForall
+
+ have(
+ (functional(h), in(n, N), relationDomain(h) === N) |- ∃(y, y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(
+ y,
+ ∃(m, m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y) /\ z ∈ y)
+ )
+ ) by Cut(
+ lastStep,
+ existentialEquivalenceDistribution of (
+ P := lambda(y, y ∈ restrRange(h, successor(n)) /\ z ∈ y),
+ Q := lambda(y, ∃(m, m ∈ successor(n) /\ (app(restrictedFunction(h, successor(n)), m) === y) /\ z ∈ y))
+ )
+ )
+
+ val introM =
+ thenHave(
+ (functional(h), in(n, N), relationDomain(h) === N) |- ∃(y, y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(
+ m,
+ ∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))
+ )
+ ) by Tableau
+
+ have((∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (m ∈ successor(n) /\ z ∈ app(restrictedFunction(h, successor(n)), m))) by Exact(
+ equalityInExistentialQuantifier of (P := lambda(y, m ∈ successor(n) /\ z ∈ y))
+ )
+
+ thenHave(m ∈ successor(n) |- (∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (m ∈ successor(n) /\ z ∈ app(h, m))) by Substitution.ApplyRules(
+ restrictedFunctionApplication
+ )
+ thenHave((∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (m ∈ successor(n) /\ z ∈ app(h, m))) by Tableau
+
+ thenHave(subset(m, n) <=> m ∈ successor(n) |- (∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (subset(m, n) /\ z ∈ app(h, m))) by RightSubstIff
+ .withParametersSimple(
+ List((m ∈ successor(n), subset(m, n))),
+ lambda(p, (∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (p /\ z ∈ app(h, m)))
+ )
+
+ have(in(n, N) |- (∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (subset(m, n) /\ z ∈ app(h, m))) by Cut(natSubset, lastStep)
+
+ thenHave(
+ in(n, N) |- ∀(m, (∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))) <=> (subset(m, n) /\ z ∈ app(h, m)))
+ ) by RightForall
+
+ have(
+ in(n, N) |- ∃(m, (∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y)))) <=> ∃(m, subset(m, n) /\ z ∈ app(h, m))
+ ) by Cut(
+ lastStep,
+ existentialEquivalenceDistribution of (
+ P := lambda(m, ∃(y, m ∈ successor(n) /\ z ∈ y /\ (app(restrictedFunction(h, successor(n)), m) === y))),
+ Q := lambda(m, subset(m, n) /\ z ∈ app(h, m))
+ )
+ )
+
+ have((functional(h), in(n, N), relationDomain(h) === N) |- ∃(y, y ∈ restrRange(h, successor(n)) /\ z ∈ y) <=> ∃(m, subset(m, n) /\ z ∈ app(h, m))) by Apply(equivalenceRewriting).on(
+ introM,
+ lastStep
+ )
+
+ val unionIsExists =
+ have((functional(h), in(n, N), relationDomain(h) === N) |- z ∈ unionRange(restrictedFunction(h, successor(n))) <=> ∃(m, subset(m, n) /\ z ∈ app(h, m))) by Apply(equivalenceRewriting).on(
+ lastStep,
+ unionAxiom.asInstanceOf
+ )
+
+ val cumulativeAssumption = ∀(m, subset(m, n) ==> subset(app(h, m), app(h, n)))
+
+ have(cumulativeAssumption |- ∃(m, subset(m, n) /\ z ∈ app(h, m)) <=> z ∈ app(h, n)) subproof {
+ val seq1 = have(z ∈ app(h, n) |- z ∈ app(h, n)) by Hypothesis
+ have(z ∈ app(h, n) |- subset(n, n) /\ z ∈ app(h, n)) by RightAnd(seq1, subsetReflexivity of (x := n))
+ thenHave(z ∈ app(h, n) |- ∃(m, subset(m, n) /\ z ∈ app(h, m))) by RightExists
+ val backward = thenHave(cumulativeAssumption |- z ∈ app(h, n) ==> ∃(m, subset(m, n) /\ z ∈ app(h, m))) by Weakening
+
+ have(cumulativeAssumption |- cumulativeAssumption) by Hypothesis
+ thenHave(cumulativeAssumption |- subset(m, n) ==> subset(app(h, m), app(h, n))) by InstantiateForall(m)
+ have((cumulativeAssumption, subset(m, n), z ∈ app(h, m)) |- forall(z, z ∈ app(h, m) ==> z ∈ app(h, n))) by Apply(equivalenceApply).on(
+ lastStep,
+ subsetAxiom
+ )
+ thenHave((cumulativeAssumption, subset(m, n) /\ z ∈ app(h, m)) |- z ∈ app(h, n)) by InstantiateForall(z)
+ thenHave((cumulativeAssumption, ∃(m, subset(m, n) /\ z ∈ app(h, m))) |- z ∈ app(h, n)) by LeftExists
+ val forward = thenHave(cumulativeAssumption |- ∃(m, subset(m, n) /\ z ∈ app(h, m)) ==> z ∈ app(h, n)) by RightImplies
+
+ have(thesis) by RightIff(forward, backward)
+ }
+
+ have((functional(h), in(n, N), relationDomain(h) === N, cumulativeAssumption) |- (z ∈ unionRange(restrictedFunction(h, successor(n)))) <=> z ∈ app(h, n)) by Apply(equivalenceRewriting).on(
+ unionIsExists,
+ lastStep
+ )
+ thenHave((functional(h), in(n, N), relationDomain(h) === N, cumulativeAssumption) |- ∀(z, z ∈ unionRange(restrictedFunction(h, successor(n))) <=> z ∈ app(h, n))) by RightForall
+
+ have(thesis) by Apply(equivalenceApply).on(lastStep, extensionalityAxiom.asInstanceOf)
+ }
+
+}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
new file mode 100644
index 0000000000000000000000000000000000000000..cb82507988075654da70cda3dd340e4dab5739cd
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Tactics.scala
@@ -0,0 +1,174 @@
+/**
+ * Defines a set of tactics to reason on Algebraic Data Types
+ */
+
+package lisa.maths.settheory.types.adt
+
+import lisa.maths.settheory.SetTheory.{*, given}
+import ADTDefinitions.*
+import Helpers.*
+
+/**
+ * Tactic performing a structural induction proof over an algebraic data type.
+ *
+ * ===Usage===
+ * {{{
+ * have(forall(x, x :: adt => P(x)) /*or*/ x :: adt |- P(x)) by Induction(x, adt) {
+ * Case(c1, x1, ..., xn) subproof {
+ * // proof of P(xi) /\ ... P(xj) => P(c1(x1, ..., xn))
+ * }
+ * ...
+ * Case(cm, x1, ..., xk) subproof {
+ * // proof of P(xi) /\ ... P(xj) => P(c1(x1, ..., xn'))
+ * }
+ * }
+ * }}}
+ *
+ * x and adt are inferred from the context if not provided by the user.
+ *
+ * Supports only 1 formula on the right hand side of the sequent.
+ * @param expectedVar the variable on which the induction is performed
+ * @param expectedADT the algebraic data type on which the induction is performed
+ */
+class Induction[M <: Arity](expectedVar: Option[Variable], expectedADT: Option[ADT[M]]) extends lisa.prooflib.ProofTacticLib.ProofTactic {
+
+ /**
+ * Given a proof of the claim for each case (possibly using the induction hypothesis),
+ * reassemble them to generate a proof of the claim of the form
+ * `∀x. x :: adt => P(x)`
+ *
+ * @param proof the proof in which the induction is performed
+ * @param cases the proofs of the claim for each case in addition to the variables used by the user
+ * @param inductionVariable the variable over which the induction is performed
+ * @param adt the algebraic data type to perform induction on
+ * @param prop the property to prove //TODO: Change to a lambda expression (Scala 3.4.2)
+ */
+ private def proveForallPredicate[N <: Arity](using proof: lisa.SetTheoryLibrary.Proof)(cases: Map[Constructor[N], (Seq[Variable], proof.Fact)], inductionVariable: Variable, adt: ADT[N], typeVariablesSubst: Seq[Term], propFun: Term => Formula, context: Set[Formula]): proof.Fact =
+
+ val prop = lambda[Term, Formula](x, propFun(x))
+ val typeVariablesSubstPairs = adt.typeVariables.toSeq.zip(typeVariablesSubst).map(SubstPair(_, _))
+ val instTerm = adt(typeVariablesSubst : _*)
+
+ adt.constructors.foldLeft[proof.Fact](adt.induction.of((typeVariablesSubstPairs :+ (P := prop)): _*)) ( (acc, c) =>
+ val inductiveCaseProof = cases(c)._1.zip(c.underlying.underlying.specification.map(_.substitute(typeVariablesSubstPairs : _*))).foldRight[proof.Fact](cases(c)._2) ( (el, acc2) =>
+ val (v, ty) = el
+ val accRight: Formula = acc2.statement.right.head
+ ty match
+ case Self =>
+ have((acc2.statement -<? prop(v)).left |- prop(v) ==> accRight) by Weakening(acc2)
+ thenHave((lastStep.statement -<? (v :: instTerm)).left |- v :: instTerm ==> (prop(v) ==> accRight)) by Weakening
+ thenHave(lastStep.statement.left |- forall(v, v :: instTerm ==> (prop(v) ==> accRight))) by RightForall
+ case GroundType(t)=>
+ thenHave((acc2.statement -<? (v :: t)).left |- v :: t ==> accRight) by Weakening
+ thenHave(lastStep.statement.left |- forall(v, v :: t ==> accRight)) by RightForall
+ )
+ acc.statement.right.head match
+ case Implies(trueInd, rest) =>
+ // println(s"Case: ${c.fullName}")
+ // println(isSame(trueInd, inductiveCaseProof.statement.right.head))
+ // println(inductiveCaseProof.statement)
+ // println(" + ")
+ // println(acc.statement)
+ // println(" = ")
+ // println((acc.statement.left ++ inductiveCaseProof.statement.left) |- rest)
+ have((acc.statement.left ++ inductiveCaseProof.statement.left) |- rest) by Sorry//Cut(inductiveCaseProof, acc)
+ case _ => throw UnreachableException
+ )
+ thenHave(context |- forall(inductionVariable, inductionVariable :: instTerm ==> prop(inductionVariable))) by Tautology //Change
+
+
+
+ /**
+ * Infers the variable, the ADT and the arguments of the ADT from a formula of the form `x :: ADT(T1, ..., Tn)`.
+ *
+ * @param f the formula to infer these elements from
+ */
+ def inferArguments(f: Formula): Option[(Variable, ADT[?], Seq[Term])] =
+ def checkFoundArguments(foundVar: Variable, foundADT: ADT[?], args: Seq[Term]): Option[(Variable, ADT[?], Seq[Term])] =
+ (expectedVar, expectedADT) match
+ case (Some(v), _) if v != foundVar => None
+ case (_, Some(a)) if a != foundADT => None
+ case _ => Some((foundVar, foundADT, args))
+
+ f match
+ case TypeAssignment(Variable(id), ADT(foundADT, args)) =>
+ checkFoundArguments(Variable(id), foundADT, args)
+ case AppliedPredicate(in, Seq[Term](Variable(id), ADT(foundADT, args))) =>
+ checkFoundArguments(Variable(id), foundADT, args)
+ case _ =>
+ None
+
+ /**
+ * Infers the variable, the ADT and the arguments of the ADT from a set of formula
+ * containing one is of the form `x :: ADT(T1, ..., Tn)`.
+ *
+ * @param s the set of formula to infer these elements from
+ */
+ def inferArguments(s: Set[Formula]): Option[(Variable, ADT[?], Seq[Term])] =
+ s.foldLeft[Option[(Variable, ADT[?], Seq[Term])]](None)((acc, prem) =>
+ acc.orElse(inferArguments(prem))
+ )
+
+ /**
+ * Infers the variable, the ADT and the arguments of the ADT from a sequent whose one of the premises
+ * is of the form `x :: ADT(T1, ..., Tn)`.
+ *
+ * @param seq the sequent to infer these elements from
+ */
+ def inferArguments(seq: Sequent): Option[(Variable, ADT[?], Seq[Term], Option[Formula])] =
+ inferArguments(seq.left).map(p => (p._1, p._2, p._3, None))
+ .orElse(
+ seq.right.head match
+ case Forall(x, Implies(assignment, prop)) =>
+ inferArguments(assignment).filter(p => p._1 == x).map(p => (p._1, p._2, p._3, Some(prop)))
+ case _ => None
+ )
+
+ /**
+ * Given a proof of the claim for each case (possibly using the induction hypothesis),
+ * reassemble the subproofs to generate a proof of the claim for every element of the ADT.
+ *
+ * @tparam N the arity of the ADT
+ * @param proof the scope in which the induction is performed
+ * @param cases the cases to prove. A [[CaseBuilder]] is a mutable data structure that register every case that
+ * has been added to the tactic.
+ * @param bot the claim
+ */
+ def apply[N <: Arity](using proof: lisa.SetTheoryLibrary.Proof)(cases: ADTSyntax.CaseBuilder[N, proof.ProofStep, (Sequent, Seq[Term], Variable)] ?=> Unit)(bot: Sequent): proof.ProofTacticJudgement =
+ inferArguments(bot) match
+ case Some((inferedVar, inferedADT, inferedArgs, inferedProp)) =>
+
+ val prop = inferedProp.getOrElse(bot.right.head)
+ val propFunction = (t: Term) => inferedProp.getOrElse(bot.right.head).substitute(inferedVar -> t)
+ val assignment = inferedVar :: inferedADT(inferedArgs : _*)
+ val context = (if inferedProp.isDefined then bot else bot -<< assignment).left
+ val builder = ADTSyntax.CaseBuilder[N, proof.ProofStep, (Sequent, Seq[Term], Variable)]((context |- prop, inferedArgs, inferedVar))
+ cases(using builder)
+
+ builder.isValid(inferedADT.asInstanceOf[ADT[N]]) match
+ case None =>
+ TacticSubproof { sp ?=>
+ proveForallPredicate(using sp)(builder.build, inferedVar, inferedADT.asInstanceOf[ADT[N]], inferedArgs, propFunction, context)
+ if !inferedProp.isDefined then
+ lastStep.statement.right.head match
+ case Forall(_, phi) =>
+ thenHave(context |- phi) by InstantiateForall(inferedVar)
+ case _ => throw UnreachableException
+
+ thenHave(bot) by Tautology
+ }
+ case Some(msg) => proof.InvalidProofTactic(msg)
+
+ case None => proof.InvalidProofTactic("No variable typed with the ADT found in the context.")
+
+}
+
+/**
+ * Companion object for the [[Induction]] tactic class.
+ */
+object Induction {
+ def apply()(using proof: lisa.SetTheoryLibrary.Proof) = new Induction(None, None)
+ def apply[N <: Arity](adt: ADT[N])(using proof: lisa.SetTheoryLibrary.Proof) = new Induction(None, Some(adt))
+ def apply(v: Variable)(using proof: lisa.SetTheoryLibrary.Proof) = new Induction(Some(v), None)
+ def apply[N <: Arity](v: Variable, adt: ADT[N])(using proof: lisa.SetTheoryLibrary.Proof) = new Induction(Some(v), Some(adt))
+}
\ No newline at end of file
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Typed.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Typed.scala
new file mode 100644
index 0000000000000000000000000000000000000000..4b1ed5713aa767c9b1200e04df792a4e5c0533f6
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Typed.scala
@@ -0,0 +1,285 @@
+/**
+ * Gives a type theoretic interpretation to algebraic data types and functions over them.
+ */
+
+package lisa.maths.settheory.types.adt
+
+import lisa.maths.settheory.SetTheory.{_, given}
+import lisa.maths.settheory.types.TypeLib.any
+import lisa.maths.settheory.types.TypeSystem.FunctionalClass
+import lisa.maths.settheory.types.TypeSystem.TypedConstantFunctional
+
+/**
+ * Type theoretic interpretation of a constructor, that is a function whose type is
+ *
+ * `c :: ∀X1, ..., Xn. T1 -> ... -> Tn -> ADT
+ *
+ * @tparam N the number of type variables appearing in the definition of this constructor's ADT
+ * @param line the line at which this constructor is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which this constructor is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param underlying the set theoretic underlying constructor
+ */
+class Constructor[N <: Arity] private[adt] (using line: sourcecode.Line, file: sourcecode.File)(
+ private[adt] val underlying: SemanticConstructor[N]
+) extends TypedConstantFunctional[N](
+ underlying.fullName,
+ underlying.typeArity,
+ FunctionalClass(Seq.fill(underlying.typeArity)(any), underlying.typeVariablesSeq, underlying.typ, underlying.typeArity),
+ underlying.intro
+ ) {
+
+ /**
+ * Name of the constructor
+ *
+ * e.g `list/cons` or `list/nil`
+ */
+ val name = underlying.fullName
+
+ /**
+ * Theorem --- Introduction rule
+ *
+ * `c :: ∀X1, ..., Xn. T1 -> ... -> Tn -> ADT
+ *
+ * where `c` is this constructor, `ADT` the ADT it belongs to and `T1, ..., Tn` the domains of the constructor's arguments.
+ * X1, ..., Xn are the type variables of the ADT.
+ */
+ val intro =
+ THM(underlying.intro.statement, s"${name} introduction rule", line.value, file.value, Theorem) {
+ have(underlying.intro)
+ }
+
+ /**
+ * Theorem --- Injectivity
+ *
+ * ` c(x1, ..., xn) = c(y1, ..., yn) <=> x1 = y1 /\ ... /\ xn = yn`
+ */
+ lazy val injectivity =
+ THM(underlying.injectivity.statement, s"${name} injectivity", line.value, file.value, Theorem) {
+ have(underlying.injectivity)
+ }
+
+ /**
+ * Type variables appearing in the signature of this constructor
+ */
+ val typeVariables: Variable ** N = underlying.typeVariables
+}
+
+/**
+ * Type theoretic polymorphic inductive datatype. Comes with a structural induction schema, injection and pattern matching.
+ *
+ * @tparam N the number of type variables appearing in the definition of this ADT
+ * @param line the line at which this ADT is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which this ADT is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param underlying
+ * @param constructors
+ */
+class ADT[N <: Arity] private[adt] (using line: sourcecode.Line, file: sourcecode.File)(
+ private[adt] val underlying: SemanticADT[N],
+ private[adt] val constructors: Seq[Constructor[N]]
+) {
+
+ /**
+ * Name of this ADT
+ */
+ val name = underlying.name
+
+ /**
+ * Identifier of this ADT.
+ */
+ val id: Identifier = underlying.id
+ ADT.identifiersToADT.addOne(id -> this)
+
+ /**
+ * Theorem --- Structural induction principle
+ *
+ * e.g. `P(nil) => (∀x :: T, l :: list(T). P(l) => P(cons(x, l)))) => ∀l :: list(T). P(l)`
+ */
+ lazy val induction =
+ THM(underlying.induction.statement, s"${name} structural induction principle", line.value, file.value, Theorem) {
+ have(underlying.induction)
+ }
+
+ /**
+ * Theorem --- Elimination rules (Pattern Matching)
+ *
+ * `x :: ADT |- ∃ x1, ..., xn. x = c1 * x1 * ... * xn \/ ... \/ ∃ x1, ..., xn'. x = cm * x1 * ... * xn'
+ *
+ * Every term of this ADT is an instance of one of its constructors.
+ *
+ * e.g. `∀l :: list(T). l = nil \/ ∃x, xs. l = cons(x, xs)`
+ */
+ lazy val elim =
+ THM(underlying.elim.statement, s"${name} elimination rule", line.value, file.value, Theorem) {
+ have(underlying.elim)
+ }
+
+ /**
+ * Theorem --- Injectivity
+ *
+ * ` c1 * x1 * ... * xn != c2 * y1 * ... * ym`
+ *
+ * Instances of different constructors are different.
+ *
+ * e.g. `cons(x, l) != nil`
+ *
+ * @param c1 the first constructor
+ * @param c2 the second constructor
+ */
+ def injectivity(c1: Constructor[N], c2: Constructor[N]) =
+ val injectivityLemma = underlying.injectivity(c1.underlying, c2.underlying)
+ THM(injectivityLemma.statement, s"${c1.name}-${c2.name} injectivity", line.value, file.value, Theorem) {
+ have(injectivityLemma)
+ }
+
+ /**
+ * Type variables appearing in the signature of this ADT
+ */
+ val typeVariables: Variable ** N = underlying.typeVariables
+
+ /**
+ * Instantiate the type variables of this ADT with given types.
+ * Checks the arity at runtime.
+ *
+ * @param args the types to instantiate the type variables with
+ */
+ def applyUnsafe(args: Term ** N): Term = underlying.term(args.toSeq)
+
+ /**
+ * Instantiate the type variables of this ADT with given types.
+ * Checks the arity at runtime.
+ *
+ * @param args the types to instantiate the type variables with
+ */
+ def applySeq(args: Seq[Term]): Term = underlying.term(args)
+
+ /**
+ * Instantiate the type variables of this ADT with given types.
+ * Checks the arity at runtime.
+ *
+ * TODO: wait Scala 3.4.2 to remove this method and extend Term ** N |-> Term instead
+ *
+ * @param args the types to instantiate the type variables with
+ */
+ def apply(args: Term*): Term = underlying.term(args)
+}
+
+private object ADT {
+ /**
+ * Global map from object identifiers to ADTs
+ */
+ private val identifiersToADT: scala.collection.mutable.Map[Identifier, ADT[?]] = scala.collection.mutable.Map.empty
+
+ /**
+ * Checks if a label is an ADT, and returns it if it is the case.
+ *
+ * @param l the label to check
+ */
+ def unapply(l: Label[?]): Option[ADT[?]] = getADT(l.id)
+
+ /**
+ * Checks if a term is an instance of an ADT and if it is the case, returns
+ * the appropriate instances of the type variables.
+ *
+ * @param term the term to check
+ */
+ def unapply(obj: Term): Option[(ADT[?], Seq[Term])] =
+ obj match
+ case l: Label[?] =>
+ val lwidened: Label[?] = l
+ unapply(lwidened).map((_, Seq.empty))
+ case AppliedFunctional(l, args) => unapply(l).map((_, args))
+ case _ => None
+
+ /**
+ * Checks if a class is an instance of an ADT and if it is the case, returns
+ * the appropriate instances of the type variables.
+ *
+ * @param c the class to check
+ */
+ def unapply(c: Class): Option[(ADT[?], Seq[Term])] =
+ c match
+ case t: Term => unapply(t)
+ case _ => None
+
+ /**
+ * Returns the ADT associated with an identifier.
+ *
+ * @param id the identifier of the ADT
+ */
+ def getADT(id: Identifier): Option[ADT[?]] = identifiersToADT.get(id)
+}
+
+/**
+ * Type theoretic function over algebraic data types. Its definition is the direct sum of the definitions of its constructors.
+ * Comes with introduction and elimination rules.
+ *
+ * @constructor gives a type theoretic interpretation to a set theoretic function over an ADT
+ * @tparam N the number of type variables appearing in the definition of this function's domain
+ * @param line the line at which this ADT is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which this ADT is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param underlying the underlying set theoretic function
+ * @param adt the domain of this function
+ */
+private class ADTFunction[N <: Arity](using line: sourcecode.Line, file: sourcecode.File)(
+ private val underlying: SemanticFunction[N],
+ private val adt: ADT[N]
+) extends TypedConstantFunctional[N](
+ underlying.fullName,
+ underlying.typeArity,
+ FunctionalClass(Seq.fill(underlying.typeArity)(any), underlying.typeVariablesSeq, underlying.typ, underlying.typeArity),
+ underlying.intro
+ ) {
+
+ /**
+ * Name of the function
+ *
+ * e.g. list/length
+ */
+ val name = underlying.fullName
+
+ /**
+ * Theorem --- Elimination rules
+ *
+ * `f * (c * x1 * ... * xn) = case(c, x1, ..., xn)`
+ *
+ * That is, when this function is applied to a constructor, it returns the corresponding case.
+ */
+ val elim: Map[Constructor[N], THM] = adt.constructors
+ .map(c =>
+ (
+ c,
+ THM(underlying.shortDefinition(c.underlying).statement, s"${name} elimination rule: ${c.name} case", line.value, file.value, Theorem) {
+ have(underlying.shortDefinition(c.underlying))
+ }
+ )
+ )
+ .toMap
+
+ /**
+ * Alias for [[this.elim]]
+ */
+ val shortDefinition: Map[Constructor[N], THM] = elim
+
+ /**
+ * Theorem --- Introduction rule
+ *
+ * `∀X1, ..., Xn. f(X1, ..., Xn) : ADT(X1, ..., Xn) -> T`
+ *
+ * where `f` is this function, `ADT` the ADT it takes argument and `T` its return type.
+ */
+ val intro: THM =
+ THM(underlying.intro.statement, s"${name} introduction rule", line.value, file.value, Theorem) {
+ have(underlying.intro)
+ }
+
+ /**
+ * Type variables in the signature of the function
+ */
+ val typeVariables: Variable ** N = underlying.typeVariables
+}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
new file mode 100644
index 0000000000000000000000000000000000000000..61dd75a7ebeabdc40fe8f5e3241709afed215374
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/Untyped.scala
@@ -0,0 +1,1752 @@
+/**
+ * This file implements tactics to generate polymorphic set theoretic inductive algebraic data types (or ADT) and prove properties about them.
+ * An algebraic data type is the least set closed under introduction rules, also known as constructors.
+ * A constructor takes arguments as input that can either belong to other types (non inductive arguments)
+ * or to the ADT itself (inductive arguments).
+ *
+ * An example of algebraic data type is the type of singly linked lists:
+ *
+ * list ::= nil() | cons(head: T, tail: list)
+ */
+
+package lisa.maths.settheory.types.adt
+
+import lisa.maths.settheory.SetTheory.{*, given}
+import Helpers.*
+import Helpers.{/\, \/, ===}
+import ADTDefinitions.*
+import ADTHelperTheorems as ADTThm
+import ADTThm.{N, pair, pairExtensionality}
+import lisa.maths.settheory.types.TypeLib.{ |=>}
+import lisa.maths.settheory.types.TypeSystem.{ :: }
+import lisa.maths.Quantifiers.{universalEquivalenceDistribution}
+import lisa.fol.FOL.Variable
+
+/**
+ * Helpers for constructors
+ */
+private object Constructors {
+
+ /**
+ * Global counter used to uniquely identify constructors and thereby avoid structural subtyping.
+ */
+ var tagCounter = 0
+}
+
+/**
+ * Syntactic set theoretical interpretation of a constructor for an algebraic data type.
+ * In set theory, a constructor is a tuple containing the arguments it has been applied to, in addition to a tag
+ * uniquely identifying it.
+ *
+ * E.g. `cons(1, nil())` is represented as `(tagcons, (1, ((tagnil, ∅), ∅)))`
+ *
+ * Constructors injectivity is proved within this class.
+ *
+ * @constructor creates a new constructor out of a user specification
+ * @param specification types that the constructor takes as arguments
+ * @param variables1 variables used to represent the arguments of the constructor
+ * @param variables2 alternative set of variables to avoid capture issues
+ */
+private class SyntacticConstructor(
+ val specification: Seq[ConstructorArgument],
+ val variables1: Seq[Variable],
+ val variables2: Seq[Variable],
+ ) {
+
+ /**
+ * Unique identifier of this constructor
+ */
+ val tag: Int = Constructors.tagCounter
+ Constructors.tagCounter = Constructors.tagCounter + 1
+
+ /**
+ * Term representation of the tag of this constructor
+ */
+ val tagTerm: Term = toTerm(tag)
+
+ /**
+ * Sequence of variables used to represent the arguments of the constructor
+ */
+ val variables: Seq[Variable] = variables1
+
+ /**
+ * Number of arguments that this constructor takes
+ */
+ val arity: Int = specification.length
+
+ /**
+ * Sequence of variables of the constructor with their respective domains.
+ */
+ val signature1: Seq[(Variable, ConstructorArgument)] = variables1.zip(specification)
+
+ /**
+ * Alternative sequence of variables of the constructor with their respective domains.
+ */
+ val signature2: Seq[(Variable, ConstructorArgument)] = variables2.zip(specification)
+
+ /**
+ * Sequence of variables of the constructor with their respective domains.
+ */
+ val signature: Seq[(Variable, ConstructorArgument)] = signature1
+
+ /**
+ * Internally, an instance of this constructor is represented as a list.
+ * The first element of this list is the tag of this constructor.
+ * The following elements are its arguments. We represent lists as chained
+ * pairs followed by the empty set.
+ *
+ * e.g. cons(1, nil()) --> (tagcons, (1, ((tagnil, ∅), ∅)))
+ *
+ * @param args the arguments of this instance of the constructor
+ */
+ def term(args: Seq[Term]): Term = pair(tagTerm, subterm(args))
+
+ /**
+ * Internal representation of an instance of this constructor in which arguments are schematic variables.
+ */
+ val term1: Term = term(variables1)
+
+ /**
+ * Internal representation of an instance of this constructor in which arguments are an alternative set of schematic variables.
+ */
+ val term2: Term = term(variables2)
+
+ /**
+ * Internal representation of an instance of this constructor in which arguments are schematic variables.
+ */
+ val term: Term = term1
+
+ /**
+ * Internal representation of an instance of this constructor without the tag
+ *
+ * @param args the arguments of this instance of the constructor
+ *
+ * @see [[this.term]]
+ */
+ def subterm(args: Seq[Term]): Term = args.foldRight[Term](emptySet)(pair(_, _))
+
+ /**
+ * Internal representation of an instance of this constructor without the tag, in which arguments are schematic variables.
+ */
+ val subterm1: Term = subterm(variables1)
+
+ /**
+ * Internal representation of an instance of this constructor without the tag, in which arguments are an alternative set
+ * of schematic variables.
+ */
+ val subterm2: Term = subterm(variables2)
+
+ /**
+ * Internal representation of an instance of this constructor without the tag, in which arguments are schematic variables.
+ */
+ val subterm: Term = subterm1
+
+ /**
+ * Theorem --- Injectivity of constructors.
+ *
+ * Two instances of this constructor are equal if and only if all of their arguments are pairwise equal
+ *
+ * e.g. cons(head1, tail1) === cons(head2, tail2) <=> head1 === head2 /\ tail1 === tail2
+ */
+ lazy val injectivity =
+ if arity == 0 then
+ Lemma(term1 === term2) {
+ have(thesis) by RightRefl
+ }
+ else
+ Lemma((term1 === term2) <=> (variables1 === variables2)) {
+
+ // STEP 1: Get rid of the tag using pair extensionality
+ have((term1 === term2) <=> (subterm1 === subterm2)) by Restate.from(pairExtensionality of (a := tagTerm, b := subterm1, c := tagTerm, d := subterm2))
+
+ // STEP 2: Repeat pair extensionality until all variables have been pulled out of the term
+ variables1
+ .zip(variables2)
+ .foldLeft(Seq.empty[Variable], variables1, Seq.empty[Variable], variables2, lastStep)((acc, v) =>
+
+ // pulledVars1 are the variables that have been pulled out of the left term
+ // remainingVars1 are the variables that are still in the left term
+ // pulledVars2 are the variables that have been pulled out of the right term
+ // remainingVars2 are the variables that are still in the right term
+ val (pulledVars1, remainingVars1, pulledVars2, remainingVars2, previousFact) = acc
+
+ // v1 and v2 are the variables that are being pulled out
+ val (v1, v2) = v
+
+ val updatedPulledVars1 = pulledVars1 :+ v1
+ val updatedPulledVars2 = pulledVars2 :+ v2
+ val updatedRemainingVars1 = remainingVars1.tail
+ val updatedRemainingVars2 = remainingVars2.tail
+
+ val subsubterm1 = subterm(updatedRemainingVars1)
+ val subsubterm2 = subterm(updatedRemainingVars2)
+
+ have(
+ (pair(v1, subsubterm1) === pair(v2, subsubterm2)) <=>
+ ((v1 === v2) /\ (subsubterm1 === subsubterm2))
+ ) by Restate.from(pairExtensionality of (a := v1, b := subsubterm1, c := v2, d := subsubterm2))
+ have(
+ ((pulledVars1 === pulledVars2) /\ (pair(v1, subsubterm1) === pair(v2, subsubterm2))) <=>
+ ((pulledVars1 === pulledVars2) /\ (v1 === v2) /\ (subsubterm1 === subsubterm2))
+ ) by Cut(
+ lastStep,
+ ADTThm.rightAndEquivalence of (p := pulledVars1 === pulledVars2, p1 := pair(v1, subsubterm1) === pair(v2, subsubterm2), p2 := (v1 === v2) /\ (subsubterm1 === subsubterm2))
+ )
+ val newFact = have(
+ (term1 === term2) <=>
+ ((updatedPulledVars1 === updatedPulledVars2) /\ (subsubterm1 === subsubterm2))
+ ) by Apply(ADTThm.equivalenceRewriting).on(lastStep, previousFact)
+
+ (updatedPulledVars1, updatedRemainingVars1, updatedPulledVars2, updatedRemainingVars2, newFact)
+ )
+ }
+
+}
+
+/**
+ * Syntactic set theoretical interpretation of an algebraic data type. That is the least set closed under [[SyntacticConstructor]].
+ *
+ * E.g. list is the smallest set containing nil and closed under the syntactic operation cons.
+ *
+ * Injectivity between different constructors, introduction rules and structural induction are proved within this class.
+ *
+ * @constructor creates a new algebraic data type out of a user specification.
+ * @param line the line at which the ADT is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which the ADT is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param name the name of the ADT
+ * @param constructors constructors of the ADT
+ * @param typeVariables type variables used in the definition of this ADT
+ */
+private class SyntacticADT[N <: Arity](using line: sourcecode.Line, file: sourcecode.File)(
+ val name: String,
+ val constructors: Seq[SyntacticConstructor],
+ val typeVariables: Variable ** N,
+ ) {
+
+ /**
+ * Sequence of type variables used in the definition of this ADT
+ */
+ val typeVariablesSeq: Seq[Variable] = typeVariables.toSeq
+
+ /**
+ * Number of type variables used in the definition of this ADT
+ */
+ val typeArity: N = typeVariablesSeq.length.asInstanceOf[N]
+
+ // ***************
+ // * INJECTIVITY *
+ // ***************
+
+ /**
+ * Theorem --- Injectivity of constructors.
+ *
+ * Two instances of different construcors are always different.
+ *
+ * e.g. Nil != Cons(head, tail)
+ */
+ def injectivity(c1: SyntacticConstructor, c2: SyntacticConstructor) =
+ require(c1.tag != c2.tag, "The given constructors must be different.")
+
+ Lemma(!(c1.term1 === c2.term2)) {
+
+ // STEP 0: Caching
+ val tagTerm1: Term = c1.tagTerm
+ val tagTerm2: Term = c2.tagTerm
+
+ // STEP 1: Prove that the tags are different
+ val diffTag = have(!(tagTerm1 === tagTerm2)) subproof {
+
+ // STEP 1.1: Order the tags
+ val minTag: Int = Math.min(c1.tag, c2.tag)
+ val maxTag: Int = Math.max(c1.tag, c2.tag)
+
+ val start = have(tagTerm1 === tagTerm2 |- toTerm(maxTag) === toTerm(minTag)) by Restate
+
+ // STEP 1.2: Apply successor injectivity to both tags until one becomes 0
+ (1 to minTag).foldLeft(start)((fact, i) =>
+ val midMaxTag = toTerm(maxTag - i)
+ val midMinTag = toTerm(minTag - i)
+ have(successor(midMaxTag) === successor(midMinTag) |- midMaxTag === midMinTag) by Cut(
+ ADTThm.successorInjectivity of (n := midMaxTag, m := midMinTag),
+ ADTThm.equivalenceApply of (p1 := successor(midMaxTag) === successor(midMinTag), p2 := midMaxTag === midMinTag)
+ )
+ have(tagTerm1 === tagTerm2 |- midMaxTag === midMinTag) by Cut(fact, lastStep)
+ )
+
+ val chainInjectivity = thenHave(!(toTerm(maxTag - minTag) === emptySet) |- !(tagTerm1 === tagTerm2)) by Restate
+
+ // STEP 1.3: Conclude using the fact that 0 is not the successor of any number
+ have(!(toTerm(maxTag - minTag) === emptySet)) by Exact(ADTThm.zeroIsNotSucc)
+ have(thesis) by Cut(lastStep, chainInjectivity)
+ }
+
+ // STEP 2: Prove that the terms are different if the tags are different
+ have(c1.term1 === c2.term2 |- (tagTerm1 === tagTerm2) /\ (c1.subterm1 === c2.subterm2)) by Apply(ADTThm.equivalenceRevApply).on(
+ pairExtensionality of (a := tagTerm1, b := c1.subterm1, c := tagTerm2, d := c2.subterm2)
+ )
+ thenHave(!(tagTerm1 === tagTerm2) |- !(c1.term1 === c2.term2)) by Weakening
+
+ // STEP 3: Conclude
+ have(!(c1.term1 === c2.term2)) by Cut(diffTag, lastStep)
+ }
+
+ // *************************
+ // * INTRODUCTION FUNCTION *
+ // *************************
+
+ /**
+ * Formula describing whether the variables of a constructor belongs to their respective domain or s when they are self-referencing.
+ *
+ * @param c The considered constructor
+ * @param s The set of elements in which self-referencing variables of the constructor are.
+ */
+ private def constructorVarsInDomain(c: SyntacticConstructor, s: Term): Formula = wellTypedFormula(c.signature)(s)
+
+ /**
+ * Formula describing whether an element x is an instance of a specific constructor.
+ *
+ * @param c The constructor we want to check if x is an instance of
+ * @param x The element we want to check if it is an instance of c
+ * @param s The set of elements in which self-referencing arguments of the constructor are.
+ */
+ private def isConstructor(c: SyntacticConstructor, x: Term, s: Term): Formula =
+ existsSeq(c.variables2, wellTypedFormula(c.signature2)(s) /\ (x === c.term2))
+
+ /**
+ * Formula describing whether an element x is an instance of one of this ADT's constructors.
+ *
+ * @param x The element we want to check if it is an instance of some constructor.
+ * @param s The set of elements in which self-referencing arguments of the constructor are.
+ */
+ private def isConstructor(x: Term, s: Term): Formula = \/(constructors.map(c => isConstructor(c, x, s)))
+
+ /**
+ * The introduction (class) function applies this ADT's constructors to the argument to given to it.
+ * It then adds to elements of the resulting set to the one given in argument. For example, if all arguments of the
+ * constructors were self-referencing we would have:
+ *
+ * introductionFunction(s) = {y | y = c(x1, ..., xn) for some c ∈ constructors and x1, ..., xn ∈ s} ∪ s
+ *
+ * In order to avoid introducing a new symbol in the theory, we describe this function with a predicate.
+ *
+ * @param s the argument of this function, i.e. set of elements on which the constructors are applied
+ * @param y the element we want to check if it is in the image of s under the introduction function.
+ *
+ * @return a formula describing whether y ∈ introductionFunction(s)
+ *
+ * @note The existence of the image of the introduction function is guaranteed by the union and replacement axioms. Moreover, it is not necessary to compute the union with s. It however simplifies further proofs. See [[this.heightSuccessorStrong]] for a proof of the equivalence of the two definitions.
+ */
+ private def isInIntroductionFunctionImage(s: Term)(y: Term): Formula = isConstructor(y, s) \/ in(y, s)
+
+
+ /**
+ * Lemma --- The introduction function is monotonic with respect to set inclusion.
+ *
+ * `s ⊆ t |- introductionFunction(s) ⊆ introductionFunction(t)`
+ */
+ private val introductionFunctionMononotic = Lemma(subset(s, t) |- isInIntroductionFunctionImage(s)(x) ==> isInIntroductionFunctionImage(t)(x)) {
+ // In the rest of the proof we assume that s ⊆ t
+
+ // STEP 0: Caching predicates that are often used
+ val subsetST = subset(s, t)
+ val isConstructorXS = isConstructor(x, s)
+ val isConstructorXT = isConstructor(x, t)
+
+ // STEP 1: Prove x ∈ s implies x ∈ t
+ have(subsetST |- forall(z, in(z, s) ==> in(z, t))) by Apply(ADTThm.equivalenceApply of (p1 := subsetST)).on(subsetAxiom.asInstanceOf)
+ val subsetElimination = thenHave(subsetST |- in(z, s) ==> in(z, t)) by InstantiateForall(z)
+
+ // STEP 2: For each constructor, prove that if x is an instance of that constructor with self referencing arguments in s
+ // then it is also an instance of some constructor with self referencing arguments in t
+ val isConstructorXSImpliesT =
+ for c <- constructors yield
+ // STEP 2.0: Caching predicates that are often used
+ // TODO change identifier
+ val labelEq = x === c.term2
+ val isConstructorCXS = isConstructor(c, x, s)
+ val isConstructorCXT = isConstructor(c, x, t)
+ val varsWellTypedS = wellTypedFormula(c.signature2)(s)
+ val varsWellTypedT = wellTypedFormula(c.signature2)(t)
+
+ if c.arity == 0 then have((subsetST, isConstructorCXS) |- isConstructorXT) by Restate
+ else
+ // STEP 2.1: Prove that we can expand the domain of the (quantified) variables of the constructor
+ val andSeq =
+ for (v, ty) <- c.signature2 yield have((subsetST, varsWellTypedS) |- in(v, ty.getOrElse(t))) by Weakening(subsetElimination of (z := v))
+ val expandingDomain = have((subsetST, varsWellTypedS) |- varsWellTypedT) by RightAnd(andSeq: _*)
+ val weakeningLabelEq = have(labelEq |- labelEq) by Hypothesis
+ have((subsetST, varsWellTypedS, labelEq) |- varsWellTypedT /\ labelEq) by RightAnd(expandingDomain, weakeningLabelEq)
+
+ // STEP 2.2: Prove that x stays an instance of this constructor if we expand the domain of the variables
+ thenHave((subsetST, varsWellTypedS, labelEq) |- isConstructorCXT) by QuantifiersIntro(c.variables2)
+ thenHave((subsetST, varsWellTypedS /\ labelEq) |- isConstructorCXT) by LeftAnd
+ thenHave((subsetST, isConstructorCXS) |- isConstructorCXT) by QuantifiersIntro(c.variables2)
+
+ // STEP 2.3: Weaken the conclusion to some constructor instead of a specific one
+ thenHave((subsetST, isConstructorCXS) |- isConstructorXT) by Weakening
+
+ // STEP 3: Prove that this holds for any constructor
+ // ? Steps 2 and 3 can be merged and optimized through the repeated use of an external theorem like [[ADTHelperTheorems.unionPreimageMonotonic]]
+ if constructors.isEmpty then have((subsetST, isConstructorXS) |- isConstructorXT) by Restate
+ else have((subsetST, isConstructorXS) |- isConstructorXT) by LeftOr(isConstructorXSImpliesT: _*)
+
+ // STEP 4: Prove the thesis by showing that making the union with the function argument does not change the monotonicity
+ thenHave(subsetST |- isConstructorXS ==> isConstructorXT) by RightImplies
+ have(thesis) by Cut(lastStep, ADTThm.unionPreimageMonotonic of (P := lambda(s, isConstructorXS)))
+ }
+
+
+ /**
+ * Lemma --- Every constructor is in the image of the introduction function.
+ *
+ * `For every c ∈ constructors, xi ∈ s, ..., xj ∈ s |- c(x1, ..., xn) ∈ introductionFunction(s)`
+ */
+ private val constructorIsInIntroductionFunction = constructors
+ .map(c =>
+ // Caching
+ val constructorVarsInDomainCS = constructorVarsInDomain(c, s)
+
+ c -> Lemma(constructorVarsInDomainCS |- isInIntroductionFunctionImage(s)(c.term)) {
+
+ have(constructorVarsInDomainCS |- constructorVarsInDomainCS /\ (c.term === c.term)) by Restate
+
+ // Replace each variable on the LHS of the equality by a quantified variable and then introduce an existential quantifier
+ (c.variables2).foldRight((c.variables1, List[Variable]()))((v, acc) =>
+
+ // At each step remove a variable and add a quantified one
+ val oldVariables = acc._1.init
+ val newVariables = v :: acc._2
+ val vars = oldVariables ++ newVariables
+
+ thenHave(constructorVarsInDomainCS |- existsSeq(newVariables, wellTypedFormula(vars.zip(c.specification))(s) /\ (c.term(vars) === c.term))) by RightExists
+
+ (oldVariables, newVariables)
+ )
+
+ thenHave(constructorVarsInDomainCS |- isInIntroductionFunctionImage(s)(c.term)) by Weakening
+ }
+ )
+ .toMap
+
+ // **********************************
+ // * EXTENDED INTRODUCTION FUNCTION *
+ // **********************************
+
+ /**
+ * The extended introduction (class) function takes a function f as an argument instead of set.
+ * - If f is not empty, it calls the introduction function on the union of the ranges of the function. Since f will
+ * always be cumulative by assumption, this is equivalent as passing as argument the broadest set among the ranges of f.
+ * - If the function is empty, it returns the empty set.
+ *
+ * This class function is in a suited format to be used within the transfinite recursion theorem, which will be called to
+ * construct the height function.
+ *
+ * @see [[this.heightFunctionUniqueness]]
+ *
+ * @param f the function given as argument to the extended introduction function
+ * @param x the element we want to check if it is in the image of f under the extended introduction function
+ * @return a formula describing whether x ∈ extendedIntroductionFunction(f)
+ */
+ private def isInExtendedIntroductionFunctionImage(f: Term)(x: Term): Formula = !(f === emptySet) /\ isInIntroductionFunctionImage(unionRange(f))(x)
+
+ /**
+ * Lemma --- The extended introduction function is monotonic with respect to set inclusion.
+ *
+ * `f ⊆ g |- extendedIntroductionFunction(f) ⊆ extendedIntroductionFunction(g)`
+ */
+ private val extendedIntroductionFunctionMonotonic = Lemma(subset(f, g) |- isInExtendedIntroductionFunctionImage(f)(x) ==> isInExtendedIntroductionFunctionImage(g)(x)) {
+
+ // STEP 0: Caching
+ val introFunUnionRangeF = isInIntroductionFunctionImage(unionRange(f))(x)
+ val introFunUnionRangeG = isInIntroductionFunctionImage(unionRange(g))(x)
+
+ // STEP 1: Instantiate monotonicity of the introduction function for the union of the ranges of f and g
+ have(subset(f, g) |- introFunUnionRangeF ==> introFunUnionRangeG) by Cut(
+ ADTThm.unionRangeMonotonic,
+ introductionFunctionMononotic of (s := unionRange(f), t := unionRange(g))
+ )
+ val left = thenHave((subset(f, g), introFunUnionRangeF) |- introFunUnionRangeG) by Restate
+
+ // STEP 2: Conclude by applying the conjuction on both sides
+ have((subset(f, g), !(f === emptySet), introFunUnionRangeF) |- isInExtendedIntroductionFunctionImage(g)(x)) by RightAnd(left, ADTThm.subsetNotEmpty of (x := f, y := g))
+ }
+
+ // *******************
+ // * HEIGHT FUNCTION *
+ // *******************
+
+ /**
+ * The height function assigns to each natural number the set of elements of the ADT of that height or below.
+ * The set of terms with height 0 is empty. Non inductive constructors have height one.
+ * The height of an instance of an inductive constructor is the maximum height of its arguments plus one.
+ * The height function is guaranteed to exists and is unique.
+ *
+ * @see [[this.heightFunctionUniqueness]]
+ *
+ * @param g the function we want to know if it is the height function
+ *
+ * @return a formula that is true if and only if g is the height function
+ */
+ private def isTheHeightFunction(h: Term): Formula =
+ functional(h) /\ (relationDomain(h) === N) /\ forall(n, in(n, N) ==> forall(x, in(x, app(h, n)) <=> isInExtendedIntroductionFunctionImage(restrictedFunction(h, n))(x)))
+
+ // Caching
+ private val fIsTheHeightFunction: Formula = isTheHeightFunction(f)
+ private val hIsTheHeightFunction: Formula = isTheHeightFunction(h)
+
+ /**
+ * Lemma --- There exists a unique height function for this ADT.
+ *
+ * `∃!h. h = height`
+ *
+ * TODO: Prove this using transfinite recursion
+ */
+ private val heightFunUniqueness = Axiom(existsOne(h, hIsTheHeightFunction))
+
+ /**
+ * Lemma --- The height function exists.
+ *
+ * `∃h. h = height`
+ */
+ private val heightFunctionExistence = Lemma(exists(h, hIsTheHeightFunction)) {
+ have(thesis) by Apply(lisa.maths.Quantifiers.existsOneImpliesExists of (P := lambda(h, hIsTheHeightFunction))).on(heightFunUniqueness.asInstanceOf)
+ }
+
+ /**
+ * Lemma --- If two functions are the height function then they are the same.
+ *
+ * `f = height /\ h = height => f = h`
+ */
+ private val heightFunctionUniqueness2 = Lemma((fIsTheHeightFunction, hIsTheHeightFunction) |- f === h) {
+ have(thesis) by Cut(heightFunUniqueness, ADTThm.existsOneUniqueness of (P := lambda(h, hIsTheHeightFunction), x := f, y := h))
+ }
+
+ /**
+ * Lemma --- The height function is not empty.
+ *
+ * `height ≠ ∅`
+ */
+ private val heightFunctionNonEmpty = Lemma(hIsTheHeightFunction |- !(h === emptySet)) {
+ // The proof goes by contradiction. If the height function is empty then its domain is empty as well.
+ // This would imply that the set of natural numbers is empty, which is a contradiction.
+ have(N === emptySet |- ()) by Restate.from(ADTThm.natNotEmpty)
+ thenHave((relationDomain(h) === emptySet, relationDomain(h) === N, relationDomain(h) === relationDomain(h)) |- ()) by LeftSubstEq.withParametersSimple(
+ List((relationDomain(h), emptySet), (relationDomain(h), N)),
+ lambda((x, y), y === x)
+ )
+ thenHave((relationDomain(h) === N, relationDomain(h) === relationDomain(h)) |- !(relationDomain(h) === emptySet)) by RightNot
+ have(thesis) by Apply(ADTThm.nonEmptyDomain).on(lastStep)
+ }
+
+ /**
+ * Lemma --- The set of elements of height n or below is the image of the extended introduction function under the height
+ * function restricted to n (consequence of transfinite recursion).
+ *
+ * `height(n) = extendedIntroductionFunction(height | n)`
+ */
+ private val heightApplication = Lemma((hIsTheHeightFunction, in(n, N)) |- in(x, app(h, n)) <=> isInExtendedIntroductionFunctionImage(restrictedFunction(h, n))(x)) {
+
+ // Caching
+ val extendedIntroFunRestrictedFunM = isInExtendedIntroductionFunctionImage(restrictedFunction(h, n))(x)
+ val heightFunApplicationDef = forall(n, in(n, N) ==> forall(x, in(x, app(h, n)) <=> extendedIntroFunRestrictedFunM))
+
+ // Nothing fancy, just instantiations and restates
+ have(heightFunApplicationDef |- heightFunApplicationDef) by Hypothesis
+ thenHave(heightFunApplicationDef |- in(n, N) ==> forall(x, in(x, app(h, n)) <=> extendedIntroFunRestrictedFunM)) by InstantiateForall(n)
+ thenHave((heightFunApplicationDef, in(n, N)) |- forall(x, in(x, app(h, n)) <=> extendedIntroFunRestrictedFunM)) by Restate
+ thenHave((heightFunApplicationDef, in(n, N)) |- in(x, app(h, n)) <=> extendedIntroFunRestrictedFunM) by InstantiateForall(x)
+ thenHave(thesis) by Weakening
+ }
+
+ /**
+ * Lemma --- The height function is monotonic
+ *
+ * `n <= m => height(n) ⊆ height(m)`
+ *
+ * TODO: Try to pull out
+ */
+ private val heightMonotonic = Lemma((hIsTheHeightFunction, in(n, N), subset(m, n)) |- subset(app(h, m), app(h, n))) {
+
+ // STEP 0: Caching
+ val extendedIntroFunRestrictedFunM = isInExtendedIntroductionFunctionImage(restrictedFunction(h, m))(x)
+
+ // STEP 1: Unfold the definition of height(m)
+ have((hIsTheHeightFunction, in(n, N), subset(m, n)) |- in(x, app(h, m)) <=> extendedIntroFunRestrictedFunM) by Apply(heightApplication).on(ADTThm.subsetIsNat.asInstanceOf)
+ val unfoldHeightApplicationM = have((hIsTheHeightFunction, in(n, N), subset(m, n), in(x, app(h, m))) |- extendedIntroFunRestrictedFunM) by Cut(
+ lastStep,
+ ADTThm.equivalenceRevApply of (p1 := in(x, app(h, m)), p2 := extendedIntroFunRestrictedFunM)
+ )
+
+ // STEP 2: Use the monotonicity of the extended introduction function
+ have(subset(m, n) |- extendedIntroFunRestrictedFunM ==> isInExtendedIntroductionFunctionImage(restrictedFunction(h, n))(x)) by Cut(
+ ADTThm.restrictedFunctionDomainMonotonic of (x := m, y := n, f := h),
+ extendedIntroductionFunctionMonotonic of (f := restrictedFunction(h, m), g := restrictedFunction(h, n))
+ )
+ have((hIsTheHeightFunction, in(n, N), subset(m, n), extendedIntroFunRestrictedFunM) |- in(x, app(h, n))) by Apply(ADTThm.equivalenceRevApply).on(lastStep, heightApplication.asInstanceOf)
+
+ // STEP 3: Fold the definition of subset
+ have((hIsTheHeightFunction, in(n, N), subset(m, n), in(x, app(h, m))) |- in(x, app(h, n))) by Cut(unfoldHeightApplicationM, lastStep)
+ thenHave((hIsTheHeightFunction, in(n, N), subset(m, n)) |- in(x, app(h, m)) ==> in(x, app(h, n))) by RightImplies
+ thenHave((hIsTheHeightFunction, in(n, N), subset(m, n)) |- forall(x, in(x, app(h, m)) ==> in(x, app(h, n)))) by RightForall
+ have(thesis) by Apply(ADTThm.equivalenceRevApply).on(lastStep, subsetAxiom.asInstanceOf)
+ }
+
+ /**
+ * Lemma --- There is no element of height 0 in the ADT.
+ *
+ * `!∃x ∈ adt. height(x) = 0`
+ */
+ private val heightZero = Lemma(hIsTheHeightFunction |- !in(x, app(h, emptySet))) {
+
+ // This is due to the fact that the extended introduction function is the empty set when the function is empty
+ // (which happens when the height is set to 0).
+ have(hIsTheHeightFunction |- in(x, app(h, emptySet)) <=> isInExtendedIntroductionFunctionImage(restrictedFunction(h, emptySet))(x)) by Cut(ADTThm.zeroIsNat, heightApplication of (n := emptySet))
+ thenHave((restrictedFunction(h, emptySet) === emptySet, hIsTheHeightFunction) |- !in(x, app(h, emptySet))) by
+ RightSubstEq.withParametersSimple(
+ List((restrictedFunction(h, emptySet), emptySet)),
+ lambda(s, in(x, app(h, emptySet)) <=> isInExtendedIntroductionFunctionImage(s)(x))
+ )
+ have(thesis) by Cut(ADTThm.restrictedFunctionEmptyDomain, lastStep)
+ }
+
+ /**
+ * Lemma --- The set of elements of height n + 1 is the set of elements of height n to which the introduction function is applied.
+ *
+ * `height(n + 1) = introductionFunction(height(n))`
+ */
+ private val heightSuccessorWeak = Lemma((hIsTheHeightFunction, in(n, N)) |- in(x, app(h, successor(n))) <=> isInIntroductionFunctionImage(app(h, n))(x)) {
+
+ // STEP 1: Prove that the restriction of height to n + 1 is not empty
+ val restrHeightNotEmpty: Formula = !(restrictedFunction(h, successor(n)) === emptySet)
+ have(!(h === emptySet) |- restrHeightNotEmpty) by Cut(ADTThm.zeroIsNotSucc, ADTThm.restrictedFunctionNotEmpty of (d := successor(n)))
+ val restrHeightNotEmptyLemma = have(hIsTheHeightFunction |- restrHeightNotEmpty) by Cut(heightFunctionNonEmpty, lastStep)
+
+ // STEP 2: Use the fact that if the function is cumulative then ∪ range(height | n + 1) = height(n) to conclude the proof
+ have((hIsTheHeightFunction, in(n, N)) |- subset(m, n) ==> subset(app(h, m), app(h, n))) by RightImplies(heightMonotonic)
+ thenHave((hIsTheHeightFunction, in(n, N)) |- forall(m, subset(m, n) ==> subset(app(h, m), app(h, n)))) by RightForall
+ val unionRangeRestr = have((hIsTheHeightFunction, in(n, N)) |- unionRange(restrictedFunction(h, successor(n))) === app(h, n)) by Apply(ADTThm.unionRangeCumulativeRestrictedFunction).on(lastStep)
+
+ have((hIsTheHeightFunction, in(n, N)) |- in(x, app(h, successor(n))) <=> isInExtendedIntroductionFunctionImage(restrictedFunction(h, successor(n)))(x)) by Apply(heightApplication).on(
+ ADTThm.equivalenceApply of (p1 := in(n, N)),
+ ADTThm.successorIsNat.asInstanceOf
+ )
+
+ thenHave(
+ (hIsTheHeightFunction, in(n, N), unionRange(restrictedFunction(h, successor(n))) === app(h, n)) |-
+ in(x, app(h, successor(n))) <=> restrHeightNotEmpty /\ isInIntroductionFunctionImage(app(h, n))(x)
+ ) by
+ RightSubstEq.withParametersSimple(
+ List((unionRange(restrictedFunction(h, successor(n))), app(h, n))),
+ lambda(s, in(x, app(h, successor(n))) <=> (restrHeightNotEmpty /\ isInIntroductionFunctionImage(s)(x)))
+ )
+
+ have((hIsTheHeightFunction, in(n, N)) |- in(x, app(h, successor(n))) <=> restrHeightNotEmpty /\ isInIntroductionFunctionImage(app(h, n))(x)) by Cut(unionRangeRestr, lastStep)
+
+ have((hIsTheHeightFunction, in(n, N), restrHeightNotEmpty) |- in(x, app(h, successor(n))) <=> isInIntroductionFunctionImage(app(h, n))(x)) by Apply(ADTThm.equivalenceAnd of (p2 := restrHeightNotEmpty))
+ .on(lastStep)
+
+ have(thesis) by Cut(restrHeightNotEmptyLemma, lastStep)
+ }
+
+ // ********
+ // * TERM *
+ // ********
+
+ /**
+ * Formula describing this ADT's term, i.e. the set of all its instances.
+ * It equal to the union of all the terms that have a height.
+ *
+ * `adt = ∪ height(n) = {x | ∃n ∈ N. x ∈ height(n)}`
+ *
+ * @param adt the set chracterizing this ADT
+ */
+ private def termDefinition(adt: Term): Formula = forall(t, in(t, adt) <=> forall(h, hIsTheHeightFunction ==> in(t, unionRange(h))))
+
+ /**
+ * Lemma --- There exists a unique set satisfying the definition of this ADT
+ *
+ * `∃!z. z = ADT
+ */
+ private val termExistence = Lemma(existsOne(z, termDefinition(z))) {
+
+ // STEP 0: Caching
+ val termDefinitionRight = forall(h, hIsTheHeightFunction ==> in(t, unionRange(h)))
+ val inUnionRangeF = in(t, unionRange(f))
+
+ // STEP 1: Prove that there exists a term satisfying the definition of this ADT.
+ // Specifically, this term is the union of all the terms with a height.
+ have(exists(z, termDefinition(z))) subproof {
+
+ // STEP 1.1: Prove the forward implication of the definition, using the uniqueness of the height function
+ have(inUnionRangeF |- inUnionRangeF) by Hypothesis
+ thenHave((f === h, inUnionRangeF) |- in(t, unionRange(h))) by RightSubstEq.withParametersSimple(
+ List((f, h)),
+ lambda(f, inUnionRangeF)
+ )
+ have((fIsTheHeightFunction, hIsTheHeightFunction, inUnionRangeF) |- in(t, unionRange(h))) by Cut(heightFunctionUniqueness2, lastStep)
+ thenHave((fIsTheHeightFunction, inUnionRangeF) |- hIsTheHeightFunction ==> in(t, unionRange(h))) by RightImplies
+ thenHave((fIsTheHeightFunction, inUnionRangeF) |- termDefinitionRight) by RightForall
+ val forward = thenHave(fIsTheHeightFunction |- inUnionRangeF ==> termDefinitionRight) by RightImplies
+
+ // STEP 1.2: Prove the backward implication of the definition
+ have(termDefinitionRight |- termDefinitionRight) by Hypothesis
+ thenHave(termDefinitionRight |- fIsTheHeightFunction ==> inUnionRangeF) by InstantiateForall(f)
+ val backward = thenHave(fIsTheHeightFunction |- termDefinitionRight ==> inUnionRangeF) by Restate
+
+ // STEP 1.3: Use the existence of the height function to prove the existence of this ADT
+ have(fIsTheHeightFunction |- inUnionRangeF <=> termDefinitionRight) by RightIff(forward, backward)
+ thenHave(fIsTheHeightFunction |- forall(t, inUnionRangeF <=> termDefinitionRight)) by RightForall
+
+ thenHave(fIsTheHeightFunction |- exists(z, forall(t, in(t, z) <=> termDefinitionRight))) by RightExists
+ thenHave(exists(f, fIsTheHeightFunction) |- exists(z, forall(t, in(t, z) <=> termDefinitionRight))) by LeftExists
+ have(thesis) by Cut(heightFunctionExistence, lastStep)
+ }
+
+ // STEP 2: Conclude using the extension by definition
+
+ have(thesis) by Cut(lastStep, uniqueByExtension of (schemPred := lambda(t, termDefinitionRight)))
+ }
+
+ /**
+ * Class function defining the ADT. Takes as parameters the type variables of the ADT and return the set of all its instances.
+ */
+ val polymorphicTerm = FunctionDefinition[N](name, line.value, file.value)(typeVariablesSeq, z, termDefinition(z), termExistence).label
+
+ /**
+ * The set of all instances of the ADT where the type variables are not instantiated (i.e. are kept variable).
+ */
+ val term = polymorphicTerm.applySeq(typeVariablesSeq)
+
+ /**
+ * Definition of this ADT's term.
+ */
+ private val termDefinition: Formula = termDefinition(term)
+
+ /**
+ * Lemma --- This ADT satisfies its definition.
+ *
+ * `adt = ∪ height(n)`
+ */
+ private val termSatisfiesDefinition = Lemma(termDefinition) {
+ have(thesis) by InstantiateForall(term)(polymorphicTerm.definition)
+ }
+
+ // *************************
+ // * TYPING / INTRODUCTION *
+ // *************************
+
+ /**
+ * Lemma --- Every element of this ADT has a height. Conversely, if an element has a height, it is in this ADT.
+ *
+ * ` x ∈ ADT <=> ∃n ∈ N. x ∈ height(n)`
+ *
+ * TODO: Split into two lemmas
+ */
+ private val termHasHeight = Lemma(hIsTheHeightFunction |- in(x, term) <=> ∃(n, in(n, N) /\ in(x, app(h, n)))) {
+
+ // STEP 0 : Instantiate the definition of this ADT and recover the forward and backward implications
+ val termDefinition = have(in(x, term) <=> forall(h, hIsTheHeightFunction ==> in(x, unionRange(h)))) by InstantiateForall(x)(termSatisfiesDefinition)
+ val termDefinitionForward = have(in(x, term) |- forall(h, hIsTheHeightFunction ==> in(x, unionRange(h)))) by Cut(
+ termDefinition,
+ ADTThm.equivalenceApply of (p1 := in(x, term), p2 := forall(h, hIsTheHeightFunction ==> in(x, unionRange(h))))
+ )
+ val termDefinitionBackward = have(forall(h, hIsTheHeightFunction ==> in(x, unionRange(h))) |- in(x, term)) by Cut(
+ termDefinition,
+ ADTThm.equivalenceRevApply of (p2 := in(x, term), p1 := forall(h, hIsTheHeightFunction ==> in(x, unionRange(h))))
+ )
+
+ // STEP 1 : Prove that an element is in this ADT if and only if it is in one of the images of the height function.
+ have(hIsTheHeightFunction |- in(x, term) <=> in(x, unionRange(h))) subproof {
+
+ // STEP 1.1 : Forward implication
+ have(forall(h, hIsTheHeightFunction ==> in(x, unionRange(h))) |- forall(h, hIsTheHeightFunction ==> in(x, unionRange(h)))) by Hypothesis
+ thenHave(forall(h, hIsTheHeightFunction ==> in(x, unionRange(h))) |- hIsTheHeightFunction ==> in(x, unionRange(h))) by InstantiateForall(h)
+ thenHave((forall(h, hIsTheHeightFunction ==> in(x, unionRange(h))), hIsTheHeightFunction) |- in(x, unionRange(h))) by Restate
+
+ val forward = have(hIsTheHeightFunction |- in(x, term) ==> in(x, unionRange(h))) by Apply(lastStep).on(termDefinitionForward)
+
+ // STEP 1.2 : Backward implication, follows from uniqueness of the height function
+ have(in(x, unionRange(h)) |- in(x, unionRange(h))) by Hypothesis
+ thenHave((f === h, in(x, unionRange(h))) |- in(x, unionRange(f))) by RightSubstEq.withParametersSimple(List((f, h)), lambda(h, in(x, unionRange(h))))
+ have((fIsTheHeightFunction, hIsTheHeightFunction, in(x, unionRange(h))) |- in(x, unionRange(f))) by Cut(heightFunctionUniqueness2, lastStep)
+ thenHave((hIsTheHeightFunction, in(x, unionRange(h))) |- fIsTheHeightFunction ==> in(x, unionRange(f))) by RightImplies
+ thenHave((hIsTheHeightFunction, in(x, unionRange(h))) |- forall(f, fIsTheHeightFunction ==> in(x, unionRange(f)))) by RightForall
+ have((hIsTheHeightFunction, in(x, unionRange(h))) |- in(x, term)) by Cut(lastStep, termDefinitionBackward)
+ val backward = thenHave(hIsTheHeightFunction |- in(x, unionRange(h)) ==> in(x, term)) by RightImplies
+
+ have(thesis) by RightIff(forward, backward)
+ }
+
+ // STEP 2: Conclude by instantiating the union range membership lemma
+ have(hIsTheHeightFunction |- in(x, term) <=> ∃(n, in(n, relationDomain(h)) /\ in(x, app(h, n)))) by Apply(ADTThm.equivalenceRewriting).on(ADTThm.unionRangeMembership.asInstanceOf, lastStep)
+
+ thenHave((hIsTheHeightFunction, relationDomain(h) === N) |- in(x, term) <=> ∃(n, in(n, N) /\ in(x, app(h, n)))) by RightSubstEq.withParametersSimple(
+ List((relationDomain(h), N)),
+ lambda(z, in(x, term) <=> ∃(n, in(n, z) /\ in(x, app(h, n))))
+ )
+ }
+
+ /**
+ * Lemma --- Every element of this ADT has a height. Conversely, if an element has a height, it is in this ADT.
+ *
+ * ` xi, ..., xj ∈ ADT <=> ∃n ∈ N. xi, ..., xj ∈ height(n)`
+ *
+ * TODO: Work this out
+ * TODO: Split into two lemmas
+ */
+ private val termsHaveHeight = constructors
+ .map(c =>
+ c -> Lemma(hIsTheHeightFunction |- (constructorVarsInDomain(c, term) <=> ∃(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n))))) {
+
+ if c.variables.isEmpty then have(thesis) by Weakening(ADTThm.existsNat)
+ else
+
+ // STEP 1: Backward implication
+
+ val backward = have(hIsTheHeightFunction |- ∃(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) ==> constructorVarsInDomain(c, term)) subproof {
+ val andSeq = for (v, ty) <- c.signature yield ty match
+ case Self =>
+ val termHasHeightBackward = have((hIsTheHeightFunction, exists(n, in(n, N) /\ in(v, app(h, n)))) |- in(v, term)) by Cut(
+ termHasHeight of (x := v),
+ ADTThm.equivalenceRevApply of (p1 := ∃(n, in(n, N) /\ in(v, app(h, n))), p2 := in(v, term))
+ )
+
+ have((in(n, N) /\ in(v, app(h, n))) |- in(n, N) /\ in(v, app(h, n))) by Restate
+ thenHave((in(n, N) /\ in(v, app(h, n))) |- exists(n, in(n, N) /\ in(v, app(h, n)))) by RightExists
+ have((hIsTheHeightFunction, in(n, N) /\ in(v, app(h, n))) |- in(v, term)) by Cut(lastStep, termHasHeightBackward)
+ thenHave((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- in(v, term)) by Weakening
+ case GroundType(t) =>
+ have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- in(v, t)) by Restate
+
+ have((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- constructorVarsInDomain(c, term)) by RightAnd(andSeq: _*)
+ thenHave((hIsTheHeightFunction, exists(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))) |- constructorVarsInDomain(c, term)) by LeftExists
+ }
+
+ // STEP 2: Forward implication
+
+ val forward = have(hIsTheHeightFunction |- constructorVarsInDomain(c, term) ==> ∃(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))) subproof {
+ val nSeq: Seq[Variable] = (0 until c.variables.size).map(i => Variable(s"n$i"))
+ val max = if c.arity == 0 then emptySet else nSeq.reduce[Term](setUnion(_, _))
+
+ val maxInN = have(/\(nSeq.map(n => in(n, N))) |- in(max, N)) by Sorry
+
+ val andSeq = for ((v, ty), ni) <- c.signature.zip(nSeq) yield
+ val niInMax = have(subset(ni, max)) by Sorry
+
+ ty match
+ case Self =>
+ have((hIsTheHeightFunction, in(max, N), subset(ni, max)) |- subset(app(h, ni), app(h, max))) by Restate.from(heightMonotonic of (m := ni, n := max))
+ have((hIsTheHeightFunction, /\(nSeq.map(n => in(n, N)))) |- subset(app(h, ni), app(h, max))) by Sorry // Apply(lastStep).on(Seq(maxInN, niInMax), excluding = nSeq)
+ have((hIsTheHeightFunction, /\(nSeq.map(n => in(n, N)))) |- forall(z, in(z, app(h, ni)) ==> in(z, app(h, max)))) by Apply(ADTThm.equivalenceApply)
+ .on(Seq(lastStep, subsetAxiom), excluding = nSeq)
+ thenHave((hIsTheHeightFunction, /\(nSeq.map(n => in(n, N)))) |- in(v, app(h, ni)) ==> in(v, app(h, max))) by InstantiateForall(v)
+ thenHave((hIsTheHeightFunction, /\(nSeq.map(n => in(n, N))), in(v, app(h, ni))) |- in(v, app(h, max))) by Restate
+ case GroundType(t) =>
+ have((/\(nSeq.map(n => in(n, N))), hIsTheHeightFunction, in(v, t)) |- in(v, t)) by Restate
+
+ have((/\(nSeq.map(n => in(n, N))), hIsTheHeightFunction, in(v, ty.getOrElse(app(h, ni)))) |- in(max, N) /\ in(v, ty.getOrElse(app(h, max)))) by RightAnd(maxInN, lastStep)
+ thenHave(nSeq.map(n => in(n, N) /\ in(v, ty.getOrElse(app(h, n)))).toSet + hIsTheHeightFunction |- in(max, N) /\ in(v, ty.getOrElse(app(h, max)))) by Weakening
+ thenHave(nSeq.map(n => in(n, N) /\ in(v, ty.getOrElse(app(h, n)))).toSet + hIsTheHeightFunction |- ∃(n, in(n, N) /\ in(v, ty.getOrElse(app(h, n))))) by RightExists
+
+ sorry
+ }
+
+ // STEP 3: Conclude
+ have(thesis) by RightIff(forward, backward)
+ }
+ )
+ .toMap
+
+ /**
+ * Lemma --- If all inductive arguments of a constructor have height below n then the instance of
+ * this constructor has height below n + 1.
+ *
+ * ` xi, ..., xj ∈ height(n) |- c(x1, ..., xn) ∈ height(n + 1)`
+ */
+ private val heightConstructor = constructors
+ .map(c =>
+ c -> Lemma((hIsTheHeightFunction, in(n, N), constructorVarsInDomain(c, app(h, n))) |- in(c.term, app(h, successor(n)))) {
+
+ // Caching
+ val constructorInIntroFunHeight = isInIntroductionFunctionImage(app(h, n))(c.term)
+
+ // Chaining the lemma on the elements of height n + 1 and the one on constructors being in the image of the introduction function
+ have((hIsTheHeightFunction, in(n, N), constructorInIntroFunHeight) |- in(c.term, app(h, successor(n)))) by Cut(
+ heightSuccessorWeak of (x := c.term),
+ ADTThm.equivalenceRevApply of (p1 := constructorInIntroFunHeight, p2 := in(c.term, app(h, successor(n))))
+ )
+ have((hIsTheHeightFunction, in(n, N), constructorVarsInDomain(c, app(h, n))) |- in(c.term, app(h, successor(n)))) by Cut(constructorIsInIntroductionFunction(c) of (s := app(h, n)), lastStep)
+ }
+ )
+ .toMap
+
+ /**
+ * Lemma --- If all inductive arguments of a constructor are in this ADT, and the non inductive ones in their respective domain,
+ * then the instance of this constructor is in this ADT as well. Also known as introduction rules.
+ *
+ * ` xi, ..., xj ∈ ADT |- c(x1, ..., xn) ∈ ADT`
+ */
+ val intro = constructors
+ .map(c => {
+ c ->
+ Lemma(simplify(constructorVarsInDomain(c, term)) |- simplify(in(c.term, term))) {
+ // STEP 0: Instantiate the forward direction of termsHaveHeight.
+ val termsHaveHeightForward = have((hIsTheHeightFunction, constructorVarsInDomain(c, term)) |- ∃(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))) by Cut(
+ termsHaveHeight(c),
+ ADTThm.equivalenceApply of (p1 := constructorVarsInDomain(c, term), p2 := exists(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n))))
+ )
+
+ // STEP 1: Prove that if an instance of a constructor has height n + 1 then it is in this ADT.
+ val left = have(in(n, N) |- in(successor(n), N)) by Cut(ADTThm.successorIsNat, ADTThm.equivalenceApply of (p1 := in(n, N), p2 := in(successor(n), N)))
+ val right = have(in(c.term, app(h, successor(n))) |- in(c.term, app(h, successor(n)))) by Hypothesis
+ have((in(n, N), in(c.term, app(h, successor(n)))) |- in(successor(n), N) /\ in(c.term, app(h, successor(n)))) by RightAnd(left, right)
+ thenHave((in(n, N), in(c.term, app(h, successor(n)))) |- exists(m, in(m, N) /\ in(c.term, app(h, m)))) by RightExists
+ have((hIsTheHeightFunction, in(n, N), in(c.term, app(h, successor(n)))) |- in(c.term, term)) by Apply(ADTThm.equivalenceRevApply).on(lastStep, termHasHeight.asInstanceOf)
+
+ // STEP 2: Prove that if the inductive arguments of the constructor have height then the instance of the constructor is in the ADT.
+ have((hIsTheHeightFunction, in(n, N), constructorVarsInDomain(c, app(h, n))) |- in(c.term, term)) by Cut(heightConstructor(c), lastStep)
+
+ // STEP 3: Prove that if the inductive arguments of the constructor are in the ADT then they have a height and therefore
+ // the instance of the constructor is in the ADT.
+ thenHave((hIsTheHeightFunction, in(n, N) /\ constructorVarsInDomain(c, app(h, n))) |- in(c.term, term)) by LeftAnd
+ thenHave((hIsTheHeightFunction, exists(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))) |- in(c.term, term)) by LeftExists
+ have((hIsTheHeightFunction, constructorVarsInDomain(c, term)) |- in(c.term, term)) by Cut(termsHaveHeightForward, lastStep)
+
+ // STEP 4: Remove lingering assumptions
+ thenHave((exists(h, hIsTheHeightFunction), constructorVarsInDomain(c, term)) |- in(c.term, term)) by LeftExists
+ have(constructorVarsInDomain(c, term) |- in(c.term, term)) by Cut(heightFunctionExistence, lastStep)
+ }
+ })
+ .toMap
+
+ // ************************
+ // * STRUCTURAL INDUCTION *
+ // ************************
+
+ /**
+ * Lemma --- An element has height n + 1 if and only if it is the instance of some constructor with inductive arguments of height n.
+ *
+ * ` x ∈ height(n + 1) <=> x = c(x1, ..., xn) for some c and xi, ..., xj ∈ height(n)`
+ */
+ private lazy val heightSuccessorStrong = Lemma((hIsTheHeightFunction, in(n, N)) |- in(x, app(h, successor(n))) <=> isConstructor(x, app(h, n))) {
+ val forward = have((hIsTheHeightFunction, in(n, N)) |- isInIntroductionFunctionImage(app(h, n))(x) ==> isConstructor(x, app(h, n))) subproof {
+
+ def inductionFormula(n: Term): Formula = isInIntroductionFunctionImage(app(h, n))(x) ==> isConstructor(x, app(h, n))
+ val inductionFormulaN: Formula = inductionFormula(n)
+ val inductionFormulaSuccN: Formula = inductionFormula(successor(n))
+
+ // STEP 1.1 : Base case
+ val isContructorXHEmptySet = isConstructor(x, app(h, emptySet))
+ val baseCaseLeft = have(isContructorXHEmptySet |- isContructorXHEmptySet) by Hypothesis
+ val baseCaseRight = have((hIsTheHeightFunction, in(x, app(h, emptySet))) |- ()) by Restate.from(heightZero)
+ have((hIsTheHeightFunction, isInIntroductionFunctionImage(app(h, emptySet))(x)) |- isContructorXHEmptySet) by LeftOr(baseCaseLeft, baseCaseRight)
+ thenHave(hIsTheHeightFunction |- isInIntroductionFunctionImage(app(h, emptySet))(x) ==> isContructorXHEmptySet) by RightImplies
+ val inductiveCaseRemaining = have((hIsTheHeightFunction, forall(n, in(n, N) ==> (inductionFormulaN ==> inductionFormulaSuccN))) |- forall(n, in(n, N) ==> inductionFormulaN)) by Cut(
+ lastStep,
+ ADTThm.natInduction of (P := lambda(n, inductionFormulaN))
+ )
+
+ // STEP 1.2: Unfolding the definition of subset
+ have(subset(app(h, n), app(h, successor(n))) |- forall(z, in(z, app(h, n)) ==> in(z, app(h, successor(n))))) by Cut(
+ subsetAxiom of (x := app(h, n), y := app(h, successor(n))),
+ ADTThm.equivalenceApply of (p1 := subset(app(h, n), app(h, successor(n))), p2 := forall(z, in(z, app(h, n)) ==> in(z, app(h, successor(n)))))
+ )
+ val subsetElimination = thenHave(subset(app(h, n), app(h, successor(n))) |- in(y, app(h, n)) ==> in(y, app(h, successor(n)))) by InstantiateForall(y)
+
+ // STEP 1.3 : Use monotonicity to prove that y ∈ height(n) => y ∈ height(n + 1)
+ have(in(n, N) |- in(successor(n), N)) by Cut(ADTThm.successorIsNat, ADTThm.equivalenceApply of (p1 := in(n, N), p2 := in(successor(n), N)))
+ have((hIsTheHeightFunction, in(n, N), subset(n, successor(n))) |- subset(app(h, n), app(h, successor(n)))) by Cut(lastStep, heightMonotonic of (n := successor(n), m := n))
+ have((hIsTheHeightFunction, in(n, N)) |- subset(app(h, n), app(h, successor(n)))) by Cut(ADTThm.subsetSuccessor, lastStep)
+ val liftHeight = have((hIsTheHeightFunction, in(n, N)) |- in(y, app(h, n)) ==> in(y, app(h, successor(n)))) by Cut(lastStep, subsetElimination)
+
+ // STEP 1.4 : Generalize the above result to show that if for some c, x = c(x1, ..., xn) with xi, ..., xj ∈ height(n)
+ // then for some c', x = c'(x1, ..., xn) with xi, ..., xj ∈ height(n + 1).
+
+ // Caching
+ val isConstructorXHN = isConstructor(x, app(h, n))
+ val isConstructorXHSuccN = isConstructor(x, app(h, successor(n)))
+ val liftConstructorHeight =
+ if constructors.size == 0 then have((hIsTheHeightFunction, in(n, N), isConstructorXHN) |- isConstructorXHSuccN) by Restate
+ else
+ val liftConstructorHeightOrSequence =
+ for c <- constructors yield
+
+ // Caching
+ val isConstructorCXHN = isConstructor(c, x, app(h, n))
+ val isConstructorCXHSuccN = isConstructor(c, x, app(h, successor(n)))
+ val constructorVarsInHN = constructorVarsInDomain(c, app(h, n))
+ val constructorVarsInHSuccN = constructorVarsInDomain(c, app(h, successor(n)))
+
+ if c.arity == 0 then have((hIsTheHeightFunction, in(n, N), isConstructorCXHN) |- isConstructorCXHSuccN) by Restate
+ else
+ val liftHeightAndSequence =
+ for (v, ty) <- c.signature
+ yield have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- in(v, ty.getOrElse(app(h, successor(n))))) by Weakening(liftHeight of (y := v))
+
+ val left = have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInHSuccN) by RightAnd(liftHeightAndSequence: _*)
+ val right = have(x === c.term |- x === c.term) by Hypothesis
+
+ have((hIsTheHeightFunction, in(n, N), constructorVarsInHN, (x === c.term)) |- constructorVarsInHSuccN /\ (x === c.term )) by RightAnd(
+ left,
+ right
+ )
+ thenHave((hIsTheHeightFunction, in(n, N), constructorVarsInHN /\ (x === c.term)) |- constructorVarsInHSuccN /\ (x === c.term)) by LeftAnd
+ thenHave((hIsTheHeightFunction, in(n, N), constructorVarsInHN /\ (x === c.term)) |- isConstructorCXHSuccN) by QuantifiersIntro(c.variables)
+ thenHave((hIsTheHeightFunction, in(n, N), isConstructorCXHN) |- isConstructorCXHSuccN) by QuantifiersIntro(c.variables)
+
+ thenHave((hIsTheHeightFunction, in(n, N), isConstructorCXHN) |- isConstructorXHSuccN) by Weakening
+
+ have((hIsTheHeightFunction, in(n, N), isConstructorXHN) |- isConstructorXHSuccN) by LeftOr(liftConstructorHeightOrSequence: _*)
+
+ // STEP 1.5: Show that x ∈ introductionFunction(height(n + 1)) => for some c, x = c(x1, ..., xn)
+ // with xi, ..., xj ∈ height(n + 1).
+ val heightSuccessorWeakForward = have((hIsTheHeightFunction, in(n, N), in(x, app(h, successor(n)))) |- isInIntroductionFunctionImage(app(h, n))(x)) by Cut(
+ heightSuccessorWeak,
+ ADTThm.equivalenceApply of (p1 := in(x, app(h, successor(n))), p2 := isInIntroductionFunctionImage(app(h, n))(x))
+ )
+ have((inductionFormulaN, isInIntroductionFunctionImage(app(h, n))(x)) |- isConstructorXHN) by Restate
+ have((hIsTheHeightFunction, in(n, N), in(x, app(h, successor(n))), inductionFormulaN) |- isConstructorXHN) by Cut(heightSuccessorWeakForward, lastStep)
+ val right = have((hIsTheHeightFunction, in(n, N), in(x, app(h, successor(n))), inductionFormulaN) |- isConstructorXHSuccN) by Cut(lastStep, liftConstructorHeight)
+ val left = have(isConstructorXHSuccN |- isConstructorXHSuccN) by Hypothesis
+ have((hIsTheHeightFunction, in(n, N), inductionFormulaN, isInIntroductionFunctionImage(app(h, successor(n)))(x)) |- isConstructorXHSuccN) by LeftOr(left, right)
+
+ // STEP 1.6: Conclude
+ thenHave((hIsTheHeightFunction, in(n, N), inductionFormulaN) |- inductionFormulaSuccN) by RightImplies
+ thenHave((hIsTheHeightFunction, in(n, N)) |- inductionFormulaN ==> inductionFormulaSuccN) by RightImplies
+ thenHave(hIsTheHeightFunction |- in(n, N) ==> (inductionFormulaN ==> inductionFormulaSuccN)) by RightImplies
+ thenHave(hIsTheHeightFunction |- forall(n, in(n, N) ==> (inductionFormulaN ==> inductionFormulaSuccN))) by RightForall
+ have(hIsTheHeightFunction |- forall(n, in(n, N) ==> inductionFormulaN)) by Cut(lastStep, inductiveCaseRemaining)
+ thenHave(hIsTheHeightFunction |- in(n, N) ==> inductionFormulaN) by InstantiateForall(n)
+ }
+
+ // STEP 2: Prove the backward implication
+ val backward = have((hIsTheHeightFunction, in(n, N)) |- isConstructor(x, app(h, n)) ==> isInIntroductionFunctionImage(app(h, n))(x)) by Restate
+
+ // STEP 3: Conclude
+ have((hIsTheHeightFunction, in(n, N)) |- isInIntroductionFunctionImage(app(h, n))(x) <=> isConstructor(x, app(h, n))) by RightIff(forward, backward)
+ have(thesis) by Apply(ADTThm.equivalenceRewriting).on(lastStep, heightSuccessorWeak.asInstanceOf)
+ }
+
+ /**
+ * Generates the structural inductive case for a given constructor.
+ *
+ * @param c the constructor
+ */
+ lazy val inductiveCase: Map[SyntacticConstructor, Formula] = constructors
+ .map(c =>
+ c -> c.signature.foldRight[Formula](P(c.term))((el, fc) =>
+ val (v, ty) = el
+ ty match
+ case Self => forall(v, in(v, term) ==> (P(v) ==> fc))
+ case GroundType(t) => forall(v, in(v, t) ==> fc)
+ )
+ )
+ .toMap
+
+ /**
+ * Lemma --- Structural induction principle for this ADT.
+ *
+ * `base cases => inductive cases => ∀x ∈ ADT. P(x)`
+ */
+ lazy val induction = Lemma(constructors.foldRight[Formula](forall(x, in(x, term) ==> P(x)))((c, f) => inductiveCase(c) ==> f)) {
+
+ // List of cases to prove for structural induction to hold
+ val structuralInductionPreconditions: Formula = /\(constructors.map(inductiveCase))
+
+ // We want to prove the claim by induction on the height of n, i.e. prove that for any
+ // n in N, P holds.
+ def inductionFormula(n: Term): Formula = forall(x, in(x, app(h, n)) ==> P(x))
+ val inductionFormulaN: Formula = inductionFormula(n)
+
+ // STEP 1: Prove the base case
+ have(hIsTheHeightFunction |- in(x, app(h, emptySet)) ==> P(x)) by Weakening(heightZero)
+ val zeroCase = thenHave(hIsTheHeightFunction |- inductionFormula(emptySet)) by RightForall
+
+ val inductiveCaseRemaining = have((hIsTheHeightFunction, forall(n, in(n, N) ==> (inductionFormulaN ==> inductionFormula(successor(n))))) |- forall(n, in(n, N) ==> inductionFormulaN)) by Cut(
+ zeroCase,
+ ADTThm.natInduction of (P := lambda(n, inductionFormulaN))
+ )
+
+ // STEP 2: Prove the inductive case
+ val succCase = have((hIsTheHeightFunction, structuralInductionPreconditions) |- forall(n, in(n, N) ==> (inductionFormulaN ==> inductionFormula(successor(n))))) subproof {
+
+ // STEP 2.1 : Prove that if the x = c(x1, ..., xn) for some c and xi, ..., xj ∈ height(n) then P(x) holds.
+ val isConstructorImpliesP = have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(x, app(h, n))) |- P(x)) subproof {
+
+ if constructors.isEmpty then have(thesis) by Restate
+ else
+ val orSeq =
+ (for c <- constructors yield
+
+ // Caching
+ val constructorPrecondition = inductiveCase(c)
+ val constructorVarsInHN = constructorVarsInDomain(c, app(h, n))
+ val constructorVarsInHNEx = ∃(n, in(n, N) /\ constructorVarsInDomain(c, app(h, n)))
+ val constructorVarsInTerm = constructorVarsInDomain(c, term)
+
+ // STEP 2.1.1: Prove that if xi, ..., xj ∈ height(n) then xi, ..., xj ∈ ADT.
+ val constructorQuantVarsInHNToTerm = have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInTerm) subproof {
+ have((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- in(n, N) /\ constructorVarsInHN) by Restate
+ val consVarL = thenHave((hIsTheHeightFunction, in(n, N), constructorVarsInHN) |- constructorVarsInHNEx) by RightExists
+ have((constructorVarsInTerm <=> constructorVarsInHNEx, constructorVarsInHNEx) |- constructorVarsInTerm) by Restate.from(
+ ADTThm.equivalenceRevApply of (p1 := constructorVarsInTerm, p2 := constructorVarsInHNEx)
+ )
+ have((hIsTheHeightFunction, constructorVarsInHNEx) |- constructorVarsInTerm) by Cut(
+ termsHaveHeight(c),
+ lastStep
+ )
+ have(thesis) by Cut(consVarL, lastStep)
+ }
+
+
+ // STEP 2.1.2: Prove that if xi, ..., xj ∈ height(n) then P(c(x1, ..., xn)).
+ have((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN) |- constructorPrecondition) by Restate
+
+ c.signature
+ .foldLeft(lastStep)((fact, el) =>
+ val (v, ty) = el
+
+ fact.statement.right.head match
+ case Forall(_, factCclWithoutForall) =>
+ thenHave((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN) |- factCclWithoutForall) by InstantiateForall(v)
+
+ factCclWithoutForall match
+ case Implies(membership, subformula) =>
+ ty match
+ case Self =>
+ subformula match
+ case Implies(hypothesis, subSubFormula) =>
+ val proofSubSubFormula = thenHave(
+ (hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInTerm, constructorVarsInHN, P(v)) |- subSubFormula
+ ) by Weakening
+
+ have(inductionFormulaN |- inductionFormulaN) by Hypothesis
+ thenHave(inductionFormulaN |- in(v, app(h, n)) ==> P(v)) by InstantiateForall(v)
+ thenHave((inductionFormulaN, constructorVarsInHN) |- P(v)) by Weakening
+
+ have((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInTerm, constructorVarsInHN) |- subSubFormula) by Cut(
+ lastStep,
+ proofSubSubFormula
+ )
+ have((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN) |- subSubFormula) by Cut(
+ constructorQuantVarsInHNToTerm,
+ lastStep
+ )
+
+ case _ => throw UnreachableException
+
+ case GroundType(t) =>
+ thenHave((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN) |- subformula) by Restate
+ case _ => throw UnreachableException
+ case _ => throw UnreachableException
+ )
+
+ thenHave((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN) |- P(c.term)) by Restate
+
+ // STEP 2.1.3: Prove that if xi, ..., xj ∈ height(n) then P(x).
+ thenHave((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN, x === c.term) |- P(x)) by RightSubstEq
+ .withParametersSimple(List((x, c.term)), lambda(x, P(x)))
+
+ thenHave((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, constructorVarsInHN /\ (x === c.term)) |- P(x)) by LeftAnd
+
+ thenHave((hIsTheHeightFunction, constructorPrecondition, in(n, N), inductionFormulaN, isConstructor(c, x, app(h, n))) |- P(x)) by QuantifiersIntro(c.variables)
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(c, x, app(h, n))) |- P(x)) by Weakening
+ ).toSeq
+
+
+ have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, isConstructor(x, app(h, n))) |- P(x)) by LeftOr(orSeq: _*)
+ }
+
+ // STEP 2.2: Prove that if x ∈ height(n + 1) then P(x) holds.
+ have((hIsTheHeightFunction, in(n, N), in(x, app(h, successor(n)))) |- isConstructor(x, app(h, n))) by Cut(
+ heightSuccessorStrong,
+ ADTThm.equivalenceApply of (p1 := in(x, app(h, successor(n))), p2 := isConstructor(x, app(h, n)))
+ )
+ have((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN, in(x, app(h, successor(n)))) |- P(x)) by Cut(lastStep, isConstructorImpliesP)
+
+ // STEP 2.3: Conclude
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN) |- in(x, app(h, successor(n))) ==> P(x)) by RightImplies
+
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N), inductionFormulaN) |- inductionFormula(successor(n))) by RightForall
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N)) |- inductionFormulaN ==> inductionFormula(successor(n))) by RightImplies
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions) |- in(n, N) ==> (inductionFormulaN ==> inductionFormula(successor(n)))) by RightImplies
+ thenHave(thesis) by RightForall
+ }
+
+ // STEP 3: Conclude
+
+ have((hIsTheHeightFunction, structuralInductionPreconditions) |- forall(n, in(n, N) ==> inductionFormulaN)) by Cut(lastStep, inductiveCaseRemaining)
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions) |- in(n, N) ==> inductionFormulaN) by InstantiateForall(n)
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N)) |- inductionFormulaN) by Restate
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N)) |- in(x, app(h, n)) ==> P(x)) by InstantiateForall(x)
+ thenHave((hIsTheHeightFunction, structuralInductionPreconditions, in(n, N) /\ in(x, app(h, n))) |- P(x)) by Restate
+ val exImpliesP = thenHave((hIsTheHeightFunction, structuralInductionPreconditions, exists(n, in(n, N) /\ in(x, app(h, n)))) |- P(x)) by LeftExists
+ have((hIsTheHeightFunction, in(x, term)) |- exists(n, in(n, N) /\ in(x, app(h, n)))) by Cut(termHasHeight, ADTThm.equivalenceApply of (p1 := in(x, term), p2 := exists(n, in(n, N) /\ in(x, app(h, n)))))
+
+ have((hIsTheHeightFunction, structuralInductionPreconditions, in(x, term)) |- P(x)) by Cut(lastStep, exImpliesP)
+ thenHave((exists(h, hIsTheHeightFunction), structuralInductionPreconditions, in(x, term)) |- P(x)) by LeftExists
+ have((structuralInductionPreconditions, in(x, term)) |- P(x)) by Cut(heightFunctionExistence, lastStep)
+ thenHave(structuralInductionPreconditions |- in(x, term) ==> P(x)) by RightImplies
+ thenHave(structuralInductionPreconditions |- forall(x, in(x, term) ==> P(x))) by RightForall
+ }
+
+}
+
+/**
+ * Semantic set theoretical interpretation of a constructor for an algebraic data type.
+ * That is a function from the arguments' domains to the set of instances of the algebraic data type.
+ *
+ * `c : T1 -> ... -> Tn -> ADT`
+ *
+ * Since polymorphism is supported, this function is parametrized by the type variables appearing inside
+ * the specification of the ADT. In this sense, a constructor is a class function whose parameters are
+ * type variables and whose body is the set theoretic function detailed above. With polymorphism, the signature
+ * thus becomes:
+ *
+ * `c(X1, ..., Xn) : T1(X1, ..., Xn) -> ... -> Tn(X1, ..., Xn) -> ADT(X1, ..., Xn)`
+ *
+ * Injectivity and introduction rule are proven within this class.
+ *
+ * @constructor generates a class function for this constructor
+ * @param line the line at which this constructor is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param file the file in which this constructor is defined. Usually fetched automatically by the compiler.
+ * Used for error reporting
+ * @param name the name of this constructor
+ * @param underlying the syntactic constructor
+ * @param adt the algebraic data type to which this constructor belongs
+ */
+private class SemanticConstructor[N <: Arity](using line: sourcecode.Line, file: sourcecode.File)(
+ val name: String,
+ val underlying: SyntacticConstructor,
+ val adt: SyntacticADT[N],
+) {
+ /**
+ * Full name of this constructor, i.e. concatenation of the ADT name and this constructor name.
+ */
+ val fullName: String = s"${adt.name}/${name}"
+
+ /**
+ * Type variables that may appear in the signature of this constructor.
+ */
+ val typeVariables: Variable ** N = adt.typeVariables
+
+ /**
+ * Sequence of type variables that may appear in the signature of this constructor.
+ */
+ val typeVariablesSeq: Seq[Variable] = adt.typeVariablesSeq
+
+ /**
+ * Number of type variables in the signature of this constructor.
+ */
+ val typeArity: N = adt.typeArity
+
+ /**
+ * Variables used for constructor arguments.
+ */
+ val variables: Seq[Variable] = underlying.variables
+
+ /**
+ * Variables used for constructor arguments.
+ */
+ val variables1: Seq[Variable] = underlying.variables1
+
+ /**
+ * Alternative set of variables used for constructor arguments.
+ */
+ val variables2: Seq[Variable] = underlying.variables2
+
+ /**
+ * Set of variables for this constructor with their respective domain or a
+ * special symbol in case the domain is the ADT.
+ *
+ * @param vars variables
+ */
+ def syntacticSignature(vars: Seq[Variable]): Seq[(Variable, ConstructorArgument)] =
+ vars.zip(underlying.specification)
+
+ /**
+ * Variables of this constructor with their respective domain or a special symbol in case the domain is the ADT.
+ */
+ val syntacticSignature: Seq[(Variable, ConstructorArgument)] = underlying.signature
+
+ /**
+ * Constructor arguments with their respective domains.
+ *
+ * @param vars this constructor arguments
+ */
+ def semanticSignature(vars: Seq[Variable]): Seq[(Variable, Term)] = vars.zip(underlying.specification.map(_.getOrElse(adt.term)))
+
+ /**
+ * Variables of this constructor with their respective domains.
+ */
+ val semanticSignature: Seq[(Variable, Term)] = semanticSignature(variables)
+
+ /**
+ * Variables of this constructor with their respective domains.
+ */
+ val semanticSignature1: Seq[(Variable, Term)] = semanticSignature
+
+ /**
+ * Alternative set of variables of this constructor with their respective domain.
+ */
+ val semanticSignature2: Seq[(Variable, Term)] = semanticSignature(variables2)
+
+ /**
+ * Type of this constructor.
+ */
+ val typ: Term = semanticSignature.unzip._2.foldRight[Term](adt.term)((a, b) => a |=> b)
+
+ /**
+ * Arity of this constructor.
+ */
+ val arity: Int = variables.size
+
+ /**
+ * Internal representation of this constructor (i.e. as a tuple).
+ */
+ val structuralTerm: Term = underlying.term
+ /**
+ * Internal representation of this constructor (i.e. as a tuple).
+ */
+ val structuralTerm1: Term = underlying.term1
+ /**
+ * Internal representation of this constructor (i.e. as a tuple) with an alternative set of variables.
+ */
+ val structuralTerm2: Term = underlying.term2
+
+ /**
+ * Definition of this constructor.
+ *
+ * Formally it is the only function whose codomain is the ADT such that for all variables x1 :: S1, ...,xn :: Sn
+ * c * x1 * ... * xn = (tagc, (x1, (..., (xn, ∅)...))
+ */
+ private val untypedDefinition = (c :: typ) /\ forallSeq(variables, wellTypedFormula(semanticSignature) ==> (appSeq(c)(variables) === structuralTerm))
+
+ /**
+ * Lemma --- Uniqueness of this constructor.
+ *
+ * ` ∃!c. c ∈ T1 -> ... -> Tn -> ADT /\ ∀x1, ..., xn. c * x1 * ...* xn = (tagc, (x1, (..., (xn, ∅)...))`
+ */
+ private val uniqueness = Axiom(existsOne(c, untypedDefinition))
+
+ /**
+ * Class function representing this constructor
+ */
+ private val classFunction = FunctionDefinition[N](fullName, line.value, file.value)(typeVariablesSeq, c, untypedDefinition, uniqueness).label
+
+ /**
+ * Identifier of this constructor.
+ */
+ val id: Identifier = classFunction.id
+
+ /**
+ * This constructor in which type variables are instantiated.
+ *
+ * @param args the instances of this constructor's type variables
+ */
+ def term(args: Seq[Term]): Term = classFunction.applySeq(args)
+
+ /**
+ * Constructor where type variables are instantiated with schematic variables.
+ */
+ private val term: Term = term(typeVariablesSeq)
+
+ /**
+ * Constructor where type variables are instantiated with schematic variables and arguments instantiated.
+ *
+ * @param args the instances of this constructor arguments
+ */
+ def appliedTerm(args: Seq[Term]): Term = appSeq(term)(args)
+
+ /**
+ * Constructor where type variables and arguments are instantiated with schematic variables.
+ */
+ val appliedTerm: Term = appliedTerm(variables)
+
+ /**
+ * Constructor where type variables and arguments are instantiated with schematic variables.
+ */
+ val appliedTerm1: Term = appliedTerm
+
+ /**
+ * Constructor where type variables and arguments are instantiated with schematic variables.
+ * Arguments variables are however drawn from an alternative set of variables.
+ */
+ val appliedTerm2: Term = appliedTerm(variables2)
+
+ /**
+ * Lemma --- This constructor is equal to its internal representation.
+ *
+ * `∀x1, ..., xn. c * x1 * ... * xn = (tagc, (x1, (..., (xn, ∅)...))`
+ */
+ val shortDefinition = Lemma(forallSeq(variables, wellTypedFormula(semanticSignature) ==> (appliedTerm === structuralTerm))) {
+ have(forall(c, (term === c) <=> untypedDefinition)) by Exact(classFunction.definition)
+ thenHave((term === term) <=> ((term :: typ) /\ forallSeq(variables, wellTypedFormula(semanticSignature) ==> (appliedTerm === structuralTerm)))) by InstantiateForall(term)
+ thenHave(thesis) by Weakening
+ }
+
+ /**
+ * Lemma --- Introduction rule for this constructor.
+ *
+ * `∀A1, ..., Am. c(X1, ..., Xm) ∈ T1(X1, ..., Xm) -> ... -> Tn(X1, ..., Xm) -> ADT(X1, ..., Xm)`
+ *
+ * where Ai are the type variables of the ADT and Ti are domains of this constructor arguments.
+ *
+ * e.g. `∀T. nil(T) ∈ list(T)` and `∀T. cons(T) ∈ T -> list(T) -> list(T)`
+ */
+ val intro = Lemma(forallSeq(typeVariablesSeq, term :: typ)) {
+ have(forall(c, (term === c) <=> untypedDefinition)) by Exact(classFunction.definition)
+ thenHave((term === term) <=> ((term :: typ) /\ forallSeq(variables, wellTypedFormula(semanticSignature) ==> (appliedTerm === structuralTerm)))) by InstantiateForall(term)
+ thenHave(term :: typ) by Weakening
+ thenHave(thesis) by QuantifiersIntro(typeVariablesSeq)
+ }
+
+ /**
+ * Theorem --- Injectivity of constructors.
+ *
+ * Two instances of this constructor are equal if and only if all of their arguments are pairwise equal
+ *
+ * e.g. Cons(head1, tail1) === Cons(head2, tail2) <=> head1 === head2 /\ tail1 === tail2
+ */
+ lazy val injectivity =
+ val vars1WellTyped: Set[Formula] = wellTypedSet(semanticSignature1)
+ val vars2WellTyped: Set[Formula] = wellTypedSet(semanticSignature2)
+
+ if arity == 0 then
+ Lemma(appliedTerm1 === appliedTerm2) {
+ have(thesis) by RightRefl
+ }
+ else
+ Lemma(vars1WellTyped ++ vars2WellTyped |- simplify((appliedTerm1 === appliedTerm2) <=> (variables1 === variables2))) {
+
+ have(forallSeq(variables1, wellTypedFormula(semanticSignature1) ==> (appliedTerm1 === structuralTerm1))) by Restate.from(shortDefinition)
+
+ variables1.foldLeft(lastStep)((fact, v) =>
+ fact.statement.right.head match
+ case Forall(_, phi) => thenHave(phi) by InstantiateForall(v)
+ case _ => throw UnreachableException
+ )
+ val tappTerm1Def = thenHave(vars1WellTyped |- appliedTerm1 === structuralTerm1) by Restate
+
+ // println(forallSeq(variables1, wellTypedFormula(semanticSignature1) ==> (appliedTerm1 === structuralTerm1)))
+ // println(forallSeq(variables2, wellTypedFormula(semanticSignature2) ==> (appliedTerm2 === structuralTerm)))
+ have(forallSeq(variables2, wellTypedFormula(semanticSignature2) ==> (appliedTerm2 === structuralTerm2))) by Restate.from(shortDefinition)
+
+ variables2.foldLeft(lastStep)((fact, v) =>
+ fact.statement.right.head match
+ case Forall(_, phi) => thenHave(phi) by InstantiateForall(v)
+ case _ => throw UnreachableException
+ )
+ val tappTerm2Def = thenHave(vars2WellTyped |- appliedTerm2 === structuralTerm2) by Restate
+
+
+ val s0 = have(vars2WellTyped + (appliedTerm1 === appliedTerm2) |- appliedTerm1 === structuralTerm2) by Cut(tappTerm2Def,
+ ADTThm.altEqualityTransitivity of (x := appliedTerm1, y := appliedTerm2, z := structuralTerm2))
+ have(vars1WellTyped + (appliedTerm1 === structuralTerm2) |- structuralTerm1 === structuralTerm2) by Cut(tappTerm1Def,
+ ADTThm.altEqualityTransitivity of (x := structuralTerm1, y := appliedTerm1, z := structuralTerm2))
+ have((vars1WellTyped ++ vars2WellTyped) + (appliedTerm1 === appliedTerm2) |- structuralTerm1 === structuralTerm2) by Cut(s0, lastStep)
+ val forward = thenHave(vars1WellTyped ++ vars2WellTyped |- (appliedTerm1 === appliedTerm2) ==> (structuralTerm1 === structuralTerm2)) by RightImplies
+
+ val s1 = have(vars1WellTyped + (structuralTerm1 === structuralTerm2) |- appliedTerm1 === structuralTerm2) by Cut(tappTerm1Def,
+ ADTThm.altEqualityTransitivity of (x := appliedTerm1, y := structuralTerm1, z := structuralTerm2))
+ have(vars2WellTyped + (appliedTerm1 === structuralTerm2) |- appliedTerm1 === appliedTerm2) by Cut(tappTerm2Def,
+ ADTThm.altEqualityTransitivity of (x := appliedTerm1, y := structuralTerm2, z := appliedTerm2))
+ have((vars1WellTyped ++ vars2WellTyped) + (structuralTerm1 === structuralTerm2) |- appliedTerm1 === appliedTerm2) by Cut(s1, lastStep)
+ val backward = thenHave(vars1WellTyped ++ vars2WellTyped |- (structuralTerm1 === structuralTerm2) ==> (appliedTerm1 === appliedTerm2)) by RightImplies
+
+ val definitionUnfolding = have(vars1WellTyped ++ vars2WellTyped |- (appliedTerm1 === appliedTerm2) <=> (structuralTerm1 === structuralTerm2)) by RightIff(forward, backward)
+ have((appliedTerm1 === appliedTerm2) <=> (structuralTerm1 === structuralTerm2) |- (appliedTerm1 === appliedTerm2) <=> /\(variables1.zip(variables2).map(_ === _))) by Sorry
+ Cut(
+ underlying.injectivity,
+ ADTThm.equivalenceRewriting of (p1 := (appliedTerm1 === appliedTerm2), p2 := (structuralTerm1 === structuralTerm2), p3 := /\(variables1.zip(variables2).map(_ === _)))
+ )
+ have(thesis) by Cut(definitionUnfolding, lastStep)
+ }
+
+
+ /**
+ * Case generated by this constructor when performing a proof by induction
+ */
+ lazy val inductiveCase: Formula =
+ syntacticSignature.foldRight[Formula](P(appliedTerm1))
+ ((el, fc) =>
+ val (v, typ) = el
+ typ match
+ case Self => forall(v, v :: adt.term ==> (P(v) ==> fc))
+ case GroundType(t) => forall(v, v :: t ==> fc)
+ )
+}
+
+/**
+ * Semantic set theoretical interpretation of an algebraic data type. That is the least set closed under [[SemanticConstructor]].
+ *
+ * E.g. list is the smallest set containing nil and closed under the cons function.
+ *
+ * Injectivity between different constructors, structural induction and elimination rule are proved within this class.
+ *
+ * @constructor generates a semantic interpretation for this ADT out of a syntactic one
+ * @param underlying the syntactic representation of this ADT
+ * @param constructors constructors of this ADT
+ */
+ private class SemanticADT[N <: Arity](
+ val underlying: SyntacticADT[N],
+ val constructors: Seq[SemanticConstructor[N]]
+ ) {
+
+ /**
+ * Name of this ADT.
+ */
+ val name: String = underlying.name
+
+ /**
+ * Identifier of this ADT.
+ */
+ val id: Identifier = underlying.polymorphicTerm.id
+
+ /**
+ * Type variables of this ADT.
+ */
+ val typeVariables: Variable ** N = underlying.typeVariables
+
+ /**
+ * Sequence of type variables of this ADT.
+ */
+ val typeVariablesSeq: Seq[Variable] = underlying.typeVariablesSeq
+
+ /**
+ * Number of type variables in this ADT.
+ */
+ val typeArity: N = underlying.typeArity
+
+ /**
+ * Term representing this ADT where type variables are instantiated with given arguments.
+ *
+ * @param args the instances of this ADT type variables
+ */
+ def term(args: Seq[Term]) = underlying.polymorphicTerm.applySeq(args)
+
+ /**
+ * Term representing this ADT where type variables are instantiated with schematic variables.
+ */
+ val term: Term = underlying.term
+
+ /**
+ * Theorem --- Injectivity of constructors.
+ *
+ * Two instances of different construcors are always different.
+ *
+ * e.g. Nil != Cons(head, tail)
+ */
+ def injectivity(c1: SemanticConstructor[N], c2: SemanticConstructor[N]) =
+
+ val vars1WellTyped: Set[Formula] = wellTypedSet(c1.semanticSignature1)
+ val vars2WellTyped: Set[Formula] = wellTypedSet(c2.semanticSignature2)
+
+ Lemma(vars1WellTyped ++ vars2WellTyped |- !(c1.appliedTerm1 === c2.appliedTerm2)) {
+
+ val defUnfolding = have((vars1WellTyped ++ vars2WellTyped) + (c1.appliedTerm1 === c2.appliedTerm2) |- c1.structuralTerm1 === c2.structuralTerm2) subproof {
+ have(forallSeq(c1.variables1, wellTypedFormula(c1.semanticSignature1) ==> (c1.appliedTerm1 === c1.structuralTerm1))) by Restate.from(c1.shortDefinition)
+
+ c1.variables1.foldLeft(lastStep)((fact, v) =>
+ fact.statement.right.head match
+ case Forall(_, phi) => thenHave(phi.substitute(v := x)) by InstantiateForall(x)
+ case _ => throw UnreachableException
+ )
+ val tappTerm1Def = thenHave(vars1WellTyped |- c1.structuralTerm1 === c1.appliedTerm1) by Restate
+
+ have(forallSeq(c2.variables2, wellTypedFormula(c2.semanticSignature2) ==> (c2.appliedTerm2 === c2.structuralTerm2))) by Restate.from(c2.shortDefinition)
+
+ c2.variables2.foldLeft(lastStep)((fact, v) =>
+ fact.statement.right.head match
+ case Forall(_, phi) => thenHave(phi) by InstantiateForall(v)
+ case _ => throw UnreachableException
+ )
+ val tappTerm2Def = thenHave(vars2WellTyped |- c2.appliedTerm2 === c2.structuralTerm2) by Restate
+
+ val s0 = have(vars2WellTyped + (c1.appliedTerm1 === c2.appliedTerm2) |- c1.appliedTerm1 === c2.structuralTerm2) by Cut(
+ tappTerm2Def,
+ ADTThm.altEqualityTransitivity of (x := c1.appliedTerm1, y := c2.appliedTerm2, z := c2.structuralTerm2)
+ )
+ have(vars1WellTyped + (c1.appliedTerm1 === c2.structuralTerm2) |- c1.structuralTerm1 === c2.structuralTerm2) by Cut(
+ tappTerm1Def,
+ ADTThm.altEqualityTransitivity of (x := c1.structuralTerm1, y := c1.appliedTerm1, z := c2.structuralTerm2)
+ )
+ have(thesis) by Cut(s0, lastStep)
+ }
+
+ have(!(c1.structuralTerm1 === c2.structuralTerm2)) by Restate.from(underlying.injectivity(c1.underlying, c2.underlying))
+ thenHave(c1.structuralTerm1 === c2.structuralTerm2 |- ()) by Restate
+
+ have((vars1WellTyped ++ vars2WellTyped) + (c1.appliedTerm1 === c2.appliedTerm2) |- ()) by Cut(defUnfolding, lastStep)
+ }
+
+ /**
+ * Theorem --- Structural induction principle for this ADT.
+ *
+ * `base cases => inductive cases => ∀x ∈ ADT. P(x)`
+ */
+ lazy val induction = Lemma(constructors.foldRight[Formula](forall(x, x :: term ==> P(x)))((c, f) => c.inductiveCase ==> f)) { sp ?=>
+ constructors.foldRight[(Formula, Formula, sp.Fact)] {
+ val prop = forall(x, x :: term ==> P(x))
+ (prop, prop, have(prop <=> prop) by Restate)
+ }((c, acc) =>
+ val (oldBefore, oldAfter, fact) = acc
+ val newBefore = underlying.inductiveCase(c.underlying) ==> oldBefore
+ val newAfter = c.inductiveCase ==> oldAfter
+
+ have(underlying.inductiveCase(c.underlying) <=> c.inductiveCase) subproof {
+ val wellTypedVars: Seq[Formula] = wellTyped(c.semanticSignature)
+ val wellTypedVarsSet = wellTypedVars.toSet
+
+
+ have(forallSeq(c.variables, wellTypedFormula(c.semanticSignature) ==> (c.appliedTerm === c.structuralTerm))) by Restate.from(c.shortDefinition)
+ if c.arity > 0 then
+ c.variables1.foldLeft(lastStep)((l, _) =>
+ lastStep.statement.right.head match
+ case Forall(v, phi) => thenHave(phi) by InstantiateForall(v)
+ case _ => throw UnreachableException
+ )
+
+ val eq = thenHave(wellTypedVarsSet |- c.appliedTerm === c.structuralTerm) by Restate
+ have(P(c.appliedTerm) <=> P(c.appliedTerm)) by Restate
+ thenHave(c.structuralTerm === c.appliedTerm |- P(c.structuralTerm) <=> P(c.appliedTerm)) by RightSubstEq.withParametersSimple(
+ List((c.structuralTerm, c.appliedTerm)),
+ lambda(s, P(c.structuralTerm) <=> P(s))
+ )
+ have(wellTypedVarsSet |- P(c.structuralTerm) <=> P(c.appliedTerm)) by Cut(eq, lastStep)
+
+ c.syntacticSignature
+ .foldRight[(Formula, Formula, Seq[Formula])]((P(c.structuralTerm), P(c.appliedTerm), wellTypedVars))((el, fc) =>
+ val (v, ty) = el
+ val (fc1, fc2, wellTypedVars) = fc
+ ty match
+ case Self =>
+ val wellTypedV: Formula = v :: term
+ have(wellTypedVars |- (P(v) ==> fc1) <=> (P(v) ==> fc2)) by Cut(lastStep, ADTThm.leftImpliesEquivalenceWeak of (p := P(v), p1 := fc1, p2 := fc2))
+ thenHave(wellTypedVars.init |- wellTypedV ==> ((P(v) ==> fc1) <=> (P(v) ==> fc2))) by RightImplies
+ have(wellTypedVars.init |- (wellTypedV ==> (P(v) ==> fc1)) <=> (wellTypedV ==> (P(v) ==> fc2))) by Cut(
+ lastStep,
+ ADTThm.leftImpliesEquivalenceStrong of (p := wellTypedV, p1 := P(v) ==> fc1, p2 := P(v) ==> fc2)
+ )
+ thenHave(wellTypedVars.init |- forall(v, (wellTypedV ==> (P(v) ==> fc1)) <=> (wellTypedV ==> (P(v) ==> fc2)))) by RightForall
+ have(wellTypedVars.init |- forall(v, (wellTypedV ==> (P(v) ==> fc1))) <=> forall(v, (wellTypedV ==> (P(v) ==> fc2)))) by Cut(
+ lastStep,
+ universalEquivalenceDistribution of (P := lambda(v, wellTypedV ==> (P(v) ==> fc1)), Q := lambda(v, wellTypedV ==> (P(v) ==> fc2)))
+ )
+ (forall(v, wellTypedV ==> (P(v) ==> fc1)), forall(v, wellTypedV ==> (P(v) ==> fc2)), wellTypedVars.init)
+ case GroundType(t) =>
+ thenHave(wellTypedVars.init |- v :: t ==> (fc1 <=> fc2)) by RightImplies
+ have(wellTypedVars.init |- (in(v, t) ==> fc1) <=> (v :: t ==> fc2)) by Cut(lastStep, ADTThm.leftImpliesEquivalenceStrong of (p := in(v, t), p1 := fc1, p2 := fc2))
+ thenHave(wellTypedVars.init |- forall(v, (in(v, t) ==> fc1) <=> (v :: t ==> fc2))) by RightForall
+ have(wellTypedVars.init |- forall(v, (in(v, t) ==> fc1)) <=> forall(v, (v :: t ==> fc2))) by Cut(
+ lastStep,
+ universalEquivalenceDistribution of (P := lambda(v, in(v, t) ==> fc1), Q := lambda(v, v :: t ==> fc2))
+ )
+ (forall(v, (in(v, t) ==> fc1)), forall(v, (v :: t ==> fc2)), wellTypedVars.init)
+ )
+ }
+ (newBefore, newAfter, have(newBefore <=> newAfter) by Apply(ADTThm.impliesEquivalence).on(lastStep, fact))
+ )
+ have(underlying.induction.statement.right.head |- thesis.right.head) by Cut(
+ lastStep,
+ ADTThm.equivalenceApply of (
+ p1 := underlying.induction.statement.right.head, p2 := thesis.right.head
+ )
+ )
+ have(thesis) by Cut(underlying.induction, lastStep)
+ }
+
+ /**
+ * Returns a map binding each constructor to formula describing whether x is an instance of it.
+ */
+ private lazy val isConstructorMap: Map[SemanticConstructor[N], Formula] =
+ constructors.map(c => c -> existsSeq(c.variables, wellTypedFormula(c.semanticSignature) /\ (x === c.appliedTerm))).toMap
+
+ /**
+ * Returns a formula describing whether x is an instance of one of this ADT's constructors.
+ */
+ private lazy val isConstructor =
+ \/(constructors.map(c => isConstructorMap(c)))
+
+ /**
+ * Theorem --- Pattern matching principle (also known as elimination rule) for this ADT.
+ *
+ * `x ∈ ADT |- x = c * x1 * ... * xn for some constructor c and xi, ..., xj ∈ ADT`
+ */
+ lazy val elim = Lemma(x :: term |- simplify(isConstructor)) {
+
+ // Induction preconditions with P(z) = z != x
+ val inductionPreconditionIneq = constructors.map(c => c -> c.inductiveCase.substitute((P -> lambda(z, !(x === z))))).toMap
+ val inductionPreconditionsIneq = /\(inductionPreconditionIneq.map(_._2))
+
+ // Weakening of the negation of the induction preconditions
+ val weakNegInductionPreconditionIneq: Map[SemanticConstructor[N], Formula] = constructors
+ .map(c =>
+ c ->
+ c.semanticSignature
+ .foldRight[Formula](x === c.appliedTerm)((el, fc) =>
+ val (v, t) = el
+ exists(v, (v :: t) /\ fc)
+ )
+ )
+ .toMap
+
+ // STEP 1: Prove that if the induction preconditions with P(z) = z != x do not hold then x is the instance of some constructor
+ val strengtheningOfInductionPreconditions = have(!inductionPreconditionsIneq |- isConstructor) subproof {
+ if constructors.isEmpty then have(thesis) by Restate
+ else
+
+ // STEP 1.1: Prove the claim for each constructor
+ val negInductionPreconditionsOrSequence =
+ for c <- constructors yield
+
+ // STEP 1.1.1: Prove the strengthening of the negations of the induction preconditions
+ val conditionStrenghtening = have(!inductionPreconditionIneq(c) |- weakNegInductionPreconditionIneq(c)) subproof {
+ have(x === c.appliedTerm |- x === c.appliedTerm) by Hypothesis
+
+ c.syntacticSignature
+ .foldRight(lastStep)((el, fact) =>
+ val (v, ty) = el
+ val left = fact.statement.left.head
+ val right = fact.statement.right.head
+
+ ty match
+ case Self =>
+ thenHave(!(x === v) /\ left |- right) by Weakening
+ case _ => ()
+
+ val weakr = thenHave(in(v, ty.getOrElse(term)) /\ left |- right) by Weakening
+ val weakl = have(in(v, ty.getOrElse(term)) /\ left |- in(v, ty.getOrElse(term))) by Restate
+
+ have((v :: ty.getOrElse(term)) /\ left |- (v :: ty.getOrElse(term)) /\ right) by RightAnd(weakl, weakr)
+ thenHave((v :: ty.getOrElse(term)) /\ left |- exists(v, (v :: ty.getOrElse(term)) /\ right)) by RightExists
+ thenHave(exists(v, (v :: ty.getOrElse(term)) /\ left) |- exists(v, (v :: ty.getOrElse(term)) /\ right)) by LeftExists
+ )
+
+ }
+
+ // STEP 1.1.2: Conclude
+ // TODO: Change to a more efficient way of proving this
+ have(weakNegInductionPreconditionIneq(c) |- isConstructorMap(c)) by Tableau
+ have(!inductionPreconditionIneq(c) |- isConstructorMap(c)) by Cut(conditionStrenghtening, lastStep)
+ thenHave(!inductionPreconditionIneq(c) |- isConstructor) by Weakening
+
+ have(thesis) by LeftOr(negInductionPreconditionsOrSequence: _*)
+ }
+
+ // STEP 2: Conclude
+ have(inductionPreconditionsIneq |- forall(z, z :: term ==> !(x === z))) by Restate.from(induction of (P := lambda(z, !(x === z))))
+ thenHave(inductionPreconditionsIneq |- x :: term ==> !(x === x)) by InstantiateForall(x)
+ val ind = thenHave(x :: term |- !inductionPreconditionsIneq) by Restate
+ have(x :: term |- isConstructor) by Cut(lastStep, strengtheningOfInductionPreconditions)
+ }
+ }
+
+
+
+
+
+
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/package.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/package.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7af2af24c35e8e64e30bc66663b2973bac08a639
--- /dev/null
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/types/adt/package.scala
@@ -0,0 +1,200 @@
+package lisa.maths.settheory.types
+
+/**
+ * Provides definitional mechanisms for Algebraic Data Types (ADTs) and tactics for reasoning about them.
+ *
+ * ===Usage===
+ *
+ * In order to use ADTs, you need to import
+ * {{{
+ * lisa.maths.settheory.types.adt.{*, given}
+ * }}}
+ *
+ * ====Defining an ADT====
+ *
+ * ADTs can be defined using the following syntax:
+ * {{{
+ * val define(adtName: ADT[N], constructors(c1, ..., cn)) = (X1, .., Xk) --> (T1, ..., Tn) | ... | (S1, ..., Sm)
+ * }}}
+ *
+ * where:
+ * - `adtName` is the identifier of the ADT
+ * - `N` is the number of poylmorphic variables
+ * - `c1 ... cn` are the identifiers of the different constructors of the ADT,
+ * - `X1, ..., Xk` are the polymorphic variables
+ * - `T1, ..., Tn, S1, ..., Sm` are the types defining the signature of each constructor.
+ * Note that `adtName` and `c1 ... cn` are scala identifiers, respectively referring to the ADT and the constructors.
+ * In addition, you cannot define two ADT with the same name, even in different scopes, as they introduce a new global definition.
+ * Type variables must be declarated as variables before being used.
+ * Here are some examples of ADT definitions:
+ * {{{
+ *
+ * //variables declaration
+ * val A = variable
+ *
+ * // Definition of booleans with two constructors tru and fals. Each of them take no argument so their signature is ()
+ * val define(bool: ADT, constructors(tru, fals)) = () | ()
+ *
+ * // Definition of options with two constructors none and some. Options are polymorphic over a type variable A.
+ * // Their second constructor, some, has signature A has it takes only a value of type A.
+ * val define(option: ADT, constructors(none, some)) = A -> () | A
+ *
+ * // Recursive definition of lists with two constructors nil and cons. Lists are polymorphic over a type variable A.
+ * // The constructor cons takes two arguments of respectively type A and list(A) and append an element to
+ * // a sublist.
+ * val define(list: ADT, constructors(nil, cons)) = A -> () | (A, list)
+ *
+ * //Definition of natural numbers.
+ * val define(nat: ADT, constructors(zero, succ)) = () | nat
+ * }}}
+ *
+ * ====Using an ADT and its theorem====
+ *
+ * Each constructor of an ADT comes with an introduction rule and an injectivity theorem.
+ * The introduction rule gives the type of the constructor and is of the form
+ *
+ * `∀ X1, ..., Xk. c(X1, ..., Xk) :: T1 -> ... Tn -> ADT(X1, ..., Xk)`
+ *
+ * The injection theorem stipulates that two instances of the same constructor are equal if and only if all their arguments are equal.
+ *
+ * For examples for lists we have
+ *
+ * nil introduction: `∀ A. nil(A) :: list(A)`
+ *
+ * cons introduction: `∀ A. cons(A) :: A -> list(A) -> list(A)`
+ *
+ * nil injectivity: `nil(A) = nil(A)`
+ *
+ * cons injectivity: `cons(A) * x0 * x1 = cons(A) * y0 * y1 <=> x0 = x1 /\ y0 = y1`
+ *
+ * Each ADT comes with an structural induction schema, an elimination rule (or pattern matching principle) and an injectivity theorem.
+ *
+ * Structural induction states that if a statement is true for each constructor assuming that the proposition is true for the constructor's
+ * arguments, then it is true for every element of the ADT.
+ *
+ * e.g. list induction: ` P(nil(A)) => (∀ x0 :: A. ∀ x1 :: list(A). P(x1) => P(cons * x0 * x1)) => ∀ x :: list(A). P(x)`
+ *
+ * Elimination rule is a direct consequence of induction and states that each instance of an ADT is an instance of one of its constructors
+ *
+ * e.g. list elimination: ` x :: list(A) => x = nil(A) \/ ∃ x0, x1. x = cons(A) * x0 * x1`
+ *
+ * Finally injectivity tells us that instances of different constructors are different
+ *
+ * e.g. nil/cons injectivity: `nil(A) != cons(A) * x0 * x1`
+ *
+ * ====Type Checking====
+ *
+ * We provide a tactic to automatically type check instances of algebraic data types.
+ * It can be called using `TypeChecker.prove`. For examples instances of lists can be
+ * typechecked as follow.
+ *
+ * {{{
+ * have(nil(A) :: list(A)) by TypeChecker.prove
+ * have((x :: A, l :: list(A)) |- cons * x * l :: list(A)) by TypeChecker.prove
+ * }}}
+ *
+ * ====Induction Tactic====
+ *
+ * We provide a tactic for performing proofs by induction.
+ * The tactic can prove goals of the form
+ *
+ * ` ∀ x :: adt. P(x)`
+ *
+ * To work the user needs to provide a proof of P(c * x0 * ... * xn) for each constructor.
+ * The syntax of the tactic is of the following form:
+ * {{{
+ * have(∀ x :: adt. P(x)) by Induction(adt) {
+ * Case(c1, v1, ..., vn) {
+ * // proof of (v1 :: T1, ..., vn :: Tn, P(vi), ..., P(vj)) |- P(c1 * v0 * ... * vn)
+ * }
+ * ...
+ * Case(ck, v1, ..., vm) {
+ * // proof of (v1 :: S1, ..., vm :: Sm, P(vi), ..., P(vj)) |- P(ck * v0 * ... * vn)
+ * }
+ * }
+ * }}}
+ *
+ * For lists it would look like:
+ * {{{
+ * have(∀ x :: list(A). P(x)) by Induction(list) {
+ * Case(nil) {
+ * // ...
+ * have(P(nil)) by //Tactic to conclude the subcase
+ * }
+ * Case(cons, x, l) {
+ * // ...
+ * have((x :: A, l :: list(A), P(l)) |- P(cons * x * l)) by //Tactic to conclude the subcase
+ * }
+ * }
+ * }}}
+ *
+ * ====Defining functions====
+ *
+ * Functions over ADT can also be defined via the following syntax:
+ *
+ * {{{
+ * val myFunction = fun(adt, returnType) {
+ * Case(c1, v1, ..., vn) {
+ * body1
+ * }
+ * ...
+ * Case(ck, v1, ..., vm) {
+ * bodyk
+ * }
+ * }
+ * }}}
+ *
+ * The body of each case is automatically typechecked at runtime.
+ * For example let's define the predecessor function over natural numbers
+ *
+ * {{{
+ * val pred = fun(nat, nat) {
+ * Case(zero) {
+ * zero
+ * }
+ * Case(succ, n) {
+ * n
+ * }
+ * }
+ * }}}
+ *
+ * Recursive functions are not yet supported.
+ *
+ * ====Using functions====
+ *
+ * Functions come with an introduction and elimination rules.
+ * Their introduction rule is of the form
+ *
+ * `∀ X1, ..., Xk. f(X1, ..., Xk) :: ADT(X1, ..., Xk) -> T`
+ *
+ * where `T` is the return type of the function
+ *
+ * On the other hand, we have an elimination rule for each constructor, giving the result of the function when applied to some
+ * constructor
+ *
+ * ` f * (ck * v1 * ... * vn) = body(ck) `
+ *
+ * For example, for the `pred` function defined above the introduction rule would be
+ *
+ * `pred :: nat -> nat`
+ *
+ * and its elimination rules
+ *
+ * ` pred * zero = zero`
+ *
+ * ` pred * (succ * n) = n`
+ *
+ * Functions are also fully compatible with the typechecking tactic. We can for instance write:
+ *
+ * {{{
+ * have(n :: nat |- pred * succ * n :: nat)
+ * }}}
+ *
+ *
+ */
+package object adt {
+ export ADTSyntax.{ |, define, constructors, adt_to_term, fun_to_term, constructor_to_term, Case, fun, -->}
+ export ADTSyntax.ADTBuilder.|
+ export lisa.maths.settheory.types.TypeSystem.*
+}
+
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index cb1ca1eeb7290babfdc96545e97397f989bebc1b..77977eb2aa151312116cc0dd188ffaf4d995a6f0 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -135,6 +135,7 @@ trait Common {
* Renames the symbol with an identifier that is fresh for the given list.
*/
def freshRename(taken: Iterable[Identifier]): Label[A]
+
}
/**
@@ -276,7 +277,7 @@ trait Common {
sealed trait FunctionLabel[N <: Arity] extends TermLabel[(Term ** N) |-> Term] with ((Term ** N) |-> Term) {
val underlyingLabel: K.TermLabel
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): (Term ** N) |-> Term
- def applyUnsafe(args: (Term ** N)): Term = AppliedFunction(this, args.toSeq)
+ def applyUnsafe(args: (Term ** N)): Term = AppliedFunctional(this, args.toSeq)
override def rename(newid: Identifier): FunctionLabel[N]
def freshRename(taken: Iterable[Identifier]): FunctionLabel[N]
}
@@ -285,7 +286,7 @@ trait Common {
* A Variable, corresponding to [[K.VariableLabel]], is a schematic symbol for terms.
* It counts both as the label and as the term itself.
*/
- case class Variable(id: Identifier) extends SchematicTermLabel[Term] with Term with Absolute {
+ class Variable(val id: Identifier) extends SchematicTermLabel[Term] with Term with Absolute {
val arity: 0 = 0
val label: Variable = this
val args: Seq[Nothing] = Seq.empty
@@ -308,13 +309,35 @@ trait Common {
def freshRename(taken: Iterable[Identifier]): Variable = rename(K.freshId(taken, id))
override def toString(): String = id
def mkString(args: Seq[Term]): String = if (args.size == 0) toString() else toString() + "(" + "illegal_arguments: " + args.mkString(", ") + ")"
+
+ def canEqual(that: Any): Boolean =
+ that.isInstanceOf[Variable]
+
+ // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Variable =>
+ ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
+ || (other.canEqual(this) // optional only if this class is marked final
+ && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
+ && ((id == other.id))))
+ case _ =>
+ false
+ }
+
+ // Intentionally avoiding the call to super.hashCode because no ancestor has overridden hashCode (see note 7 below)
+ override def hashCode(): Int =
+ id.##
+ }
+ object Variable {
+ def unapply(variable: Variable): Option[Identifier] = Some(variable.id)
}
/**
* A Constant, corresponding to [[K.ConstantLabel]], is a label for terms.
* It counts both as the label and as the term itself.
*/
- case class Constant(id: Identifier) extends Term with Absolute with ConstantTermLabel[Constant] with LisaObject[Constant] {
+ class Constant(val id: Identifier) extends Term with Absolute with ConstantTermLabel[Constant] with LisaObject[Constant] {
val arity: 0 = 0
val label: Constant = this
val args: Seq[Nothing] = Seq.empty
@@ -328,17 +351,39 @@ trait Common {
def freshRename(taken: Iterable[Identifier]): Constant = rename(K.freshId(taken, id))
override def toString(): String = id
def mkString(args: Seq[Term]): String = if (args.size == 0) toString() else toString() + "(" + "illegal_arguments: " + args.mkString(", ") + ")"
+
+ def canEqual(that: Any): Boolean =
+ that.isInstanceOf[Constant]
+
+ // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: Constant =>
+ ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
+ || (other.canEqual(this) // optional only if this class is marked final
+ && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
+ && ((id == other.id))))
+ case _ =>
+ false
+ }
+
+ // Intentionally avoiding the call to super.hashCode because no ancestor has overridden hashCode (see note 7 below)
+ override def hashCode(): Int =
+ id.##
+ }
+ object Constant {
+ def unapply(constant: Constant): Option[Identifier] = Some(constant.id)
}
/**
* A schematic functional label (corresponding to [[K.SchematicFunctionLabel]]) is a functional label and also a schematic label.
* It can be substituted by any expression of type (Term ** N) |-> Term
*/
- case class SchematicFunctionLabel[N <: Arity](val id: Identifier, val arity: N) extends SchematicTermLabel[(Term ** N) |-> Term] with FunctionLabel[N] {
+ class SchematicFunctionLabel[N <: Arity](val id: Identifier, val arity: N) extends SchematicTermLabel[(Term ** N) |-> Term] with FunctionLabel[N] {
val underlyingLabel: K.SchematicTermLabel = K.SchematicFunctionLabel(id, arity)
- def unapplySeq(t: AppliedFunction): Seq[Term] = t match {
- case AppliedFunction(label, args) if (label == this) => args
+ def unapplySeq(t: AppliedFunctional): Seq[Term] = t match {
+ case AppliedFunctional(label, args) if (label == this) => args
case _ => Seq.empty
}
@nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
@@ -359,16 +404,41 @@ trait Common {
override def toString(): String = id
def mkString(args: Seq[Term]): String = toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Term]): String = mkString(args)
+
+ def canEqual(that: Any): Boolean =
+ that.isInstanceOf[SchematicFunctionLabel[?]]
+
+ // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: SchematicFunctionLabel[N] =>
+ ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
+ || (other.canEqual(this) // optional only if this class is marked final
+ && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
+ && ((id == other.id)
+ && (arity == other.arity))))
+ case _ =>
+ false
+ }
+
+ // Intentionally avoiding the call to super.hashCode because no ancestor has overridden hashCode (see note 7 below)
+ override def hashCode(): Int =
+ 31 * (
+ id.##
+ ) + arity.##
+ }
+ object SchematicFunctionLabel {
+ def unapply[N <: Arity](sfl: SchematicFunctionLabel[N]): Option[(Identifier, N)] = Some((sfl.id, sfl.arity))
}
/**
* A constant functional label of arity N.
*/
- case class ConstantFunctionLabel[N <: Arity](id: Identifier, arity: N) extends ConstantTermLabel[((Term ** N) |-> Term)] with FunctionLabel[N] {
+ class ConstantFunctionLabel[N <: Arity](val id: Identifier, val arity: N) extends ConstantTermLabel[((Term ** N) |-> Term)] with FunctionLabel[N] {
val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, arity)
private var infix: Boolean = false
- def unapplySeq(t: AppliedFunction): Seq[Term] = t match {
- case AppliedFunction(label, args) if (label == this) => args
+ def unapplySeq(t: AppliedFunctional): Seq[Term] = t match {
+ case AppliedFunctional(label, args) if (label == this) => args
case _ => Seq.empty
}
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ConstantFunctionLabel[N] = this
@@ -377,20 +447,44 @@ trait Common {
def rename(newid: Identifier): ConstantFunctionLabel[N] = ConstantFunctionLabel(newid, arity)
def freshRename(taken: Iterable[Identifier]): ConstantFunctionLabel[N] = rename(K.freshId(taken, id))
override def toString(): String = id
- def mkString(args: Seq[Term]): String = if (infix) (args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated()) else toString() + "(" + args.mkString(", ") + ")"
+ def mkString(args: Seq[Term]): String =
+ if (infix & args.size == 2) (args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated()) else toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Term]): String = if (infix) "(" + mkString(args) + ")" else mkString(args)
+
+ def canEqual(that: Any): Boolean =
+ that.isInstanceOf[SchematicFunctionLabel[?]]
+
+ // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: ConstantFunctionLabel[N] =>
+ ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
+ || (other.canEqual(this) // optional only if this class is marked final
+ && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
+ && ((id == other.id)
+ && (arity == other.arity))))
+ case _ =>
+ false
+ }
+
+ // Intentionally avoiding the call to super.hashCode because no ancestor has overridden hashCode (see note 7 below)
+ override def hashCode(): Int =
+ 31 * (
+ id.##
+ ) + arity.##
}
object ConstantFunctionLabel {
def infix[N <: Arity](id: Identifier, arity: N): ConstantFunctionLabel[N] =
val x = ConstantFunctionLabel[N](id, arity)
x.infix = true
x
+ def unapply[N <: Arity](cfl: ConstantFunctionLabel[N]): Option[(Identifier, N)] = Some((cfl.id, cfl.arity))
}
/**
* A term made from a functional label of arity N and N arguments
*/
- case class AppliedFunction(label: FunctionLabel[?], args: Seq[Term]) extends Term with Absolute {
+ class AppliedFunctional(val label: FunctionLabel[?], val args: Seq[Term]) extends Term with Absolute {
override val underlying = K.Term(label.underlyingLabel, args.map(_.underlying))
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term =
label.substituteUnsafe(map).applyUnsafe(args.map[Term]((x: Term) => x.substituteUnsafe(map)))
@@ -399,6 +493,31 @@ trait Common {
def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
override def toString: String = label.mkString(args)
override def toStringSeparated(): String = label.mkStringSeparated(args)
+
+ def canEqual(that: Any): Boolean =
+ that.isInstanceOf[AppliedFunctional]
+
+ // Intentionally avoiding the call to super.equals because no ancestor has overridden equals (see note 7 below)
+ override def equals(that: Any): Boolean =
+ that match {
+ case other: AppliedFunctional =>
+ ((this eq other) // optional, but highly recommended sans very specific knowledge about this exact class implementation
+ || (other.canEqual(this) // optional only if this class is marked final
+ && (hashCode == other.hashCode) // optional, exceptionally execution efficient if hashCode is cached, at an obvious space inefficiency tradeoff
+ && ((label == other.label)
+ && (args == other.args))))
+ case _ =>
+ false
+ }
+
+ // Intentionally avoiding the call to super.hashCode because no ancestor has overridden hashCode (see note 7 below)
+ override def hashCode(): Int =
+ 31 * (
+ label.##
+ ) + args.##
+ }
+ object AppliedFunctional {
+ def unapply(af: AppliedFunctional): Option[(FunctionLabel[?], Seq[Term])] = Some((af.label, af.args))
}
//////////////////////////////////////
@@ -570,8 +689,8 @@ trait Common {
*/
case class SchematicPredicateLabel[N <: Arity](id: Identifier, arity: N) extends SchematicAtomicLabel[(Term ** N) |-> Formula] with PredicateLabel[N] {
val underlyingLabel: K.SchematicPredicateLabel = K.SchematicPredicateLabel(id, arity)
- def unapplySeq(t: AppliedFunction): Seq[Term] = t match {
- case AppliedFunction(label, args) if (label == this) => args
+ def unapplySeq(t: AppliedFunctional): Seq[Term] = t match {
+ case AppliedFunctional(label, args) if (label == this) => args
case _ => Seq.empty
}
@nowarn("msg=the type test for.*cannot be checked at runtime because its type arguments")
diff --git a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
index 576a279c370fe7cb2572a8455cd4d533debb1ebb..402ad81ba096ca8f90d4f2a850645534c4a567b5 100644
--- a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
@@ -130,4 +130,6 @@ object FOLHelpers {
def asFrontLambda(l: K.LambdaTermFormula): LambdaExpression[Term, Formula, ?] = LambdaExpression(l.vars.map(asFrontLabel), asFront(l.body), l.vars.size)
def asFrontLambda(l: K.LambdaFormulaFormula): LambdaExpression[Formula, Formula, ?] = LambdaExpression(l.vars.map(asFrontLabel), asFront(l.body), l.vars.size)
+ def freshVariable[A <: LisaObject[A]](obj: A, name: Identifier): Variable = Variable(freshId(obj.allSchematicLabels.map(_.id), name))
+ def freshVariable[A <: LisaObject[A]](objs: Iterable[A], name: Identifier): Variable = Variable(freshId(objs.flatMap(_.allSchematicLabels).map(_.id), name))
}
diff --git a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
index 2bc2a98405a173ff63d1821cf78421d53c3b8c2b..bfc1523755fcdc3f1fd961db8924b0e4155141a1 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Lambdas.scala
@@ -36,7 +36,7 @@ trait Lambdas extends Common {
*/
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): LambdaExpression[T, R, N] = {
val newSubst = map -- seqBounds
- val conflict = map.values.flatMap(_.freeSchematicLabels).toSet.intersect(bounds.asInstanceOf)
+ val conflict = map.values.flatMap(_.freeSchematicLabels).toSet.intersect(bounds.toSet.asInstanceOf)
if (conflict.nonEmpty) {
val taken = (map.values.flatMap(_.allSchematicLabels).map(_.id) ++ map.keys.map(_.id)).toList
val newBounds = seqBounds.scanLeft[List[Identifier]](taken)((list, v: SchematicLabel[T]) => freshId(list, v.id) :: list).map(_.head).zip(seqBounds).map(v => v._2.rename(v._1))
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index 1f13bf8498f0eb2b309d746687cc6e6f88070e8a..792c75aa199107bbc5f7a6b6fd626f68d47f7350 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -17,8 +17,8 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
case class Sequent(left: Set[Formula], right: Set[Formula]) extends LisaObject[Sequent] with Absolute {
def underlying: lisa.kernel.proof.SequentCalculus.Sequent = K.Sequent(left.map(_.underlying), right.map(_.underlying))
- def allSchematicLabels: Set[SchematicLabel[?]] = left.flatMap(_.allSchematicLabels)
- def freeSchematicLabels: Set[SchematicLabel[?]] = left.flatMap(_.freeSchematicLabels)
+ def allSchematicLabels: Set[SchematicLabel[?]] = left.flatMap(_.allSchematicLabels) ++ right.flatMap(_.allSchematicLabels)
+ def freeSchematicLabels: Set[SchematicLabel[?]] = left.flatMap(_.freeSchematicLabels) ++ right.flatMap(_.freeSchematicLabels)
def substituteUnsafe(map: Map[SchematicLabel[?], ? <: LisaObject[?]]): Sequent = Sequent(left.map(_.substituteUnsafe(map)), right.map(_.substituteUnsafe(map)))
/*Ok for now but what when we have more*/
@@ -89,7 +89,7 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
case (s, p) => (s, Seq(s0, s1, s2) ++ p)
}
- case _ => throw new IllegalArgumentException("Right side of sequent must be a single universaly quantified formula")
+ case _ => throw new IllegalArgumentException("Right side of sequent must be a single universally quantified formula")
}
}
@@ -215,7 +215,7 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
* @tparam S The type of elements in that set
* @tparam T The type to convert from
*/
- protected trait FormulaSetConverter[T] {
+ trait FormulaSetConverter[T] {
def apply(t: T): Set[Formula]
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
index f7bcd5f8fc8cb4892ca7cac0c3b91a2ed38203b0..34f8878fd37e4cbb4b616acd77bf819abcc4bac1 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicMain.scala
@@ -15,6 +15,7 @@ trait BasicMain {
}
val stringWriter: java.io.StringWriter = new java.io.StringWriter()
}
+ export om.output
/**
* This specific implementation make sure that what is "shown" in theory files is only printed for the one we run, and not for the whole library.
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 678cd18cd1f32ad499c04558e0ae76c6d3759069..0501f1b40fb89b60dc9d9677d2f716f32f59bd69 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -446,6 +446,7 @@ object BasicStepTactic {
proof.ValidProofTactic(bot, Seq(K.LeftExists(botK, -1, phiK, xK)), Seq(premise))
}
+ var debug = false
def apply(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
lazy val premiseSequent = proof.getSequent(premise)
lazy val pivot = bot.left.diff(premiseSequent.left)
@@ -470,14 +471,14 @@ object BasicStepTactic {
case Some(F.BinderFormula(F.Exists, x, phi)) => LeftExists.withParameters(phi, x)(premise)(bot)
case _ => proof.InvalidProofTactic("Could not infer an existensially quantified pivot from premise and conclusion.")
}
- } else proof.InvalidProofTactic("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
+ } else proof.InvalidProofTactic("Ambigous application of LeftExists, multiple pivots corresponding to the unquantified formula found.")
else if (pivot.tail.isEmpty)
pivot.head match {
case F.BinderFormula(F.Exists, x, phi) => LeftExists.withParameters(phi, x)(premise)(bot)
case _ => proof.InvalidProofTactic("Could not infer an existentially quantified pivot from premise and conclusion.")
}
else
- proof.InvalidProofTactic("Left-hand side of conclusion + φ is not the same as left-hand side of premise + ∃x. φ.")
+ proof.InvalidProofTactic("Ambigous application of LeftExists, multiple pivots corresponding to the quantified formula found.")
}
}
@@ -1440,7 +1441,7 @@ object BasicStepTactic {
}
}
- // TODO make specific support for subproofs written inside tactics.
+ // TODO make specific support for subproofs written inside tactics.kkkkkkk
inline def TacticSubproof(using proof: Library#Proof)(inline computeProof: proof.InnerProof ?=> Unit): proof.ProofTacticJudgement =
val iProof: proof.InnerProof = new proof.InnerProof(None)
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
index 37460714fec21b08effac3a1ae1309af11d85fb1..9d64e278451f0a5ee0a47d6f36e01b5abc0f1f28 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/Library.scala
@@ -43,6 +43,7 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
def isDraft = _draft.nonEmpty
val knownDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
+ val shortDefs: scala.collection.mutable.Map[F.ConstantLabel[?], Option[JUSTIFICATION]] = scala.collection.mutable.Map.empty
def addSymbol(s: F.ConstantFunctionLabel[?] | F.ConstantPredicateLabel[?] | F.Constant): Unit = {
s match {
@@ -57,6 +58,10 @@ abstract class Library extends lisa.prooflib.WithTheorems with lisa.prooflib.Pro
case None => throw new UserLisaException.UndefinedSymbolException("Unknown symbol", label, this)
case Some(value) => value
}
+ def getShortDefinition(label: F.ConstantLabel[?]): Option[JUSTIFICATION] = shortDefs.get(label) match {
+ case None => throw new UserLisaException.UndefinedSymbolException("Unknown symbol", label, this)
+ case Some(value) => value
+ }
/**
* An alias to create a Theorem
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index e612d0ebae89addeca813a9e4f8adbf38508a0bc..adda8986c435984a2a7e9d8b70411f827e8abe9b 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -1,5 +1,6 @@
package lisa.prooflib
+import lisa.kernel.proof.SCProofChecker.checkSCProof
import lisa.prooflib.BasicStepTactic.Rewrite
import lisa.prooflib.BasicStepTactic.*
import lisa.prooflib.ProofTacticLib.*
@@ -20,13 +21,13 @@ trait ProofsHelpers {
given Library = library
- class HaveSequent private[ProofsHelpers] (bot: Sequent) {
- val x: lisa.fol.FOL.Sequent = bot
+ class HaveSequent /*private[ProofsHelpers]*/ (val bot: Sequent) {
+ // val x: lisa.fol.FOL.Sequent = bot
inline infix def by(using proof: library.Proof, line: sourcecode.Line, file: sourcecode.File): By { val _proof: proof.type } = By(proof, line, file).asInstanceOf
class By(val _proof: library.Proof, line: sourcecode.Line, file: sourcecode.File) {
- private val bot = HaveSequent.this.bot ++ (F.iterable_to_set(_proof.getAssumptions) |- ())
+ val bot = HaveSequent.this.bot ++ (F.iterable_to_set(_proof.getAssumptions) |- ())
inline infix def apply(tactic: Sequent => _proof.ProofTacticJudgement): _proof.ProofStep & _proof.Fact = {
tactic(bot).validate(line, file)
}
@@ -44,7 +45,7 @@ trait ProofsHelpers {
}
- class AndThenSequent private[ProofsHelpers] (bot: Sequent) {
+ class AndThenSequent private[ProofsHelpers] (val bot: Sequent) {
inline infix def by(using proof: library.Proof, line: sourcecode.Line, file: sourcecode.File): By { val _proof: proof.type } =
By(proof, line, file).asInstanceOf[By { val _proof: proof.type }]
@@ -290,7 +291,17 @@ trait ProofsHelpers {
val lambda: LambdaExpression[Term, Term, N],
out: F.Variable,
j: JUSTIFICATION
- ) extends FunctionDefinition[N](fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {}
+ ) extends FunctionDefinition[N](fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {
+
+ private val term = label.applySeq(lambda.bounds.asInstanceOf)
+ private val simpleProp = lambda.body === term
+ val simplePropName = "simpleDef_" + fullName
+ val simpleDef = THM(simpleProp, simplePropName, line, file, InternalStatement)({
+ have(thesis) by Restate.from(this of term)
+ })
+ shortDefs.update(label, Some(simpleDef))
+
+ }
object SimpleFunctionDefinition {
def apply[N <: F.Arity](using om: OutputManager)(fullName: String, line: Int, file: String)(lambda: LambdaExpression[Term, Term, N]): SimpleFunctionDefinition[N] = {
@@ -416,4 +427,17 @@ trait ProofsHelpers {
}
+ /**
+ * Check correctness of the proof, using LISA's logical kernel, to the current point.
+ */
+ def sanityProofCheck(using p: Proof)(message: String): Unit = {
+ val csc = p.toSCProof
+ if checkSCProof(csc).isValid then
+ println("Proof is valid. " + message)
+ Thread.sleep(100)
+ else
+ checkProof(csc)
+ throw Exception("Proof is not valid: " + message)
+ }
+
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
index 8e470c1436be3327df813d8d5a38a317e1ada3e3..d9a2cd98450a6b2d73d49fa364ff096933ec14c2 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
@@ -50,22 +50,22 @@ object SimpleDeducedSteps {
object Discharge extends ProofTactic {
def apply(using lib: Library, proof: lib.Proof)(premises: proof.Fact*)(premise: proof.Fact): proof.ProofTacticJudgement = {
- val ss = premises map (e => proof.getSequent(e))
- val seqs = ss map (e => e.underlying)
+ val ss = premises zip (premises map (e => proof.getSequent(e)))
+ val seqs = ss.map(_._2)
if (!seqs.forall(_.right.size == 1))
return proof.InvalidProofTactic("When discharging this way, the discharged sequent must have only a single formula on the right handside.")
- val s = seqs.head
- val f = s.right.head
- val first = K.Cut((proof.getSequent(premise).underlying removeLeft f) ++ (s removeRight f), -2, -1, f)
-
- proof.ValidProofTactic(
- (proof.getSequent(premise) removeAllLeft (ss.flatMap(_.right).toSet)) ++<< (F.Sequent(ss.flatMap(_.left).toSet, Set())),
- seqs.tail.zipWithIndex.scanLeft(first)((prev, next) => {
- val f = next._1.right.head
- K.Cut((prev.bot removeLeft f) ++ (next._1 removeRight f), -next._2 - 3, next._2, f)
- }),
- proof.mostRecentStep +: premises
- )
+ val seqAny = ss.find((_, s) => premise.statement.left.exists(f2 => F.isSame(s.right.head, f2)))
+ if (seqAny.isEmpty)
+ Restate.from(premise)(premise.statement)
+ else
+ TacticSubproof: ip ?=>
+ ss.foldLeft(premise: ip.Fact)((prem, discharge) =>
+ val seq = discharge._2
+ if prem.statement.left.exists(f => F.isSame(f, seq.right.head)) then
+ val goal = prem.statement -<? seq.right.head ++<? (seq.left |- ())
+ lib.have(Cut(discharge._1, prem)(goal))
+ else prem
+ )
}
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index b6d542ce39788d19f21aef9ff31f90231b847a2e..fc920eb1b7b8a027f88a4a976eb87e0964599828 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -67,6 +67,8 @@ trait WithTheorems {
private var assumptions: List[F.Formula] = assump
private var eliminations: List[(F.Formula, (Int, F.Sequent) => List[K.SCProofStep])] = Nil
+ def cleanAssumptions: Unit = assumptions = Nil
+
/**
* the theorem that is being proved (paritally, if subproof) by this proof.
*
@@ -560,7 +562,6 @@ trait WithTheorems {
val innerJustification: theory.Theorem =
if library._draft.nonEmpty && library._draft.get.value != file
then // if the draft option is activated, and the theorem is not in the file where the draft option is given, then we replace the proof by sorry
- // println("skip!")
theory.theorem(name, goal.underlying, SCProof(SC.Sorry(goal.underlying)), IndexedSeq.empty) match {
case K.Judgement.ValidJustification(just) =>
just
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 122f418d0380e12854820d9ba339db22ec967a2a..70d4045217e2d5016825f1cce37b8b80c588b775 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -348,7 +348,7 @@ object KernelHelpers {
def theorem(name: String, statement: Sequent, proof: SCProof, justifications: Seq[theory.Justification]): RunningTheoryJudgement[theory.Theorem] = {
if (statement == proof.conclusion) theory.makeTheorem(name, statement, proof, justifications)
else if (isSameSequent(statement, proof.conclusion)) theory.makeTheorem(name, statement, proof.appended(Restate(statement, proof.length - 1)), justifications)
- else InvalidJustification(s"The proof proves ${FOLPrinter.prettySequent(proof.conclusion)} instead of claimed ${FOLPrinter.prettySequent(statement)}", None)
+ else InvalidJustification(s"The proof proves \n ${FOLPrinter.prettySequent(proof.conclusion)}\ninstead of claimed \n ${FOLPrinter.prettySequent(statement)}", None)
}
/**
diff --git a/lisa-utils/src/main/scala/lisa/utils/memoization/Memoized.scala b/lisa-utils/src/main/scala/lisa/utils/memoization/Memoized.scala
new file mode 100644
index 0000000000000000000000000000000000000000..43afb55273071cf33022a9153c7e4934e8c8b097
--- /dev/null
+++ b/lisa-utils/src/main/scala/lisa/utils/memoization/Memoized.scala
@@ -0,0 +1,37 @@
+package lisa.utils.memoization
+
+case class MemoizationStats(hits: Int, miss: Int, faulted: Int):
+ def withHit = MemoizationStats(hits + 1, miss, faulted)
+ def withMiss = MemoizationStats(hits, miss + 1, faulted)
+ def withFault = MemoizationStats(hits, miss, faulted + 1)
+
+case object InfiniteRecursionDetectedException extends Exception
+
+class Memoized[From, To](fun: From => To) extends Function[From, To]:
+ private val visited = scala.collection.mutable.HashSet.empty[From]
+ private val memory = scala.collection.mutable.HashMap.empty[From, To]
+ private var stats = MemoizationStats(0, 0, 0)
+
+ protected def handleFault(): To =
+ throw InfiniteRecursionDetectedException
+
+ def apply(v: From): To =
+ val stored = memory.get(v)
+ val seen = visited.contains(v)
+ if stored.isEmpty then
+ // compute
+ visited.add(v)
+ if seen then
+ stats = stats.withFault
+ handleFault()
+ else
+ stats = stats.withMiss
+ memory.update(v, fun(v))
+ else stats = stats.withHit
+ memory(v)
+
+class MemoizedWithDefault[From, To](fun: From => To, default: To) extends Memoized[From, To](fun):
+ override def handleFault(): To = default
+
+def memoized[A, B](f: A => B): A => B = Memoized(f)
+def memoized[A, B](f: A => B, default: B): A => B = MemoizedWithDefault(f, default)
diff --git a/lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala b/lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala
index c74f53614d084679f5d8c565953baae62bc804bd..988ead99857ddd93c1ab4b07db0c96c9e7f8e066 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/TheoriesHelpersTest.scala
@@ -28,7 +28,8 @@ class TheoriesHelpersTest extends AnyFunSuite {
judgement.get
fail("Shouldn't be able to get a theorem from an invalid judgement")
} catch {
- case InvalidJustificationException(msg, None) => assert(msg.matches("The proof proves .* instead of .*"))
+
+ case InvalidJustificationException(msg, None) => ()
}
// same theorem but with correct statement
diff --git a/refman/lisa.pdf b/refman/lisa.pdf
index 8855ed46532f486aef780ff64bb619ca8f1a58e5..80036345874145be30b7dc8a7edc9bd947f413f0 100644
Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ