diff --git a/build.sbt b/build.sbt
index b63857e10c6ab502311a06054cf485a2cee8e468..a8d676f14d721174f4bf58a61d285a702c769b08 100644
--- a/build.sbt
+++ b/build.sbt
@@ -1,28 +1,25 @@
-inThisBuild(
- Def.settings(
- organization := "ch.epfl.lara",
- organizationName := "LARA",
- organizationHomepage := Some(url("https://lara.epfl.ch")),
- licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html")),
- versionScheme := Some("semver-spec"),
- scalacOptions ++= Seq(
+ThisBuild / version := "0.6"
+ThisBuild / homepage := Some(url("https://github.com/epfl-lara/lisa"))
+ThisBuild / startYear := Some(2021)
+ThisBuild / organization := "ch.epfl.lara"
+ThisBuild / organizationName := "LARA"
+ThisBuild / organizationHomepage := Some(url("https://lara.epfl.ch"))
+ThisBuild / licenses := Seq("Apache-2.0" -> url("https://www.apache.org/licenses/LICENSE-2.0.html"))
+ThisBuild / versionScheme := Some("semver-spec")
+ThisBuild / scalacOptions ++= Seq(
"-feature",
"-deprecation",
"-unchecked"
- ),
- javacOptions ++= Seq("-encoding", "UTF-8"),
- semanticdbEnabled := true,
- semanticdbVersion := scalafixSemanticdb.revision,
- scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
- )
-)
+ )
+ThisBuild / javacOptions ++= Seq("-encoding", "UTF-8")
+ThisBuild / semanticdbEnabled := true
+ThisBuild / semanticdbVersion := scalafixSemanticdb.revision
+ThisBuild / scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
+
val commonSettings = Seq(
- version := "0.6",
crossScalaVersions := Seq("2.12.13", "2.13.4", "3.0.1", "3.2.0"),
- organization := "ch.epfl.lara",
- scalacOptions ++= Seq("-Ximport-suggestion-timeout", "0"),
run / fork := true
)
@@ -30,13 +27,11 @@ val commonSettings = Seq(
val scala2 = "2.13.8"
val scala3 = "3.2.2"
-
-
-val commonSettings2 = Seq(
+val commonSettings2 = commonSettings ++ Seq(
scalaVersion := scala2,
scalacOptions ++= Seq("-Ypatmat-exhaust-depth", "50")
)
-val commonSettings3 = Seq(
+val commonSettings3 = commonSettings ++ Seq(
scalaVersion := scala3,
scalacOptions ++= Seq(
"-language:implicitConversions",
@@ -59,6 +54,7 @@ def githubProject(repo: String, commitHash: String) = RootProject(uri(s"$repo#$c
lazy val scallion = githubProject("https://github.com/sankalpgambhir/scallion.git", "6434e21bd08872cf547c8f0efb67c963bfdf4190")
lazy val silex = githubProject("https://github.com/epfl-lara/silex.git", "fc07a8670a5fa8ea2dd5649a00424710274a5d18")
+
scallion/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
silex/scalacOptions ~= (_.filterNot(Set("-Wvalue-discard")))
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index deb0e55f6236db1e9f9c2fc16f794157cda8ec67..0e12da49bfc73f2d8dea3c45f0e743023d501fc2 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -49,15 +49,6 @@ trait Common {
case l: Seq[T] => l.map(f).asInstanceOf[(U ** (N))]
case tup: Tuple => tup.map[[t] =>> U]([u] => (x: u) => f(x.asInstanceOf[T])).asInstanceOf
}
- /*
- object ** {
- def unapply[T, N <: Arity](p: T**N): T***N = ValueOf[N] match {
- case n: -1 => Some(p)
- case n: 0 => if (p.size == 0) Some(EmptyTuple) else None
- case n: _ => if (p.size == n) p match {case Tuple => p; case Seq} else None
- }
- }
- */
}
@@ -235,7 +226,6 @@ trait Common {
def freshRename(taken: Iterable[Identifier]): TermLabel
def mkString(args: Seq[Term]): String
def mkStringSeparated(args: Seq[Term]): String = mkString(args)
- // def unapply(t:Term):Option[Seq[Term]]
}
/**
@@ -327,7 +317,6 @@ trait Common {
override val underlyingLabel: K.VariableLabel = K.VariableLabel(id)
override val underlying = K.VariableTerm(underlyingLabel)
override def apply(args: Term ** 0) = this
- def unapply(t: Variable): Option[Seq[Term]] = if (t == this) Some(Seq()) else None
@nowarn("msg=Unreachable")
override def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Term = {
map.get(this.asInstanceOf) match {
@@ -358,7 +347,6 @@ trait Common {
override val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, 0)
override val underlying = K.Term(underlyingLabel, Seq())
override def apply(args: Term ** 0) = this
- def unapply(t: Constant): Option[Term ** 0] = if (t == this) Some(Seq()) else None
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Constant = this
override def rename(newid: Identifier): Constant = Constant(newid)
def freshRename(taken: Iterable[Identifier]): Constant = rename(K.freshId(taken, id))
@@ -375,7 +363,10 @@ trait Common {
case class SchematicFunctionLabel[N <: Arity](val id: Identifier, val arity: N) extends SchematicTermLabel with SchematicLabel[(Term ** N) |-> Term] with ((Term ** N) |-> Term) {
val underlyingLabel: K.SchematicTermLabel = K.SchematicFunctionLabel(id, arity)
def apply(args: (Term ** N)): Term = AppliedTerm(this, args.toSeq)
- def unapply(t: AppliedTerm): Option[Term ** N] = t match { case AppliedTerm(label, args) if (label == this) => Some(args); case _ => None }
+ def unapplySeq(t: AppliedTerm): Seq[Term] = t match {
+ case AppliedTerm(label, args) if (label == this) => args
+ case _ => Seq.empty
+ }
@nowarn
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): ((Term ** N) |-> Term) = {
map.get(this.asInstanceOf) match {
@@ -403,7 +394,10 @@ trait Common {
val underlyingLabel: K.ConstantFunctionLabel = K.ConstantFunctionLabel(id, arity)
var infix: Boolean = false
def apply(args: (Term ** N)): Term = AppliedTerm(this, args.toSeq)
- def unapply(t: AppliedTerm): Option[Term ** N] = t match { case AppliedTerm(label, args) if (label == this) => Some(args); case _ => None }
+ def unapplySeq(t: AppliedTerm): Seq[Term] = t match {
+ case AppliedTerm(label, args) if (label == this) => args
+ case _ => Seq.empty
+ }
inline def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type =
this
def rename(newid: Identifier): ConstantFunctionLabel[N] = ConstantFunctionLabel(newid, arity)
@@ -509,7 +503,6 @@ trait Common {
val underlyingLabel: K.VariableFormulaLabel = K.VariableFormulaLabel(id)
val underlying = K.PredicateFormula(underlyingLabel, Seq())
override def apply(args: Term ** 0): Formula = this
- def unapply(t: VariableFormula): Option[Term ** 0] = if (t == this) Some(EmptyTuple) else None
@nowarn("msg=Unreachable")
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): Formula = {
map.get(this.asInstanceOf) match {
@@ -539,7 +532,6 @@ trait Common {
val underlyingLabel: K.ConstantPredicateLabel = K.ConstantPredicateLabel(id, 0)
val underlying = K.PredicateFormula(underlyingLabel, Seq())
override def apply(args: Term ** 0): Formula = this
- def unapply(t: ConstantFormula): Option[Term ** 0] = if (t == this) Some(EmptyTuple) else None
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
@@ -556,7 +548,10 @@ trait Common {
case class SchematicPredicateLabel[N <: Arity](id: Identifier, arity: N) extends SchematicVarOrPredLabel with SchematicLabel[(Term ** N) |-> Formula] with ((Term ** N) |-> Formula) {
val underlyingLabel: K.SchematicPredicateLabel = K.SchematicPredicateLabel(id, arity)
def apply(args: (Term ** N)): Formula = PredicateFormula(this, args.toSeq)
- def unapply(t: PredicateFormula): Option[Term ** N] = t match { case PredicateFormula(label, args) if (label == this) => Some(args); case _ => None }
+ def unapplySeq(t: AppliedTerm): Seq[Term] = t match {
+ case AppliedTerm(label, args) if (label == this) => args
+ case _ => Seq.empty
+ }
@nowarn
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): |->[Term ** N, Formula] = {
map.get(this.asInstanceOf) match {
@@ -584,7 +579,10 @@ trait Common {
val underlyingLabel: K.ConstantPredicateLabel = K.ConstantPredicateLabel(id, arity)
private var infix = false
def apply(args: (Term ** N)): Formula = PredicateFormula(this, args.toSeq)
- def unapply(t: PredicateFormula): Option[Term ** N] = t match { case PredicateFormula(label, args) if (label == this) => Some(args); case _ => None }
+ def unapplySeq(f: PredicateFormula): Seq[Term] = f match {
+ case PredicateFormula(label, args) if (label == this) => args
+ case _ => Seq.empty
+ }
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
@@ -656,7 +654,10 @@ trait Common {
}
// def apply(args: Seq[Formula]): Formula = apply(args)
def apply(args: Formula ** N): Formula = ConnectorFormula(this, args.toSeq)
- def unapply(t: ConnectorFormula): Option[Seq[Formula]] = t match { case ConnectorFormula(label, args) if (label == this) => Some(args); case _ => None }
+ def unapplySeq(f: PredicateFormula): Seq[Term] = f match {
+ case PredicateFormula(label, args) if (label == this) => args
+ case _ => Seq.empty
+ }
def freeSchematicLabels: Set[SchematicLabel[?]] = Set(this)
def allSchematicLabels: Set[SchematicLabel[?]] = Set(this)
def rename(newid: Identifier): SchematicConnectorLabel[N] = SchematicConnectorLabel(newid, arity)
@@ -675,7 +676,10 @@ trait Common {
def id: Identifier = underlyingLabel.id
def substituteUnsafe(map: Map[SchematicLabel[_], LisaObject[_]]): this.type = this
def apply(args: Formula ** N): Formula = ConnectorFormula(this, args.toSeq)
- def unapply(t: ConnectorFormula): Option[Seq[Formula]] = t match { case ConnectorFormula(label, args) if (label == this) => Some(args); case _ => None }
+ def unapplySeq(f: ConnectorFormula): Seq[Formula] = f match {
+ case ConnectorFormula(label, args) if (label == this) => args
+ case _ => Seq.empty
+ }
def freeSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def allSchematicLabels: Set[SchematicLabel[?]] = Set.empty
def rename(newid: Identifier): ConstantConnectorLabel[N] = throw new Error("Can't rename a constant connector label")
diff --git a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
index 30002495f67947749f44d1ee459bd46415986818..e4039adf9f798e4b3c2e9b74b61baab86a1a9412 100644
--- a/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/FOLHelpers.scala
@@ -65,7 +65,7 @@ object FOLHelpers {
case n: 0 => Constant(cfl.id)
case n: N => ConstantFunctionLabel[N](cfl.id, n)
def asFrontLabel(stl: K.SchematicTermLabel): SchematicTermLabel = stl match
- case v: K.VariableLabel => asFrontLabel(stl)
+ case v: K.VariableLabel => asFrontLabel(v)
case v: K.SchematicFunctionLabel => asFrontLabel(v)
def asFrontLabel[N <: Arity](sfl: K.SchematicFunctionLabel): SchematicFunctionLabel[N] =
SchematicFunctionLabel(sfl.id, sfl.arity.asInstanceOf)
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index e2bbd1c0d9bd74b8809f74f721e8d3135d79cb20..31c62f3c40029626c4745bea61cba5e90944eee8 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -146,7 +146,10 @@ trait Sequents extends Common with lisa.fol.Lambdas {
infix def --?(s1: Sequent): Sequent = this removeAll s1
infix def ++?(s1: Sequent): Sequent = this addAllIfNotExists s1
- override def toString = left.mkString("; ") + " ⊢ " + right.mkString("; ")
+ override def toString =
+ (if left.size == 1 then left.head.toString else "( " + left.mkString(", ") + " )") +
+ " ⊢ " +
+ (if right.size == 1 then right.head.toString else "( " + right.mkString(", ") + " )")
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 8d066ea2a4a14a14549ddbe1209e7b08b53ec433..80f40640caa88e7b4e6322e3bb517ff961da7a8e 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -1354,25 +1354,34 @@ object BasicStepTactic {
proof.ValidProofTactic(res, Seq(K.InstSchema(botK, -1, mConK, mPredK, mTermK)), Seq(premise))
}
}
+ object Subproof extends ProofTactic {
+ def apply(using proof: Library#Proof)(statement: Option[F.Sequent])(iProof: proof.InnerProof) = {
+ val bot: Option[F.Sequent] = statement
+ val botK: Option[K.Sequent] = statement map (_.underlying)
+ if (iProof.length == 0) throw (new UnimplementedProof(proof.owningTheorem))
+ val scproof: K.SCProof = iProof.toSCProof
+ val premises: Seq[proof.Fact] = iProof.getImports.map(of => of._1)
+ val judgement: proof.ProofTacticJudgement = {
+ if (botK.isEmpty)
+ proof.ValidProofTactic(iProof.mostRecentStep.bot, scproof.steps, premises)
+ else if (!K.isSameSequent(botK.get, scproof.conclusion))
+ proof.InvalidProofTactic(
+ s"The subproof does not prove the desired conclusion.\n\tExpected: ${FOLPrinter.prettySequent(botK.get)}\n\tObtained: ${FOLPrinter.prettySequent(scproof.conclusion)}"
+ )
+ else
+ proof.ValidProofTactic(bot.get, scproof.steps :+ K.Restate(botK.get, scproof.length - 1), premises)
+ }
+ judgement
+ }
+ }
- class SUBPROOF(using val proof: Library#Proof)(statement: Option[F.Sequent])(computeProof: proof.InnerProof ?=> Unit) extends ProofTactic {
+ class SUBPROOF(using val proof: Library#Proof)(statement: Option[F.Sequent])(val iProof: proof.InnerProof) extends ProofTactic {
val bot: Option[F.Sequent] = statement
val botK: Option[K.Sequent] = statement map (_.underlying)
+ if (iProof.length == 0)
+ throw (new UnimplementedProof(proof.owningTheorem))
+ val scproof: K.SCProof = iProof.toSCProof
- val iProof: proof.InnerProof = new proof.InnerProof(statement.asInstanceOf)
- val scproof: K.SCProof = {
- try {
- computeProof(using iProof)
- } catch {
- case e: NotImplementedError =>
- throw (new UnimplementedProof(proof.owningTheorem))
- case e: UserLisaException =>
- throw (e)
- }
- if (iProof.length == 0)
- throw (new UnimplementedProof(proof.owningTheorem))
- iProof.toSCProof
- }
val premises: Seq[proof.Fact] = iProof.getImports.map(of => of._1)
def judgement: proof.ProofTacticJudgement = {
if (botK.isEmpty)
@@ -1384,20 +1393,17 @@ object BasicStepTactic {
}
}
+ // TODO make specific support for subproofs written inside tactics.
+
+ inline def TacticSubproof(using proof: Library#Proof)(inline computeProof: proof.InnerProof ?=> Unit): proof.ProofTacticJudgement =
+ val iProof: proof.InnerProof = new proof.InnerProof(None)
+ computeProof(using iProof)
+ SUBPROOF(using proof)(None)(iProof).judgement.asInstanceOf[proof.ProofTacticJudgement]
+
object Sorry extends ProofTactic with ProofSequentTactic {
def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
proof.ValidProofTactic(bot, Seq(K.Sorry(bot.underlying)), Seq())
}
}
- // TODO make specific support for subproofs written inside tactics.
-
- def TacticSubproof(using proof: Library#Proof)(computeProof: proof.InnerProof ?=> Unit) =
- SUBPROOF(using proof)(None)(computeProof).judgement.asInstanceOf[proof.ProofTacticJudgement]
-
- /*
- def TacticSubproof(using proof: Library#Proof)(botK: Option[Sequent])(computeProof: proof.InnerProof ?=> Unit) =
- SUBPROOF(using proof)(Some(botK))(computeProof).judgement.asInstanceOf[proof.ProofTacticJudgement]
- */
-
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index 037cbf302a5c850c721d2895d396051a48b24bb6..5fe1901e905d8b75b42e3645aac0a36519aea82f 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -35,9 +35,11 @@ trait ProofsHelpers {
}
}
- inline infix def subproof(using proof: Library#Proof, om: OutputManager, line: sourcecode.Line, file: sourcecode.File)(tactic: proof.InnerProof ?=> Unit): proof.ProofStep = {
+ infix def subproof(using proof: Library#Proof, om: OutputManager, line: sourcecode.Line, file: sourcecode.File)(computeProof: proof.InnerProof ?=> Unit): proof.ProofStep = {
val botWithAssumptions = HaveSequent.this.bot ++ (proof.getAssumptions |- ())
- (new BasicStepTactic.SUBPROOF(using proof)(Some(botWithAssumptions))(tactic)).judgement.validate(line, file).asInstanceOf[proof.ProofStep]
+ val iProof: proof.InnerProof = new proof.InnerProof(Some(botWithAssumptions))
+ computeProof(using iProof)
+ (new BasicStepTactic.SUBPROOF(using proof)(Some(botWithAssumptions))(iProof)).judgement.validate(line, file).asInstanceOf[proof.ProofStep]
}
}
@@ -176,6 +178,9 @@ trait ProofsHelpers {
val f: F.Formula,
j: JUSTIFICATION
) extends DEFINITION(line, file) {
+ def repr: String =
+ s" ${if (withSorry) " Sorry" else ""} Definition of function symbol ${label(vars)} := the ${out} such that ${(out === label(vars)) <=> f})\n"
+
// val expr = LambdaExpression[Term, Formula, N](vars, f, valueOf[N])
lazy val label: ConstantFunctionLabelOfArity[N] = (if (vars.length == 0) F.Constant(name) else F.ConstantFunctionLabel[N](name, vars.length.asInstanceOf)).asInstanceOf
@@ -188,8 +193,8 @@ trait ProofsHelpers {
UserInvalidDefinitionException(
name,
s"The given justification is not valid for a definition" +
- s"The justification should be of the form ${FOLPrinter.prettySequent((() |- F.BinderFormula(F.ExistsOne, out, F.VariableFormula("phi"))).underlying)}" +
- s"instead of the given ${FOLPrinter.prettySequent(conclusion.underlying)}"
+ s"The justification should be of the form ${(() |- F.BinderFormula(F.ExistsOne, out, F.VariableFormula("phi")))}" +
+ s"instead of the given ${conclusion.underlying}"
)
)
}
@@ -211,8 +216,8 @@ trait ProofsHelpers {
UserInvalidDefinitionException(
name,
s"The given justification is not valid for a definition" +
- s"The justification should be of the form ${FOLPrinter.prettySequent((() |- F.BinderFormula(F.ExistsOne, out, F.VariableFormula("phi"))).underlying)}" +
- s"instead of the given ${FOLPrinter.prettySequent(conclusion.underlying)}"
+ s"The justification should be of the form ${(() |- F.BinderFormula(F.ExistsOne, out, F.VariableFormula("phi")))}" +
+ s"instead of the given ${conclusion.underlying}"
)
)
}
@@ -283,7 +288,11 @@ trait ProofsHelpers {
val lambda: LambdaExpression[Term, Term, N],
out: F.Variable,
j: JUSTIFICATION
- ) extends FunctionDefinition[N](name, fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {}
+ ) extends FunctionDefinition[N](name, fullName, line, file)(lambda.bounds.asInstanceOf, out, out === lambda.body, j) {
+ override def repr: String =
+ s" Definition of function symbol ${label(lambda.bounds.asInstanceOf)} := ${lambda.body}${if (j.withSorry) " (!! Relies on Sorry)" else ""}\n"
+
+ }
object SimpleFunctionDefinition {
def apply[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(lambda: LambdaExpression[Term, Term, N]): SimpleFunctionDefinition[N] = {
@@ -300,7 +309,8 @@ trait ProofsHelpers {
class PredicateDefinition[N <: F.Arity](using om: OutputManager)(name: String, fullName: String, line: Int, file: String)(val lambda: LambdaExpression[Term, Formula, N])
extends DEFINITION(line, file) {
-
+ override def repr: String =
+ s" Definition of predicate symbol ${label(lambda.bounds.asInstanceOf)} := ${lambda.body}"
lazy val vars: Seq[F.Variable] = lambda.bounds.asInstanceOf
val arity = lambda.arity
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
index 0c8ee41f065852f2c7365e9a50a29bcc8ea75609..8e470c1436be3327df813d8d5a38a317e1ada3e3 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/SimpleDeducedSteps.scala
@@ -160,12 +160,12 @@ object SimpleDeducedSteps {
def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
try {
- val sp = new BasicStepTactic.SUBPROOF(using proof)(Some(bot))({
+ val sp = TacticSubproof {
// lazy val premiseSequent = proof.getSequent(premise)
- val s1 = proof.library.have(bot +<< bot.right.head) by Restate
- proof.library.have(bot) by LeftForall(s1)
- })
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof substitution fail.")
+ val s1 = lib.have(bot +<< bot.right.head) by Restate
+ lib.have(bot) by LeftForall(s1)
+ }
+ BasicStepTactic.unwrapTactic(sp)("Subproof substitution fail.")
} catch {
case e: Exception => proof.InvalidProofTactic("Impossible to justify desired step with instantiation.")
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala b/lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala
index 584bb3b212f458353f690d16d591491102791fa4..b5e720b7b50a19a8807c6dfec096526c0e0a4d4a 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/Substitution.scala
@@ -21,13 +21,13 @@ import F.|-
object Substitution {
def validRule(using lib: lisa.prooflib.Library, proof: lib.Proof)(r: (proof.Fact | F.Formula | lib.JUSTIFICATION)): Boolean =
r match {
- case F.equality(_) => true
- case F.Iff(_) => true
+ case F.equality(_, _) => true
+ case F.Iff(_, _) => true
+ case _: Formula => false
case j: lib.JUSTIFICATION => j.statement.right.size == 1 && validRule(j.statement.right.head)
case f: proof.Fact @unchecked => proof.sequentOfFact(f).right.size == 1 && validRule(proof.sequentOfFact(f).right.head)
// case j: RunningTheory#Justification =>
// proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.size == 1 && validRule(proof.sequentOfFact(j.asInstanceOf[lib.theory.Justification]).right.head)
- case _ => false
}
object ApplyRules extends ProofTactic {
@@ -565,13 +565,13 @@ object Substitution {
case f: proof.Fact =>
val seq = proof.getSequent(f)
val phi = seq.right.head
- val sp = new BasicStepTactic.SUBPROOF(using proof)(None)({
+ val sp = TacticSubproof {
val x = applyLeftRight(phi)(premise)(rightLeft, toLeft, toRight)
proof.library.have(x)
proof.library.andThen(SimpleDeducedSteps.Discharge(f))
- })
+ }
- BasicStepTactic.unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof substitution fail.")
+ BasicStepTactic.unwrapTactic(sp)("Subproof substitution fail.")
}
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index 7b27153f60d16bbcb32af8948de9f75ad3848215..27a9aa6877d158226222afbc7cec71646bd96c86 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -289,7 +289,7 @@ trait WithTheorems {
if (statement.underlying != theory.sequentFromJustification(innerAxiom)) {
throw new InvalidAxiomException("The provided kernel axiom and desired statement don't match.", name, axiom, library)
}
- def repr: String = innerJustification.repr
+ def repr: String = s" Axiom $name := $axiom"
}
def Axiom(name: String, axiom: F.Formula): AXIOM = {
@@ -302,7 +302,7 @@ trait WithTheorems {
// def Axiom(using om: OutputManager, line: Int, file: String)(ax: theory.Axiom): AXIOM = AXIOM(line, file, ax.)
abstract class DEFINITION(line: Int, file: String) extends JUSTIFICATION {
- def repr: String = innerJustification.repr
+
def label: F.ConstantLabel[?]
knownDefs.update(label, Some(this))
@@ -318,7 +318,7 @@ trait WithTheorems {
val innerJustification: theory.Theorem = prove(computeProof)
def prettyGoal: String = lisa.utils.FOLPrinter.prettySequent(goal.underlying)
- def repr: String = innerJustification.repr
+ def repr: String = s" ${if (withSorry) " Sorry" else ""} Theorem $name := $statement\n"
private def prove(computeProof: Proof ?=> Unit): theory.Theorem = {
try {
diff --git a/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala b/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
index f1dc59402eccc2edf0d0e58c96e1ac097cbb14d9..3e3264e7f6e19bb5e630c2d494d1aeff696312d7 100644
--- a/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
+++ b/src/main/scala/lisa/automation/settheory/SetTheoryTactics.scala
@@ -71,7 +71,7 @@ object SetTheoryTactics {
* import ∃ z. t ∈ z <=> (t ∈ x /\ P(t, x)) |- ∃! z. t ∈ z <=> (t ∈ x /\ P(t, x)) Unique by Extension [[uniqueByExtension]] Instantiation
* have () |- ∃! z. t ∈ z <=> (t ∈ x /\ P(t, x)) Cut
*/
- val sp = SUBPROOF(using proof)(Some(botWithAssumptions)) { // TODO check if isInstanceOf first
+ val sp = TacticSubproof { // TODO check if isInstanceOf first
val existence = have(() |- exists(t1, fprop(t1))) by Weakening(comprehensionSchema of (z -> originalSet, φ -> separationPredicate))
val existsToUnique = have(exists(t1, fprop(t1)) |- existsOne(t1, fprop(t1))) by Weakening(SetTheory.uniqueByExtension of schemPred -> lambda(t2, prop))
@@ -81,7 +81,7 @@ object SetTheoryTactics {
}
// safely check, unwrap, and return the proof judgement
- unwrapTactic(sp.judgement.asInstanceOf[proof.ProofTacticJudgement])("Subproof for unique comprehension failed.")
+ unwrapTactic(sp)("Subproof for unique comprehension failed.")
}
}