From 15976bf5c6c358cc5c1ac980eea1e8d3a0c163b0 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@bluewin.ch>
Date: Tue, 25 Oct 2022 11:31:37 +0200
Subject: [PATCH] Quickfix (#83)
* Correct bug related to instantiatePredicateSchemas not instantiating variable formulas
* Corrected bug linked to the equivalence checker no distinguishing schematic and constant symbols
* removed the display parameter from kernel subproofs
* Removed display option from subproof. Add back the missing RewriteTrue case in the printer. Correct issue with equivalence checker.
* scalafix
---
build.sbt | 1 +
.../front/parser/KernelRuleIdentifiers.scala | 3 +--
.../lisa/kernel/fol/EquivalenceChecker.scala | 20 +++++++++++++++----
.../scala/lisa/kernel/fol/Substitutions.scala | 2 +-
.../lisa/kernel/proof/SCProofChecker.scala | 2 +-
.../lisa/kernel/proof/SequentCalculus.scala | 2 +-
.../src/main/scala/lisa/utils/Printer.scala | 4 ++--
.../main/scala/lisa/utils/ProofsShrink.scala | 18 ++++++++---------
.../lisa/utils/tactics/BasicStepTactic.scala | 2 +-
.../utils/tactics/SimpleDeducedSteps.scala | 2 +-
.../lisa/proven/mathematics/SetTheory.scala | 15 +++++---------
.../ProofUnconditionalizer.scala | 7 ++++---
12 files changed, 43 insertions(+), 35 deletions(-)
diff --git a/build.sbt b/build.sbt
index 82262342..19b56224 100644
--- a/build.sbt
+++ b/build.sbt
@@ -10,6 +10,7 @@ inThisBuild(
"-deprecation",
"-unchecked"
),
+ javacOptions ++= Seq("-encoding", "UTF-8"),
semanticdbEnabled := true,
semanticdbVersion := scalafixSemanticdb.revision,
scalafixDependencies += "com.github.liancheng" %% "organize-imports" % "0.6.0"
diff --git a/lisa-front/src/main/scala/lisa/front/parser/KernelRuleIdentifiers.scala b/lisa-front/src/main/scala/lisa/front/parser/KernelRuleIdentifiers.scala
index 4a66a974..e9d4abff 100644
--- a/lisa-front/src/main/scala/lisa/front/parser/KernelRuleIdentifiers.scala
+++ b/lisa-front/src/main/scala/lisa/front/parser/KernelRuleIdentifiers.scala
@@ -85,8 +85,7 @@ private[front] case class KernelRuleIdentifiers(symbols: FrontSymbols) {
case _: SC.RightSubstIff => RightSubstIff
case _: SC.InstFunSchema => FunInstantiation
case _: SC.InstPredSchema => PredInstantiation
- case SC.SCSubproof(_, _, true) => SubproofShown
- case SC.SCSubproof(_, _, false) => SubproofHidden
+ case _: SC.SCSubproof => SubproofShown
}
}
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
index 7949c815..b81d1244 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -201,7 +201,10 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
if (phi.normalForm.nonEmpty) return pDisjNormal(phi.normalForm.get, acc)
val r: List[NormalFormula] = phi match {
case SimplePredicate(id, args) =>
- val lab = "pred_" + id.id + "_" + id.arity
+ val lab = id match {
+ case _: ConstantPredicateLabel => "cons_pred_" + id.id + "_" + id.arity
+ case _: SchematicVarOrPredLabel => "schem_pred_" + id.id + "_" + id.arity
+ }
if (id == top) {
phi.normalForm = Some(NLiteral(true))
} else if (id == bot) {
@@ -216,7 +219,10 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
}
phi.normalForm.get :: acc
case SimpleConnector(id, args) =>
- val lab = "conn_" + id.id + "_" + id.arity
+ val lab = id match {
+ case _: ConstantConnectorLabel => "cons_conn_" + id.id + "_" + id.arity
+ case _: SchematicConnectorLabel => "schem_conn_" + id.id + "_" + id.arity
+ }
phi.normalForm = Some(NormalConnector(id, args.map(_.normalForm.get), updateCodesSig((lab, args map OCBSLCode))))
phi.normalForm.get :: acc
case SNeg(child) => pNeg(child, phi, acc)
@@ -243,7 +249,10 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
if (phi.normalForm.nonEmpty) return pNegNormal(phi.normalForm.get, parent, acc)
val r: List[NormalFormula] = phi match {
case SimplePredicate(id, args) =>
- val lab = "pred_" + id.id + "_" + id.arity
+ val lab = id match {
+ case _: ConstantPredicateLabel => "cons_pred_" + id.id + "_" + id.arity
+ case _: SchematicVarOrPredLabel => "schem_pred_" + id.id + "_" + id.arity
+ }
if (id == top) {
phi.normalForm = Some(NLiteral(true))
parent.normalForm = Some(NLiteral(false))
@@ -265,7 +274,10 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
}
parent.normalForm.get :: acc
case SimpleConnector(id, args) =>
- val lab = "conn_" + id.id + "_" + id.arity
+ val lab = id match {
+ case _: ConstantConnectorLabel => "cons_conn_" + id.id + "_" + id.arity
+ case _: SchematicConnectorLabel => "schem_conn_" + id.id + "_" + id.arity
+ }
phi.normalForm = Some(NormalConnector(id, args.map(_.normalForm.get), updateCodesSig((lab, args map OCBSLCode))))
parent.normalForm = Some(NNeg(phi.normalForm.get, updateCodesSig(("neg", List(phi.normalForm.get.code)))))
parent.normalForm.get :: acc
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
index 7f810269..cd8bdc3d 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -155,7 +155,7 @@ trait Substitutions extends FormulaDefinitions {
phi match {
case PredicateFormula(label, args) =>
label match {
- case label: SchematicPredicateLabel if m.contains(label) => m(label)(args)
+ case label: SchematicVarOrPredLabel if m.contains(label) => m(label)(args)
case _ => phi
}
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchemas(_, m)))
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 822bd7fa..1f222193 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -466,7 +466,7 @@ object SCProofChecker {
SCInvalidProof(SCProof(step), Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
else SCInvalidProof(SCProof(step), Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
- case SCSubproof(sp, premises, _) =>
+ case SCSubproof(sp, premises) =>
if (premises.size == sp.imports.size) {
val invalid = premises.zipWithIndex.find { case (no, p) => !isSameSequent(ref(no), sp.imports(p)) }
if (invalid.isEmpty) {
diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 16fa26ef..e812ad6f 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -329,7 +329,7 @@ object SequentCalculus {
* @param display A boolean value indicating whether the subproof needs to be expanded when printed. Should probably go and
* be replaced by encapsulation.
*/
- case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display: Boolean = true) extends SCProofStep {
+ case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty) extends SCProofStep {
// premises is a list of ints similar to t1, t2... that verifies that imports of the subproof sp are justified by previous steps.
val bot: Sequent = sp.conclusion
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
index 75c5837e..b68c8281 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Printer.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala
@@ -123,11 +123,12 @@ object Printer {
)
step match {
- case sp @ SCSubproof(_, _, display) if display || forceDisplaySubproofs =>
+ case sp @ SCSubproof(_, _) =>
pretty("Subproof", sp.premises*) +: prettySCProofRecursive(sp.sp, level + 1, currentTree, (if (i == 0) topMostIndices else IndexedSeq.empty) :+ i)
case other =>
val line = other match {
case Rewrite(_, t1) => pretty("Rewrite", t1)
+ case RewriteTrue(_) => pretty("RewriteTrue")
case Hypothesis(_, _) => pretty("Hypo.")
case Cut(_, t1, t2, _) => pretty("Cut", t1, t2)
case LeftAnd(_, t1, _, _) => pretty("Left ∧", t1)
@@ -155,7 +156,6 @@ object Printer {
case RightSubstIff(_, t1, _, _) => pretty("R. SubstIff", t1)
case InstFunSchema(_, t1, _) => pretty("?Fun Instantiation", t1)
case InstPredSchema(_, t1, _) => pretty("?Pred Instantiation", t1)
- case SCSubproof(_, _, false) => pretty("Subproof (hidden)")
case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
}
Seq(line)
diff --git a/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala b/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
index c9ada08f..d6772d1d 100644
--- a/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/ProofsShrink.scala
@@ -19,7 +19,7 @@ object ProofsShrink {
*/
def proofSize(proof: SCProof): Int =
proof.steps.map {
- case SCSubproof(sp, _, _) => 1 + proofSize(sp)
+ case SCSubproof(sp, _) => 1 + proofSize(sp)
case _ => 1
}.sum
@@ -30,7 +30,7 @@ object ProofsShrink {
*/
def proofDepth(proof: SCProof): Int =
proof.steps.map {
- case SCSubproof(sp, _, _) => 1 + proofDepth(sp)
+ case SCSubproof(sp, _) => 1 + proofDepth(sp)
case _ => 1
}.max
@@ -88,7 +88,7 @@ object ProofsShrink {
val (finalAcc, _) = steps.foldLeft((IndexedSeq.empty[SCProofStep], IndexedSeq.empty[(Int, Sequent)])) { case ((acc, localToGlobal), step) =>
def resolve(i: Int): (Int, Sequent) = if (i >= 0) localToGlobal(i) else topPremises(-i - 1)
val newAcc = step match {
- case SCSubproof(subProof, subPremises, _) =>
+ case SCSubproof(subProof, subPremises) =>
val (rewrittenPremises, rewrittenSeq) = subPremises.zipWithIndex.flatMap { case (i, j) =>
val (k, sequent) = resolve(i)
val imported = subProof.imports(j)
@@ -123,9 +123,9 @@ object ProofsShrink {
def deadStepsEliminationInternal(proof: SCProof, eliminateDeadImports: Boolean): (SCProof, IndexedSeq[Int]) = {
// We process the leaves first, otherwise we could miss dead branches (subproofs that more imports than necessary)
val processedSteps = proof.steps.map {
- case SCSubproof(sp, premises, display) =>
+ case SCSubproof(sp, premises) =>
val (newSubProof, newImportsIndices) = deadStepsEliminationInternal(sp, true)
- SCSubproof(newSubProof, newImportsIndices.map(premises), display)
+ SCSubproof(newSubProof, newImportsIndices.map(premises))
case other => other
}
val graph = processedSteps.map(_.premises)
@@ -202,8 +202,8 @@ object ProofsShrink {
&& step.premises.sizeIs == 1 && isSequentSubset(getSequentLocal(step.premises.head), step.bot) =>
Left(Weakening(step.bot, step.premises.head))
// Recursive
- case SCSubproof(sp, premises, display) =>
- Left(SCSubproof(simplifyProof(sp), premises, display))
+ case SCSubproof(sp, premises) =>
+ Left(SCSubproof(simplifyProof(sp), premises))
// Double rewrite
case Rewrite(bot1, LocalStep(Rewrite(bot2, t2))) if isSameSequent(bot1, bot2) =>
Left(Rewrite(bot1, t2))
@@ -267,8 +267,8 @@ object ProofsShrink {
val (newSteps, _, _) = proof.steps.zipWithIndex.foldLeft((IndexedSeq.empty[SCProofStep], initialMap, initialCache)) { case ((acc, map, cache), (step, i)) =>
val sequent = step.bot
val mappedStep = mapPremises(step, map) match {
- case SCSubproof(sp, premises, display) =>
- SCSubproof(factorProof(sp), premises, display)
+ case SCSubproof(sp, premises) =>
+ SCSubproof(factorProof(sp), premises)
case other => other
}
val (newMap, newCache) = cache.get(sequent) match {
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
index 612bd42a..4f2651e8 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -958,7 +958,7 @@ object BasicStepTactic {
case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display: Boolean = true) extends ProofStep {
def asSCProof(currentProof: Library#Proof): ProofStepJudgement =
sp match {
- case sp: SCProof => SC.SCSubproof(sp, premises, display)
+ case sp: SCProof => SC.SCSubproof(sp, premises)
}
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
index 5516124b..5bb30600 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
@@ -278,7 +278,7 @@ object SimpleDeducedSteps {
res match {
case ProofStepJudgement.InvalidProofStep(_, _) => res
- case ProofStepJudgement.ValidProofStep(SC.SCSubproof(proof: SCProof, _, _)) => {
+ case ProofStepJudgement.ValidProofStep(SC.SCSubproof(proof: SCProof, _)) => {
// check if the same sequent was obtained
SC.SCSubproof(
proof withNewSteps IndexedSeq(SC.Rewrite(bot, proof.length - 1)),
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index 1b902db3..6f0d4304 100644
--- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala
+++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
@@ -93,8 +93,7 @@ object SetTheory extends lisa.Main {
val p1_3 = SC.RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g)))
SCProof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom))
},
- Seq(-1),
- display = true
+ Seq(-1)
) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
val p1 = SC.SCSubproof(
{
@@ -102,8 +101,7 @@ object SetTheory extends lisa.Main {
val p1_1 = instantiateForall(SCProof(IndexedSeq(p1_0), IndexedSeq(() |- pairAxiom)), x, y, z)
p1_1
},
- Seq(-1),
- display = true
+ Seq(-1)
) // |- (z in {x,y}) <=> (z=x \/ z=y)
val p2 = SC.SCSubproof(
{
@@ -157,8 +155,7 @@ object SetTheory extends lisa.Main {
val pa0_1_5 = SC.RightIff(emptySeq +> ((f1 \/ f1) <=> f1), 2, 4, (f1 \/ f1), f1)
val r = SCProof(pa0_0_0, pa0_1_1, pa0_1_2, pa0_1_3, pa0_1_4, pa0_1_5)
r
- },
- display = false
+ }
) // |- (((z=x)∨(z=x))↔(z=x))
val pa0_1 = SC.RightSubstEq(
emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)),
@@ -185,8 +182,7 @@ object SetTheory extends lisa.Main {
val pa1_0 = SC.RightRefl(emptySeq +> (y1 === y1), y1 === y1)
val pa1_1 = SC.RightOr(emptySeq +> ((y1 === y1) \/ (y1 === x1)), 0, y1 === y1, y1 === x1)
SCProof(pa1_0, pa1_1)
- },
- display = false
+ }
) // |- (y'=x' \/ y'=y')
val ra3 = byEquiv(pa0.bot.right.head, pa1.bot.right.head)(pa0, pa1) // ({x,y}={x',y'}) y=x|- ((y'=x)
val pal = SC.RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g))
@@ -210,8 +206,7 @@ object SetTheory extends lisa.Main {
val pa1_0 = SC.RightRefl(emptySeq +> (y === y), y === y)
val pa1_1 = SC.RightOr(emptySeq +> ((y === y) \/ (y === x)), 0, y === y, y === x)
SCProof(pa1_0, pa1_1)
- },
- display = false
+ }
) // |- (y=x)∨(y=y)
val rb0 = byEquiv(pb0_0.bot.right.head, pb0_1.bot.right.head)(pb0_0, pb0_1) // ({x,y}={x',y'}) |- (y=x')∨(y=y')
val pb1 =
diff --git a/src/main/scala/lisa/utilities/prooftransform/ProofUnconditionalizer.scala b/src/main/scala/lisa/utilities/prooftransform/ProofUnconditionalizer.scala
index fa9dba79..61ff2b0d 100644
--- a/src/main/scala/lisa/utilities/prooftransform/ProofUnconditionalizer.scala
+++ b/src/main/scala/lisa/utilities/prooftransform/ProofUnconditionalizer.scala
@@ -224,7 +224,7 @@ case class ProofUnconditionalizer(prOrig: SCProof) extends ProofTransformer(prOr
})
// We must separate the case for subproofs for they need to use the modified version of the precedent
val inner = pS match {
- case SCSubproof(_, _, _) =>
+ case SCSubproof(_, _) =>
SCProof(
hypothesis.toIndexedSeq ++ rewrites.toIndexedSeq ++ IndexedSeq(
mapStep(
@@ -275,6 +275,7 @@ case class ProofUnconditionalizer(prOrig: SCProof) extends ProofTransformer(prOr
*/
protected def mapStep(pS: SCProofStep, f: Set[Formula] => Set[Formula], fi: Seq[Int] => Seq[Int] = identity, fsub: Seq[Sequent] = Nil): SCProofStep = pS match {
case Rewrite(bot, t1) => Rewrite(f(bot.left) |- bot.right, fi(pS.premises).head)
+ case RewriteTrue(bot) => RewriteTrue(f(bot.left) |- bot.right)
case Hypothesis(bot, phi) => Hypothesis(f(bot.left) |- bot.right, phi)
case Cut(bot, t1, t2, phi) => Cut(f(bot.left) |- bot.right, fi(pS.premises).head, fi(pS.premises).last, phi)
case LeftAnd(bot, t1, phi, psi) => LeftAnd(f(bot.left) |- bot.right, fi(pS.premises).head, phi, psi)
@@ -302,8 +303,8 @@ case class ProofUnconditionalizer(prOrig: SCProof) extends ProofTransformer(prOr
case RightSubstIff(bot, t1, equals, lambdaPhi) => RightSubstIff(f(bot.left) |- bot.right, fi(pS.premises).head, equals, lambdaPhi)
case InstFunSchema(bot, t1, insts) => InstFunSchema(instantiateFunctionSchemaInSequent(f(bot.left) |- bot.right, insts).left |- bot.right, fi(pS.premises).head, insts)
case InstPredSchema(bot, t1, insts) => InstPredSchema(instantiatePredicateSchemaInSequent(f(bot.left) |- bot.right, insts).left |- bot.right, fi(pS.premises).head, insts)
- case SCSubproof(pp, t, b) => {
- SCSubproof(ProofUnconditionalizer(pp).transformPrivate(fsub.toIndexedSeq ++ t.filter(_ >= 0).map(i => appended_steps(i).bot).toIndexedSeq), fi(t), b)
+ case SCSubproof(pp, t) => {
+ SCSubproof(ProofUnconditionalizer(pp).transformPrivate(fsub.toIndexedSeq ++ t.filter(_ >= 0).map(i => appended_steps(i).bot).toIndexedSeq), fi(t))
}
}
--
GitLab