diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index c5d2967ded8c571b051e165f166bf87c27d894cc..f367a551bade5d3d7904cf35eb1a3e63c5e35d34 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -258,6 +258,8 @@ object Printer {
case RightSubstEq(_, t1, _, _, _, _) => pretty("R. SubstEq", t1)
case LeftSubstIff(_, t1, _, _, _, _) => pretty("L. SubstIff", t1)
case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
+ case InstantiateSchematicFunction(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
+ case InstantiateSchematicPredicate(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
case SCSubproof(_, _, false) => pretty("SCSubproof (hidden)")
case other => throw new Exception(s"No available method to print this proof step, consider updating Printer.scala\n$other")
}
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 8e1e772bde023e8c6bb5f7494a29e34e43620ce8..da0ab913031b47a7465a2d510c4568b47676060f 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -112,7 +112,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* Those variables are replaced by the actual arguments of p.
* @return phi[psi(a1,..., an)/p]
*/
- def instantiatePredicateSchema(phi: Formula, p: SchematicPredicateLabel, psi: Formula, a: List[VariableLabel]): Formula = {
+ def instantiatePredicateSchema(phi: Formula, p: SchematicPredicateLabel, psi: Formula, a: Seq[VariableLabel]): Formula = {
require(a.length == p.arity)
phi match {
case PredicateFormula(label, args) =>
@@ -139,7 +139,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
* Those variables are replaced by the actual arguments of f.
* @return phi[r(a1,..., an)/f]
*/
- def instantiateFunctionSchema(phi: Formula, f: SchematicFunctionLabel, r: Term, a: List[VariableLabel]): Formula = {
+ def instantiateFunctionSchema(phi: Formula, f: SchematicFunctionLabel, r: Term, a: Seq[VariableLabel]): Formula = {
require(a.length == f.arity)
phi match {
case PredicateFormula(label, args) => PredicateFormula(label, args.map(instantiateFunctionSchema(_, f, r, a)))
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 03411af89036811ad6b942419ba3f739c7daccfc..25c23e0e72aab95c21e93f1c7d0f1121d958388b 100644
--- a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -87,7 +87,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
* Those variables are replaced by the actual arguments of f.
* @return t[r(a1,..., an)/f]
*/
- def instantiateFunctionSchema(t: Term, f: SchematicFunctionLabel, r: Term, a: List[VariableLabel]): Term = {
+ def instantiateFunctionSchema(t: Term, f: SchematicFunctionLabel, r: Term, a: Seq[VariableLabel]): Term = {
require(a.length == f.arity)
t match {
case VariableTerm(label) => t
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 372699abbe43d3a6f84c9d4e505cfc843ca599d2..f2e55a7ed4e5729b1fa0be48696bad0a10d56aab 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -401,6 +401,35 @@ object SCProofChecker {
else (false, Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[τ/?q] and φ[ψ/?q], but it isn't the case." )
else (false, Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
else (false, Nil, "Predicate schema ?q must have arity 0.")
+ /**
+ * <pre>
+ * Γ |- Δ
+ * ---------------------
+ * Γ[?f/r(a)] |- Δ[?f/r(a)]
+ * </pre>
+ */
+ case InstantiateSchematicFunction(bot, t1, f, r, a) =>
+ val expected = (ref(t1).left.map(phi => instantiateFunctionSchema(phi, f, r, a)), ref(t1).right.map(phi => instantiateFunctionSchema(phi, f, r, a)))
+ if (isSameSet(bot.left, expected._1))
+ if (isSameSet(bot.right, expected._2))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
+ else (false, Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
+
+ /**
+ * <pre>
+ * Γ |- Δ
+ * ---------------------
+ * Γ[?p/ψ(a)] |- Δ[?p/ψ(a)]
+ * </pre>
+ */
+ case InstantiateSchematicPredicate(bot, t1, p, psi, a) =>
+ val expected = (ref(t1).left.map(phi => instantiatePredicateSchema(phi, p, psi, a)), ref(t1).right.map(phi => instantiatePredicateSchema(phi, p, psi, a)))
+ if (isSameSet(bot.left, expected._1))
+ if (isSameSet(bot.right, expected._2))
+ (true, Nil, "")
+ else (false, Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
+ else (false, Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] must be the same as left-hand side of conclusion.")
case SCSubproof(sp, premises, _) =>
if (premises.size == sp.imports.size){
@@ -409,7 +438,7 @@ object SCProofChecker {
val r_subproof = checkSCProof(sp)
if (r_subproof._1)
(true, Nil, "")
- else (false, r_subproof._2, "Subproof reports an error:\n"+r_subproof._3)
+ else (false, r_subproof._2, r_subproof._3)
} else (false, Nil, s"Premise number ${invalid.get._1} (refering to step ${invalid.get}) is not the same as import number ${invalid.get._1} of the subproof.")
} else (false, Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index cf79543367bde60c6c3ce6827dff22f56f695eaf..7dce18204a55474b2a23154f09d012b0d2a85b51 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -1,6 +1,7 @@
package lisa.kernel.proof
-import lisa.kernel.fol.FOL._
+import lisa.kernel.fol.FOL.*
+
import scala.collection.immutable.Set
@@ -276,6 +277,22 @@ object SequentCalculus {
* </pre>
*/
case class RightSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
+ /**
+ * <pre>
+ * Γ |- Δ
+ * ---------------------
+ * Γ[?f/r(a)] |- Δ[?f/r(a)]
+ * </pre>
+ */
+ case class InstantiateSchematicFunction(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] )
+ /**
+ * <pre>
+ * Γ |- Δ
+ * ---------------------
+ * Γ[?p/ψ(a)] |- Δ[?p/ψ(a)]
+ * </pre>
+ */
+ case class InstantiateSchematicPredicate(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] )
// Proof Organisation rules
case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display:Boolean = true) extends SCProofStep {