diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala index 85e4592822b8eeeafaddd0f8bad3d4ef9adae13f..57fee33e2167989fbe243ee11d5ed264eadb9d01 100644 --- a/lisa-examples/src/main/scala/Example.scala +++ b/lisa-examples/src/main/scala/Example.scala @@ -139,15 +139,15 @@ object Example { p.formulas.foreach(printAnnotatedFormula) } - val P = SchematicPredicateLabel("P", 1) - - val Q = PredicateFormula(SchematicPredicateLabel("Q", 0), Seq()) - val R = PredicateFormula(SchematicPredicateLabel("R", 0), Seq()) - val S = PredicateFormula(SchematicPredicateLabel("S", 0), Seq()) - val T = PredicateFormula(SchematicPredicateLabel("T", 0), Seq()) - val A = PredicateFormula(SchematicPredicateLabel("A", 0), Seq()) - val B = PredicateFormula(SchematicPredicateLabel("B", 0), Seq()) - val C = PredicateFormula(SchematicPredicateLabel("C", 0), Seq()) + val P = SchematicNPredicateLabel("P", 1) + + val Q = PredicateFormula(VariableFormulaLabel("Q"), Seq()) + val R = PredicateFormula(VariableFormulaLabel("R"), Seq()) + val S = PredicateFormula(VariableFormulaLabel("S"), Seq()) + val T = PredicateFormula(VariableFormulaLabel("T"), Seq()) + val A = PredicateFormula(VariableFormulaLabel("A"), Seq()) + val B = PredicateFormula(VariableFormulaLabel("B"), Seq()) + val C = PredicateFormula(VariableFormulaLabel("C"), Seq()) val x = VariableLabel("x") val f = ConstantFunctionLabel("f", 1) diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala index f1d01c420b8cd805aa678670f090442dabac2ed4..1faa2a2089790ded35da0cb57ae4d7a02c5e4456 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala @@ -6,17 +6,11 @@ package lisa.kernel.fol private[fol] trait CommonDefinitions { val MaxArity: Int = 1000000 - /** - * An object with arity information for tree-like structures. - */ - protected trait Arity { - val arity: Int - } - /** * An labelled node for tree-like structures. */ protected trait Label { + val arity: Int val id: String } diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala index 0a19f26084ffd3a4912fbe5964c6ba85743cb7b8..1e95ed08c63c51061732198d32ef0a8affa0688e 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaDefinitions.scala @@ -13,7 +13,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD sealed abstract class Formula extends TreeWithLabel[FormulaLabel] { def constantFunctions: Set[ConstantFunctionLabel] - def schematicFunctions: Set[SchematicFunctionLabel] + def schematicTerms: Set[SchematicTermLabel] def constantPredicates: Set[ConstantPredicateLabel] def schematicPredicates: Set[SchematicPredicateLabel] @@ -35,7 +35,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD } override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions) - override def schematicFunctions: Set[SchematicFunctionLabel] = args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions) + override def schematicTerms: Set[SchematicTermLabel] = args.foldLeft(Set.empty[SchematicTermLabel])((prev, next) => prev union next.schematicTerms) } /** @@ -45,7 +45,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD override def freeVariables: Set[VariableLabel] = args.foldLeft(Set.empty[VariableLabel])((prev, next) => prev union next.freeVariables) override def constantFunctions: Set[ConstantFunctionLabel] = args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions) - override def schematicFunctions: Set[SchematicFunctionLabel] = args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions) + override def schematicTerms: Set[SchematicTermLabel] = args.foldLeft(Set.empty[SchematicTermLabel])((prev, next) => prev union next.schematicTerms) override def constantPredicates: Set[ConstantPredicateLabel] = args.foldLeft(Set.empty[ConstantPredicateLabel])((prev, next) => prev union next.constantPredicates) override def schematicPredicates: Set[SchematicPredicateLabel] = args.foldLeft(Set.empty[SchematicPredicateLabel])((prev, next) => prev union next.schematicPredicates) @@ -58,7 +58,7 @@ private[fol] trait FormulaDefinitions extends FormulaLabelDefinitions with TermD override def freeVariables: Set[VariableLabel] = inner.freeVariables - bound override def constantFunctions: Set[ConstantFunctionLabel] = inner.constantFunctions - override def schematicFunctions: Set[SchematicFunctionLabel] = inner.schematicFunctions + override def schematicTerms: Set[SchematicTermLabel] = inner.schematicTerms - bound override def constantPredicates: Set[ConstantPredicateLabel] = inner.constantPredicates override def schematicPredicates: Set[SchematicPredicateLabel] = inner.schematicPredicates diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala index b1d14331fd7cf0c906c45f4335b8073d6b6e6cee..d3252743d03d02a7a784f8a287e4d24c0941da14 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala @@ -34,7 +34,7 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions { * The label for a predicate, namely a function taking a fixed number of terms and returning a formula. * In logical terms it is a predicate symbol. */ - sealed abstract class PredicateLabel extends FormulaLabel with Arity { + sealed abstract class PredicateLabel extends FormulaLabel { require(arity < MaxArity && arity >= 0) } @@ -51,12 +51,24 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions { /** * A predicate symbol that can be instantiated with any formula. */ - sealed case class SchematicPredicateLabel(id: String, arity: Int) extends PredicateLabel + sealed abstract class SchematicPredicateLabel extends PredicateLabel with SchematicLabel + + /** + * A predicate symbol of non-zero arity that can be instantiated with any formula taking arguments. + */ + sealed case class SchematicNPredicateLabel(id: String, arity: Int) extends SchematicPredicateLabel + + /** + * A predicate symbol of arity 0 that can be instantiated with any formula. + */ + sealed case class VariableFormulaLabel(id: String) extends SchematicPredicateLabel { + val arity = 0 + } /** * The label for a connector, namely a function taking a fixed number of formulas and returning another formula. */ - sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel with Arity { + sealed abstract class ConnectorLabel(val id: String, val arity: Int) extends FormulaLabel { require(arity < MaxArity && arity >= -1) } @@ -73,7 +85,9 @@ private[fol] trait FormulaLabelDefinitions extends CommonDefinitions { /** * The label for a binder, namely an object with a body that has the ability to bind variables in it. */ - sealed abstract class BinderLabel(val id: String) extends FormulaLabel + sealed abstract class BinderLabel(val id: String) extends FormulaLabel { + val arity = 1 + } case object Forall extends BinderLabel(id = "∀") diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala index 0f2fe1f43a5653f38f8bb02e432a771e014b3515..edc866474c905103753647a745e61d235fd6ae73 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala @@ -8,9 +8,8 @@ trait Substitutions extends FormulaDefinitions { * @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) + case class LambdaTermTerm(vars: Seq[VariableLabel], body: Term) { + def apply(args: Seq[Term]): Term = substituteVariables(body, (vars zip args).toMap) } /** @@ -19,10 +18,9 @@ trait Substitutions extends FormulaDefinitions { * @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)) + case class LambdaTermFormula(vars: Seq[VariableLabel], body: Formula) { def apply(args: Seq[Term]): Formula = { - instantiateFunctionSchemas(body, (vars zip (args map (LambdaTermTerm(Nil, _)))).toMap) + substituteVariables(body, (vars zip args).toMap) } // def instantiateFunctionSchemas(phi: Formula, m: Map[SchematicFunctionLabel, LambdaTermTerm]):Formula = ??? } @@ -33,8 +31,7 @@ trait Substitutions extends FormulaDefinitions { * @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)) + case class LambdaFormulaFormula(vars: Seq[VariableFormulaLabel], body: Formula) { def apply(args: Seq[Formula]): Formula = instantiatePredicateSchemas(body, (vars zip (args map (LambdaTermFormula(Nil, _)))).toMap) } @@ -53,47 +50,24 @@ trait Substitutions extends FormulaDefinitions { 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. + * If the arity of one of the function symbol to substitute doesn't match the corresponding number of arguments, 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. + * variable 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 = { + def instantiateTermSchemas(t: Term, m: Map[SchematicTermLabel, LambdaTermTerm]): Term = { require(m.forall { case (symbol, LambdaTermTerm(arguments, body)) => arguments.length == symbol.arity }) t match { - case VariableTerm(_) => t + case VariableTerm(label) => m.get(label).map(_.apply(Nil)).getOrElse(t) case FunctionTerm(label, args) => - val newArgs = args.map(instantiateFunctionSchemas(_, m)) + val newArgs = args.map(instantiateTermSchemas(_, 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) + m.get(label).map(_(newArgs)).getOrElse(FunctionTerm(label, newArgs)) } } } @@ -123,27 +97,26 @@ trait Substitutions extends FormulaDefinitions { } /** - * Instantiate a schematic function symbol in a formula, using higher-order instantiation. - * + * 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 doesn't match the corresponding number of arguments, it will produce an error. * @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] + * @param m The map from schematic function symbols to "terms with holes". A such term is a pair containing a list of + * variable symbols (holes) and a term that is the body of the functional term. + * @return t[m] */ - def instantiateFunctionSchemas(phi: Formula, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Formula = { + def instantiateTermSchemas(phi: Formula, m: Map[SchematicTermLabel, 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 PredicateFormula(label, args) => PredicateFormula(label, args.map(a => instantiateTermSchemas(a, m))) + case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateTermSchemas(_, m))) case BinderFormula(label, bound, inner) => - val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet + val newSubst = m - bound + val fv: Set[VariableLabel] = newSubst.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)) + BinderFormula(label, newBoundVariable, instantiateTermSchemas(newInner, newSubst)) + } else BinderFormula(label, bound, instantiateTermSchemas(inner, newSubst)) } } @@ -151,11 +124,9 @@ trait Substitutions extends FormulaDefinitions { * 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] + * @param m The map from schematic function symbols to "terms with holes". A such term is a pair containing a list of + * variable symbols (holes) and a term that is the body of the functional term. + * @return t[m] */ def instantiatePredicateSchemas(phi: Formula, m: Map[SchematicPredicateLabel, LambdaTermFormula]): Formula = { require(m.forall { case (symbol, LambdaTermFormula(arguments, body)) => arguments.length == symbol.arity }) diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala index e98ca824e4da99f615811a391b3c53556b8908a4..23359f1017e90ddbc870968ed026005ba27cd74a 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermDefinitions.scala @@ -8,10 +8,20 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions { protected trait TreeWithLabel[A] { val label: A + /** + * @return The list of free variables in the term + */ def freeVariables: Set[VariableLabel] + /** + * @return The list of constant (i.e. non schematic) function symbols, including of arity 0. + */ def constantFunctions: Set[ConstantFunctionLabel] - def schematicFunctions: Set[SchematicFunctionLabel] + + /** + * @return The list of schematic function symbols (including free variables) in the term + */ + def schematicTerms: Set[SchematicTermLabel] } /** @@ -30,7 +40,7 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions { override def freeVariables: Set[VariableLabel] = Set(label) override def constantFunctions: Set[ConstantFunctionLabel] = Set.empty - override def schematicFunctions: Set[SchematicFunctionLabel] = Set.empty + override def schematicTerms: Set[SchematicTermLabel] = Set(label) } /** @@ -48,9 +58,9 @@ private[fol] trait TermDefinitions extends TermLabelDefinitions { case l: ConstantFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions) + l case l: SchematicFunctionLabel => args.foldLeft(Set.empty[ConstantFunctionLabel])((prev, next) => prev union next.constantFunctions) } - override def schematicFunctions: Set[SchematicFunctionLabel] = label match { - case l: ConstantFunctionLabel => args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions) - case l: SchematicFunctionLabel => args.foldLeft(Set.empty[SchematicFunctionLabel])((prev, next) => prev union next.schematicFunctions) + l + override def schematicTerms: Set[SchematicTermLabel] = label match { + case l: ConstantFunctionLabel => args.foldLeft(Set.empty[SchematicTermLabel])((prev, next) => prev union next.schematicTerms) + case l: SchematicFunctionLabel => args.foldLeft(Set.empty[SchematicTermLabel])((prev, next) => prev union next.schematicTerms) + l } val arity: Int = args.size diff --git a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala index c2691946010a4332bf45db3716e58305d75aaf5b..3c2ca18d6023d055ff82e040edd23b27c3ad4bee 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala @@ -29,22 +29,13 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions { } } - /** - * The label of a term which is a variable. - * - * @param id The name of the variable, for example "x" or "y". - */ - sealed case class VariableLabel(id: String) extends TermLabel { - val name: String = id - } - /** * The label of a function-like term. Constants are functions of arity 0. * There are two kinds of function symbols: Standards and schematic. * Standard function symbols denote a particular function. Schematic function symbols * can be instantiated with any term. This is particularly useful to express axiom schemas. */ - sealed abstract class FunctionLabel extends TermLabel with Arity { + sealed abstract class FunctionLabel extends TermLabel { require(arity >= 0 && arity < MaxArity) } @@ -56,13 +47,27 @@ private[fol] trait TermLabelDefinitions extends CommonDefinitions { */ sealed case class ConstantFunctionLabel(id: String, arity: Int) extends FunctionLabel with ConstantLabel + sealed trait SchematicTermLabel extends TermLabel {} + /** * A schematic function symbol that can be substituted. * * @param id The name of the function symbol. * @param arity The arity of the function symbol. A function symbol of arity 0 is a constant */ - sealed case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel + sealed case class SchematicFunctionLabel(id: String, arity: Int) extends FunctionLabel with SchematicTermLabel { + require(arity >= 1 && arity < MaxArity) + } + + /** + * The label of a term which is a variable. + * + * @param id The name of the variable, for example "x" or "y". + */ + sealed case class VariableLabel(id: String) extends SchematicTermLabel { + val name: String = id + val arity = 0 + } /** * A function returning true if and only if the two symbols are considered "the same". diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala index ce544cf2be2997754b29dcb4de9129f8fa2b3be7..5d17880e22ae33e408c0f5d10612bd119b90638b 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/RunningTheory.scala @@ -121,7 +121,7 @@ class RunningTheory { val LambdaTermFormula(vars, body) = expression if (belongsToTheory(body)) if (isAvailable(label)) - if (body.freeVariables.isEmpty && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty) { + if (body.schematicTerms.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty) { val newDef = PredicateDefinition(label, expression) predDefinitions.update(label, Some(newDef)) knownSymbols.update(label.id, label) @@ -155,8 +155,8 @@ class RunningTheory { ): RunningTheoryJudgement[this.FunctionDefinition] = { val LambdaTermFormula(vars, body) = expression if (belongsToTheory(body)) - if (isAvailable(label)) - if (body.freeVariables.subsetOf(Set(out)) && body.schematicFunctions.subsetOf(vars.toSet) && body.schematicPredicates.isEmpty) + if (isAvailable(label)) { + if (body.schematicTerms.subsetOf((vars appended out).toSet) && body.schematicPredicates.isEmpty) if (proof.imports.forall(i => justifications.exists(j => isSameSequent(i, sequentFromJustification(j))))) { val r = SCProofChecker.checkSCProof(proof) r match { @@ -176,7 +176,7 @@ class RunningTheory { } } else InvalidJustification("Not all imports of the proof are correctly justified.", None) else InvalidJustification("The definition is not allowed to contain schematic symbols or free variables.", None) - else InvalidJustification("The specified symbol id is already part of the theory and can't be redefined.", None) + } else InvalidJustification("The specified symbol id is already part of the theory and can't be redefined.", None) else InvalidJustification("All symbols in the conclusion of the proof must belong to the theory. You need to add missing symbols to the theory.", None) } @@ -184,7 +184,7 @@ class RunningTheory { case Theorem(name, proposition) => proposition case Axiom(name, ax) => Sequent(Set.empty, Set(ax)) case PredicateDefinition(label, LambdaTermFormula(vars, body)) => - val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, vars.map(FunctionTerm(_, Seq()))), body)) + val inner = ConnectorFormula(Iff, Seq(PredicateFormula(label, vars.map(VariableTerm)), body)) Sequent(Set(), Set(inner)) case FunctionDefinition(label, out, LambdaTermFormula(vars, body)) => val inner = BinderFormula( @@ -193,7 +193,7 @@ class RunningTheory { ConnectorFormula( Iff, Seq( - PredicateFormula(equality, Seq(FunctionTerm(label, vars.map(FunctionTerm.apply(_, Seq()))), VariableTerm(out))), + PredicateFormula(equality, Seq(FunctionTerm(label, vars.map(VariableTerm)), VariableTerm(out))), body ) ) diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala index 0892ef5d274a3587c375b33d9ab84dcb5d2920f5..de5b860c061a596c3a751138713dc2218f60fd96 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProof.scala @@ -1,6 +1,5 @@ package lisa.kernel.proof -import lisa.kernel.proof.SCProofChecker._ import lisa.kernel.proof.SequentCalculus._ /** diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala index a2ff683d4f1c4f57cd93165f41e70aba858dce60..b11218c3c4952f4a8c5ad968090ca6bff99d6c60 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala @@ -438,7 +438,7 @@ object SCProofChecker { * </pre> */ case InstFunSchema(bot, t1, insts) => - val expected = (ref(t1).left.map(phi => instantiateFunctionSchemas(phi, insts)), ref(t1).right.map(phi => instantiateFunctionSchemas(phi, insts))) + val expected = (ref(t1).left.map(phi => instantiateTermSchemas(phi, insts)), ref(t1).right.map(phi => instantiateTermSchemas(phi, insts))) if (isSameSet(bot.left, expected._1)) if (isSameSet(bot.right, expected._2)) SCValidProof(SCProof(step)) diff --git a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala index 15d677b98d8f62a67d696fa03f0ea7d9e861ee3b..75c34935b10dd1b2c741f74cadd43d4111ac2839 100644 --- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala +++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala @@ -2,8 +2,6 @@ package lisa.kernel.proof import lisa.kernel.fol.FOL._ -import scala.collection.immutable.Set - /** * The concrete implementation of sequent calculus (with equality). * This file specifies the sequents and the allowed operations on them, the deduction rules of sequent calculus. @@ -301,7 +299,7 @@ object SequentCalculus { * Γ[r(a)/?f] |- Δ[r(a)/?f] * </pre> */ - case class InstFunSchema(bot: Sequent, t1: Int, insts: Map[SchematicFunctionLabel, LambdaTermTerm]) extends SCProofStep { val premises = Seq(t1) } + case class InstFunSchema(bot: Sequent, t1: Int, insts: Map[SchematicTermLabel, LambdaTermTerm]) extends SCProofStep { val premises = Seq(t1) } /** * <pre> diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala index f38aa7b1edd8ee07cd64b0cbb1ce565097bbe8d8..ecf2c80c013309ee549d9291eff2374abfa82b4c 100644 --- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala +++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZAxioms.scala @@ -11,7 +11,7 @@ private[settheory] trait SetTheoryZAxioms extends SetTheoryDefinitions { private val (x, y, z) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("z")) - private final val sPhi = SchematicPredicateLabel("P", 2) + private final val sPhi = SchematicNPredicateLabel("P", 2) final val emptySetAxiom: Formula = forall(x, !in(x, emptySet())) final val extensionalityAxiom: Formula = forall(x, forall(y, forall(z, in(z, x) <=> in(z, y)) <=> (x === y))) diff --git a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala index bd95ad4551a1c40f9cf94799a63cba71e1a93a06..e075fabbb9f5fe687ef71cfe859c1c8b5691a51c 100644 --- a/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala +++ b/lisa-theories/src/main/scala/lisa/settheory/SetTheoryZFAxioms.scala @@ -9,7 +9,7 @@ import lisa.utils.Helpers.{_, given} private[settheory] trait SetTheoryZFAxioms extends SetTheoryZAxioms { private val (x, y, a, b) = (VariableLabel("x"), VariableLabel("y"), VariableLabel("A"), VariableLabel("B")) - private final val sPsi = SchematicPredicateLabel("P", 3) + private final val sPsi = SchematicNPredicateLabel("P", 3) final val replacementSchema: Formula = forall( a, diff --git a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala index e372a02e2bba7521a30d19f3ed6117872053289c..a5bb1b41c8fbd8d8f62b8b7718fce150e5df30ec 100644 --- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala +++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala @@ -89,8 +89,10 @@ trait KernelHelpers { given Conversion[VariableLabel, VariableTerm] = VariableTerm.apply given Conversion[VariableTerm, VariableLabel] = _.label given Conversion[PredicateFormula, PredicateLabel] = _.label + given Conversion[PredicateLabel, Formula] = _.apply() given Conversion[FunctionTerm, FunctionLabel] = _.label given Conversion[SchematicFunctionLabel, Term] = _.apply() + given Conversion[VariableFormulaLabel, PredicateFormula] = PredicateFormula.apply(_, Nil) given Conversion[(Boolean, List[Int], String), Option[(List[Int], String)]] = tr => if (tr._1) None else Some(tr._2, tr._3) given Conversion[Formula, Sequent] = () |- _ @@ -147,8 +149,8 @@ trait KernelHelpers { 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, m: Map[SchematicFunctionLabel, LambdaTermTerm]): Sequent = { - s.left.map(phi => instantiateFunctionSchemas(phi, m)) |- s.right.map(phi => instantiateFunctionSchemas(phi, m)) + def instantiateFunctionSchemaInSequent(s: Sequent, m: Map[SchematicTermLabel, LambdaTermTerm]): Sequent = { + s.left.map(phi => instantiateTermSchemas(phi, m)) |- s.right.map(phi => instantiateTermSchemas(phi, m)) } } diff --git a/lisa-utils/src/main/scala/lisa/utils/Library.scala b/lisa-utils/src/main/scala/lisa/utils/Library.scala index 3863a9b618b41fe93f533bd7954a51312aa8a8cb..1cc2db84bce30730c8ac9a0ae85b7bebbd436cde 100644 --- a/lisa-utils/src/main/scala/lisa/utils/Library.scala +++ b/lisa-utils/src/main/scala/lisa/utils/Library.scala @@ -53,12 +53,12 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre> */ - def PROOF(proof: Proof)(using String => Unit): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof) + def PROOF(proof: Proof)(using String => Unit)(using Throwable => Nothing): TheoremNameWithProof = TheoremNameWithProof(name, statement, proof) /** * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre> */ - def PROOF(steps: IndexedSeq[SCProofStep])(using String => Unit): TheoremNameWithProof = TheoremNameWithProof(name, statement, Proof(steps)) + def PROOF(steps: IndexedSeq[SCProofStep])(using String => Unit)(using Throwable => Nothing): TheoremNameWithProof = TheoremNameWithProof(name, statement, Proof(steps)) } /** @@ -80,7 +80,7 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> THEOREM("name") of "the sequent concluding the proof" PROOF { the proof } using (assumptions) </pre> */ - case class TheoremNameWithProof(name: String, statement: String, proof: Proof)(using String => Unit) { + case class TheoremNameWithProof(name: String, statement: String, proof: Proof)(using String => Unit)(using Throwable => Nothing) { infix def using(justifications: theory.Justification*): theory.Theorem = theory.theorem(name, statement, proof, justifications) match { case Judgement.ValidJustification(just) => last = Some(just) @@ -101,7 +101,7 @@ abstract class Library(val theory: RunningTheory) { */ def simpleDefinition(symbol: String, expression: LambdaTermTerm): Judgement[theory.FunctionDefinition] = { val LambdaTermTerm(vars, body) = expression - val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicFunctions.map(_.id)).toSet, "y")) + val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ body.schematicTerms.map(_.id)).toSet, "y")) val proof: Proof = simpleFunctionDefinition(expression, out) theory.functionDefinition(symbol, LambdaTermFormula(vars, out === body), out, proof, Nil) } @@ -109,9 +109,9 @@ abstract class Library(val theory: RunningTheory) { /** * Allows to create a definition by existential uniqueness of a function symbol: */ - def complexDefinition(symbol: String, vars: Seq[SchematicFunctionLabel], v: SchematicFunctionLabel, f: Formula, proof: Proof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] = { - val out: VariableLabel = VariableLabel(freshId((vars.map(_.id) ++ f.schematicFunctions.map(_.id)).toSet, "y")) - theory.functionDefinition(symbol, LambdaTermFormula(vars, instantiateFunctionSchemas(f, Map(v -> LambdaTermTerm(Nil, out)))), out, proof, just) + def complexDefinition(symbol: String, vars: Seq[VariableLabel], v: VariableLabel, f: Formula, proof: Proof, just: Seq[Justification]): Judgement[theory.FunctionDefinition] = { + theory.functionDefinition(symbol, LambdaTermFormula(vars, f), v, proof, just) + // theory.functionDefinition(symbol, LambdaTermFormula(vars, instantiateTermSchemas(f, Map(v -> LambdaTermTerm(Nil, out)))), out, proof, just) } /** @@ -125,12 +125,12 @@ abstract class Library(val theory: RunningTheory) { * or * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - case class FunSymbolDefine(symbol: String, vars: Seq[SchematicFunctionLabel]) { + case class FunSymbolDefine(symbol: String, vars: Seq[VariableLabel]) { /** * Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre> */ - infix def as(t: Term)(using String => Unit): ConstantFunctionLabel = { + infix def as(t: Term)(using String => Unit)(using Throwable => Nothing): ConstantFunctionLabel = { val definition = simpleDefinition(symbol, LambdaTermTerm(vars, t)) match { case Judgement.ValidJustification(just) => last = Some(just) @@ -143,7 +143,7 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> DEFINE("symbol", arguments) as "definition" </pre> */ - infix def as(f: Formula)(using String => Unit): ConstantPredicateLabel = { + infix def as(f: Formula)(using String => Unit)(using Throwable => Nothing): ConstantPredicateLabel = { val definition = simpleDefinition(symbol, LambdaTermFormula(vars, f)) match { case Judgement.ValidJustification(just) => last = Some(just) @@ -156,13 +156,13 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - infix def asThe(out: SchematicFunctionLabel): DefinitionNameAndOut = DefinitionNameAndOut(symbol, vars, out) + infix def asThe(out: VariableLabel): DefinitionNameAndOut = DefinitionNameAndOut(symbol, vars, out) } /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - case class DefinitionNameAndOut(symbol: String, vars: Seq[SchematicFunctionLabel], out: SchematicFunctionLabel) { + case class DefinitionNameAndOut(symbol: String, vars: Seq[VariableLabel], out: VariableLabel) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> @@ -173,7 +173,7 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - case class DefinitionWaitingProof(symbol: String, vars: Seq[SchematicFunctionLabel], out: SchematicFunctionLabel, f: Formula) { + case class DefinitionWaitingProof(symbol: String, vars: Seq[VariableLabel], out: VariableLabel, f: Formula) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> @@ -184,12 +184,12 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - case class DefinitionWithProof(symbol: String, vars: Seq[SchematicFunctionLabel], out: SchematicFunctionLabel, f: Formula, proof: Proof) { + case class DefinitionWithProof(symbol: String, vars: Seq[VariableLabel], out: VariableLabel, f: Formula, proof: Proof) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - infix def using(justifications: theory.Justification*)(using String => Unit): ConstantFunctionLabel = { + infix def using(justifications: theory.Justification*)(using String => Unit)(using Throwable => Nothing): ConstantFunctionLabel = { val definition = complexDefinition(symbol, vars, out, f, proof, justifications) match { case Judgement.ValidJustification(just) => last = Some(just) @@ -202,13 +202,13 @@ abstract class Library(val theory: RunningTheory) { /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - infix def using(u: Unit)(using String => Unit): ConstantFunctionLabel = using() + infix def using(u: Unit)(using String => Unit)(using Throwable => Nothing): ConstantFunctionLabel = using() } /** * Syntax: <pre> DEFINE("symbol", arguments) asThe x suchThat P(x) PROOF { the proof } using (assumptions) </pre> */ - def DEFINE(symbol: String, vars: SchematicFunctionLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars) + def DEFINE(symbol: String, vars: VariableLabel*): FunSymbolDefine = FunSymbolDefine(symbol, vars) /** * For a definition of the type f(x) := term, construct the required proof ∃!y. y = term. diff --git a/lisa-utils/src/main/scala/lisa/utils/Printer.scala b/lisa-utils/src/main/scala/lisa/utils/Printer.scala index c19f126692a699e4a15b9b2250f2acf8f61f2ec5..f6e3c2593971d417b299db9c7f33b09c25894c81 100644 --- a/lisa-utils/src/main/scala/lisa/utils/Printer.scala +++ b/lisa-utils/src/main/scala/lisa/utils/Printer.scala @@ -67,7 +67,7 @@ object Printer { case _ => val labelString = label match { case ConstantPredicateLabel(id, _) => id - case SchematicPredicateLabel(id, _) => s"?$id" + case s: SchematicPredicateLabel => s"?${s.id}" } prettyFunction(labelString, args.map(prettyTerm(_, compact)), compact) } @@ -150,7 +150,7 @@ object Printer { * @return the string representation of this term */ def prettyTerm(term: Term, compact: Boolean = false): String = term match { - case VariableTerm(label) => label.id + case VariableTerm(label) => s"?${label.id}" case FunctionTerm(label, args) => label match { case `emptySet` => diff --git a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala index 58678892f711194ad40db6cf2c2723b13feeef8e..384aff2acbcaa5a8c6c0bec3f00fb1becb3158cc 100644 --- a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala +++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala @@ -2,6 +2,7 @@ package lisa.utils import lisa.kernel.fol.FOL.* import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification +import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustificationException import lisa.kernel.proof.SequentCalculus.* import lisa.kernel.proof.* import lisa.utils.Printer @@ -75,13 +76,11 @@ trait TheoriesHelpers extends KernelHelpers { case d: RunningTheory#Definition => d match { case pd: RunningTheory#PredicateDefinition => - output(s" Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.expression.vars.map(_())*) <=> pd.expression.body)}\n") // (label, args, phi) + output(s" Definition of predicate symbol ${pd.label.id} := ${Printer.prettyFormula(pd.label(pd.expression.vars.map(VariableTerm)*) <=> pd.expression.body)}\n") // (label, args, phi) case fd: RunningTheory#FunctionDefinition => - output(s" Definition of function symbol ${Printer.prettyTerm(fd.label(fd.expression.vars.map(_())*))} := the ${fd.out.id} such that ${Printer - .prettyFormula((fd.out === fd.label(fd.expression.vars.map(_())*)) <=> fd.expression.body)})\n") + output(s" Definition of function symbol ${Printer.prettyTerm(fd.label(fd.expression.vars.map(VariableTerm)*))} := the ${fd.out.id} such that ${Printer + .prettyFormula((fd.out === fd.label(fd.expression.vars.map(VariableTerm)*)) <=> fd.expression.body)})\n") } - // output(Printer.prettySequent(thm.proposition)) - // thm } just } @@ -93,7 +92,7 @@ trait TheoriesHelpers extends KernelHelpers { * If the Judgement is valid, show the inner justification and returns it. * Otherwise, output the error leading to the invalid justification and throw an error. */ - def showAndGet(using output: String => Unit): J = { + def showAndGet(using output: String => Unit)(using finishOutput: Throwable => Nothing): J = { theoryJudgement match { case RunningTheoryJudgement.ValidJustification(just) => just.show @@ -102,7 +101,7 @@ trait TheoriesHelpers extends KernelHelpers { case Some(judgement) => Printer.prettySCProof(judgement) case None => "" }}") - theoryJudgement.get + finishOutput(InvalidJustificationException(message, error)) } } } diff --git a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala index f39b1bd20c597fa984f8552ff98e24c49b3ab53c..19c8e6702ec9ab648b59e3af2b0028c916924302 100644 --- a/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala +++ b/lisa-utils/src/test/scala/lisa/kernel/FolTests.scala @@ -101,7 +101,7 @@ class FolTests extends AnyFunSuite { private val a = PredicateFormula(ConstantPredicateLabel("A", 0), Seq()) private val b = PredicateFormula(ConstantPredicateLabel("B", 0), Seq()) private val fp = ConstantPredicateLabel("F", 1) - private val sT = SchematicFunctionLabel("t", 0) + private val sT = VariableLabel("t") def test_some_random_formulas(n: Int, maxDepth: Int): Unit = { (0 to n).foreach(_ => println(formulaGenerator(maxDepth))) diff --git a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala index 786e63add0d36d6b10cd5b3fc4a7ac8876ab0600..d01a59f3518b52ed028bab03f8b506d92241e444 100644 --- a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala +++ b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala @@ -17,7 +17,7 @@ class IncorrectProofsTests extends ProofCheckerSuite { // Shorthand implicit def proofStepToProof(proofStep: SCProofStep): SCProof = SCProof(proofStep) - val (fl, gl, hl) = (SchematicPredicateLabel("f", 0), SchematicPredicateLabel("g", 0), SchematicPredicateLabel("h", 0)) + val (fl, gl, hl) = (VariableFormulaLabel("f"), VariableFormulaLabel("g"), VariableFormulaLabel("h")) val f = PredicateFormula(fl, Seq.empty) // Some arbitrary formulas val g = PredicateFormula(gl, Seq.empty) val h = PredicateFormula(hl, Seq.empty) diff --git a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala index 53fa5f17b0109acd7a48727b477825413a41be94..d00afd8968387ea163b9a40397d7d9cc756d3a96 100644 --- a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala +++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala @@ -22,7 +22,7 @@ class ProofTests extends AnyFunSuite { private val a = PredicateFormula(ConstantPredicateLabel("A", 0), Seq()) private val b = PredicateFormula(ConstantPredicateLabel("B", 0), Seq()) private val fp = ConstantPredicateLabel("F", 1) - val sT = SchematicFunctionLabel("t", 0) + val sT = VariableLabel("t") test("Verification of Pierce law") { val s0 = Hypothesis(a |- a, a) @@ -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, List((x, y)), LambdaTermFormula(Seq(sT), fp(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/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala index 6765e70a02d2699b790d3a93fe6c2b0ee15794ed..6c3d6c4fe04861db76bbaee5963bdf54a716e503 100644 --- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala +++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala @@ -11,27 +11,28 @@ import org.scalatest.funsuite.AnyFunSuite import scala.language.adhocExtensions abstract class ProofCheckerSuite extends AnyFunSuite { + import lisa.kernel.fol.FOL.* protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = ( - SchematicFunctionLabel("x", 0), - SchematicFunctionLabel("y", 0), - SchematicFunctionLabel("z", 0), - SchematicFunctionLabel("w", 0), - SchematicFunctionLabel("x'", 0), - SchematicFunctionLabel("y'", 0), - SchematicFunctionLabel("z'", 0), - SchematicFunctionLabel("w'", 0) + VariableLabel("x"), + VariableLabel("y"), + VariableLabel("z"), + VariableLabel("w"), + VariableLabel("x'"), + VariableLabel("y'"), + VariableLabel("z'"), + VariableLabel("w'") ) protected val (x, y, z, w, xp, yp, zp, wp) = ( - FunctionTerm(xl, Seq.empty), - FunctionTerm(yl, Seq.empty), - FunctionTerm(zl, Seq.empty), - FunctionTerm(wl, Seq.empty), - FunctionTerm(xpl, Seq.empty), - FunctionTerm(ypl, Seq.empty), - FunctionTerm(zpl, Seq.empty), - FunctionTerm(wpl, Seq.empty) + VariableTerm(xl), + VariableTerm(yl), + VariableTerm(zl), + VariableTerm(wl), + VariableTerm(xpl), + VariableTerm(ypl), + VariableTerm(zpl), + VariableTerm(wpl) ) protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v")) diff --git a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala index d19514fbf8b4e353f501fb0108050025a1c32f6f..33f62829dfcd6905417bc6592845310c925ff59f 100644 --- a/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala +++ b/lisa-utils/src/test/scala/lisa/utils/PrinterTest.scala @@ -28,17 +28,17 @@ class PrinterTest extends AnyFunSuite { assert(prettyFormula(ConnectorFormula(Neg, Seq(ConnectorFormula(Neg, Seq(ConnectorFormula(And, Seq(a, b))))))) == "¬¬(a ∧ b)") assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(a)), ConnectorFormula(And, Seq(ConnectorFormula(Neg, Seq(b)), ConnectorFormula(Neg, Seq(c))))))) == "¬a ∧ ¬b ∧ ¬c") - assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (x = x)") + assert(prettyFormula(ConnectorFormula(And, Seq(a, PredicateFormula(equality, Seq(x, x))))) == "a ∧ (?x = ?x)") - assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. x = x") - assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. x = x") + assert(prettyFormula(BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))) == "∀x. ?x = ?x") + assert(prettyFormula(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, PredicateFormula(equality, Seq(x, x)))))) == "a ∧ ∀x. ?x = ?x") assert(prettyFormula(ConnectorFormula(And, Seq(BinderFormula(Forall, x, b), a))) == "(∀x. b) ∧ a") assert(prettyFormula(ConnectorFormula(And, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "(a ∧ ∀x. b) ∧ a") assert(prettyFormula(ConnectorFormula(Or, Seq(ConnectorFormula(And, Seq(a, BinderFormula(Forall, x, b))), a))) == "a ∧ (∀x. b) ∨ a") assert(prettyFormula(BinderFormula(Forall, x, BinderFormula(Exists, y, BinderFormula(ExistsOne, z, a)))) == "∀x. ∃y. ∃!z. a") - assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(x, y, z)") + assert(prettyFormula(PredicateFormula(ConstantPredicateLabel("f", 2), Seq(x, y, z))) == "f(?x, ?y, ?z)") } } diff --git a/src/main/scala/lisa/proven/Main.scala b/src/main/scala/lisa/proven/Main.scala index e69a7102df8c926c334659937f63d76a2305b515..bf01e93e0444e24ae0943b88255ee9607788c585 100644 --- a/src/main/scala/lisa/proven/Main.scala +++ b/src/main/scala/lisa/proven/Main.scala @@ -10,6 +10,10 @@ trait Main { private var outString: List[String] = List() private val lineBreak = "\n" given output: (String => Unit) = s => outString = lineBreak :: s :: outString + given finishOutput: (Throwable => Nothing) = e => { + main(Array[String]()) + throw e + } /** * This specific implementation make sure that what is "shown" in theory files is only printed for the one we run, and not for the whole library. diff --git a/src/main/scala/lisa/proven/mathematics/Mapping.scala b/src/main/scala/lisa/proven/mathematics/Mapping.scala index 7267e0c7add9ce057eb8b98795a68f11441bfd05..ae17e07702ee3e63f20eb9ad29d6fcb8bfea63e1 100644 --- a/src/main/scala/lisa/proven/mathematics/Mapping.scala +++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala @@ -14,24 +14,18 @@ object Mapping extends lisa.proven.Main { THEOREM("functionalMapping") of "∀a. (a ∈ ?A) ⇒ ∃!x. ?phi(x, a) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ ?A) ∧ ?phi(x, a)" PROOF { val a = VariableLabel("a") - val b = VariableLabel("b") 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 f = SchematicFunctionLabel("f", 0) - val h = SchematicPredicateLabel("h", 0) - val A = SchematicFunctionLabel("A", 0)() + val f = VariableLabel("f") + val h = VariableFormulaLabel("h") + val A = VariableLabel("A") val X = VariableLabel("X") val B = VariableLabel("B") val B1 = VariableLabel("B1") - val phi = SchematicPredicateLabel("phi", 2) - val sPhi = SchematicPredicateLabel("P", 2) - val sPsi = SchematicPredicateLabel("P", 3) + val phi = SchematicNPredicateLabel("phi", 2) + val sPhi = SchematicNPredicateLabel("P", 2) + val sPsi = SchematicNPredicateLabel("P", 3) val H = existsOne(x, phi(x, a)) val H1 = forall(a, in(a, A) ==> H) @@ -42,9 +36,9 @@ object Mapping extends lisa.proven.Main { val s3 = hypothesis(H1) val i1 = () |- replacementSchema val p0 = InstPredSchema( - () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1)))), + () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y, a, x), phi(x, a)))), -1, - Map(sPsi -> LambdaTermFormula(Seq(y1, a1, x1), phi(x1, a1))) + Map(sPsi -> LambdaTermFormula(Seq(y, a, x), phi(x, a))) ) val p1 = instantiateForall(Proof(steps(p0), imports(i1)), A) val s4 = SCSubproof(p1, Seq(-1)) // @@ -53,20 +47,19 @@ object Mapping extends lisa.proven.Main { val i2 = () |- comprehensionSchema // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,z) /\ sPhi(x,z))))) val q0 = InstPredSchema( - () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a))))), + () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x, z), exists(a, in(a, A) /\ phi(x, a))))), -1, - Map(sPhi -> LambdaTermFormula(Seq(x1, z1), exists(a, in(a, A) /\ phi(x1, a)))) + Map(sPhi -> LambdaTermFormula(Seq(x, z), exists(a, in(a, A) /\ phi(x, a)))) ) val q1 = instantiateForall(Proof(steps(q0), imports(i2)), B) val s7 = SCSubproof(q1, Seq(-2)) // ∃y. ∀x. (x ∈ y) ↔ (x ∈ B) ∧ ∃a. a ∈ A /\ x = (a, b) := exists(y, F(y) ) Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7), imports(i1, i2)) val s8 = SCSubproof({ val y1 = VariableLabel("y1") - val f = SchematicFunctionLabel("f", 0) val s0 = hypothesis(in(y1, B)) - val s1 = RightSubstEq((in(y1, B), x === y1) |- in(x, B), 0, List((x, y1)), LambdaTermFormula(Seq(f), in(f(), B))) + 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 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) @@ -200,7 +193,7 @@ object Mapping extends lisa.proven.Main { 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)))) + 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)))), @@ -249,25 +242,19 @@ object Mapping extends lisa.proven.Main { 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 f = SchematicFunctionLabel("f", 0) - val h = SchematicPredicateLabel("h", 0) - val A = SchematicFunctionLabel("A", 0)() + val f = VariableLabel("f") + val h = VariableFormulaLabel("h") + val A = VariableLabel("A") val X = VariableLabel("X") - val B = SchematicFunctionLabel("B", 0)() + val B = VariableLabel("B") val B1 = VariableLabel("B1") - val phi = SchematicPredicateLabel("phi", 2) - val psi = SchematicPredicateLabel("psi", 3) + val phi = SchematicNPredicateLabel("phi", 2) + val psi = SchematicNPredicateLabel("psi", 3) val H = existsOne(x, phi(x, a)) val H1 = forall(a, in(a, A) ==> H) val i1 = thm"functionalMapping" - 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 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, List((in(b, B), And())), LambdaFormulaFormula(Seq(h), h() ==> H2)) @@ -280,9 +267,9 @@ object Mapping extends lisa.proven.Main { 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))), + forall(b, in(b, B) ==> existsOne(X, phi(X, b))) |- instantiateTermSchemas(i1.right.head, Map(A -> LambdaTermTerm(Nil, B))), -1, - Map(SchematicFunctionLabel("A", 0) -> LambdaTermTerm(Nil, B)) + Map(A -> 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( @@ -290,7 +277,7 @@ object Mapping extends lisa.proven.Main { 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_))))) + 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)))))), @@ -318,14 +305,14 @@ object Mapping extends lisa.proven.Main { val z = VariableLabel("z") val z1 = VariableLabel("z1") val F = SchematicFunctionLabel("F", 1) - val f = SchematicFunctionLabel("f", 0) - val phi = SchematicPredicateLabel("phi", 1) - val g = SchematicPredicateLabel("g", 0) + val f = VariableLabel("f") + val phi = SchematicNPredicateLabel("phi", 1) + val g = VariableFormulaLabel("g") val g2 = SCSubproof({ val s0 = hypothesis(F(x1) === z) - 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 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) @@ -366,39 +353,38 @@ object Mapping extends lisa.proven.Main { val b = VariableLabel("b") val x = VariableLabel("x") val x1 = VariableLabel("x1") - val x_ = SchematicFunctionLabel("x", 0) - val y_ = SchematicFunctionLabel("y", 0) + val y = VariableLabel("y") val F = SchematicFunctionLabel("F", 1) - val A = SchematicFunctionLabel("A", 0)() - val B = SchematicFunctionLabel("B", 0)() - val phi = SchematicPredicateLabel("phi", 1) - val psi = SchematicPredicateLabel("psi", 3) + val A = VariableLabel("A") + val B = VariableLabel("B") + val phi = SchematicNPredicateLabel("phi", 1) + val psi = SchematicNPredicateLabel("psi", 3) val i1 = thm"lemmaLayeredTwoArgumentsMap" val i2 = thm"applyFunctionToUniqueObject" - 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 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) Proof(steps(s0, s1, s2), imports(i1, i2)) } using (thm"lemmaLayeredTwoArgumentsMap", thm"applyFunctionToUniqueObject") show - val A = SchematicFunctionLabel("A", 0) - val B = SchematicFunctionLabel("B", 0) - private val sz = SchematicFunctionLabel("z", 0) + val A = VariableLabel("A") + val B = VariableLabel("B") + private val z = VariableLabel("z") val cartesianProduct: ConstantFunctionLabel = - DEFINE("cartProd", A, B) asThe sz suchThat { + DEFINE("cartProd", A, B) asThe z suchThat { val a = VariableLabel("a") val b = VariableLabel("b") val x = VariableLabel("x") val x0 = VariableLabel("x0") val x1 = VariableLabel("x1") - val A = SchematicFunctionLabel("A", 0)() - val B = SchematicFunctionLabel("B", 0)() - exists(x, (sz === union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b))))))) + val A = VariableLabel("A") + val B = VariableLabel("B") + exists(x, (z === union(x)) /\ forall(x0, in(x0, x) <=> exists(b, in(b, B) /\ forall(x1, in(x1, x0) <=> exists(a, in(a, A) /\ (x1 === oPair(a, b))))))) } PROOF { def makeFunctional(t: Term): Proof = { val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x")) @@ -414,16 +400,9 @@ object Mapping extends lisa.proven.Main { 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)() - val X = VariableLabel("X") - val B = SchematicFunctionLabel("B", 0)() - val phi = SchematicPredicateLabel("phi", 1) - val psi = SchematicPredicateLabel("psi", 3) + val A = VariableLabel("A") + val B = VariableLabel("B") + val psi = SchematicNPredicateLabel("psi", 3) val i1 = thm"mapTwoArguments" // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!z. ∃x. (z = U(x)) ∧ ∀x_0. (x_0 ∈ x) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x_0) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b) @@ -438,9 +417,9 @@ object Mapping extends lisa.proven.Main { }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b) val s1 = InstPredSchema( - instantiatePredicateSchemaInSequent(i1, Map(psi -> LambdaTermFormula(Seq(x_, a_, b_), x_ === oPair(a_, b_)))), + 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_))) + Map(psi -> LambdaTermFormula(Seq(x, a, b), x === oPair(a, b))) ) val s2 = Cut(() |- s1.bot.right, 0, 1, s1.bot.left.head) Proof(steps(s0, s1, s2), imports(i1)) diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala index 22822eb716ee39a060abd33cc3a0992ff657d4d4..353443915428af8a159d73d6a8f7dbc96b346ae4 100644 --- a/src/main/scala/lisa/proven/mathematics/SetTheory.scala +++ b/src/main/scala/lisa/proven/mathematics/SetTheory.scala @@ -9,12 +9,12 @@ import lisa.proven.tactics.ProofTactics.* object SetTheory extends lisa.proven.Main { THEOREM("russelParadox") of "∀x. (x ∈ ?y) ↔ ¬(x ∈ x) ⊢" PROOF { - val y = SchematicFunctionLabel("y", 0) - val x_ = VariableLabel("x") + val y = VariableLabel("y") + val x = VariableLabel("x") val contra = in(y, y) <=> !in(y, y) val s0 = Hypothesis(contra |- contra, contra) - val s1 = LeftForall(forall(x_, in(x_, y) <=> !in(x_, x_)) |- contra, 0, in(x_, y) <=> !in(x_, x_), x_, y) - val s2 = Rewrite(forall(x_, in(x_, y) <=> !in(x_, x_)) |- (), 1) + val s1 = LeftForall(forall(x, in(x, y) <=> !in(x, x)) |- contra, 0, in(x, y) <=> !in(x, x), x, y) + val s2 = Rewrite(forall(x, in(x, y) <=> !in(x, x)) |- (), 1) Proof(s0, s1, s2) } using () thm"russelParadox".show @@ -24,7 +24,7 @@ object SetTheory extends lisa.proven.Main { val x = VariableLabel("x") val y = VariableLabel("y") val z = VariableLabel("z") - val h = SchematicPredicateLabel("h", 0) + val h = VariableFormulaLabel("h") val fin = SCSubproof( { val pr0 = SCSubproof( @@ -47,7 +47,7 @@ object SetTheory extends lisa.proven.Main { Sequent(pr1.bot.right, Set(in(z, pair(x, y)) <=> in(z, pair(y, x)))), 0, List(((x === z) \/ (y === z), in(z, pair(y, x)))), - LambdaFormulaFormula(Seq(h), in(z, pair(x, y)) <=> h()) + 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 = RightForall(Sequent(Set(), Set(forall(z, pr2.bot.right.head))), 3, pr2.bot.right.head, z) @@ -80,8 +80,8 @@ object SetTheory extends lisa.proven.Main { val x1 = VariableLabel("x'") val y1 = VariableLabel("y'") val z = VariableLabel("z") - val g = SchematicFunctionLabel("g", 0) - val h = SchematicPredicateLabel("h", 0) + val g = VariableLabel("g") + val h = VariableFormulaLabel("h") val pxy = pair(x, y) val pxy1 = pair(x1, y1) val p0 = SCSubproof( @@ -92,7 +92,7 @@ object SetTheory extends lisa.proven.Main { 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, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g()))) + val p1_3 = RightSubstEq(emptySeq +< (pxy === pxy1) +> (zf <=> in(z, pxy1)), 2, List((pxy, pxy1)), LambdaTermFormula(Seq(g), zf <=> in(z, g))) Proof(IndexedSeq(p1_0, p1_1, p1_2, p1_3), IndexedSeq(() |- pairAxiom)) }, Seq(-1), @@ -119,13 +119,13 @@ object SetTheory extends lisa.proven.Main { emptySeq +< (pxy === pxy1) +> (in(z, pxy1) <=> ((z === x) \/ (z === y))), 1, List((pxy, pxy1)), - LambdaTermFormula(Seq(g), in(z, g()) <=> ((z === x) \/ (z === y))) + 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, List(((z === x1) \/ (z === y1), in(z, pxy1))), - LambdaFormulaFormula(Seq(h), h() <=> ((z === x) \/ (z === y))) + 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) Proof(IndexedSeq(p0, p1, p2, p3, p4, p5), IndexedSeq(() |- pairAxiom)) @@ -166,13 +166,13 @@ object SetTheory extends lisa.proven.Main { 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))) + 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))) + 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'))) @@ -191,7 +191,7 @@ object SetTheory extends lisa.proven.Main { 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, List((x, y)), LambdaTermFormula(Seq(g), y1 === g())) + val pal = RightSubstEq(emptySeq ++< pa0.bot +> (y1 === y), ra3.length - 1, List((x, y)), LambdaTermFormula(Seq(g), y1 === g)) Proof(ra3.steps, IndexedSeq(pam1.bot)).appended(pal) // (x=y), ({x,y}={x',y'}) |- (y'=y) }, IndexedSeq(-1) @@ -217,7 +217,7 @@ object SetTheory extends lisa.proven.Main { ) // |- (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, List((x, x1)), LambdaTermFormula(Seq(g), (y === g()) \/ (y === y1))) + 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, @@ -237,7 +237,7 @@ object SetTheory extends lisa.proven.Main { 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, List((x, x1)), LambdaTermFormula(Seq(g), (y1 === y) /\ (g() === x))) // ({x,y}={x',y'}), x=x' |- (x=x' /\ y=y') + 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, @@ -275,7 +275,7 @@ object SetTheory extends lisa.proven.Main { pd0_1.bot.right |- ((x1 === x) \/ (x1 === y)), 0, List(((x1 === x) \/ (x1 === y), (x1 === x1) \/ (x1 === y1))), - LambdaFormulaFormula(Seq(h), h()) + 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(Proof(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' @@ -330,40 +330,38 @@ object SetTheory extends lisa.proven.Main { thm"unorderedPair_deconstruction".show THEOREM("noUniversalSet") of "∀x. x ∈ ?z ⊢" PROOF { - val x = SchematicFunctionLabel("x", 0) - val z = SchematicFunctionLabel("z", 0) - val x1 = VariableLabel("x") - val y1 = VariableLabel("y") - val z1 = VariableLabel("z") - val h = SchematicPredicateLabel("h", 0) - val sPhi = SchematicPredicateLabel("P", 2) + val x = VariableLabel("x") + val y = VariableLabel("y") + val z = VariableLabel("z") + val h = VariableFormulaLabel("h") + val sPhi = SchematicNPredicateLabel("P", 2) // forall(z, exists(y, forall(x, in(x,y) <=> (in(x,y) /\ sPhi(x,z))))) val i1 = () |- comprehensionSchema val i2 = thm"russelParadox" // forall(x1, in(x1,y) <=> !in(x1, x1)) |- () - val p0 = 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 p0 = InstPredSchema(() |- forall(z, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))), -1, Map(sPhi -> LambdaTermFormula(Seq(x, z), !in(x, x)))) val s0 = SCSubproof(instantiateForall(Proof(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 s1 = hypothesis(in(x, y) <=> (in(x, z) /\ !in(x, x))) // 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)), + (in(x, z) <=> And(), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> (And() /\ !in(x, x)), 1, - List((in(x1, z), And())), - LambdaFormulaFormula(Seq(h), in(x1, y1) <=> (h() /\ !in(x1, x1))) + List((in(x, z), And())), + LambdaFormulaFormula(Seq(h), in(x, y) <=> (h /\ !in(x, x))) ) // 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, 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))))) + val s3 = Rewrite((in(x, z), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 2) + val s4 = LeftForall((forall(x, in(x, z)), in(x, y) <=> (in(x, z) /\ !in(x, x))) |- in(x, y) <=> !in(x, x), 3, in(x, z), x, x) + val s5 = LeftForall((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- in(x, y) <=> !in(x, x), 4, in(x, y) <=> (in(x, z) /\ !in(x, x)), x, x) + val s6 = RightForall((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- forall(x, in(x, y) <=> !in(x, x)), 5, in(x, y) <=> !in(x, x), x) + val s7 = InstFunSchema(forall(x, in(x, y) <=> !in(x, x)) |- (), -2, Map(y -> LambdaTermTerm(Nil, y))) + val s8 = Cut((forall(x, in(x, z)), forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x)))) |- (), 6, 7, forall(x, in(x, y) <=> !in(x, x))) + val s9 = LeftExists((forall(x, in(x, z)), exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))) |- (), 8, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))), y) + val s10 = Cut(forall(x, in(x, z)) |- (), 0, 9, exists(y, forall(x, in(x, y) <=> (in(x, z) /\ !in(x, x))))) Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10), imports(i1, i2)) } using (ax"comprehensionSchema", thm"russelParadox") show - private val sx = SchematicFunctionLabel("x", 0) - private val sy = SchematicFunctionLabel("y", 0) - val oPair: ConstantFunctionLabel = DEFINE("", sx, sy) as pair(pair(sx, sy), pair(sx, sx)) + private val x = VariableLabel("x") + private val y = VariableLabel("y") + val oPair: ConstantFunctionLabel = DEFINE("", x, y) as pair(pair(x, y), pair(x, x)) show } diff --git a/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala index c48c282d8d2951663a38da9fdd9e8d45895ca25a..65ce706f5723c6d4c5b5d9ac46bb211b81c0093d 100644 --- a/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala +++ b/src/main/scala/lisa/proven/tactics/SimplePropositionalSolver.scala @@ -149,7 +149,7 @@ object SimplePropositionalSolver { } else { val f = s.left.find(f => s.right.contains(f)) - List(Hypothesis(s, if (f.nonEmpty) f.get else PredicateFormula(SchematicPredicateLabel("P", 0), Seq()))) + List(Hypothesis(s, if (f.nonEmpty) f.get else PredicateFormula(VariableFormulaLabel("P"), Seq()))) } }