Proof transformations (#66)

Proof Transformation: Utility to transform a conditional proof into an unconditional proof of a conditional statement. Move the imports to the left of the conclusion.

src/main/scala/lisa/utilities/prooftransform/ProofUnconditionalizer.scala

+package lisa.utilities.prooftransform
+import lisa.kernel.fol.FOL.*
+import lisa.kernel.proof.SCProof
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.utils.Helpers.*
+import lisa.utils.Printer
+
+/**
+ * A generic transformation on a proof with some useful utilities functions.
+ *
+ * Beware that the parameter should really be the same proof you will mainly work on
+ * @param pr the proof to apply the transformation on
+ */
+abstract class ProofTransformer(pr: SCProof) {
+
+  // PUBLIC FUNCTIONS###################################################################################################################
+  /**
+   * Main transformation function, should be the only function needed to be called by the user
+   *
+   * @return the transformed proof
+   */
+  def transform(): SCProof
+
+  // PRIVATE FUNCTIONS##################################################################################################################
+  /**
+   * Gives for a given step all step that lead to it
+   *
+   * @param step the step for which the predecessors are to be found
+   * @return a set of all steps that lead to the given step
+   */
+  protected def adjacencyMatrix[A](pr: IndexedSeq[A], imports: A => Seq[Int]): Map[Int, Set[Int]] = {
+    val steps = pr
+    val adjMat = scala.collection.mutable.Map[Int, Set[Int]]().withDefault(_ => Set.empty)
+
+    steps.zipWithIndex.foreach((step, i) => {
+      adjMat(i) = Set.empty ++ adjMat(i)
+      imports(step).foreach((prem) => {
+        if (prem > 0)
+          adjMat(prem) = adjMat(prem) + i
+      })
+    })
+    adjMat.toMap
+  }
+
+  /**
+   * Gives a set of step indices that are the maximal tree spanning from the given step index embeded in the given proof
+   *
+   * @param st the root of the tree
+   * @param pr the proof to be used as a graph
+   * @return a set of step indices that are the maximal tree spanning from the given step index embeded in the given proof
+   */
+  protected def findBranch(st: Int, pr: SCProof): Seq[Int] = {
+
+    val adjMat = adjacencyMatrix(pr.steps, (s) => s.premises)
+
+    pr(st).premises.filter(_ > 0) match {
+      case Nil => Seq(st)
+      case pp if adjMat(st).size == 1 => st +: pp.flatMap((prem) => findBranch(prem, pr))
+      case _ => Nil
+    }
+
+  }
+
+  /**
+   * Assigns to each node of a DAG all the imports (as defined in the parameters) attainable from it
+   * Executes in liniear time
+   * @param top_sort a topologically sorted array representing the DAG
+   * @param children returns a list of all nodes linked to a given node
+   * @param imports implementation dependent
+   * @return node -> [imports(v) | exists a path between node and v]
+   */
+  protected def dependency_finder[A](top_sort: IndexedSeq[A], children: A => Seq[A], imports: A => Seq[Int]): Map[A, Set[Int]] = {
+    var cache = scala.collection.mutable.Map[A, Set[Int]]().withDefault(_ => Set())
+    def is_leaf(node: A): Boolean = imports(node).isEmpty | imports(node).forall(_ < 0)
+    val adjMat = adjacencyMatrix(top_sort, imports)
+
+    val rev = top_sort.reverse
+    def inner(v: A): Seq[Int] = v match {
+      case _ if is_leaf(v) => {
+        cache(v) = imports(v).toSet
+        imports(v)
+      }
+      case _ => {
+        val current = imports(v).filter(_ < 0)
+        val res = children(v).flatMap(inner) ++ current
+        cache(v) = res.toSet
+        res
+      }
+    }
+    // Checks for empty proof
+    val roots = adjMat.filter((i, s) => s.isEmpty).keySet.map(top_sort(_))
+    roots.foreach(inner)
+    cache.toMap
+  }
+
+  protected def sequentToFormulaNullable(s: Sequent): Formula = (s.left.toSeq, s.right.toSeq) match {
+
+    case (Nil, _) => ConnectorFormula(Or, s.right.toSeq)
+    case (_, Nil) => ConnectorFormula(And, s.left.toSeq)
+    case (h :: Nil, _) => ConnectorFormula(Implies, List(h, ConnectorFormula(Or, s.right.toSeq)))
+    case (_, h :: Nil) => ConnectorFormula(Implies, List(ConnectorFormula(And, s.left.toSeq), h))
+    case (_, _) => sequentToFormula(s)
+
+  }
+}
+
+/**
+ * A transformation that ensures its result is a proof where no instantiaiton are left, rreplaced by imports and rewrites of their conclusion
+ *
+ * @param pr the proof to be modified
+ */
+case class ProofInstantiationRemover(pr: SCProof) extends ProofTransformer(pr) {
+
+  private val adjMat = adjacencyMatrix(pr.steps, s => s.premises)
+  private val neg_premises = dependency_finder(pr.steps, ps => ps.premises.filter(_ >= 0).map(pr.steps(_)), ps => ps.premises)
+
+  // PUBLIC FUNCTIONS###################################################################################################################
+  /**
+   * Maps a proof to a new proof where Instantiations are replaced by hypothesis
+   *
+   * @return the modified proof
+   */
+  def transform(): SCProof = instsAsImports(pr)
+
+  // PRIVATE FUNCTIONS##################################################################################################################
+  /**
+   * determines if a step is a problematic instantiation that should be transformed into an import
+   *
+   * @param step the step to check for
+   * @return whether the given step is an Instantiation tha thas a link to an import
+   */
+  private def isInst(step: SCProofStep): Boolean = step match {
+    case InstPredSchema(_, t, _) if !neg_premises.getOrElse(step, Seq.empty).isEmpty => true
+    case InstFunSchema(_, t, _) if !neg_premises.getOrElse(step, Seq.empty).isEmpty => true
+    case _ => false
+  }
+
+  /**
+   * Maps Instantiations to Rewrites of imports
+   *
+   * @return a proof where all instantiations are rewrites of imports
+   */
+  private def instsAsImports(pr: SCProof): SCProof = {
+    val imps = pr.steps.zipWithIndex.filter((st, j) => isInst(st)).map(_._2).zipWithIndex
+
+    val mImps = imps.toMap
+    val mSteps = pr.steps.zipWithIndex.map((s, j) =>
+      s match {
+        case _ if isInst(s) => Rewrite(() |- sequentToFormulaNullable(s.bot), -pr.imports.length - mImps(j) - 1)
+        case _ => s
+      }
+    )
+
+    SCProof(mSteps, pr.imports ++ imps.map((j, i) => mSteps(j).bot))
+  }
+
+}
+
+case class ProofUnconditionalizer(prOrig: SCProof) extends ProofTransformer(prOrig) {
+
+  // ATTRIBUTES#########################################################################################################################
+  private val pr = ProofInstantiationRemover(prOrig).transform()
+  private val neg_premises = dependency_finder(pr.steps, ps => ps.premises.filter(_ >= 0).map(pr.steps(_)), ps => ps.premises)
+
+  // We use a var because Subproofs require the results of precedent steps, topological order on proofs ensure we can always do this
+  private var appended_steps = IndexedSeq[SCProofStep]()
+  // PREDICATES#########################################################################################################################
+  /**
+   * Wether a step needs to be more modified than just appending hypothesis on the left of the conclusion
+   *
+   * @param sc the step to analyse
+   * @return whether the step has a negative premise
+   */
+  private def is_problematic(sc: SCProofStep): Boolean = sc.premises.exists(_ < 0)
+
+  // PUBLIC FUNCTIONS###################################################################################################################
+  /**
+   * Maps a proof to a new proof where all imports are made into suppositions on the left of the conclusion
+   *
+   * @return A proof where each steps has the necessary imports added as suppostitions on the left of their bottom
+   */
+  def transform(): SCProof = transformPrivate(IndexedSeq.empty)
+
+  // PRIVATE FUNCTIONS##################################################################################################################
+  /**
+   * Private version used to keep track of imports that should not be removed, useful for SubProofs
+   *
+   * @param keep The indices not to be removed from the transformed proof
+   * @return a proof zhose imports have been removed except for those present in keep
+   */
+  private def transformPrivate(keep: IndexedSeq[Sequent]): SCProof = {
+    pr.steps.zipWithIndex.foreach((pS, i) => {
+      appended_steps = appended_steps.appended(if (is_problematic(pS)) {
+        mapProb(pS)
+      } else {
+        mapStep(pS, b => neg_premises.getOrElse(pS, Set[Int]()).map(i => sequentToFormulaNullable(pr.imports(-i - 1))) ++ b)
+      })
+    })
+    SCProof(appended_steps.toIndexedSeq, keep)
+  }
+
+  /**
+   * Deals with steps that have a negative premise
+   * The strategy is to systematically add an hypothesis to introduce the import, rewrite it
+   * to remove unwanted clutter and apply strictly the same transformation as if there was no negative premise.
+   * To not mess with indices of proof and to keep a clearer proof structure all those steps are wrapped into a SubProof
+   *
+   * @param pS thestep to be modified
+   * @return a subproof whose conclusion is the same step as in the argument but with changed premises and a left side bottom modified as
+   * in the general algorithm
+   */
+  private def mapProb(pS: SCProofStep) = {
+    val premises = pS.premises
+      .filter(_ < 0)
+      .map(i => pr.imports(-i - 1))
+    val hypothesis = premises
+      .map((se) => {
+        val h = Hypothesis((se.left + sequentToFormulaNullable(se)) |- (se.right + sequentToFormulaNullable(se)), sequentToFormulaNullable(se))
+        h
+      })
+    val rewrites = hypothesis.zipWithIndex.map((h, i) => {
+      val r = Rewrite(h.bot.left |- (h.bot.right - sequentToFormulaNullable(premises(i))), i)
+      r
+    })
+    // We must separate the case for subproofs for they need to use the modified version of the precedent
+    val inner = pS match {
+      case SCSubproof(_, _, _) =>
+        SCProof(
+          hypothesis.toIndexedSeq ++ rewrites.toIndexedSeq ++ IndexedSeq(
+            mapStep(
+              pS,
+              b => neg_premises(pS).map(i => sequentToFormulaNullable(pr.imports(-i - 1))) ++ b,
+              s =>
+                s.map(i =>
+                  i match {
+                    case i if i < 0 => -i - 2 + hypothesis.length
+                    case i => -i
+                  }
+                ),
+              rewrites.map(_.bot)
+            )
+          ),
+          pS.premises.filter(_ >= 0).map(appended_steps(_).bot).toIndexedSeq
+        )
+
+      case _ =>
+        SCProof(
+          hypothesis.toIndexedSeq ++ IndexedSeq(
+            mapStep(
+              pS,
+              b => neg_premises(pS).map(i => sequentToFormulaNullable(pr.imports(-i - 1))) ++ b,
+              premise =>
+                premise.zipWithIndex.map((i, j) =>
+                  i match {
+                    case i if i < 0 => j
+                    case i => -j
+                  }
+                )
+            )
+          ),
+          pS.premises.filter(_ >= 0).map(appended_steps(_).bot).toIndexedSeq
+        )
+    }
+    SCSubproof(inner, pS.premises.filter(_ >= 0))
+  }
+
+  /**
+   * This function transform generically a proof step into another one
+   *
+   * @param pS the proofstep to modify
+   * @param f the transformation on left side of bottom
+   * @param fi transformation on premises
+   * @param fsub sequents to keep on subproofs
+   * @return a proofstep where each function is applied to the corresponding
+   */
+  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 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)
+    case LeftOr(bot, t, disjuncts) => LeftOr(f(bot.left) |- bot.right, fi(t), disjuncts)
+    case LeftImplies(bot, t1, t2, phi, psi) => LeftImplies(f(bot.left) |- bot.right, fi(pS.premises).head, t2, phi, psi)
+    case LeftIff(bot, t1, phi, psi) => LeftIff(f(bot.left) |- bot.right, fi(pS.premises).head, phi, psi)
+    case LeftNot(bot, t1, phi) => LeftNot(f(bot.left) |- bot.right, fi(pS.premises).head, phi)
+    case LeftForall(bot, t1, phi, x, t) => LeftForall(f(bot.left) |- bot.right, fi(pS.premises).head, phi, x, t)
+    case LeftExists(bot, t1, phi, x) => LeftExists(f(bot.left) |- bot.right, fi(pS.premises).head, phi, x)
+    case LeftExistsOne(bot, t1, phi, x) => LeftExistsOne(f(bot.left) |- bot.right, fi(pS.premises).head, phi, x)
+    case RightAnd(bot, t, cunjuncts) => RightAnd(f(bot.left) |- bot.right, fi(t), cunjuncts)
+    case RightOr(bot, t1, phi, psi) => RightOr(f(bot.left) |- bot.right, fi(pS.premises).head, phi, psi)
+    case RightImplies(bot, t1, phi, psi) => RightImplies(f(bot.left) |- bot.right, fi(pS.premises).head, phi, psi)
+    case RightIff(bot, t1, t2, phi, psi) => RightIff(f(bot.left) |- bot.right, fi(pS.premises).head, fi(pS.premises).last, phi, psi)
+    case RightNot(bot, t1, phi) => RightNot(f(bot.left) |- bot.right, fi(pS.premises).head, phi)
+    case RightForall(bot, t1, phi, x) => RightForall(f(bot.left) |- bot.right, fi(pS.premises).head, phi, x)
+    case RightExists(bot, t1, phi, x, t) => RightExists(f(bot.left) |- bot.right, fi(pS.premises).head, phi, x, t)
+    case RightExistsOne(bot, t1, phi, x) => RightExistsOne(f(bot.left) |- bot.right, fi(pS.premises).head, phi, x)
+    case Weakening(bot, t1) => Weakening(f(bot.left) |- bot.right, fi(pS.premises).head)
+    case LeftRefl(bot, t1, fa) => LeftRefl(f(bot.left) |- bot.right, fi(pS.premises).head, fa)
+    case RightRefl(bot, fa) => RightRefl(f(bot.left) |- bot.right, fa)
+    case LeftSubstEq(bot, t1, equals, lambdaPhi) => LeftSubstEq(f(bot.left) |- bot.right, fi(pS.premises).head, equals, lambdaPhi)
+    case RightSubstEq(bot, t1, equals, lambdaPhi) => RightSubstEq(f(bot.left) |- bot.right, fi(pS.premises).head, equals, lambdaPhi)
+    case LeftSubstIff(bot, t1, equals, lambdaPhi) => LeftSubstIff(f(bot.left) |- bot.right, fi(pS.premises).head, equals, lambdaPhi)
+    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)
+    }
+  }
+
+}

src/test/scala/lisa/utilities/Transformations.scala

+package lisa.utilities
+import lisa.automation.kernel.Destructors.*
+import lisa.automation.kernel.ProofTactics.*
+import lisa.kernel.fol.*
+import lisa.kernel.proof.SCProof
+import lisa.test.ProofCheckerSuite
+import lisa.utils.Helpers.given_Conversion_VariableLabel_Term
+import lisa.utils.Printer
+
+class Transformations extends ProofCheckerSuite {
+  import lisa.settheory.SetTheoryLibrary.*
+
+  test("Trasnsformation initialises well with empty proof and returns an empty proof") {
+    val nullSCProof = SCProof()
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(nullSCProof)
+    assert(transf.transform() == nullSCProof)
+  }
+
+  /**
+   * Any proof where there are no imports shoud not be modified
+   * Dummy proofs of varying size should be tested
+   */
+  test("A proof with no imports is not modified") {
+    val phi = SchematicPredicateLabel("phi", 0)
+
+    val intro = Hypothesis((phi()) |- (phi()), phi())
+    val outro = Rewrite((phi()) |- (phi()), 0)
+
+    val noImpProof = SCProof(IndexedSeq(intro, outro), IndexedSeq.empty)
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(noImpProof)
+
+    assert((transf.transform() == noImpProof))
+    checkProof(noImpProof)
+  }
+
+  test("A proof with imports is to be modified") {
+    val phi = SchematicPredicateLabel("phi", 0)
+
+    val intro = Rewrite(() |- phi(), -1)
+    val outro = Weakening(intro.bot.right |- intro.bot.right, 0)
+
+    val noImpProof = SCProof(IndexedSeq(intro, outro), IndexedSeq(intro.bot))
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(noImpProof).transform()
+
+    checkProof(transf)
+    assert(transf != noImpProof)
+    assert(isSameSequent(transf.steps.last.bot, (sequentToFormula(intro.bot)) |- intro.bot.right))
+  }
+
+  test("A proof with imports and a step taking multiple premises should be modified accordingly") {
+    val phi = SchematicPredicateLabel("phi", 0)()
+    val psi = SchematicPredicateLabel("psi", 0)()
+
+    val into1 = Rewrite(() |- phi, -2)
+    val into2 = Rewrite(() |- psi, -1)
+    val merge = RightAnd(() |- ConnectorFormula(And, (into1.bot.right ++ into2.bot.right).toSeq), Seq(-2, 0), (into1.bot.right ++ into2.bot.right).toSeq)
+
+    val noImpProof = SCProof(IndexedSeq(into2, merge), IndexedSeq(into2.bot, into1.bot))
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(noImpProof).transform()
+
+    checkProof(transf)
+    assert(transf != noImpProof)
+    assert(isSameSequent(transf.steps.last.bot, (sequentToFormula(into1.bot), sequentToFormula(into2.bot)) |- merge.bot.right))
+  }
+
+  test("A proof with imports and a subproof should be modified accordingly") {
+    val phi = SchematicPredicateLabel("phi", 0)()
+    val intro = Rewrite(() |- phi, -1)
+    val outro = SCSubproof(SCProof(IndexedSeq(Weakening(intro.bot.right |- intro.bot.right, -1)), IndexedSeq(intro.bot)), IndexedSeq(0))
+    val noImpProof = SCProof(IndexedSeq(intro, outro), IndexedSeq(intro.bot))
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(noImpProof).transform()
+
+    checkProof(transf)
+    assert(transf != noImpProof)
+    assert(isSameSequent(transf.steps.last.bot, (outro.bot.left + sequentToFormula(intro.bot)) |- outro.bot.right))
+
+  }
+
+  test("A proof with imports and a complete instantiation should be modified accordingly") {
+    val phi = SchematicPredicateLabel("phi", 0)
+    val psi = SchematicPredicateLabel("psi", 2)
+    val x = VariableLabel("x")
+    val y = VariableLabel("y")
+
+    val intro = Rewrite(() |- phi(), -1)
+    val outro = InstPredSchema(() |- psi(x, y), 0, Map((phi, LambdaTermFormula(Seq(), psi(x, y)))))
+    val noImpProof = SCProof(IndexedSeq(intro, outro), IndexedSeq(intro.bot))
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(noImpProof).transform()
+
+    checkProof(transf)
+    assert(transf != noImpProof)
+    assert(isSameSequent(transf.steps.last.bot, (sequentToFormula(outro.bot)) |- outro.bot.right))
+
+  }
+
+  test("A proof with imports and two partial instantiations should be modified accordingly") {
+    val phi = SchematicPredicateLabel("phi", 0)
+    val psi = SchematicPredicateLabel("psi", 2)
+    val lambda = SchematicPredicateLabel("lambda", 2)
+    val x = VariableLabel("x")
+    val y = VariableLabel("y")
+
+    val intro = Rewrite(() |- phi(), -1)
+    val mid = InstPredSchema(() |- psi(x, y) <=> phi(), 0, Map((phi, LambdaTermFormula(Seq(), psi(x, y) <=> phi()))))
+    val outro = InstPredSchema(() |- psi(x, y) <=> lambda(x, y), 1, Map((phi, LambdaTermFormula(Seq(), lambda(x, y)))))
+    val weak = Weakening((psi(x, y)) |- psi(x, y) <=> lambda(x, y), 2)
+    val noImpProof = SCProof(IndexedSeq(intro, mid, outro, weak), IndexedSeq(intro.bot))
+    val transf = lisa.utilities.prooftransform.ProofUnconditionalizer(noImpProof).transform()
+
+    checkProof(transf)
+    assert(transf != noImpProof)
+    assert(isSameSequent(transf.steps.last.bot, ((weak.bot.left + sequentToFormula(outro.bot))) |- weak.bot.right))
+  }
+
+  test("A proof with instantiation can be transformed into one with a rewrite and an import") {
+    val phi = SchematicPredicateLabel("phi", 0)
+    val psi = SchematicPredicateLabel("psi", 2)
+    val x = VariableLabel("x")
+    val y = VariableLabel("y")
+
+    val intro = Rewrite(() |- phi(), -1)
+    val outro = InstPredSchema(() |- psi(x, y), 0, Map((phi, LambdaTermFormula(Seq(), psi(x, y)))))
+    val noImpProof = SCProof(IndexedSeq(intro, outro), IndexedSeq(intro.bot))
+    val transf = lisa.utilities.prooftransform.ProofInstantiationRemover(noImpProof).transform()
+
+    checkProof(transf)
+    assert(transf != noImpProof)
+    assert(isSameSequent(transf.steps.last.bot, () |- outro.bot.right))
+  }
+}