From dd55c7f2699bf1aa6d9f04ed2db331f7370dbd62 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <simon.guilloud@bluewin.ch>
Date: Thu, 27 Oct 2022 12:02:24 +0200
Subject: [PATCH] Substitutions (#84)
* Simple tactic for substitution of equals for equals and equivalent for equivalents.
* Some corrections in the EquivalenceChecker
* Moved InstantiateBinder to helpers.
* Some more changes regarding tactics and proof steps.
---
lisa-examples/src/main/scala/Example.scala | 1 +
.../lisa/kernel/fol/EquivalenceChecker.scala | 124 ++++++-----
.../scala/lisa/kernel/fol/Substitutions.scala | 3 -
.../main/scala/lisa/utils/KernelHelpers.scala | 10 +
.../lisa/utils/tactics/BasicStepTactic.scala | 1 +
.../lisa/utils/tactics/ProofsHelpers.scala | 8 +
.../utils/tactics/SimpleDeducedSteps.scala | 11 +-
.../automation/kernel/SimpleSimplifier.scala | 208 ++++++++++++++++++
8 files changed, 301 insertions(+), 65 deletions(-)
create mode 100644 src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala
diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 00a566cf..3737c53e 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -1,5 +1,6 @@
import lisa.Main
import lisa.automation.kernel.SimplePropositionalSolver.*
+import lisa.automation.kernel.SimpleSimplifier.*
import lisa.kernel.fol.FOL.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
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 b81d1244..e7a0fe25 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/EquivalenceChecker.scala
@@ -58,62 +58,71 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
* A class that encapsulate "runtime" information of the equivalence checker. It performs memoization for efficiency.
*/
class LocalEquivalenceChecker {
- private val unsugaredVersion = scala.collection.mutable.HashMap[Formula, SimpleFormula]()
+ private val unsugaredVersion = scala.collection.mutable.HashMap[Formula, SimpleFormula]()
// transform a LISA formula into a simpler, desugarised version with less symbols. Conjunction, implication, iff, existsOne are treated as alliases and translated.
- def removeSugar(phi: Formula): SimpleFormula = unsugaredVersion.getOrElseUpdate(
- phi, {
- phi match {
- case PredicateFormula(label, args) => SimplePredicate(label, args.toList)
- case ConnectorFormula(label, args) =>
- label match {
- case Neg => SNeg(removeSugar(args(0)))
- case Implies =>
- val l = removeSugar(args(0))
- val r = removeSugar(args(1))
- SOr(List(SNeg(l), r))
- case Iff =>
- val l = removeSugar(args(0))
- val r = removeSugar(args(1))
- val c1 = SNeg(SOr(List(SNeg(l), r)))
- val c2 = SNeg(SOr(List(SNeg(r), l)))
- SNeg(SOr(List(c1, c2)))
- case And =>
- SNeg(SOr(args.map(c => SNeg(removeSugar(c))).toList))
- case Or => SOr((args map removeSugar).toList)
- case _ => SimpleConnector(label, args.toList.map(removeSugar))
- }
- case BinderFormula(label, bound, inner) =>
- label match {
- case Forall => SForall(bound.id, removeSugar(inner))
- case Exists => SExists(bound.id, removeSugar(inner))
- case ExistsOne =>
- val y = VariableLabel(freshId(inner.freeVariables.map(_.id), bound.id))
- val c1 = SimplePredicate(equality, List(VariableTerm(bound), VariableTerm(y)))
- val c2 = removeSugar(inner)
- val c1_c2 = SOr(List(SNeg(c1), c2))
- val c2_c1 = SOr(List(SNeg(c2), c1))
- SExists(y.id, SForall(bound.id, SNeg(SOr(List(SNeg(c1_c2), SNeg(c2_c1))))))
- }
- }
+ def removeSugar1(phi: Formula): SimpleFormula = {
+ phi match {
+ case PredicateFormula(label, args) =>
+ if (label == top) SLiteral(true)
+ else if (label == bot) SLiteral(false)
+ else SimplePredicate(label, args.toList)
+ case ConnectorFormula(label, args) =>
+ label match {
+ case Neg => SNeg(removeSugar1(args(0)))
+ case Implies =>
+ val l = removeSugar1(args(0))
+ val r = removeSugar1(args(1))
+ SOr(List(SNeg(l), r))
+ case Iff =>
+ val l = removeSugar1(args(0))
+ val r = removeSugar1(args(1))
+ val c1 = SNeg(SOr(List(SNeg(l), r)))
+ val c2 = SNeg(SOr(List(SNeg(r), l)))
+ SNeg(SOr(List(c1, c2)))
+ case And =>
+ SNeg(SOr(args.map(c => SNeg(removeSugar1(c))).toList))
+ case Or => SOr((args map removeSugar1).toList)
+ case _ => SimpleConnector(label, args.toList.map(removeSugar1))
+ }
+ case BinderFormula(label, bound, inner) =>
+ label match {
+ case Forall => SForall(bound.id, removeSugar1(inner))
+ case Exists => SExists(bound.id, removeSugar1(inner))
+ case ExistsOne =>
+ val y = VariableLabel(freshId(inner.freeVariables.map(_.id), bound.id))
+ val c1 = SimplePredicate(equality, List(VariableTerm(bound), VariableTerm(y)))
+ val c2 = removeSugar1(inner)
+ val c1_c2 = SOr(List(SNeg(c1), c2))
+ val c2_c1 = SOr(List(SNeg(c2), c1))
+ SExists(y.id, SForall(bound.id, SNeg(SOr(List(SNeg(c1_c2), SNeg(c2_c1))))))
+ }
}
- )
+ }
+
+ def toLocallyNameless(t: Term, subst: Map[VariableLabel, Int], i: Int): Term = {
+ t match {
+ case Term(label: VariableLabel, _) =>
+ if (subst.contains(label)) VariableTerm(VariableLabel("x" + (i - subst(label))))
+ else VariableTerm(VariableLabel("_" + label.id))
+ case Term(label, args) => Term(label, args.map(c => toLocallyNameless(c, subst, i)))
+ }
+ }
- def toLocallyNameless(t: Term, subst: Map[VariableLabel, Int], i: Int): Term = t match {
- case Term(label: VariableLabel, _) =>
- if (subst.contains(label)) VariableTerm(VariableLabel("x" + (i - subst(label))))
- else VariableTerm(VariableLabel("_" + label))
- case Term(label, args) => Term(label, args.map(c => toLocallyNameless(c, subst, i)))
+ def toLocallyNameless(phi: SimpleFormula, subst: Map[VariableLabel, Int], i: Int): SimpleFormula = {
+ phi match {
+ case SimplePredicate(id, args) => SimplePredicate(id, args.map(c => toLocallyNameless(c, subst, i)))
+ case SimpleConnector(id, args) => SimpleConnector(id, args.map(f => toLocallyNameless(f, subst, i)))
+ case SNeg(child) => SNeg(toLocallyNameless(child, subst, i))
+ case SOr(children) => SOr(children.map(toLocallyNameless(_, subst, i)))
+ case SForall(x, inner) => SForall("", toLocallyNameless(inner, subst + (VariableLabel(x) -> i), i + 1))
+ case SExists(x, inner) => SExists("", toLocallyNameless(inner, subst + (VariableLabel(x) -> i), i + 1))
+ case SLiteral(b) => phi
+ }
}
- def toLocallyNameless(phi: SimpleFormula, subst: Map[VariableLabel, Int], i: Int): SimpleFormula = phi match {
- case SimplePredicate(id, args) => SimplePredicate(id, args.map(c => toLocallyNameless(c, subst, i)))
- case SimpleConnector(id, args) => SimpleConnector(id, args.map(f => toLocallyNameless(f, subst, i)))
- case SNeg(child) => SNeg(toLocallyNameless(child, subst, i))
- case SOr(children) => SOr(children.map(toLocallyNameless(_, subst, i)))
- case SForall(x, inner) => SForall("", toLocallyNameless(inner, subst + (VariableLabel(x) -> i), i + 1))
- case SExists(x, inner) => SExists("", toLocallyNameless(inner, subst + (VariableLabel(x) -> i), i + 1))
- case SLiteral(b) => phi
+ def removeSugar(phi: Formula): SimpleFormula = {
+ unsugaredVersion.getOrElseUpdate(phi, toLocallyNameless(removeSugar1(phi), Map.empty, 0))
}
private val codesSig: mutable.HashMap[(String, Seq[Int]), Int] = mutable.HashMap()
@@ -130,7 +139,6 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
codesSigTerms.getOrElseUpdate((label, Nil), codesSigTerms.size)
case Term(label, args) =>
val c = args map codesOfTerm
-
codesSigTerms.getOrElseUpdate((label, c), codesSigTerms.size)
}
)
@@ -274,10 +282,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
}
parent.normalForm.get :: acc
case SimpleConnector(id, args) =>
- val lab = id match {
- case _: ConstantConnectorLabel => "cons_conn_" + id.id + "_" + id.arity
- case _: SchematicConnectorLabel => "schem_conn_" + id.id + "_" + id.arity
- }
+ val lab = "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
@@ -343,7 +348,7 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
def check(formula1: Formula, formula2: Formula): Boolean = {
getCode(formula1) == getCode(formula2)
}
- def getCode(formula: Formula): Int = OCBSLCode(toLocallyNameless(removeSugar(formula), Map.empty, 0))
+ def getCode(formula: Formula): Int = OCBSLCode(removeSugar(formula))
def isSame(term1: Term, term2: Term): Boolean = codesOfTerm(term1) == codesOfTerm(term2)
@@ -359,13 +364,17 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
val codesSet1 = s1.map(this.getCode)
val codesSet2 = s2.map(this.getCode)
codesSet1.subsetOf(codesSet2)
-
}
+
def contains(s: Set[Formula], f: Formula): Boolean = {
val codesSet = s.map(this.getCode)
val codesFormula = this.getCode(f)
codesSet.contains(codesFormula)
}
+ def normalForm(phi: Formula): NormalFormula = {
+ getCode(phi)
+ removeSugar(phi).normalForm.get
+ }
}
def isSame(term1: Term, term2: Term): Boolean = (new LocalEquivalenceChecker).isSame(term1, term2)
@@ -377,4 +386,5 @@ private[fol] trait EquivalenceChecker extends FormulaDefinitions {
def isSubset(s1: Set[Formula], s2: Set[Formula]): Boolean = (new LocalEquivalenceChecker).isSubset(s1, s2)
def contains(s: Set[Formula], f: Formula): Boolean = (new LocalEquivalenceChecker).contains(s, f)
+
}
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 cd8bdc3d..2e743aa0 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -195,7 +195,4 @@ trait Substitutions extends FormulaDefinitions {
}
}
- @deprecated
- def instantiateBinder(f: BinderFormula, t: Term): Formula = substituteVariables(f.inner, Map(f.bound -> t))
-
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index 16af6f19..c8f42e39 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -199,4 +199,14 @@ trait KernelHelpers {
given Conversion[String, Term] = parseTerm(_)
given Conversion[String, VariableLabel] = s => VariableLabel(if (s.head == '?') s.tail else s)
+ def lambda(x: VariableLabel, t: Term) = LambdaTermTerm(Seq(x), t)
+ def lambda(xs: Seq[VariableLabel], t: Term) = LambdaTermTerm(xs, t)
+
+ def lambda(x: VariableLabel, phi: Formula) = LambdaTermFormula(Seq(x), phi)
+ def lambda(xs: Seq[VariableLabel], phi: Formula) = LambdaTermFormula(xs, phi)
+
+ def lambda(X: VariableFormulaLabel, phi: Formula) = LambdaFormulaFormula(Seq(X), phi)
+ def lambda(Xs: Seq[VariableFormulaLabel], phi: Formula) = LambdaFormulaFormula(Xs, phi)
+
+ def instantiateBinder(f: BinderFormula, t: Term): Formula = substituteVariables(f.inner, Map(f.bound -> t))
}
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 4f2651e8..9c02f590 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/BasicStepTactic.scala
@@ -5,6 +5,7 @@ import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SequentCalculus.SCProofStep
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.proof.{SequentCalculus => SC}
+import lisa.utils.Helpers.*
import lisa.utils.Library
import lisa.utils.tactics.ProofStepLib.{_, given}
diff --git a/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
index 2fa04fdd..3471a8b4 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/ProofsHelpers.scala
@@ -87,6 +87,10 @@ trait ProofsHelpers {
proofStack.head.newImportedFact(just)
}
+ def andThen(pswp: ProofStepWithoutPrem)(using String => Unit)(using Throwable => Nothing): library.Proof#DoubleStep = {
+ val r = pswp.asProofStep(Seq(proof.mostRecentStep._2))
+ r.validate(library)
+ }
/**
* Assume the given formula in all future left hand-side of claimed sequents.
@@ -107,6 +111,10 @@ trait ProofsHelpers {
}
}
+ extension (pswp: ProofStepWithoutPrem) {
+ def by(premises: Seq[Library#Proof#Fact])(using String => Unit)(using Throwable => Nothing) = pswp.asProofStep(premises).validate(library)
+ }
+
given Conversion[ProofStepWithoutBotNorPrem[0], ProofStepWithoutBot] = _.asProofStepWithoutBot(Seq())
// case class InstantiatedJustification(just:theory.Justification, instsPred: Map[SchematicVarOrPredLabel, LambdaTermFormula], instsTerm: Map[SchematicTermLabel, LambdaTermTerm], instForall:Seq[Term])
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 5bb30600..0575b554 100644
--- a/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/tactics/SimpleDeducedSteps.scala
@@ -7,6 +7,7 @@ import lisa.kernel.proof.SequentCalculus.RewriteTrue
import lisa.kernel.proof.SequentCalculus.SCProofStep
import lisa.kernel.proof.SequentCalculus.Sequent
import lisa.kernel.proof.{SequentCalculus => SC}
+import lisa.utils.Helpers.*
import lisa.utils.Helpers.{_, given}
import lisa.utils.Library
import lisa.utils.tactics.BasicStepTactic.SCSubproof
@@ -90,7 +91,7 @@ object SimpleDeducedSteps {
phi match {
case psi @ FOL.BinderFormula(FOL.Forall, _, _) => {
- val in = FOL.instantiateBinder(psi, t)
+ val in = instantiateBinder(psi, t)
this.asSCProof(currentProof.getSequent(premises(0)) -> phi +> in, premises, currentProof)
}
@@ -112,11 +113,11 @@ object SimpleDeducedSteps {
val tempVar = FOL.VariableLabel(FOL.freshId(psi.freeVariables.map(_.id), "x"))
// instantiate the formula with input
- val in = FOL.instantiateBinder(psi, t)
+ val in = instantiateBinder(psi, t)
// construct proof
val p0 = SC.Hypothesis(in |- in, in)
- val p1 = SC.LeftForall(phi |- in, 0, FOL.instantiateBinder(psi, tempVar), tempVar, t)
+ val p1 = SC.LeftForall(phi |- in, 0, instantiateBinder(psi, tempVar), tempVar, t)
val p2 = SC.Cut(bot, -1, 1, phi)
/**
@@ -226,12 +227,12 @@ object SimpleDeducedSteps {
val tempVar = FOL.VariableLabel(FOL.freshId(psi.freeVariables.map(_.id), "x"))
// instantiate the formula with input
- val in = FOL.instantiateBinder(psi, t)
+ val in = instantiateBinder(psi, t)
val bot = p.conclusion -> f +> in
// construct proof
val p0 = SC.Hypothesis(in |- in, in)
- val p1 = SC.LeftForall(f |- in, 0, FOL.instantiateBinder(psi, tempVar), tempVar, t)
+ val p1 = SC.LeftForall(f |- in, 0, instantiateBinder(psi, tempVar), tempVar, t)
val p2 = SC.Cut(bot, -1, 1, f)
/**
diff --git a/src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala b/src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala
new file mode 100644
index 00000000..c87d1b88
--- /dev/null
+++ b/src/main/scala/lisa/automation/kernel/SimpleSimplifier.scala
@@ -0,0 +1,208 @@
+package lisa.automation.kernel
+
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.utils.Helpers.*
+import lisa.utils.Printer
+import lisa.utils.tactics.ProofStepJudgement
+import lisa.utils.tactics.ProofStepLib.*
+
+import scala.collection
+
+object SimpleSimplifier {
+
+ private def condflat[T](s: Seq[(T, Boolean)]): (Seq[T], Boolean) = (s.map(_._1), s.exists(_._2))
+
+ def nFreshId(froms: Iterable[String], n: Int): IndexedSeq[String] = {
+ val max = if (froms.isEmpty) 0 else froms.map(c => ("0" + c.filter(_.isDigit)).toInt).max
+ Range(0, n).map(i => "_" + (max + i))
+ }
+
+ private def findSubterm2(t: Term, subs: Seq[(VariableLabel, Term)]): (Term, Boolean) = {
+ val eq = subs.find(s => isSame(t, s._2))
+ if (eq.nonEmpty) (eq.get._1(), true)
+ else {
+ val induct = condflat(t.args.map(te => findSubterm2(te, subs)))
+ if (!induct._2) (t, false)
+ else (Term(t.label, induct._1), true)
+
+ }
+
+ }
+
+ private def findSubterm2(f: Formula, subs: Seq[(VariableLabel, Term)]): (Formula, Boolean) = {
+ f match {
+ case PredicateFormula(label, args) =>
+ val induct = condflat(args.map(findSubterm2(_, subs)))
+ if (!induct._2) (f, false)
+ else (PredicateFormula(label, induct._1), true)
+ case ConnectorFormula(label, args) =>
+ val induct = condflat(args.map(findSubterm2(_, subs)))
+ if (!induct._2) (f, false)
+ else (ConnectorFormula(label, induct._1), true)
+ case BinderFormula(label, bound, inner) =>
+ val fv_in_f = subs.flatMap(e => e._2.freeVariables + e._1)
+ if (!fv_in_f.contains(bound)) {
+ val induct = findSubterm2(inner, subs)
+ if (!induct._2) (f, false)
+ else (BinderFormula(label, bound, induct._1), true)
+ } else {
+ val newv = VariableLabel(freshId((f.freeVariables ++ fv_in_f).map(_.id), bound.id))
+ val newInner = substituteVariables(inner, Map(bound -> newv()))
+ val induct = findSubterm2(newInner, subs)
+ if (!induct._2) (f, false)
+ else (BinderFormula(label, newv, induct._1), true)
+ }
+ }
+ }
+
+ private def findSubformula2(f: Formula, subs: Seq[(VariableFormulaLabel, Formula)]): (Formula, Boolean) = {
+ val eq = subs.find(s => isSame(f, s._2))
+ if (eq.nonEmpty) (eq.get._1(), true)
+ else
+ f match {
+ case PredicateFormula(label, args) =>
+ (f, false)
+ case ConnectorFormula(label, args) =>
+ val induct = condflat(args.map(findSubformula2(_, subs)))
+ if (!induct._2) (f, false)
+ else (ConnectorFormula(label, induct._1), true)
+ case BinderFormula(label, bound, inner) =>
+ val fv_in_f = subs.flatMap(_._2.freeVariables)
+ if (!fv_in_f.contains(bound)) {
+ val induct = findSubformula2(inner, subs)
+ if (!induct._2) (f, false)
+ else (BinderFormula(label, bound, induct._1), true)
+ } else {
+ val newv = VariableLabel(freshId((f.freeVariables ++ fv_in_f).map(_.id), bound.id))
+ val newInner = substituteVariables(inner, Map(bound -> newv()))
+ val induct = findSubformula2(newInner, subs)
+ if (!induct._2) (f, false)
+ else (BinderFormula(label, newv, induct._1), true)
+ }
+ }
+ }
+ def findSubterm(t: Term, subs: Seq[(VariableLabel, Term)]): Option[LambdaTermTerm] = {
+ val vars = subs.map(_._1)
+ val r = findSubterm2(t, subs)
+ if (r._2) Some(LambdaTermTerm(vars, r._1))
+ else None
+ }
+
+ def findSubterm(f: Formula, subs: Seq[(VariableLabel, Term)]): Option[LambdaTermFormula] = {
+ val vars = subs.map(_._1)
+ val r = findSubterm2(f, subs)
+ if (r._2) Some(LambdaTermFormula(vars, r._1))
+ else None
+ }
+
+ def findSubformula(f: Formula, subs: Seq[(VariableFormulaLabel, Formula)]): Option[LambdaFormulaFormula] = {
+ val vars = subs.map(_._1)
+ val r = findSubformula2(f, subs)
+ if (r._2) Some(LambdaFormulaFormula(vars, r._1))
+ else None
+ }
+
+ case class applySubst(phi: Formula) extends ProofStepWithoutPrem {
+ override def asSCProof(premises: Seq[Int], currentProof: lisa.utils.Library#Proof): ProofStepJudgement = {
+ val originSequent = currentProof.getSequent(premises.head)
+ val leftOrigin = ConnectorFormula(And, originSequent.left.toSeq)
+ val rightOrigin = ConnectorFormula(Or, originSequent.right.toSeq)
+
+ phi match {
+ case PredicateFormula(label, args) if label == equality =>
+ val left = args(0)
+ val right = args(1)
+ val fv_in_phi = (originSequent.left ++ originSequent.right).flatMap(_.freeVariables).map(_.id)
+ val v = VariableLabel(nFreshId(fv_in_phi, 1).head)
+ val isolatedLeft = originSequent.left.filterNot(f => isSame(f, phi)).map(f => (f, findSubterm(f, IndexedSeq(v -> left))))
+ val isolatedRight = originSequent.right.map(f => (f, findSubterm(f, IndexedSeq(v -> left))))
+ if (isolatedLeft.forall(_._2.isEmpty) && isolatedRight.forall(_._2.isEmpty))
+ return ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), s"There is no instance of ${Printer.prettyTerm(left)} to replace.")
+
+ val leftForm = ConnectorFormula(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val rightForm = ConnectorFormula(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val newleft = isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) + phi
+ val newright = isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right)))
+ val result1: Sequent = (ConnectorFormula(And, newleft.toSeq), phi) |- rightOrigin
+ val result2: Sequent = result1.left |- ConnectorFormula(And, newright.toSeq)
+
+ val proof: SCProof = SCProof(
+ IndexedSeq(
+ Rewrite(leftOrigin |- rightOrigin, -1),
+ LeftSubstEq(result1, 0, List(left -> right), LambdaTermFormula(Seq(v), leftForm)),
+ RightSubstEq(result2, 1, List(left -> right), LambdaTermFormula(Seq(v), rightForm)),
+ Rewrite(newleft |- newright, 2)
+ ),
+ IndexedSeq(originSequent)
+ )
+ val subproof: SCSubproof = SCSubproof(
+ proof,
+ Seq(premises.head)
+ )
+ ProofStepJudgement.ValidProofStep(subproof)
+ case ConnectorFormula(label, args) if label == Iff =>
+ val left = args(0)
+ val right = args(1)
+ val fv_in_phi = (originSequent.left ++ originSequent.right).flatMap(_.schematicFormulaLabels).map(_.id)
+ val H = VariableFormulaLabel(nFreshId(fv_in_phi, 1).head)
+ val isolatedLeft = originSequent.left.filterNot(f => isSame(f, phi)).map(f => (f, findSubformula(f, IndexedSeq(H -> left))))
+ val isolatedRight = originSequent.right.map(f => (f, findSubformula(f, IndexedSeq(H -> left))))
+ if (isolatedLeft.forall(_._2.isEmpty) && isolatedRight.forall(_._2.isEmpty))
+ return ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), s"There is no instance of ${Printer.prettyFormula(left)} to replace.")
+
+ val leftForm = ConnectorFormula(And, isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val rightForm = ConnectorFormula(Or, isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get.body).toSeq)
+ val newleft = isolatedLeft.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right))) + phi
+ val newright = isolatedRight.map((f, ltf) => if (ltf.isEmpty) f else ltf.get(Seq(right)))
+ val result1: Sequent = (ConnectorFormula(And, newleft.toSeq), phi) |- rightOrigin
+ val result2: Sequent = result1.left |- ConnectorFormula(Or, newright.toSeq)
+
+ val proof: SCProof = SCProof(
+ IndexedSeq(
+ Rewrite(leftOrigin |- rightOrigin, -1),
+ LeftSubstIff(result1, 0, List(left -> right), LambdaFormulaFormula(Seq(H), leftForm)),
+ RightSubstIff(result2, 1, List(left -> right), LambdaFormulaFormula(Seq(H), rightForm)),
+ Rewrite(newleft |- newright, 2)
+ ),
+ IndexedSeq(originSequent)
+ )
+ val subproof: SCSubproof = SCSubproof(
+ proof,
+ Seq(premises.head)
+ )
+ ProofStepJudgement.ValidProofStep(subproof)
+ case _ => ProofStepJudgement.InvalidProofStep(this.asProofStep(premises), s"Formula in applySingleSimp need to be of the form a=b or q<=>p and not ${phi.label}")
+ }
+
+ }
+ }
+
+ def simplifySeq(seq: Sequent, ruleseq: IndexedSeq[PredicateFormula], rulesiff: IndexedSeq[ConnectorFormula]): SCProof = {
+ /*
+ val takenVarsIff = (seq.left.flatMap(_.schematicPredicateLabels) ++ seq.right.flatMap(_.schematicPredicateLabels) ++ ruleseq.flatMap(_.schematicPredicateLabels) ++ rulesiff.flatMap(_.schematicPredicateLabels)).map(_.id)
+ val varsIff = nFreshId(takenVarsIff, rulesiff.length).map(VariableFormulaLabel)
+ val subsIff = varsIff.zip(rulesiff.map(_.args(0)))
+
+ val substs: Set[(Formula, LambdaFormulaFormula)] = seq.left.map(f => (f, findSubformula(f, subsIff)) )
+ val newseq = substs.map(_._2(rulesiff.map(_.args(1)))) |- seq.right
+ val step1 = ??? // LeftSubstIff(newseq, prev.length-1, )
+ */
+ ???
+ }
+
+ def simplifySequent(seq: Sequent): SCProof = {
+ val (ruleseq, rulesiff, rem): (List[PredicateFormula], List[ConnectorFormula], List[Formula]) =
+ seq.left.foldLeft((List[PredicateFormula](), List[ConnectorFormula](), List[Formula]()))((prev, f) => {
+ f match {
+ case f @ PredicateFormula(label, _) if label == equality => (f :: prev._1, prev._2, prev._3)
+ case f @ ConnectorFormula(label, _) if label == iff => (prev._1, f :: prev._2, prev._3)
+ case _ => prev
+ }
+ })
+
+ ???
+ }
+
+}
--
GitLab