diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 35fb39c1141d25b063e25c0ea833d34734482735..2b3f6df5157aebff8257f571e03e54d4d86f58ed 100644
--- a/src/main/scala/lisa/kernel/Printer.scala
+++ b/src/main/scala/lisa/kernel/Printer.scala
@@ -283,12 +283,12 @@ object Printer {
case LeftIff(_, t1, _, _) => pretty("Left ↔", t1)
case LeftRefl(_, t1, _) => pretty("L. Refl", t1)
case RightRefl(_, _) => pretty("R. Refl")
- case LeftSubstEq(_, t1, _, _, _, _) => pretty("L. SubstEq", t1)
- case RightSubstEq(_, t1, _, _, _, _) => pretty("R. SubstEq", t1)
- case LeftSubstIff(_, t1, _, _, _, _) => pretty("L. SubstIff", t1)
- case RightSubstIff(_, t1, _, _, _, _) => pretty("R. SubstIff", t1)
- case InstFunSchema(_, t1, _, _, _) => pretty("?Fun Instantiation", t1)
- case InstPredSchema(_, t1, _, _, _) => pretty("?Pred Instantiation", t1)
+ case LeftSubstEq(_, t1, _, _) => pretty("L. SubstEq", t1)
+ case RightSubstEq(_, t1, _, _) => pretty("R. SubstEq", t1)
+ case LeftSubstIff(_, t1, _, _) => pretty("L. SubstIff", t1)
+ 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")
}
diff --git a/src/main/scala/lisa/kernel/fol/FOL.scala b/src/main/scala/lisa/kernel/fol/FOL.scala
index 6f09ba07e254e60994196c68795ab58e8278b000..6491a6171eeffcf36f18b9b58838ce5db1a251b9 100644
--- a/src/main/scala/lisa/kernel/fol/FOL.scala
+++ b/src/main/scala/lisa/kernel/fol/FOL.scala
@@ -7,6 +7,7 @@ package lisa.kernel.fol
* import lisa.fol.FOL._
* </pre>
*/
-object FOL extends FormulaDefinitions with EquivalenceChecker {
+object FOL extends FormulaDefinitions with EquivalenceChecker with Substitutions {
+
}
diff --git a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
index 053be248ab164361b41091eea38be6c92da538ef..16b0c899c4f8c4d496507a4e4233d5df173ee664 100644
--- a/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala
@@ -66,107 +66,8 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD
override def schematicPredicates: Set[SchematicPredicateLabel] = inner.schematicPredicates
}
- /**
- * Performs the substitution of x by r in f. May rename bound variables of f if necessary
- * to avoid capture of free variables in r.
- *
- * @param f The base formula
- * @param x A variable, which should be free in f
- * @param r A term that will replace x in f
- * @return f[r/x]
- */
- def substituteVariable(f: Formula, x: VariableLabel, r: Term): Formula = f match {
- case PredicateFormula(label, args) => PredicateFormula(label, args.map(substituteVariable(_, x, r)))
- case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteVariable(_, x, r)))
- case BinderFormula(label, bound, inner) =>
- if (isSame(bound, x)) f
- else {
- val fv = r.freeVariables
- if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
- val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
- BinderFormula(label, newBoundVariable, substituteVariable(newInner, x, r))
- }
- else BinderFormula(label, bound, substituteVariable(inner, x, r))
- }
- }
-
def bindAll(binder: BinderLabel, vars: Seq[VariableLabel], phi:Formula): Formula =
vars.foldLeft(phi)((f, v) => BinderFormula(binder, v, f))
- /**
- * Performs simultaneous substitution of multiple variables by multiple terms in a formula f.
- *
- * @param f The base formula
- * @param m A map from variables to terms.
- * @return t[m]
- */
- def simultaneousSubstitution(f: Formula, m: Map[VariableLabel, Term]): Formula = f match {
- case PredicateFormula(label, args) => PredicateFormula(label, args.map(simultaneousSubstitution(_, m)))
- case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(simultaneousSubstitution(_, m)))
- case BinderFormula(label, bound, inner) =>
- val newSubst = m - bound
- val fv = m.values.flatMap(_.freeVariables).toSet
- if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
- val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
- BinderFormula(label, newBoundVariable, simultaneousSubstitution(newInner, newSubst))
- }
- else BinderFormula(label, bound, simultaneousSubstitution(inner, newSubst))
- }
-
- /**
- * Instantiate a schematic predicate symbol in a formula, using higher-order instantiation.
- *
- * @param phi The base formula
- * @param p The symbol to replace
- * @param psi A formula, seen as a function, that will replace p in t.
- * @param a The "arguments" of psi when seen as a function rather than a ground formula.
- * 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: Seq[VariableLabel]): Formula = {
- require(a.length == p.arity)
- phi match {
- case PredicateFormula(label, args) =>
- if (isSame(label, p)) simultaneousSubstitution(psi, (a zip args).toMap)
- else phi
- case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchema(_, p, psi, a)))
- case BinderFormula(label, bound, inner) =>
- val fv: Set[VariableLabel] = psi.freeVariables -- a
- if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
- val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
- BinderFormula(label, newBoundVariable, instantiatePredicateSchema(newInner, p, psi, a))
- } else BinderFormula(label, bound, instantiatePredicateSchema(inner, p, psi, a))
- }
- }
-
- /**
- * Instantiate a schematic function symbol in a formula, using higher-order instantiation.
- *
- * @param phi The base formula
- * @param f The symbol to replace
- * @param r A term, seen as a function, that will replace f in t.
- * @param a The "arguments" of r when seen as a function rather than a ground term.
- * 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: Seq[VariableLabel]): Formula = {
- require(a.length == f.arity)
- phi match {
- case PredicateFormula(label, args) => PredicateFormula(label, args.map(instantiateFunctionSchema(_, f, r, a)))
- case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateFunctionSchema(_, f, r, a)))
- case BinderFormula(label, bound, inner) =>
- val fv: Set[VariableLabel] = r.freeVariables -- a.toSet
- if (fv.contains(bound)) {
- val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
- val newInner = substituteVariable(inner, bound, VariableTerm(newBoundVariable))
- BinderFormula(label, newBoundVariable, instantiateFunctionSchema(newInner, f, r, a))
- } else BinderFormula(label, bound, instantiateFunctionSchema(inner, f, r, a))
- }
- }
-
- def instantiateBinder(f: BinderFormula, t: Term): Formula = substituteVariable(f.inner, f.bound, t)
-
+
}
diff --git a/src/main/scala/lisa/kernel/fol/Substitutions.scala b/src/main/scala/lisa/kernel/fol/Substitutions.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5f9d1391b6dcbb9ab77e9efcd63a67d11874180d
--- /dev/null
+++ b/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -0,0 +1,182 @@
+package lisa.kernel.fol
+
+trait Substitutions extends FormulaDefinitions{
+
+ /**
+ * A lambda term to express a "term with holes". Main use is to be substituted in place of a function schema.
+ * Morally equivalent to a 2-tuples containing the same informations.
+ * @param vars The names of the "holes" in the term, necessarily of arity 0. The bound variables of the functional term.
+ * @param body The term represented by the object, up to instantiation of the bound schematic variables in args.
+ */
+ case class LambdaTermTerm(vars:Seq[SchematicFunctionLabel], body:Term){
+ require(vars.forall(_.arity == 0))
+ def apply(args:Seq[Term]): Term = instantiateNullaryFunctionSchemas(body, (vars zip args).toMap)
+ }
+
+ /**
+ * A lambda formula to express a "formula with holes". Main use is to be substituted in place of a predicate schema.
+ * Morally equivalent to a 2-tuples containing the same informations.
+ * @param vars The names of the "holes" in a formula, necessarily of arity 0. The bound variables of the functional formula.
+ * @param body The formula represented by the object, up to instantiation of the bound schematic variables in args.
+ */
+ case class LambdaTermFormula(vars:Seq[SchematicFunctionLabel], body:Formula){
+ require(vars.forall(_.arity == 0))
+ def apply(args:Seq[Term]):Formula ={
+ instantiateFunctionSchemas(body, (vars zip (args map(LambdaTermTerm(Nil, _)))).toMap)
+ }
+ //def instantiateFunctionSchemas(phi: Formula, m: Map[SchematicFunctionLabel, LambdaTermTerm]):Formula = ???
+ }
+
+ /**
+ * A lambda formula to express a "formula with holes". Usefull for rules such as Iff substitution
+ * Morally equivalent to a 2-tuples containing the same informations.
+ * @param vars The names of the "holes" in a formula, necessarily of arity 0.
+ * @param body The formula represented by the object, up to instantiation of the bound schematic variables in args.
+ */
+ case class LambdaFormulaFormula(vars:Seq[SchematicPredicateLabel], body:Formula){
+ require(vars.forall(_.arity == 0))
+ def apply(args:Seq[Formula]):Formula = instantiatePredicateSchemas(body, (vars zip (args map(LambdaTermFormula(Nil, _)))).toMap)
+ }
+
+ //////////////////////////
+ // **--- ON TERMS ---** //
+ //////////////////////////
+
+ /**
+ * Performs simultaneous substitution of multiple variables by multiple terms in a term t.
+ * @param t The base term
+ * @param m A map from variables to terms.
+ * @return t[m]
+ */
+ def substituteVariables(t: Term, m: Map[VariableLabel, Term]): Term = t match {
+ case VariableTerm(label) => m.getOrElse(label, t)
+ case FunctionTerm(label, args) => FunctionTerm(label, args.map(substituteVariables(_, m)))
+ }
+
+ /**
+ * Performs simultaneous substitution of multiple nullary schematic function symbols by multiple terms in a base term t.
+ * If one of the symbol is not of arity 0, it will produce an error.
+ * It is needed for the implementation of the general FunctionSchemas instantiation method.
+ * @param t The base term
+ * @param m A map from nullary schematic function label to terms.
+ * @return t[m]
+ */
+ private def instantiateNullaryFunctionSchemas(t: Term, m: Map[SchematicFunctionLabel, Term]): Term = {
+ require(m.forall{ case (symbol, term) => symbol.arity == 0})
+ t match {
+ case VariableTerm(_) => t
+ case FunctionTerm(label, args) => label match
+ case label: SchematicFunctionLabel if label.arity == 0 => m.getOrElse(label, t)
+ case label => FunctionTerm(label, args.map(instantiateNullaryFunctionSchemas(_, m)))
+ }
+ }
+
+ /**
+ * Performs simultaneous substitution of schematic function symbol by "functional" terms, or terms with holes.
+ * If the arity of one of the function symbol to substitute don't match the corresponding number of arguments, or if
+ * one of the "terms with holes" contains a non-nullary symbol, it will produce an error.
+ * @param t The base term
+ * @param m The map from schematic function symbols to "terms with holes". A such term is a pair containing a list of
+ * nullary schematic function symbols (holes) and a term that is the body of the functional term.
+ * @return t[m]
+ */
+ def instantiateFunctionSchemas(t: Term, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Term = {
+ require(m.forall{case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity})
+ t match {
+ case VariableTerm(_) => t
+ case FunctionTerm(label, args) =>
+ val newArgs = args.map(instantiateFunctionSchemas(_, m))
+ label match
+ case label: ConstantFunctionLabel => FunctionTerm(label, newArgs)
+ case label: SchematicFunctionLabel =>
+ if (m.contains(label))
+ m(label)(newArgs) //= instantiateNullaryFunctionSchemas(m(label).body, (m(label).vars zip newArgs).toMap)
+ else FunctionTerm(label, newArgs)
+
+
+ }
+ }
+
+ /////////////////////////////
+ // **--- ON FORMULAS ---** //
+ /////////////////////////////
+
+ /**
+ * Performs simultaneous substitution of multiple variables by multiple terms in a formula f.
+ *
+ * @param f The base formula
+ * @param m A map from variables to terms.
+ * @return t[m]
+ */
+ def substituteVariables(f: Formula, m: Map[VariableLabel, Term]): Formula = f match {
+ case PredicateFormula(label, args) => PredicateFormula(label, args.map(substituteVariables(_, m)))
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(substituteVariables(_, m)))
+ case BinderFormula(label, bound, inner) =>
+ val newSubst = m - bound
+ val fv = m.values.flatMap(_.freeVariables).toSet
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
+ BinderFormula(label, newBoundVariable, substituteVariables(newInner, newSubst))
+ }
+ else BinderFormula(label, bound, substituteVariables(inner, newSubst))
+ }
+
+ /**
+ * Instantiate a schematic function symbol in a formula, using higher-order instantiation.
+ *
+ * @param phi The base formula
+ * @param f The symbol to replace
+ * @param r A term, seen as a function, that will replace f in t.
+ * @param a The "arguments" of r when seen as a function rather than a ground term.
+ * Those variables are replaced by the actual arguments of f.
+ * @return phi[r(a1,..., an)/f]
+ */
+ def instantiateFunctionSchemas(phi: Formula, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Formula = {
+ require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity })
+ phi match {
+ case PredicateFormula(label, args) => PredicateFormula(label, args.map(instantiateFunctionSchemas(_, m)))
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateFunctionSchemas(_, m)))
+ case BinderFormula(label, bound, inner) =>
+ val fv: Set[VariableLabel] = (m.flatMap {case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables}).toSet
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
+ BinderFormula(label, newBoundVariable, instantiateFunctionSchemas(newInner, m))
+ } else BinderFormula(label, bound, instantiateFunctionSchemas(inner, m))
+ }
+ }
+
+
+ /**
+ * Instantiate a schematic predicate symbol in a formula, using higher-order instantiation.
+ *
+ * @param phi The base formula
+ * @param p The symbol to replace
+ * @param psi A formula, seen as a function, that will replace p in t.
+ * @param a The "arguments" of psi when seen as a function rather than a ground formula.
+ * Those variables are replaced by the actual arguments of p.
+ * @return phi[psi(a1,..., an)/p]
+ */
+ def instantiatePredicateSchemas(phi: Formula, m: Map[SchematicPredicateLabel, LambdaTermFormula]): Formula = {
+ require(m.forall { case (symbol, LambdaTermFormula(arguments, body)) => arguments.length == symbol.arity })
+ phi match {
+ case PredicateFormula(label, args) =>
+ label match
+ case label: SchematicPredicateLabel if m.contains(label) => m(label)(args)
+ case label => phi
+ case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchemas(_, m)))
+ case BinderFormula(label, bound, inner) =>
+ val fv: Set[VariableLabel] = (m.flatMap {case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables}).toSet
+ if (fv.contains(bound)) {
+ val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
+ val newInner = substituteVariables(inner, Map(bound -> VariableTerm(newBoundVariable)))
+ BinderFormula(label, newBoundVariable, instantiatePredicateSchemas(newInner, m))
+ } else BinderFormula(label, bound, instantiatePredicateSchemas(inner, m))
+ }
+ }
+
+
+ def instantiateBinder(f: BinderFormula, t: Term): Formula = substituteVariables(f.inner, Map(f.bound -> t))
+
+}
diff --git a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
index 33a9d54e8457a89b49a195e29f052953a0b8ddf3..c60914864017c0eb0b9fe7a12cad11f9f2a4ea40 100644
--- a/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
+++ b/src/main/scala/lisa/kernel/fol/TermDefinitions.scala
@@ -58,49 +58,6 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions {
val arity: Int = args.size
}
- /**
- * Performs the substitution of x by r in t.
- *
- * @param t The base term
- * @param x A variable, which should be free in t
- * @param r A term that will replace x in t.
- * @return t[r/x]
- */
- def substituteVariable(t: Term, x: VariableLabel, r: Term): Term = t match {
- case VariableTerm(label) => if (isSame(label, x)) r else t
- case FunctionTerm(label, args) => FunctionTerm(label, args.map(substituteVariable(_, x, r)))
- }
- /**
- * Performs simultaneous substitution of multiple variables by multiple terms in a term t.
- *
- * @param t The base term
- * @param m A map from variables to terms.
- * @return t[m]
- */
- def simultaneousSubstitution(t: Term, m: Map[VariableLabel, Term]): Term = t match {
- case VariableTerm(label) => m.getOrElse(label, t)
- case FunctionTerm(label, args) => FunctionTerm(label, args.map(simultaneousSubstitution(_, m)))
- }
- /**
- * instantiate a schematic function symbol in a term, using higher-order instantiation.
- *
- * @param t The base term
- * @param f The symbol to replace
- * @param r A term, seen as a function, that will replace f in t.
- * @param a The "arguments" of r when seen as a function rather than a ground term.
- * 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: Seq[VariableLabel]): Term = {
- require(a.length == f.arity)
- t match {
- case VariableTerm(label) => t
- case FunctionTerm(label, args) =>
- val newArgs = args.map(instantiateFunctionSchema(_, f, r, a))
- if (isSame(label, f)) simultaneousSubstitution(r, (a zip newArgs).toMap)
- else FunctionTerm(label, newArgs)
- }
- }
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 616b2e14537472079bd279ec3e917664fb205ba3..8a1391c0f8f980bcf792a8b4e69d07f8438c5ebc 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -38,14 +38,14 @@ object SCProofChecker {
* ------------
* Γ |- Δ
*/
- case Rewrite(s, t1) =>
+ case Rewrite(s, t1) =>
if (isSameSequent(s, ref(t1))) SCValidProof else SCInvalidProof(Nil, s"The premise and the conclusion are not trivially equivalent.")
/*
*
* --------------
* Γ, φ |- φ, Δ
*/
- case Hypothesis(Sequent(left, right), phi) =>
+ case Hypothesis(Sequent(left, right), phi) =>
if (contains(left, phi))
if (contains(right, phi)) SCValidProof
@@ -56,7 +56,7 @@ object SCProofChecker {
* ------------------------
* Γ, Σ |-Δ, Π
*/
- case Cut(b, t1, t2, phi) =>
+ case Cut(b, t1, t2, phi) =>
if (isSameSet(b.left + phi, ref(t1).left union ref(t2).left))
if (isSameSet(b.right + phi, ref(t2).right union ref(t1).right))
if (contains(ref(t2).left, phi))
@@ -73,7 +73,7 @@ object SCProofChecker {
* -------------- or -------------
* Γ, φ∧ψ |- Δ Γ, φ∧ψ |- Δ
*/
- case LeftAnd(b, t1, phi, psi) =>
+ case LeftAnd(b, t1, phi, psi) =>
if (isSameSet(ref(t1).right, b.right))
val phiAndPsi = ConnectorFormula(And, Seq(phi, psi))
if (isSameSet(b.left + phi, ref(t1).left + phiAndPsi) ||
@@ -87,7 +87,7 @@ object SCProofChecker {
* ------------------------
* Γ, Σ, φ∨ψ |- Δ, Π
*/
- case LeftOr(b, t, disjuncts) =>
+ case LeftOr(b, t, disjuncts) =>
if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)) )
val phiOrPsi = ConnectorFormula(Or, disjuncts)
if (isSameSet(disjuncts.foldLeft(b.left)(_ + _), t.map(ref(_).left).reduce(_ union _) + phiOrPsi))
@@ -99,7 +99,7 @@ object SCProofChecker {
* ------------------------
* Γ, Σ, φ→ψ |- Δ, Π
*/
- case LeftImplies(b, t1, t2, phi, psi) =>
+ case LeftImplies(b, t1, t2, phi, psi) =>
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(b.right + phi, ref(t1).right union ref(t2).right))
if (isSameSet(b.left + psi, ref(t1).left union ref(t2).left + phiImpPsi))
@@ -111,7 +111,7 @@ object SCProofChecker {
* -------------- or ---------------
* Γ, φ↔ψ |- Δ Γ, φ↔ψ |- Δ
*/
- case LeftIff(b, t1, phi, psi) =>
+ case LeftIff(b, t1, phi, psi) =>
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
val psiImpPhi = ConnectorFormula(Implies, Seq(psi, phi))
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
@@ -128,7 +128,7 @@ object SCProofChecker {
* --------------
* Γ, ¬φ |- Δ
*/
- case LeftNot(b, t1, phi) =>
+ case LeftNot(b, t1, phi) =>
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.left, ref(t1).left + nPhi))
if (isSameSet(b.right + phi, ref(t1).right))
@@ -141,9 +141,9 @@ object SCProofChecker {
* -------------------
* Γ, ∀x. φ |- Δ
*/
- case LeftForall(b, t1, phi, x, t) =>
+ case LeftForall(b, t1, phi, x, t) =>
if (isSameSet(b.right, ref(t1).right))
- if (isSameSet(b.left + substituteVariable(phi, x, t), ref(t1).left + BinderFormula(Forall, x, phi)))
+ if (isSameSet(b.left + substituteVariables(phi, Map(x -> t)), ref(t1).left + BinderFormula(Forall, x, phi)))
SCValidProof
else SCInvalidProof(Nil, "Left-hand side of conclusion + φ[t/x] must be the same as left-hand side of premise + ∀x. φ")
else SCInvalidProof(Nil, "Right-hand side of conclusion must be the same as right-hand side of premise")
@@ -153,7 +153,7 @@ object SCProofChecker {
* ------------------- if x is not free in the resulting sequent
* Γ, ∃x. φ|- Δ
*/
- case LeftExists(b, t1, phi, x) =>
+ case LeftExists(b, t1, phi, x) =>
if (isSameSet(b.right, ref(t1).right))
if (isSameSet(b.left + phi, ref(t1).left + BinderFormula(Exists, x, phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
@@ -167,7 +167,7 @@ object SCProofChecker {
* ---------------------------- if y is not free in φ
* Γ, ∃!x. φ |- Δ
*/
- case LeftExistsOne(b, t1, phi, x) =>
+ case LeftExistsOne(b, t1, phi, x) =>
val y = VariableLabel(freshId(phi.freeVariables.map(_.id) + x.id, "y"))
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.right, ref(t1).right))
@@ -182,7 +182,7 @@ object SCProofChecker {
* ------------------------
* Γ, Σ |- φ∧ψ, Π, Δ
*/
- case RightAnd(b, t, cunjuncts) =>
+ case RightAnd(b, t, cunjuncts) =>
val phiAndPsi = ConnectorFormula(And, cunjuncts)
if (isSameSet(b.left, t.map(ref(_).left).reduce(_ union _)))
if (isSameSet(cunjuncts.foldLeft(b.right)(_ + _), t.map(ref(_).right).reduce(_ union _) + phiAndPsi))
@@ -194,7 +194,7 @@ object SCProofChecker {
* -------------- or ---------------
* Γ |- φ∨ψ, Δ Γ |- φ∨ψ, Δ
*/
- case RightOr(b, t1, phi, psi) =>
+ case RightOr(b, t1, phi, psi) =>
val phiOrPsi = ConnectorFormula(Or, Seq(phi, psi))
if (isSameSet(ref(t1).left, b.left))
if (isSameSet(b.right + phi, ref(t1).right + phiOrPsi) ||
@@ -208,7 +208,7 @@ object SCProofChecker {
* --------------
* Γ |- φ→ψ, Δ
*/
- case RightImplies(b, t1, phi, psi) =>
+ case RightImplies(b, t1, phi, psi) =>
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
if (isSameSet(ref(t1).left, b.left + phi))
if (isSameSet(b.right + psi, ref(t1).right + phiImpPsi))
@@ -220,7 +220,7 @@ object SCProofChecker {
* ----------------------------
* Γ, Σ |- φ↔b, Π, Δ
*/
- case RightIff(b, t1, t2, phi, psi) =>
+ case RightIff(b, t1, t2, phi, psi) =>
val phiImpPsi = ConnectorFormula(Implies, Seq(phi, psi))
val psiImpPhi = ConnectorFormula(Implies, Seq(psi, phi))
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
@@ -234,7 +234,7 @@ object SCProofChecker {
* --------------
* Γ |- ¬φ, Δ
*/
- case RightNot(b, t1, phi) =>
+ case RightNot(b, t1, phi) =>
val nPhi = ConnectorFormula(Neg, Seq(phi))
if (isSameSet(b.right, ref(t1).right + nPhi))
if (isSameSet(b.left + phi, ref(t1).left))
@@ -246,7 +246,7 @@ object SCProofChecker {
* ------------------- if x is not free in the resulting sequent
* Γ |- ∀x. φ, Δ
*/
- case RightForall(b, t1, phi, x) =>
+ case RightForall(b, t1, phi, x) =>
if (isSameSet(b.left, ref(t1).left))
if (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x ,phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
@@ -259,9 +259,9 @@ object SCProofChecker {
* -------------------
* Γ |- ∃x. φ, Δ
*/
- case RightExists(b, t1, phi, x, t) =>
+ case RightExists(b, t1, phi, x, t) =>
if (isSameSet(b.left, ref(t1).left))
- if (isSameSet(b.right + substituteVariable(phi, x, t), ref(t1).right + BinderFormula(Exists, x ,phi)))
+ if (isSameSet(b.right + substituteVariables(phi, Map(x -> t)), ref(t1).right + BinderFormula(Exists, x ,phi)))
SCValidProof
else SCInvalidProof(Nil, "Right-hand side of the conclusion + φ[t/x] must be the same as right-hand side of the premise + ∃x. φ")
else SCInvalidProof(Nil, "Left-hand sides or conclusion and premise must be the same.")
@@ -273,7 +273,7 @@ object SCProofChecker {
* Γ|- ∃!x. φ, Δ
* </pre>
*/
- case RightExistsOne(b, t1, phi, x) =>
+ case RightExistsOne(b, t1, phi, x) =>
val y = VariableLabel(freshId(phi.freeVariables.map(_.id), "x"))
val temp = BinderFormula(Exists, y, BinderFormula(Forall, x, ConnectorFormula(Iff, List(PredicateFormula(equality, List(VariableTerm(x), VariableTerm(y))), phi))))
if (isSameSet(b.left, ref(t1).left))
@@ -289,7 +289,7 @@ object SCProofChecker {
* --------------
* Γ, Σ |- Δ
*/
- case Weakening(b, t1) =>
+ case Weakening(b, t1) =>
if (isSubset(ref(t1).left, b.left))
if (isSubset(ref(t1).right, b.right))
SCValidProof
@@ -302,7 +302,7 @@ object SCProofChecker {
* --------------
* Γ |- Δ
*/
- case LeftRefl(b, t1, phi) =>
+ case LeftRefl(b, t1, phi) =>
phi match {
case PredicateFormula(`equality`, Seq(left, right)) =>
if (isSame(left, right))
@@ -320,7 +320,7 @@ object SCProofChecker {
* --------------
* |- s=s
*/
- case RightRefl(b, phi) =>
+ case RightRefl(b, phi) =>
phi match {
case PredicateFormula(`equality`, Seq(left, right)) =>
if (isSame(left, right))
@@ -336,7 +336,8 @@ object SCProofChecker {
* ---------------------
* Γ, s=t, φ[t/?f] |- Δ
*/
- case LeftSubstEq(b, t1, s, t, phi, f) =>
+ case LeftSubstEq(b, t1, s, t, phi, f) =>
+ case LeftSubstEq(b, t1, equals, lambdaPhi) =>
val sEqT = PredicateFormula(equality, Seq(s, t))
val phi_s_for_f = instantiateFunctionSchema(phi, f, s, Nil)
val phi_t_for_f = instantiateFunctionSchema(phi, f, t, Nil)
@@ -355,7 +356,7 @@ object SCProofChecker {
* ---------------------
* Γ, s=t |- φ[t/?f], Δ
*/
- case RightSubstEq(b, t1, s, t, phi, f) =>
+ case RightSubstEq(b, t1, s, t, phi, f) =>
val sEqt = PredicateFormula(equality, Seq(s, t))
if (f.arity == 0)
if (isSameSet(ref(t1).left + sEqt, b.left))
@@ -372,7 +373,7 @@ object SCProofChecker {
* ---------------------
* Γ, ψ↔τ, φ[τ/?q] |- Δ
*/
- case LeftSubstIff(b, t1, psi, tau, phi, q) =>
+ case LeftSubstIff(b, t1, psi, tau, phi, q) =>
val psiIffTau = ConnectorFormula(Iff, Seq(psi, tau))
val phi_tau_for_q = instantiatePredicateSchema(phi, q, tau, Nil)
val phi_psi_for_q = instantiatePredicateSchema(phi, q, psi, Nil)
@@ -390,7 +391,7 @@ object SCProofChecker {
* ---------------------
* Γ, ψ↔τ |- φ[τ/?p], Δ
*/
- case RightSubstIff(b, t1, psi, tau, phi, q) =>
+ case RightSubstIff(b, t1, psi, tau, phi, q) =>
val psiIffTau = ConnectorFormula(Iff, Seq(psi, tau))
val phi_tau_for_q = instantiatePredicateSchema(phi, q, tau, Nil)
val phi_psi_for_q = instantiatePredicateSchema(phi, q, psi, Nil)
@@ -409,7 +410,7 @@ object SCProofChecker {
* Γ[r(a)/?f] |- Δ[r(a)/?f]
* </pre>
*/
- case InstFunSchema(bot, t1, f, r, a) =>
+ case InstFunSchema(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))
@@ -424,7 +425,7 @@ object SCProofChecker {
* Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
* </pre>
*/
- case InstPredSchema(bot, t1, p, psi, a) =>
+ case InstPredSchema(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))
@@ -433,7 +434,7 @@ object SCProofChecker {
SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?p/ψ(a)] must be the same as right-hand side of conclusion.")
else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?p/ψ(a)] 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((no, p) => !isSameSequent(ref(no), sp.imports(p)) )
if (invalid.isEmpty){
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 1166e1c46705195f1235e4b6090952d4542464d1..8f20615690428b2a55d4f68400cbdc1483943ed7 100644
--- a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -247,36 +247,36 @@ object SequentCalculus {
case class RightRefl(bot: Sequent, fa: Formula) extends SCProofStep{val premises = Seq()}
/**
* <pre>
- * Γ, φ[s/?f] |- Δ
+ * Γ, φ(s1,...,sn) |- Δ
* ---------------------
- * Γ, s=t, φ[t/?f ] |- Δ
+ * Γ, s1=t1, ..., sn=tn, φ(t1,...tn) |- Δ
* </pre>
*/
- case class LeftSubstEq(bot: Sequent, t1: Int, s: Term, t: Term, phi: Formula, f: SchematicFunctionLabel) extends SCProofStep{val premises = Seq(t1)}
+ case class LeftSubstEq(bot: Sequent, t1: Int, equals: List[(Term, Term)], lambdaPhi:LambdaTermFormula) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
- * Γ |- φ[s/?f], Δ
+ * Γ |- φ(s1,...,sn), Δ
* ---------------------
- * Γ, s=t |- φ[t/?f], Δ
+ * Γ, s1=t1, ..., sn=tn |- φ(t1,...tn), Δ
* </pre>
*/
- case class RightSubstEq(bot: Sequent, t1: Int, s: Term, t: Term, phi: Formula, f: SchematicFunctionLabel) extends SCProofStep{val premises = Seq(t1)}
+ case class RightSubstEq(bot: Sequent, t1: Int, equals: List[(Term, Term)] ,lambdaPhi:LambdaTermFormula) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
- * Γ, φ[a/?p] |- Δ
+ * Γ, φ(a1,...an) |- Δ
* ---------------------
- * Γ, a↔b, φ[b/?p] |- Δ
+ * Γ, a1↔b1, ..., an↔bn, φ(b1,...bn) |- Δ
* </pre>
*/
- case class LeftSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
+ case class LeftSubstIff(bot: Sequent, t1: Int, equals: List[(Formula, Formula)], lambdaPhi:LambdaFormulaFormula) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
- * Γ |- φ[a/?p], Δ
+ * Γ |- φ(a1,...an), Δ
* ---------------------
- * Γ, a↔b |- φ[b/?p], Δ
+ * Γ, a1↔b1, ..., an↔bn |- φ(b1,...bn), Δ
* </pre>
*/
- case class RightSubstIff(bot: Sequent, t1: Int, fa: Formula, fb: Formula, phi: Formula, h: SchematicPredicateLabel) extends SCProofStep{val premises = Seq(t1)}
+ case class RightSubstIff(bot: Sequent, t1: Int, equals: List[(Formula, Formula)], lambdaPhi:LambdaFormulaFormula) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
* Γ |- Δ
@@ -284,7 +284,7 @@ object SequentCalculus {
* Γ[r(a)/?f] |- Δ[r(a)/?f]
* </pre>
*/
- case class InstFunSchema(bot:Sequent, t1:Int, f:SchematicFunctionLabel, r:Term, a: Seq[VariableLabel] ) extends SCProofStep{val premises = Seq(t1)}
+ case class InstFunSchema(bot:Sequent, t1:Int, f:SchematicFunctionLabel, lambdaT: LambdaTermTerm ) extends SCProofStep{val premises = Seq(t1)}
/**
* <pre>
* Γ |- Δ
@@ -292,7 +292,7 @@ object SequentCalculus {
* Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
* </pre>
*/
- case class InstPredSchema(bot:Sequent, t1:Int, p:SchematicPredicateLabel, psi:Formula, a: Seq[VariableLabel] ) extends SCProofStep{val premises = Seq(t1)}
+ case class InstPredSchema(bot:Sequent, t1:Int, p:SchematicPredicateLabel, lambdaPhi:LambdaTermFormula ) extends SCProofStep{val premises = Seq(t1)}
// Proof Organisation rules
case class SCSubproof(sp: SCProof, premises: Seq[Int] = Seq.empty, display:Boolean = true) extends SCProofStep {