diff --git a/src/main/scala/lisa/KernelHelpers.scala b/src/main/scala/lisa/KernelHelpers.scala
index 5b0e55adbd4aa56134a161157ac9e0a3ae417ab4..22578e034eb971daf89b8912b2a6964354ffb079 100644
--- a/src/main/scala/lisa/KernelHelpers.scala
+++ b/src/main/scala/lisa/KernelHelpers.scala
@@ -137,11 +137,11 @@ object KernelHelpers {
infix def |-[B, T2 <: B](right: T2)(using SetConverter[Formula, T2]): Sequent = Sequent(any2set(left), any2set(right))
- def instantiatePredicateSchemaInSequent(s: Sequent, p: SchematicPredicateLabel, psi: Formula, a: Seq[VariableLabel]): Sequent = {
- s.left.map(phi => instantiatePredicateSchema(phi, p, psi, a)) |- s.right.map(phi => instantiatePredicateSchema(phi, p, psi, a))
+ def instantiatePredicateSchemaInSequent(s: Sequent, m: Map[SchematicPredicateLabel, LambdaTermFormula]): Sequent = {
+ s.left.map(phi => instantiatePredicateSchemas(phi, m)) |- s.right.map(phi => instantiatePredicateSchemas(phi, m))
}
- def instantiateFunctionSchemaInSequent(s: Sequent, f: SchematicFunctionLabel, r: Term, a: Seq[VariableLabel]): Sequent = {
- s.left.map(phi => instantiateFunctionSchema(phi, f, r, a)) |- s.right.map(phi => instantiateFunctionSchema(phi, f, r, a))
+ def instantiateFunctionSchemaInSequent(s: Sequent, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Sequent = {
+ s.left.map(phi => instantiateFunctionSchemas(phi, m)) |- s.right.map(phi => instantiateFunctionSchemas(phi, m))
}
diff --git a/src/main/scala/lisa/kernel/Printer.scala b/src/main/scala/lisa/kernel/Printer.scala
index 35fb39c1141d25b063e25c0ea833d34734482735..9e17a4f6c411e615f061e5f9275d765e4cce484b 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/Judgement.scala b/src/main/scala/lisa/kernel/proof/Judgement.scala
index 20f6740f21583ab0cc9e52ca229b8ce9713360c9..9089d43d5d2266e49b8656d8f8516d97673f9af0 100644
--- a/src/main/scala/lisa/kernel/proof/Judgement.scala
+++ b/src/main/scala/lisa/kernel/proof/Judgement.scala
@@ -52,7 +52,7 @@ sealed abstract class RunningTheoryJudgement[J<:RunningTheory#Justification] {
}
def get:J = this match {
case ValidJustification(just) => just
- case InvalidJustification(message, error) => None.get
+ case InvalidJustification(message, error) => throw new NoSuchElementException("InvalidJustification.get")
}
}
diff --git a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
index 616b2e14537472079bd279ec3e917664fb205ba3..81a2b7fca49a420d2a9e9a62ec8267a023d2a6ab 100644
--- a/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -16,16 +16,16 @@ object SCProofChecker {
* This function verifies that a single SCProofStep is correctly applied. It verify that the step only refers to sequents with a lower number, and that
* the type and parameters of the proofstep correspond to the sequent claimed sequent.
*
- * @param no The number of the given proof step. Needed to vewrify that the proof step doesn't refer to posterior sequents.
- * @param step The proof step whose correctness needs to be checked
+ * @param no The number of the given proof step. Needed to vewrify that the proof step doesn't refer to posterior sequents.
+ * @param step The proof step whose correctness needs to be checked
* @param references A function that associates sequents to a range of positive and negative integers that the proof step may refer to. Typically,
* a proof's [[SCProof.getSequent]] function.
* @return
*/
- def checkSingleSCStep(no:Int, step: SCProofStep, references : Int => Sequent, importsSize: Option[Int]=None): SCProofCheckerJudgement = {
+ def checkSingleSCStep(no: Int, step: SCProofStep, references: Int => Sequent, importsSize: Option[Int] = None): SCProofCheckerJudgement = {
val ref = references
val false_premise = step.premises.find(i => i >= no)
- val false_premise2 = if (importsSize.nonEmpty) step.premises.find(i => i< -importsSize.get) else None
+ val false_premise2 = if (importsSize.nonEmpty) step.premises.find(i => i < -importsSize.get) else None
val r: SCProofCheckerJudgement =
if (false_premise.nonEmpty)
@@ -57,15 +57,15 @@ object SCProofChecker {
* Γ, Σ |-Δ, Π
*/
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))
- if (contains(ref(t1).right, phi))
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of first premise does not contain φ as claimed.")
- else SCInvalidProof(Nil, s"Left-hand side of second premise does not contain φ as claimed.")
- else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
- else SCInvalidProof(Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
+ 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))
+ if (contains(ref(t1).right, phi))
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of first premise does not contain φ as claimed.")
+ else SCInvalidProof(Nil, s"Left-hand side of second premise does not contain φ as claimed.")
+ else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ is not the union of the right-hand sides of the premises.")
+ else SCInvalidProof(Nil, s"Left-hand side of conclusion + φ is not the union of the left-hand sides of the premises.")
// Left rules
/*
@@ -88,7 +88,7 @@ object SCProofChecker {
* Γ, Σ, φ∨ψ |- Δ, Π
*/
case LeftOr(b, t, disjuncts) =>
- if (isSameSet(b.right, t.map(ref(_).right).reduce(_ union _)) )
+ 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))
SCValidProof
@@ -116,9 +116,9 @@ object SCProofChecker {
val psiImpPhi = ConnectorFormula(Implies, Seq(psi, phi))
val phiIffPsi = ConnectorFormula(Iff, Seq(phi, psi))
if (isSameSet(ref(t1).right, b.right))
- if (isSameSet(b.left + phiImpPsi , ref(t1).left + phiIffPsi) ||
- isSameSet(b.left + psiImpPhi , ref(t1).left + phiIffPsi) ||
- isSameSet(b.left + phiImpPsi + psiImpPhi , ref(t1).left + phiIffPsi))
+ if (isSameSet(b.left + phiImpPsi, ref(t1).left + phiIffPsi) ||
+ isSameSet(b.left + psiImpPhi, ref(t1).left + phiIffPsi) ||
+ isSameSet(b.left + phiImpPsi + psiImpPhi, ref(t1).left + phiIffPsi))
SCValidProof
else SCInvalidProof(Nil, "Left-hand side of conclusion + φ↔ψ must be same as left-hand side of premise + either φ→ψ, ψ→φ or both.")
else SCInvalidProof(Nil, "Right-hand sides of premise and conclusion must be the same.")
@@ -143,7 +143,7 @@ object SCProofChecker {
*/
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")
@@ -186,7 +186,7 @@ object SCProofChecker {
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))
- SCValidProof
+ SCValidProof
else SCInvalidProof(Nil, s"Right-hand side of conclusion + φ + ψ is not the same as the union of the right-hand sides of the premises φ∧ψ.")
else SCInvalidProof(Nil, s"Left-hand side of conclusion is not the union of the left-hand sides of the premises.")
/*
@@ -201,7 +201,7 @@ object SCProofChecker {
isSameSet(b.right + psi, ref(t1).right + phiOrPsi) ||
isSameSet(b.right + phi + psi, ref(t1).right + phiOrPsi))
SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
+ else SCInvalidProof(Nil, "Right-hand side of conclusion + φ∧ψ must be same as right-hand side of premise + either φ, ψ or both.")
else SCInvalidProof(Nil, "Left-hand sides of the premise and the conclusion must be the same.")
/*
* Γ, φ |- ψ, Δ
@@ -248,7 +248,7 @@ object SCProofChecker {
*/
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 (isSameSet(b.right + phi, ref(t1).right + BinderFormula(Forall, x, phi)))
if ((b.left union b.right).forall(f => !f.freeVariables.contains(x)))
SCValidProof
else SCInvalidProof(Nil, "The variable x must not be free in the resulting sequent.")
@@ -261,16 +261,16 @@ object SCProofChecker {
*/
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.")
/**
* <pre>
- * Γ |- ∃y.∀x. (x=y) ↔ φ, Δ
+ * Γ |- ∃y.∀x. (x=y) ↔ φ, Δ
* ---------------------------- if y is not free in φ
- * Γ|- ∃!x. φ, Δ
+ * Γ|- ∃!x. φ, Δ
* </pre>
*/
case RightExistsOne(b, t1, phi, x) =>
@@ -332,114 +332,112 @@ object SCProofChecker {
}
/*
- * Γ, φ[s/?f] |- Δ
+ * Γ, φ(s_) |- Δ
* ---------------------
- * Γ, s=t, φ[t/?f] |- Δ
+ * Γ, (s=t)_, φ(t_)|- Δ
*/
- case LeftSubstEq(b, t1, s, t, phi, f) =>
- 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)
- if (f.arity == 0)
- if (isSameSet(b.right, ref(t1).right))
- if (isSameSet(b.left + phi_t_for_f, ref(t1).left + sEqT + phi_s_for_f) ||
- isSameSet(b.left + phi_s_for_f, ref(t1).left + sEqT + phi_t_for_f))
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ[s/?f] must be the same as left-hand side of the premise + s=t + φ[t/?f] (or with s and t swapped).")
- else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
- else SCInvalidProof(Nil, "Function schema ?f must have arity 0")
+ case LeftSubstEq(b, t1, equals, lambdaPhi) =>
+ val (s_es, t_es) = equals.unzip
+ val phi_s_for_f = lambdaPhi(s_es)
+ val phi_t_for_f = lambdaPhi(t_es)
+ val sEqT_es = equals map {case (s, t) => PredicateFormula(equality, Seq(s, t))}
+
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(b.left + phi_t_for_f, ref(t1).left ++ sEqT_es + phi_s_for_f) ||
+ isSameSet(b.left + phi_s_for_f, ref(t1).left ++ sEqT_es + phi_t_for_f))
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ(s_) must be the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
/*
- * Γ |- φ[s/?f], Δ
+ * Γ |- φ(s_), Δ
* ---------------------
- * Γ, s=t |- φ[t/?f], Δ
+ * Γ, (s=t)_ |- φ(t_), Δ
*/
- 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))
- val phi_s_for_f = instantiateFunctionSchema(phi, f, s, Nil)
- val phi_t_for_f = instantiateFunctionSchema(phi, f, t, Nil)
- if (isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
- isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f))
- SCValidProof
- else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ[s/?f] φ[t/?f], but it isn't the case." )
- else SCInvalidProof(Nil, "Left-hand sides of the premise + s=t must be the same as left-hand side of the premise.")
- else SCInvalidProof(Nil, "Function schema ?f must have arity 0.")
+ case RightSubstEq(b, t1, equals, lambdaPhi) =>
+ val sEqT_es = equals map {case (s, t) => PredicateFormula(equality, Seq(s, t))}
+ if (isSameSet(ref(t1).left ++ sEqT_es, b.left))
+ val (s_es, t_es) = equals.unzip
+ val phi_s_for_f = lambdaPhi(s_es)
+ val phi_t_for_f = lambdaPhi(t_es)
+ if (isSameSet(b.right + phi_s_for_f, ref(t1).right + phi_t_for_f) ||
+ isSameSet(b.right + phi_t_for_f, ref(t1).right + phi_s_for_f))
+ SCValidProof
+ else SCInvalidProof(Nil, s"Right-hand side of the premise and the conclusion should be the same with each containing one of φ(s_) φ(t_), but it isn't the case.")
+ else SCInvalidProof(Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
/*
- * Γ, φ[ψ/?q] |- Δ
+ * Γ, φ(ψ_) |- Δ
* ---------------------
- * Γ, ψ↔τ, φ[τ/?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)
- if (q.arity == 0)
- if (isSameSet(b.right, ref(t1).right))
- if (isSameSet(ref(t1).left + psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
- isSameSet(ref(t1).left + psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q))
- SCValidProof
- else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ[ψ/?q] must be the same as left-hand side of the premise + ψ↔τ + φ[τ/?q] (or with ψ and τ swapped).")
- else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
- else SCInvalidProof(Nil, "Predicate schema ?q must have arity 0.")
+ case LeftSubstIff(b, t1, equals, lambdaPhi) =>
+ val psiIffTau = equals map {case (psi, tau) => ConnectorFormula(Iff, Seq(psi, tau))}
+ val (phi_s, tau_s) = equals.unzip
+ val phi_tau_for_q = lambdaPhi(phi_s)
+ val phi_psi_for_q = lambdaPhi(tau_s)
+ if (isSameSet(b.right, ref(t1).right))
+ if (isSameSet(ref(t1).left ++ psiIffTau + phi_tau_for_q, b.left + phi_psi_for_q) ||
+ isSameSet(ref(t1).left ++ psiIffTau + phi_psi_for_q, b.left + phi_tau_for_q))
+ SCValidProof
+ else SCInvalidProof(Nil, "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ↔τ)_ + φ(τ_) (or with ψ and τ swapped).")
+ else SCInvalidProof(Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
/*
* Γ |- φ[ψ/?p], Δ
* ---------------------
* Γ, ψ↔τ |- φ[τ/?p], Δ
*/
- 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)
- if (q.arity == 0)
- if (isSameSet(ref(t1).left + psiIffTau, b.left))
- if (isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
- isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q))
- SCValidProof
- else SCInvalidProof(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 SCInvalidProof(Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
- else SCInvalidProof(Nil, "Predicate schema ?q must have arity 0.")
+ case RightSubstIff(b, t1, equals, lambdaPhi) =>
+ val psiIffTau = equals map {case (psi, tau) => ConnectorFormula(Iff, Seq(psi, tau))}
+ val (phi_s, tau_s) = equals.unzip
+ val phi_tau_for_q = lambdaPhi(phi_s)
+ val phi_psi_for_q = lambdaPhi(tau_s)
+ if (isSameSet(ref(t1).left ++ psiIffTau, b.left))
+ if (isSameSet(b.right + phi_tau_for_q, ref(t1).right + phi_psi_for_q) ||
+ isSameSet(b.right + phi_psi_for_q, ref(t1).right + phi_tau_for_q))
+ SCValidProof
+ else SCInvalidProof(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 SCInvalidProof(Nil, "Left-hand sides of the premise + ψ↔τ must be the same as left-hand side of the premise.")
+
/**
* <pre>
- * Γ |- Δ
+ * Γ |- Δ
* --------------------------
- * Γ[r(a)/?f] |- Δ[r(a)/?f]
+ * Γ[r(a)/?f] |- Δ[r(a)/?f]
* </pre>
*/
- 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)))
+ case InstFunSchema(bot, t1, insts) =>
+ val expected = (ref(t1).left.map(phi => instantiateFunctionSchemas(phi, insts)), ref(t1).right.map(phi => instantiateFunctionSchemas(phi, insts)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
SCValidProof
- else SCInvalidProof(Nil, "Right-hand side of premise instantiated with [?f/r(a)] must be the same as right-hand side of conclusion.")
- else SCInvalidProof(Nil, "Left-hand side of premise instantiated with [?f/r(a)] must be the same as left-hand side of conclusion.")
+ else SCInvalidProof(Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(Nil, "Left-hand side of premise instantiated with the map 'insts' must be the same as left-hand side of conclusion.")
/**
* <pre>
- * Γ |- Δ
+ * Γ |- Δ
* --------------------------
- * Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
+ * Γ[ψ(a)/?p] |- Δ[ψ(a)/?p]
* </pre>
*/
- 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)))
+ case InstPredSchema(bot, t1, insts) =>
+ val expected = (ref(t1).left.map(phi => instantiatePredicateSchemas(phi, insts)), ref(t1).right.map(phi => instantiatePredicateSchemas(phi, insts)))
if (isSameSet(bot.left, expected._1))
if (isSameSet(bot.right, expected._2))
SCValidProof
else
- 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.")
+ SCInvalidProof(Nil, "Right-hand side of premise instantiated with the map 'insts' must be the same as right-hand side of conclusion.")
+ else SCInvalidProof(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, _) =>
- if (premises.size == sp.imports.size){
- val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)) )
- if (invalid.isEmpty){
+ if (premises.size == sp.imports.size) {
+ val invalid = premises.zipWithIndex.find((no, p) => !isSameSequent(ref(no), sp.imports(p)))
+ if (invalid.isEmpty) {
checkSCProof(sp)
} else SCInvalidProof(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 SCInvalidProof(Nil, "Number of premises and imports don't match: "+premises.size+" "+sp.imports.size)
+ } else SCInvalidProof(Nil, "Number of premises and imports don't match: " + premises.size + " " + sp.imports.size)
}
r
@@ -448,6 +446,7 @@ object SCProofChecker {
/**
* Verifies if a given pure SequentCalculus is conditionally correct, as the imported sequents are assumed.
* If the proof is not correct, the functrion will report the faulty line and a brief explanation.
+ *
* @param proof A SC proof to check
* @return SCValidProof if the proof is correct, else SCInvalidProof with the path to the incorrect proof step
* and an explanation.
diff --git a/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
index 1166e1c46705195f1235e4b6090952d4542464d1..a6b1ef6c0a834c77140e4ee51423688cc1123a18 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, insts: Map[SchematicFunctionLabel, 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, insts: Map[SchematicPredicateLabel, 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 {
diff --git a/src/main/scala/proven/DSetTheory/Part1.scala b/src/main/scala/proven/DSetTheory/Part1.scala
index c3dd6d3c2265a3e8c0486605f4bb321aa1dc0ae5..eb52d8f473e165b6a47fbb9c4e1ff238627c0174 100644
--- a/src/main/scala/proven/DSetTheory/Part1.scala
+++ b/src/main/scala/proven/DSetTheory/Part1.scala
@@ -4,6 +4,7 @@ import lisa.kernel.proof.SequentCalculus.*
import lisa.KernelHelpers.{*, given}
import lisa.kernel.Printer
import lisa.kernel.Printer.{prettyFormula, prettySCProof}
+import lisa.kernel.fol.FOL
import proven.tactics.ProofTactics.*
import proven.tactics.Destructors.*
import lisa.settheory.AxiomaticSetTheory.*
@@ -19,20 +20,23 @@ object Part1 {
def axiom(f:Formula):theory.Axiom = theory.getAxiom(f).get
- private val x = SchematicFunctionLabel("x", 0)()
- private val y = SchematicFunctionLabel("y", 0)()
+ private val x = SchematicFunctionLabel("x", 0)
+ private val y = SchematicFunctionLabel("y", 0)
+ private val z = SchematicFunctionLabel("z", 0)
private val x1 = VariableLabel("x")
private val y1 = VariableLabel("y")
private val z1 = VariableLabel("z")
- private val z = SchematicFunctionLabel("z", 0)()
private val f = SchematicFunctionLabel("f", 0)
private val g = SchematicFunctionLabel("g", 0)
private val h = SchematicPredicateLabel("h", 0)
+ given Conversion[SchematicFunctionLabel, Term] with
+ def apply(s:SchematicFunctionLabel): Term = s()
-/**
- */
+ /**
+
+ */
val russelParadox: SCProof = {
val contra = (in(y,y)) <=> !(in(y,y))
val s0 = Hypothesis(contra |- contra, contra)
@@ -48,15 +52,15 @@ object Part1 {
//forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z)))))
val i1 = () |- comprehensionSchema
val i2 = russelParadox.conclusion // forall(x1, in(x1,y) <=> !in(x1, x1)) |- ()
- val p0: SCProofStep = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))), -1, sPhi, !in(x1, x1), Seq(x1, z1))
+ val p0: SCProofStep = InstPredSchema(() |- forall(z1, exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x(), x()))))
val s0 = SCSubproof(instantiateForall(SCProof(IndexedSeq(p0), IndexedSeq(i1)), z), Seq(-1)) //exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z1) /\ !in(x1, x1))))
val s1 = hypothesis(in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) //in(x,y) <=> (in(x,z) /\ in(x, x)) |- in(x,y) <=> (in(x,z) /\ in(x, x))
- val s2 = RightSubstIff((in(x1, z) <=> And(), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> (And() /\ !in(x1, x1)), 1, in(x1, z), And(), in(x1,y1) <=> (h() /\ !in(x1, x1)), h) //in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
+ val s2 = RightSubstIff((in(x1, z) <=> And(), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> (And() /\ !in(x1, x1)), 1, List((in(x1, z), And())), LambdaFormulaFormula(Seq(h), in(x1,y1) <=> (h() /\ !in(x1, x1)))) //in(x1,y1) <=> (in(x1,z1) /\ in(x1, x1)) |- in(x,y) <=> (And() /\ in(x1, x1))
val s3 = Rewrite((in(x1, z), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> !in(x1, x1), 2)
val s4 = LeftForall((forall(x1, in(x1, z)), in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))) |- in(x1,y1) <=> !in(x1, x1), 3, in(x1, z), x1, x1)
val s5 = LeftForall((forall(x1, in(x1, z)), forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) |- in(x1,y1) <=> !in(x1, x1), 4, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)), x1, x1)
val s6 = RightForall((forall(x1, in(x1, z)), forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) |- forall(x1, in(x1,y1) <=> !in(x1, x1)), 5, in(x1,y1) <=> !in(x1, x1), x1)
- val s7 = InstFunSchema(forall(x1, in(x1,y1) <=> !in(x1, x1)) |- (), -2, SchematicFunctionLabel("y", 0), y1, Nil)
+ val s7 = InstFunSchema(forall(x1, in(x1,y1) <=> !in(x1, x1)) |- (), -2, Map(SchematicFunctionLabel("y", 0) -> LambdaTermTerm(Nil, y1)))
val s8 = Cut((forall(x1, in(x1, z)), forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) |- (), 6, 7, forall(x1, in(x1,y1) <=> !in(x1, x1)))
val s9 = LeftExists((forall(x1, in(x1, z)), exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))))) |- (), 8, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1))), y1)
val s10 = Cut(forall(x1, in(x1, z)) |- (), 0, 9, exists(y1, forall(x1, in(x1,y1) <=> (in(x1,z) /\ !in(x1, x1)))) )
@@ -70,6 +74,11 @@ object Part1 {
val x = VariableLabel("x")
val y = VariableLabel("y")
val z = VariableLabel("z")
+ val a1 = SchematicFunctionLabel("a", 0)
+ val b1 = SchematicFunctionLabel("b", 0)
+ val x1 = SchematicFunctionLabel("x", 0)
+ val y1 = SchematicFunctionLabel("y", 0)
+ val z1 = SchematicFunctionLabel("z", 0)
val A = SchematicFunctionLabel("A", 0)()
val X = VariableLabel("X")
val B = VariableLabel("B")
@@ -83,14 +92,14 @@ object Part1 {
//val s3 = RightForall((H) |- forall(a, in(a, A) ==> existsOne(x, phi(x, a))), 2, in(a, A) ==> existsOne(x, phi(x, a)), a) // () |- ∀a∈A. ∃!x. phi(x, a)
val s3 = hypothesis(H1)
val i1 = ()|- replacementSchema
- val p0 = InstPredSchema(()|- instantiatePredicateSchema(replacementSchema, sPsi, phi(x, a), Seq(y,a,x)), -1, sPsi, phi(x, a), Seq(y,a,x))
+ val p0 = InstPredSchema(()|- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y1,a1,x1), phi(x1, a1)))), -1, Map(sPsi -> LambdaTermFormula(Seq(y1,a1,x1), phi(x1, a1))))
val p1 = instantiateForall(SCProof(Vector(p0), Vector(i1)), A)
val s4 = SCSubproof(p1, Seq(-1)) //
val s5 = Rewrite(s3.bot.right.head |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x)) ))), 4)
val s6 = Cut((H1) |- exists(B, forall(x, in(x, A) ==> exists(y, in(y, B) /\ (phi(y, x)) ))), 3,5, s3.bot.right.head) // ⊢ ∃B. ∀x. (x ∈ A) ⇒ ∃y. (y ∈ B) ∧ (y = (x, b))
val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z)))))
- val q0 = InstPredSchema(() |- instantiatePredicateSchema(comprehensionSchema, sPhi, exists(a, in(a, A) /\ (phi(x, a))), Seq(x,z)), -1, sPhi, exists(a, in(a, A) /\ (phi(x, a))), Seq(x,z))
+ val q0 = InstPredSchema(() |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a)))))
val q1 = instantiateForall(SCProof(Vector(q0), Vector(i2)), B)
val s7 = SCSubproof(q1, Seq(-2)) //∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) )
SCProof(Vector(s0, s1, s2, s3, s4, s5, s6, s7), Vector(i1, i2))
@@ -112,19 +121,19 @@ object Part1 {
*/
val s0 = hypothesis(in(y1, B))
- val s1 = RightSubstEq((in(y1, B), x===y1) |- in(x, B), 0, x, y1, in(f(), B), f)
- val s2 = LeftSubstIff(Set( in(y1, B), (x===y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, (x===y1), phi(x, a), h(), h)
- val s3 = LeftSubstEq(Set( y===y1, in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, y, y1, (x===f()) <=> phi(x, a), f)
- val s4 = LeftSubstIff(Set( (y===y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, phi(y1, a), y1===y, h(), h)
+ val s1 = RightSubstEq((in(y1, B), x===y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f(), B)))
+ val s2 = LeftSubstIff(Set( in(y1, B), (x===y1) <=> phi(x, a), phi(x, a)) |- in(x, B), 1, List(((x===y1), phi(x, a))), LambdaFormulaFormula(Seq(h), h()))
+ val s3 = LeftSubstEq(Set( y===y1, in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 2, List((y, y1)), LambdaTermFormula(Seq(f), (x===f()) <=> phi(x, a)))
+ val s4 = LeftSubstIff(Set( (y===y1) <=> phi(y1, a), phi(y1, a), in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 3, List((phi(y1, a), y1===y)), LambdaFormulaFormula(Seq(h), h()))
val s5 = LeftForall(Set( forall(x, (y===x) <=> phi(x, a)), phi(y1, a), in(y1, B), (x===y) <=> phi(x, a), phi(x, a)) |- in(x, B), 4, (y===x) <=> phi(x, a), x, y1)
val s6 = LeftForall(Set( forall(x, (y===x) <=> phi(x, a)), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 5, (x===y) <=> phi(x, a), x, x)
val s7 = LeftExists(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), phi(y1, a), in(y1, B), phi(x, a)) |- in(x, B), 6, forall(x, (y===x) <=> phi(x, a)), y)
val s8 = Rewrite(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), phi(y1, a) /\ in(y1, B), phi(x, a)) |- in(x, B), 7)
val s9 = LeftExists(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), exists(y1, phi(y1, a) /\ in(y1, B)), phi(x, a)) |- in(x, B), 8, phi(y1, a) /\ in(y1, B), y1)
val s10 = Rewrite(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), And() ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a)) |- in(x, B), 9)
- val s11 = LeftSubstIff(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A))|- in(x, B), 10, And(), in(a, A), h() ==> exists(y, phi(y, a) /\ in(y, B)), h )
+ val s11 = LeftSubstIff(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), phi(x, a), in(a, A))|- in(x, B), 10, List((And(), in(a, A))), LambdaFormulaFormula(Seq(h), h() ==> exists(y, phi(y, a) /\ in(y, B)) ))
val s12 = LeftForall(Set( exists(y, forall(x, (y===x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 11, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)), a, a)
- val s13 = LeftSubstIff(Set( in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 12, And(), in(a, A), h() ==> exists(y, forall(x, (y===x) <=> phi(x, a))), h )
+ val s13 = LeftSubstIff(Set( in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 12, List((And(), in(a, A))), LambdaFormulaFormula(Seq(h), h() ==> exists(y, forall(x, (y===x) <=> phi(x, a))) ))
val s14 = LeftForall(Set( forall(a, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a), in(a, A))|- in(x, B), 13, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a))), a, a)
val s15 = Rewrite(Set( forall(a, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), phi(x, a) /\ in(a, A))|- in(x, B), 14)
val s16 = LeftExists(Set( forall(a, in(a, A) ==> exists(y, forall(x, (y===x) <=> phi(x, a)))), forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B))), exists(a, phi(x, a) /\ in(a, A)))|- in(x, B), 15, phi(x, a) /\ in(a, A), a)
@@ -185,15 +194,15 @@ object Part1 {
val s15 = SCSubproof({
val i1 = s13.bot // G, F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
val i2 = ()|- extensionalityAxiom
- val t0 = RightSubstIff(Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1), -1, in(x, X), exists(a, in(a, A) /\ (phi(x, a))), h() <=> in(x, B1), h) //redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
+ val t0 = RightSubstIff(Set(H1, G, F, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, X) <=> in(x, B1), -1, List((in(x, X), exists(a, in(a, A) /\ (phi(x, a))))), LambdaFormulaFormula(Seq(h), h() <=> in(x, B1))) //redGoal2 F, (z ∈ X) <=> ∃a. a ∈ A ∧ z = (a, b) |- (z ∈ X) <=> (z ∈ B1)
val t1 = LeftForall(Set(H1, G, F, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) |- in(x, X) <=> in(x, B1), 0, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))), x, x ) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- (z ∈ X) <=> (z ∈ B1)
val t2 = RightForall(t1.bot.left |- forall(x, in(x, X) <=> in(x, B1)), 1, in(x, X) <=> in(x, B1), x) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- ∀z. (z ∈ X) <=> (z ∈ B1)
val t3 = SCSubproof(instantiateForall(SCProof(Vector(Rewrite(()|- extensionalityAxiom, -1)), Vector(()|-extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1)))
- val t4 = RightSubstIff(t1.bot.left++t3.bot.right |- X===B1, 2, X===B1, forall(z, in(z, X) <=> in(z, B1)), h(), h) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
+ val t4 = RightSubstIff(t1.bot.left++t3.bot.right |- X===B1, 2, List((X===B1, forall(z, in(z, X) <=> in(z, B1)) )), LambdaFormulaFormula(Seq(h), h())) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)], (∀z. (z ∈ X) <=> (z ∈ B1)) <=> (X === B1))) |- X=B1
val t5 = Cut(t1.bot.left |- X===B1, 3, 4, t3.bot.right.head) //redGoal2 F, [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] |- X=B1
val t6 = Rewrite(Set(H1, G, F) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))) ==> (X===B1), 5) // F |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] ==> X=B1
val i3 = s14.bot // F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val t7 = RightSubstEq(Set(H1, G, F, X===B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), -3, X, B1, forall(x, in(x, f()) <=> exists(a, in(a, A) /\ (phi(x, a)))), f) //redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val t7 = RightSubstEq(Set(H1, G, F, X===B1) |- forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), -3, List((X, B1)), LambdaTermFormula(Seq(f), forall(x, in(x, f()) <=> exists(a, in(a, A) /\ phi(x, a)) ))) //redGoal1 F, X=B1 |- [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
val t8 = Rewrite(Set(H1, G, F) |- X===B1 ==> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), 7) //redGoal1 F |- X=B1 ==> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)] -------second half with t6
val t9 = RightIff(Set(H1, G, F) |- (X===B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))), 6, 8, X===B1, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))) //goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
@@ -205,7 +214,7 @@ object Part1 {
val s19 = Rewrite(s18.bot.left |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 18) // ∃B1. F |- ∃!X. [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
val s20 = Cut((G, H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 7, 19, exists(B1, F))
val s21 = LeftExists((H1, exists(B, G)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))), 20, G, B)
- val s22 = Cut((H1) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
+ val s22 = Cut(H1 |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ phi(x, a)))), 6, 21, exists(B, G))
val steps = Vector(s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15,s16,s17,s18,s19,s20,s21,s22)
SCProof(steps, Vector(i1, i2, i3))
}
@@ -221,6 +230,12 @@ object Part1 {
val x1 = VariableLabel("x1")
val y = VariableLabel("y")
val z = VariableLabel("z")
+ val a_ = SchematicFunctionLabel("a",0)
+ val b_ = SchematicFunctionLabel("b",0)
+ val x_ = SchematicFunctionLabel("x",0)
+ val x1_ = SchematicFunctionLabel("x1",0)
+ val y_ = SchematicFunctionLabel("y",0)
+ val z_ = SchematicFunctionLabel("z",0)
val A = SchematicFunctionLabel("A", 0)()
val X = VariableLabel("X")
val B = SchematicFunctionLabel("B", 0)()
@@ -230,15 +245,15 @@ object Part1 {
val H = existsOne(x, phi(x, a))
val H1 = forall(a, in(a, A) ==> H)
val i1 = thmMapFunctional.conclusion
- val H2 = instantiatePredicateSchema(H1, phi, psi(x, a, b), Seq(x, a))
- val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, phi, psi(x, a, b), Seq(x, a))
+ val H2 = instantiatePredicateSchemas(H1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
+ val s0 = InstPredSchema((H2) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), -1, Map(phi -> LambdaTermFormula(Seq(x_, a_), psi(x_, a_, b))))
val s1 = Weakening((H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 0)
- val s2 = LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, in(b, B), And(), h() ==> H2, h)
+ val s2 = LeftSubstIff((in(b, B) ==> H2, in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 1, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2))
val s3 = LeftForall((forall(b, in(b, B) ==> H2), in(b, B)) |- existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 2, in(b, B) ==> H2, b, b)
val s4 = Rewrite(forall(b, in(b, B) ==> H2) |- in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), 3)
val s5 = RightForall(forall(b, in(b, B) ==> H2) |- forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))), 4, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b)))), b)
- val s6 = InstFunSchema(forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchema(i1.right.head, SchematicFunctionLabel("A", 0), B, Seq()), -1, SchematicFunctionLabel("A", 0), B, Seq())
- val s7 = InstPredSchema(forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))), 6, phi, forall(x,in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))), Seq(X, b))
+ val s6 = InstFunSchema(forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateFunctionSchemas(i1.right.head, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B))), -1, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B)))
+ val s7 = InstPredSchema(forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))), 6, Map(phi -> LambdaTermFormula(Seq(y_, b_), forall(x, in(x, y_) <=> exists(a, in(a, A) /\ psi(x, a, b_))))))
val s8 = Cut(forall(b, in(b, B) ==> H2) |- existsOne(X, forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))), 5, 7, forall(b, in(b, B) ==> existsOne(X, forall(x, in(x, X) <=> exists(a, in(a, A) /\ psi(x, a, b))))))
SCProof(Vector(s0,s1,s2,s3,s4,s5,s6,s7, s8), Vector(i1))
@@ -279,8 +294,8 @@ object Part1 {
val g2 = SCSubproof({
val s0 = hypothesis(F(x1) === z)
- val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, x, x1, F(f()) === z, f)
- val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, x === x1, phi(x), g(), g)
+ val s1 = LeftSubstEq((x === x1, F(x) === z) |- F(x1) === z, 0, List((x, x1)), LambdaTermFormula(Seq(f), F(f()) === z))
+ val s2 = LeftSubstIff(Set(phi(x) <=> (x === x1), phi(x), F(x) === z) |- F(x1) === z, 1, List((x === x1, phi(x))), LambdaFormulaFormula(Seq(g), g()))
val s3 = LeftForall(Set(forall(x, phi(x) <=> (x === x1)), phi(x), F(x) === z) |- F(x1) === z, 2, phi(x) <=> (x === x1), x, x)
val s4 = Rewrite(Set(forall(x, phi(x) <=> (x === x1)), phi(x) /\ (F(x) === z)) |- F(x1) === z, 3)
val s5 = LeftExists(Set(forall(x, phi(x) <=> (x === x1)), exists(x, phi(x) /\ (F(x) === z))) |- F(x1) === z, 4,phi(x) /\ (F(x) === z), x)
@@ -336,6 +351,10 @@ object Part1 {
val b = VariableLabel("b")
val x = VariableLabel("x")
val x1 = VariableLabel("x1")
+ val a_ = SchematicFunctionLabel("a",0)
+ val b_ = SchematicFunctionLabel("b",0)
+ val x_ = SchematicFunctionLabel("x",0)
+ val y_ = SchematicFunctionLabel("y",0)
val F = SchematicFunctionLabel("F", 1)
val A = SchematicFunctionLabel("A", 0)()
val X = VariableLabel("X")
@@ -345,11 +364,11 @@ object Part1 {
val i1 = lemma1.conclusion
val i2 = lemmaApplyFToObject.conclusion
- val rPhi = forall(x, in(x, X) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
- val seq0 = instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X))
- val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
- val seq1 = instantiateFunctionSchemaInSequent(seq0, F, union(x), Seq(x))
- val s1 = InstFunSchema(seq1, 0, F, union(x), Seq(x))
+ val rPhi = forall(x, in(x, y_) <=> exists(b, in(b, B) /\ forall(x1,in(x1, x) <=> exists(a, in(a, A) /\ psi(x1, a, b)))))
+ val seq0 = instantiatePredicateSchemaInSequent(i2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi)))
+ val s0 = InstPredSchema(seq0, -2, Map(phi -> LambdaTermFormula(Seq(y_), rPhi))) //val s0 = InstPredSchema(instantiatePredicateSchemaInSequent(i2, phi, rPhi, Seq(X)), -2, phi, rPhi, Seq(X))
+ val seq1 = instantiateFunctionSchemaInSequent(seq0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
+ val s1 = InstFunSchema(seq1, 0, Map(F -> LambdaTermTerm(Seq(x_), union(x_))))
val s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
SCProof(Vector(s0,s1,s2), Vector(i1, i2))
}
@@ -362,6 +381,9 @@ object Part1 {
val a = VariableLabel("a")
val b = VariableLabel("b")
val x = VariableLabel("x")
+ val a_ = SchematicFunctionLabel("a",0)
+ val b_ = SchematicFunctionLabel("b",0)
+ val x_ = SchematicFunctionLabel("x",0)
val x1 = VariableLabel("x1")
val F = SchematicFunctionLabel("F", 1)
val A = SchematicFunctionLabel("A", 0)()
@@ -381,19 +403,20 @@ object Part1 {
SCProof(Vector(s0,s1,s2,s3,s4,s5))
}) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
- val s1 = InstPredSchema(instantiatePredicateSchemaInSequent(i1, psi, x===oPair(a,b), Seq(x, a, b)), -1, psi, x===oPair(a,b), Seq(x, a, b))
+ val s1 = InstPredSchema(instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ ===oPair(a_,b_)))), -1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ ===oPair(a_,b_))))
val s2 = Cut(()|-s1.bot.right, 0, 1, s1.bot.left.head)
val vA = VariableLabel("A")
val vB = VariableLabel("B")
- val s3 = InstFunSchema(instantiateFunctionSchemaInSequent(s2.bot, SchematicFunctionLabel("A", 0), vA, Nil), 2, SchematicFunctionLabel("A", 0), vA, Nil)
- val s4 = InstFunSchema(instantiateFunctionSchemaInSequent(s3.bot, SchematicFunctionLabel("B", 0), vA, Nil), 3, SchematicFunctionLabel("B", 0), vA, Nil)
+ val s3 = InstFunSchema(instantiateFunctionSchemaInSequent(s2.bot, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, vA))), 2, Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, vA)))
+ val s4 = InstFunSchema(instantiateFunctionSchemaInSequent(s3.bot, Map(SchematicFunctionLabel("B", 0) -> LambdaTermTerm(Nil, vA))), 3, Map(SchematicFunctionLabel("B", 0) -> LambdaTermTerm(Nil, vA)))
val s5 = RightForall(()|- forall(vA, s4.bot.right.head), 4, s4.bot.right.head, vA)
val s6 = RightForall(()|- forall(vB, s5.bot.right.head), 5, s5.bot.right.head, vB)
SCProof(Vector(s0, s1, s2, s3, s4, s5, s6), Vector(i1))
}
println("cartesian")
+ /*
val thm_lemmaCartesianProduct = theory.proofToTheorem("lemmaCartesianProduct", lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments)).get
val vA = VariableLabel("A")
@@ -402,7 +425,7 @@ object Part1 {
val def_oPair = theory.makeFunctionDefinition(lemmaCartesianProduct, Seq(thm_lemmaMapTwoArguments), cart_product, Seq(vA, vB), VariableLabel("z"), innerOfDefinition(lemmaCartesianProduct.conclusion.right.head)).get
-
+*/
@@ -432,21 +455,20 @@ object Part1 {
val error = SCProofChecker.checkSCProof(proof)
println(prettySCProof(proof, error))
}
-/*
- println("thmMapFunctional")
+ println("\nthmMapFunctional")
checkProof(thmMapFunctional)
- println("lemma1")
+ println("\nlemma1")
checkProof(lemma1)
- println("lemmaApplyFToObject")
+ println("\nlemmaApplyFToObject")
checkProof(lemmaApplyFToObject)
- println("lemmaMapTwoArguments")
+ println("\nlemmaMapTwoArguments")
checkProof(lemmaMapTwoArguments)
- println("lemmaCartesianProduct")
+ println("\nlemmaCartesianProduct")
checkProof(lemmaCartesianProduct)
-*/
-
}
}
+
+
// have union ∀x. ∀z. x ∈ Uz <=> ∃y. (x ∈ y /\ y ∈ z)
// have x ∈ UY <=> ∃y. (x ∈ y /\ y ∈ Y)
//
diff --git a/src/main/scala/proven/ElementsOfSetTheory.scala b/src/main/scala/proven/ElementsOfSetTheory.scala
index 36e7e30809d24659faef2a77df30f500ba398360..afe6e031b0db63ad098509e70e49f9ca87a9beba 100644
--- a/src/main/scala/proven/ElementsOfSetTheory.scala
+++ b/src/main/scala/proven/ElementsOfSetTheory.scala
@@ -10,6 +10,7 @@ import lisa.settheory.AxiomaticSetTheory.*
import scala.collection.immutable.SortedSet
import lisa.kernel.proof.{SCProof, SCProofChecker}
import lisa.settheory.AxiomaticSetTheory
+import proven.ElementsOfSetTheory.theory
import scala.collection.immutable
@@ -52,10 +53,8 @@ object ElementsOfSetTheory {
val pr0 = SCSubproof(pairSame13, Seq(-1, -2))
val pr1 = SCSubproof(pairSame23, Seq(-1, -2))
val pr2 = RightSubstIff(Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))), 0,
- (x === z) \/ (y === z),
- in(z, pair(y, x)),
- in(z, pair(x, y)) <=> h(),
- h)
+ List(((x === z) \/ (y === z), in(z, pair(y, x)))),
+ LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h()))
val pr3 = Cut(Sequent(pr1.bot.left, pr2.bot.right), 1, 2, pr2.bot.left.head)
//val pr4 = LeftAxiom(Sequent(Set(), pr2.bot.right), 3, pr1.bot.left.head, "")
val pr4 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z)
@@ -65,7 +64,7 @@ object ElementsOfSetTheory {
val fin4 = generalizeToForall(fin3, fin3.conclusion.right.head, y)
fin4.copy(imports = imps)
} // |- ∀∀({x$1,y$2}={y$2,x$1})
- val thm_proofUnorderedPairSymmetry = theory.proofToTheorem("proofUnorderedPairSymmetry", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
+ val thm_proofUnorderedPairSymmetry: theory.Theorem = theory.proofToTheorem("proofUnorderedPairSymmetry", proofUnorderedPairSymmetry, Seq(axiom(extensionalityAxiom), axiom(pairAxiom))).get
val proofUnorderedPairDeconstruction: SCProof = {
@@ -78,7 +77,7 @@ object ElementsOfSetTheory {
val p1_0 = hypothesis(zf)
val p1_1 = RightImplies(emptySeq +> (zf ==> zf), 0, zf, zf)
val p1_2 = RightIff(emptySeq +> (zf <=> zf), 1, 1, zf, zf) // |- (z in {x,y} <=> z in {x,y})
- val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, pxy, pxy1, zf <=> in(z, g()), g)
+ val p1_3 = 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) // ({x,y}={x',y'}) |- ((z∈{x,y})↔(z∈{x',y'}))
val p1 = SCSubproof({
@@ -92,15 +91,13 @@ object ElementsOfSetTheory {
p2_1
}, Seq(-1), display = true) // |- (z in {x',y'}) <=> (z=x' \/ z=y')
val p3 = RightSubstEq(
- emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))), 1, pxy, pxy1, in(z, g()) <=> ((z === x) \/ (z === y)), g
+ emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))), 1, List((pxy, pxy1)), LambdaTermFormula(Seq(g), in(z, g()) <=> ((z === x) \/ (z === y)) )
) // ({x,y}={x',y'}) |- ((z∈{x',y'})↔((z=x)∨(z=y)))
val p4 = RightSubstIff(
emptySeq +< p3.bot.left.head +< p2.bot.right.head +> (((z === x) \/ (z === y)) <=> ((z === x1) \/ (z === y1))),
3,
- (z === x1) \/ (z === y1),
- in(z, pxy1),
- h() <=> ((z === x) \/ (z === y)),
- h
+ List(((z === x1) \/ (z === y1), in(z, pxy1))),
+ LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y)))
) // ((z∈{x',y'})↔((x'=z)∨(y'=z))), ({x,y}={x',y'}) |- (((z=x)∨(z=y))↔((z=x')∨(z=y')))
val p5 = Cut(emptySeq ++< p3.bot ++> p4.bot, 2, 4, p2.bot.right.head)
SCProof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(()|-pairAxiom))
@@ -126,8 +123,8 @@ object ElementsOfSetTheory {
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 = RightSubstEq(emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)), -1, x, y, (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1)), g) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
- val pa0_2 = RightSubstIff(emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))), 1, f1, f1 \/ f1, h() <=> ((z === x1) \/ (z === y1)), h)
+ val pa0_1 = RightSubstEq(emptySeq +< (pxy === pxy1) +< (x === y) +> ((f1 \/ f1) <=> (z === x1) \/ (z === y1)), -1, List((x, y)), LambdaTermFormula(Seq(g), (f1 \/ (z === g())) <=> ((z === x1) \/ (z === y1))) ) // ({x,y}={x',y'}) y=x|- (z=x)\/(z=x) <=> (z=x' \/ z=y')
+ val pa0_2 = RightSubstIff(emptySeq +< (pxy === pxy1) +< (x === y) +< (f1 <=> (f1 \/ f1)) +> (f1 <=> ((z === x1) \/ (z === y1))), 1, List((f1, f1 \/ f1)), LambdaFormulaFormula(Seq(h), h() <=> ((z === x1) \/ (z === y1))))
val pa0_3 = Cut(emptySeq +< (pxy === pxy1) +< (x === y) +> (f1 <=> ((z === x1) \/ (z === y1))), 0, 2, f1 <=> (f1 \/ f1)) // (x=y), ({x,y}={x',y'}) |- ((z=x)↔((z=x')∨(z=y')))
val pa0_4 = RightForall(emptySeq +< (pxy === pxy1) +< (x === y) +> forall(z, f1 <=> ((z === x1) \/ (z === y1))), 3, f1 <=> ((z === x1) \/ (z === y1)), z)
val ra0_0 = instantiateForall(SCProof(IndexedSeq(pa0_0, pa0_1, pa0_2, pa0_3, pa0_4), IndexedSeq(pa0_m1.bot)), y1) // (x=y), ({x,y}={x',y'}) |- ((y'=x)↔((y'=x')∨(y'=y')))
@@ -139,7 +136,7 @@ object ElementsOfSetTheory {
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 = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, x, y, y1 === g(), g)
+ val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g()))
SCProof(ra3.steps, IndexedSeq(pam1.bot)) appended pal // (x=y), ({x,y}={x',y'}) |- (y'=y)
}, IndexedSeq(-1)) // (x=y), ({x,y}={x',y'}) |- (y'=y)
,
@@ -155,7 +152,7 @@ object ElementsOfSetTheory {
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 = RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, x, x1, (y === g()) \/ (y === y1), g)
+ val pb1 = RightSubstEq(emptySeq ++< rb0.conclusion +< (x === x1) +> ((y === x) \/ (y === y1)), rb0.length - 1, List((x, x1)), LambdaTermFormula(Seq(g), (y === g()) \/ (y === y1)))
val rb1 = destructRightOr(
rb0 appended pb1, // ({x,y}={x',y'}) , x=x'|- (y=x)∨(y=y')
y === x, y === y1
@@ -167,7 +164,7 @@ object ElementsOfSetTheory {
).steps, IndexedSeq(pcm1.bot)), IndexedSeq(-1)) // (x=x'), ({x,y}={x',y'}) |- (y'=y)
val pc1 = RightRefl(emptySeq +> (x === x), x === x)
val pc2 = RightAnd(emptySeq ++< pc0.bot +> ((y1 === y) /\ (x === x)), Seq(0, 1), Seq(y1 === y, x === x)) // ({x,y}={x',y'}), x=x' |- (x=x /\ y=y')
- val pc3 = RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, x, x1, (y1 === y) /\ (g() === x), g) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
+ val pc3 = RightSubstEq(emptySeq ++< pc2.bot +> ((y1 === y) /\ (x1 === x)), 2, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g() === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')
val pc4 = RightOr(emptySeq ++< pc3.bot +> (pc3.bot.right.head \/ ((x === y1) /\ (y === x1))), 3, pc3.bot.right.head, (x === y1) /\ (y === x1)) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y')\/(x=y' /\ y=x')
val r = SCProof(IndexedSeq(pc0, pc1, pc2, pc3, pc4), IndexedSeq(pcm1.bot))
r
@@ -189,7 +186,7 @@ object ElementsOfSetTheory {
val rd0_1_1 = instantiateForall(SCProof(IndexedSeq(pd0_1_0), IndexedSeq(pd0_m1.bot)), x1) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
rd0_1_1
}, IndexedSeq(-1)) // ({x,y}={x',y'}) |- (x'=x \/ x'=y) <=> (x'=x' \/ x'=y')
- val pd0_2 = RightSubstIff(pd0_1.bot.right |- ((x1===x) \/ (x1===y)), 0,(x1===x) \/ (x1===y), (x1===x1) \/ (x1===y1),SchematicPredicateLabel("h", 0)(), SchematicPredicateLabel("h", 0) ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
+ val pd0_2 = RightSubstIff(pd0_1.bot.right |- ((x1===x) \/ (x1===y)), 0, List(((x1===x) \/ (x1===y), (x1===x1) \/ (x1===y1))), LambdaFormulaFormula(Seq(h), h()) ) // (x'=x \/ x'=y) <=> (x'=x' \/ x'=y') |- (x'=x \/ x'=y)
val pd0_3 = Cut(pd0_1.bot.left |- pd0_2.bot.right, 1,2, pd0_1.bot.right.head) // ({x,y}={x',y'}) |- (x=x' \/ y=x')
destructRightOr(SCProof(IndexedSeq(pd0_0, pd0_1, pd0_2, pd0_3), IndexedSeq(pd0_m1.bot)), x === x1, y === x1) // ({x,y}={x',y'}) |- x=x', y=x'
}, IndexedSeq(-1)) // ({x,y}={x',y'}) |- x=x', y=x' --
diff --git a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 9c7c151505387f5acb63e80589bc2266101ee380..14f1de7881d7060c4954d37973aaa9899ead8967 100644
--- a/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -43,23 +43,23 @@ class IncorrectProofsTests extends ProofCheckerSuite {
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, x, z, x === y, yl) // wrong variable replaced
+ RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y)) // wrong variable replaced
),
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- RightSubstEq(emptySeq +< (x === y) +> (z === y), 0, x, z, x === y, xl) // missing hypothesis
+ RightSubstEq(emptySeq +< (x === y) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === y)) // missing hypothesis
),
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, x, z, x === z, xl) // replacement mismatch
+ RightSubstEq(emptySeq +< (x === y) +< (x === z) +> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === z)) // replacement mismatch
),
SCProof(
Hypothesis(emptySeq +< (x === y) +> (x === y), x === y),
- LeftSubstEq(emptySeq +< (z === y) +< (x === z) +> (x === y), 0, x, z, x === y, yl)
+ LeftSubstEq(emptySeq +< (z === y) +< (x === z) +> (x === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y))
),
SCProof(
Hypothesis(emptySeq +< (f <=> g) +> (f <=> g), f <=> g),
- LeftSubstIff(emptySeq +< (h <=> g) +< (f <=> h) +> (f <=> g), 0, f, h, f <=> g, gl)
+ LeftSubstIff(emptySeq +< (h <=> g) +< (f <=> h) +> (f <=> g), 0, List((f, h)), LambdaFormulaFormula(Seq(gl), f <=> g))
),
SCProof(
Hypothesis(emptySeq +< f +> f, f),
diff --git a/src/test/scala/lisa/kernel/ProofTests.scala b/src/test/scala/lisa/kernel/ProofTests.scala
index 8389948f31f03fe9f877b3c202ca4c63e43921aa..b26dbe442a7d7330a925517fa944b88545c34e75 100644
--- a/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/src/test/scala/lisa/kernel/ProofTests.scala
@@ -36,7 +36,7 @@ class ProofTests extends AnyFunSuite {
test("Verification of substitution") {
val t0 = Hypothesis(fp(x)|-fp(x), fp(x))
- val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, x, y, fp(sT()), sT)
+ val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, List((x, y)), LambdaTermFormula(Seq(sT), fp(sT())))
val pr = new SCProof(IndexedSeq(t0, t1))
assert(predicateVerifier(pr).isValid)
}
diff --git a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
index 413c19c457c0175e9a637499a1d8360ada471d70..da4387b54eb92e7452256d97e784074ab2039b4f 100644
--- a/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
+++ b/src/test/scala/lisa/proven/ElementsOfSetTheoryTests.scala
@@ -50,10 +50,8 @@ class ElementsOfSetTheoryTests extends ProofCheckerSuite {
val xy = u === v
val h = SchematicPredicateLabel("h", 0)
val t2 = RightSubstIff(Sequent(Set((xy \/ xy) <=> xy), Set(xy <=> in(u, pair(v, v)))), 0,
- (v === u) \/ (v === u),
- v === u,
- in(u, pair(v, v)) <=> PredicateFormula(h, Seq.empty),
- h)
+ List(((v === u) \/ (v === u), v === u)),
+ LambdaFormulaFormula(Seq(h), in(u, pair(v, v)) <=> PredicateFormula(h, Seq.empty)))
val t3 = Cut(Sequent(Set(), Set(xy <=> in(u, pair(v, v)))), 1, 2, (xy \/ xy) <=> xy)
val p0 = SCProof(IndexedSeq(t0, t1, t2, t3), IndexedSeq(() |- pairAxiom))