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..901989ed75a87d06d4d07ac7efcf9a291238359e 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/CommonDefinitions.scala
@@ -17,6 +17,7 @@ private[fol] trait CommonDefinitions {
* 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..2290bb7b88d4b921fd3621c2e93350a79f93f829 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..c8f99bebd450a6ea83b9857a870adaa49c71b9ad 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/FormulaLabelDefinitions.scala
@@ -73,7 +73,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..cf91986365fefb81fb19866eab87c887a9448bdf 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 = ???
}
@@ -53,47 +51,25 @@ 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 +99,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 +126,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..c456cc476b4d4b4e9e974808f836adcf877ffdd1 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/TermLabelDefinitions.scala
@@ -29,15 +29,6 @@ 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.
@@ -56,13 +47,25 @@ 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
+
+ /**
+ * 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..faaec02d1408fdc92fba82f26f9e5df2b69cd190 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -2,7 +2,6 @@ package lisa.kernel.proof
import lisa.kernel.fol.FOL._
-import scala.collection.immutable.Set
/**
* The concrete implementation of sequent calculus (with equality).
@@ -301,7 +300,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-utils/src/main/scala/lisa/utils/KernelHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
index e372a02e2bba7521a30d19f3ed6117872053289c..d574cd63f97bdbea6fbe23f043234b967fc417c3 100644
--- a/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/KernelHelpers.scala
@@ -147,8 +147,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..88baf19472559e86ec912318969f05a2f477715d 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/TheoriesHelpers.scala b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
index 58678892f711194ad40db6cf2c2723b13feeef8e..12629781545782f2aaec58a33da185ab1ad1a62a 100644
--- a/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/TheoriesHelpers.scala
@@ -1,7 +1,7 @@
package lisa.utils
import lisa.kernel.fol.FOL.*
-import lisa.kernel.proof.RunningTheoryJudgement.InvalidJustification
+import lisa.kernel.proof.RunningTheoryJudgement.{InvalidJustification, InvalidJustificationException}
import lisa.kernel.proof.SequentCalculus.*
import lisa.kernel.proof.*
import lisa.utils.Printer
@@ -75,13 +75,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 +91,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 +100,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/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..7f5c4e7a2c27344e4bd10da2c18a423e284f3ebd 100644
--- a/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
+++ b/lisa-utils/src/test/scala/lisa/test/ProofCheckerSuite.scala
@@ -11,48 +11,49 @@ 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)
- )
- 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)
- )
-
- protected val (sl, tl, ul, vl) = (VariableLabel("s"), VariableLabel("t"), VariableLabel("u"), VariableLabel("v"))
- protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
-
- def checkProof(proof: SCProof): Unit = {
- val judgement = checkSCProof(proof)
- println(Printer.prettySCProof(judgement))
- println(s"\n(${proof.totalLength} proof steps in total)")
- }
-
- def checkProof(proof: SCProof, expected: Sequent): Unit = {
- val judgement = checkSCProof(proof)
- assert(judgement.isValid, "\n" + Printer.prettySCProof(judgement))
- assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
- }
-
- def checkIncorrectProof(incorrectProof: SCProof): Unit = {
- assert(
- !checkSCProof(incorrectProof).isValid,
- s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}"
+
+ import lisa.kernel.fol.FOL.*
+
+ protected val (xl, yl, zl, wl, xpl, ypl, zpl, wpl) = (
+ 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) = (
+ 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"))
+ protected val (s, t, u, v) = (VariableTerm(sl), VariableTerm(tl), VariableTerm(ul), VariableTerm(vl))
+
+ def checkProof(proof: SCProof): Unit = {
+ val judgement = checkSCProof(proof)
+ println(Printer.prettySCProof(judgement))
+ println(s"\n(${proof.totalLength} proof steps in total)")
+ }
+
+ def checkProof(proof: SCProof, expected: Sequent): Unit = {
+ val judgement = checkSCProof(proof)
+ assert(judgement.isValid, "\n" + Printer.prettySCProof(judgement))
+ assert(isSameSequent(proof.conclusion, expected), s"(${Printer.prettySequent(proof.conclusion)} did not equal ${Printer.prettySequent(expected)})")
+ }
+
+ def checkIncorrectProof(incorrectProof: SCProof): Unit = {
+ assert(
+ !checkSCProof(incorrectProof).isValid,
+ s"(incorrect proof with conclusion '${Printer.prettySequent(incorrectProof.conclusion)}' was accepted by the proof checker)\nSequent: ${incorrectProof.conclusion}"
+ )
+ }
}
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..a70079678e189c240902b6350829076ffa40861e 100644
--- a/src/main/scala/lisa/proven/mathematics/Mapping.scala
+++ b/src/main/scala/lisa/proven/mathematics/Mapping.scala
@@ -11,440 +11,420 @@ import SetTheory.*
*/
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 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)
+ 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 f = VariableLabel("f")
+ val h = SchematicPredicateLabel("h", 0)
+ 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 H = existsOne(x, phi(x, a))
- val H1 = forall(a, in(a, A) ==> H)
- val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
- val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
- val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
- // 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(
- () |- 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(Proof(steps(p0), imports(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(
- () |- 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(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 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,
- 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,
- 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 H = existsOne(x, phi(x, a))
+ val H1 = forall(a, in(a, A) ==> H)
+ val s0 = hypothesis(H) // () |- existsOne(x, phi(x, a)))
+ val s1 = Weakening((H, in(a, A)) |- existsOne(x, phi(x, a)), 0)
+ val s2 = Rewrite((H) |- in(a, A) ==> existsOne(x, phi(x, a)), 1)
+ // 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(
+ () |- instantiatePredicateSchemas(replacementSchema, Map(sPsi -> LambdaTermFormula(Seq(y, a, x), phi(x, a)))),
+ -1,
+ Map(sPsi -> LambdaTermFormula(Seq(y, a, x), phi(x, 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
+ val p1 = instantiateForall(Proof(steps(p0), imports(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(
+ () |- instantiatePredicateSchemas(comprehensionSchema, Map(sPhi -> LambdaTermFormula(Seq(x, z), exists(a, in(a, A) /\ phi(x, a))))),
+ -1,
+ Map(sPhi -> LambdaTermFormula(Seq(x, z), exists(a, in(a, A) /\ phi(x, a))))
)
- val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
- val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(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), 16)
- Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
- // goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
- // redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
- // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
- // redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
- // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
- // redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
- // redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
- // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
- // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
- // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
+ 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 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 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,
+ 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,
+ 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
+ )
+ val truc = forall(a, in(a, A) ==> exists(y, phi(y, a) /\ in(y, B)))
+ val s17 = Rewrite(Set(forall(a, in(a, A) ==> existsOne(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), 16)
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17))
+ // goal H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+ // redGoal ∀a.(a ∈ A) => ∃!x. phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s17
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B) s16
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A ∧ phi(x, a) |- (x ∈ B) s15
+ // redGoal ∀a.(a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s14
+ // redGoal (a ∈ A) => ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s13
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s12
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A, phi(x, a) |- (x ∈ B) s11
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s11
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), T ⇒ ∃y. y ∈ B ∧ phi(y, a), a ∈ A <=> T, phi(x, a) |- (x ∈ B) s10
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), ∃y1. y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s9
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B ∧ phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s8
+ // redGoal ∃y. ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s7
+ // redGoal ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s6
+ // redGoal (x=y) ↔ phi(x, a), ∀x. (x=y) ↔ phi(x, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s5
+ // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, phi(y1, a), a ∈ A, phi(x, a) |- (x ∈ B) s4
+ // redGoal (x=y) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s3
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, phi(x, a) |- (x ∈ B) s2
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (x ∈ B) s1
+ // redGoal (x=y1) ↔ phi(x, a), (y1=y) ↔ phi(y1, a), y1 ∈ B, (y1=y), a ∈ A, x=y1 |- (y1 ∈ B) s0
- }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
+ }) // H, ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ phi(y, a), ∃a. a ∈ A ∧ phi(x, a) |- (x ∈ B)
- val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
- val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
- val s9 = SCSubproof({
- val p0 = instantiateForall(Proof(hypothesis(F)), x)
- val left = in(x, B1)
- val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
- val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
- p3
- }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
- val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
- val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
- val s12 = SCSubproof({
- val p0 = instantiateForall(Proof(hypothesis(F)), x)
- val left = in(x, B1)
- val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
- val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
- val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
- val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
- val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
- val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
- p5
- }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
- val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val s14 =
- RightForall(
- (H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- 13,
- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))),
- x
- ) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val G = forall(a, in(a, A) ==> exists(y, in(y, B) /\ (phi(y, a))))
+ val F = forall(x, iff(in(x, B1), in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))))
+ val s9 = SCSubproof({
+ val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p2 = destructRightAnd(p1, (right ==> left), (left ==> right)) // F |- in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) => in(x, B1)
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B), exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), p2.length - 1)))
+ p3
+ }) // have F, (x ∈ B), ∃a. a ∈ A ∧ x = (a, b) |- (x ∈ B1)
+ val s10 = Cut(Set(F, G, H1, exists(a, in(a, A) /\ (phi(x, a)))) |- in(x, B1), 8, 9, in(x, B)) // redGoal F, ∃a. a ∈ A ∧ x = (a, b), ∀a. (a ∈ A) ⇒ ∃y. y ∈ B ∧ y = (a, b) |- (x ∈ B1)
+ val s11 = Rewrite(Set(H1, G, F) |- exists(a, in(a, A) /\ (phi(x, a))) ==> in(x, B1), 10) // F |- ∃a. a ∈ A ∧ x = (a, b) => (x ∈ B1) --- half
+ val s12 = SCSubproof({
+ val p0 = instantiateForall(Proof(hypothesis(F)), x)
+ val left = in(x, B1)
+ val right = in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a)))
+ val p1 = p0.withNewSteps(Vector(Rewrite(F |- (left ==> right) /\ (right ==> left), p0.length - 1)))
+ val p2 = destructRightAnd(p1, (left ==> right), (right ==> left)) // F |- in(x, B1) => in(x, B) /\ exists(a, in(a, A) /\ (phi(x, a))) =>
+ val p3 = p2.withNewSteps(Vector(Rewrite(Set(F, in(x, B1)) |- exists(a, in(a, A) /\ (phi(x, a))) /\ in(x, B), p2.length - 1)))
+ val p4 = destructRightAnd(p3, exists(a, in(a, A) /\ (phi(x, a))), in(x, B))
+ val p5 = p4.withNewSteps(Vector(Rewrite(F |- in(x, B1) ==> exists(a, in(a, A) /\ (phi(x, a))), p4.length - 1)))
+ p5
+ }) // have F |- (x ∈ B1) ⇒ ∃a. a ∈ A ∧ x = (a, b) --- other half
+ val s13 = RightIff((H1, G, F) |- in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))), 11, 12, in(x, B1), exists(a, in(a, A) /\ (phi(x, a)))) // have F |- (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
+ val s14 =
+ RightForall(
+ (H1, G, F) |- forall(x, in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ 13,
+ in(x, B1) <=> exists(a, in(a, A) /\ (phi(x, a))),
+ x
+ ) // G, F |- ∀x. (x ∈ B1) <=> ∃a. a ∈ A ∧ x = (a, b)
- val i3 = () |- extensionalityAxiom
- 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,
- 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(Proof(steps(Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ 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,
- 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)]
+ val i3 = () |- extensionalityAxiom
+ 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,
+ 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(Proof(steps(Rewrite(() |- extensionalityAxiom, -1)), imports(() |- extensionalityAxiom)), X, B1), Vector(-2)) // (∀z. (z ∈ X) <=> (z ∈ 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,
+ 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)]
- Proof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
- },
- Vector(13, -3, 14)
- ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s16 = RightForall(
- (H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
- 15,
- (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
- X
- ) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- val s17 = RightExists(
- (H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
- 16,
- forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
- y,
- B1
- )
- val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
- 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 res = steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
- Proof(res, imports(i1, i2, i3))
+ Proof(steps(t0, t1, t2, t3, t4, t5, t6, t7, t8, t9), imports(i1, i2, i3))
+ },
+ Vector(13, -3, 14)
+ ) // goal F |- X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s16 = RightForall(
+ (H1, G, F) |- forall(X, (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
+ 15,
+ (X === B1) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))),
+ X
+ ) // goal F |- ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ val s17 = RightExists(
+ (H1, G, F) |- exists(y, forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a)))))),
+ 16,
+ forall(X, (X === y) <=> forall(x, in(x, X) <=> exists(a, in(a, A) /\ (phi(x, a))))),
+ y,
+ B1
+ )
+ val s18 = LeftExists((exists(B1, F), G, H1) |- s17.bot.right, 17, F, B1) // ∃B1. F |- ∃B1. ∀X. X=B1 <=> [∀x. (x ∈ X) <=> ∃a. a ∈ A ∧ x = (a, b)]
+ 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 res = steps(s0, s1, s2, s3, s4, s5, s6, s7, s8, s9, s10, s11, s12, s13, s14, s15, s16, s17, s18, s19, s20, s21, s22)
+ Proof(res, imports(i1, i2, i3))
} using (ax"replacementSchema", ax"comprehensionSchema", ax"extensionalityAxiom")
- show
+ show
- THEOREM("lemmaLayeredTwoArgumentsMap") of
- "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- 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 X = VariableLabel("X")
- val B = SchematicFunctionLabel("B", 0)()
- val B1 = VariableLabel("B1")
- val phi = SchematicPredicateLabel("phi", 2)
- val psi = SchematicPredicateLabel("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 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))
- 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))) |- 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)))))
- )
- Proof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
- // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
- // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
- // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
- // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
- // by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s6
- // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s7
+ THEOREM("lemmaLayeredTwoArgumentsMap") of
+ "∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ ?B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ ?A) ∧ ?psi(x1, a, b)" PROOF {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
+ val f = VariableLabel("f")
+ val h = SchematicPredicateLabel("h", 0)
+ val A = VariableLabel("A")
+ val X = VariableLabel("X")
+ val B = VariableLabel("B")
+ val B1 = VariableLabel("B1")
+ val phi = SchematicPredicateLabel("phi", 2)
+ val psi = SchematicPredicateLabel("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 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))
+ 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))) |- instantiateTermSchemas(i1.right.head, Map(A -> 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)))))
+ )
+ Proof(Vector(s0, s1, s2, s3, s4, s5, s6, s7, s8), Vector(i1))
+ // have ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s0
+ // have (b ∈ B), ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s1
+ // have (b ∈ B), (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s2
+ // have (b ∈ B), ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s3
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s4
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) ⊢ ∀b. (b ∈ B) ⇒ ∃!X. ∀x. (x ∈ X) ↔ ∃a. (a ∈ A) ∧ ?psi(x, a, b) s5
+ // by thmMapFunctional have ∀b. (b ∈ B) ⇒ ∃!x. ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) ⊢ ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) phi(x, b) = ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s6
+ // have ∀b. (b ∈ B) ⇒ ∀a. (a ∈ A) ⇒ ∃!x. ?psi(x, a, b) |- ∃!X. ∀x. (x ∈ X) ↔ ∃b. (b ∈ B) ∧ ∀x1. (x1 ∈ x) ↔ ∃a. (a ∈ A) ∧ ?psi(x1, a, b) s7
} using (thm"functionalMapping")
- show
+ show
- THEOREM("applyFunctionToUniqueObject") of
- "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- 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)
+ THEOREM("applyFunctionToUniqueObject") of
+ "∃!x. ?phi(x) ⊢ ∃!z. ∃x. (z = ?F(x)) ∧ ?phi(x)" PROOF {
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val z = VariableLabel("z")
+ val z1 = VariableLabel("z1")
+ val F = SchematicFunctionLabel("F", 1)
+ val f = VariableLabel("f")
+ val phi = SchematicPredicateLabel("phi", 1)
+ val g = SchematicPredicateLabel("g", 0)
- 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 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)
- val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
- Proof(steps(s0, s1, s2, s3, s4, s5, s6))
- }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
+ 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 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)
+ val s6 = Rewrite(forall(x, phi(x) <=> (x === x1)) |- exists(x, phi(x) /\ (F(x) === z)) ==> (F(x1) === z), 5)
+ Proof(steps(s0, s1, s2, s3, s4, s5, s6))
+ }) // redGoal2 ∀x. x=x1 <=> phi(x) ⊢ ∃x. z=F(x) /\ phi(x) ==> F(x1)=z g2.s5
- val g1 = SCSubproof({
- val s0 = hypothesis(phi(x1))
- val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
- val s2 = hypothesis(z === F(x1))
- val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
- val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
- val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
- Proof(steps(s0, s1, s2, s3, s4, s5))
- })
+ val g1 = SCSubproof({
+ val s0 = hypothesis(phi(x1))
+ val s1 = LeftForall(forall(x, (x === x1) <=> phi(x)) |- phi(x1), 0, (x === x1) <=> phi(x), x, x1)
+ val s2 = hypothesis(z === F(x1))
+ val s3 = RightAnd((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- (z === F(x1)) /\ phi(x1), Seq(2, 1), Seq(z === F(x1), phi(x1)))
+ val s4 = RightExists((forall(x, (x === x1) <=> phi(x)), z === F(x1)) |- exists(x, (z === F(x)) /\ phi(x)), 3, (z === F(x)) /\ phi(x), x, x1)
+ val s5 = Rewrite(forall(x, (x === x1) <=> phi(x)) |- z === F(x1) ==> exists(x, (z === F(x)) /\ phi(x)), 4)
+ Proof(steps(s0, s1, s2, s3, s4, s5))
+ })
- val s0 = g1
- val s1 = g2
- val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
- val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
- val s4 = RightExists(
- forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
- 3,
- forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
- z1,
- F(x1)
- )
- val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
- val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
- Proof(Vector(s0, s1, s2, s3, s4, s5, s6))
+ val s0 = g1
+ val s1 = g2
+ val s2 = RightIff(forall(x, (x === x1) <=> phi(x)) |- (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), 0, 1, z === F(x1), exists(x, (z === F(x)) /\ phi(x)))
+ val s3 = RightForall(forall(x, (x === x1) <=> phi(x)) |- forall(z, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x))), 2, (z === F(x1)) <=> exists(x, (z === F(x)) /\ phi(x)), z)
+ val s4 = RightExists(
+ forall(x, (x === x1) <=> phi(x)) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))),
+ 3,
+ forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x))),
+ z1,
+ F(x1)
+ )
+ val s5 = LeftExists(exists(x1, forall(x, (x === x1) <=> phi(x))) |- exists(z1, forall(z, (z === z1) <=> exists(x, (z === F(x)) /\ phi(x)))), 4, forall(x, (x === x1) <=> phi(x)), x1)
+ val s6 = Rewrite(existsOne(x, phi(x)) |- existsOne(z, exists(x, (z === F(x)) /\ phi(x))), 5) // goal ∃!x. phi(x) ⊢ ∃!z. ∃x. z=F(x) /\ phi(x)
+ Proof(Vector(s0, s1, s2, s3, s4, s5, s6))
} using ()
- show
+ show
- THEOREM("mapTwoArguments") of
- "∀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)" PROOF {
- val a = VariableLabel("a")
- val b = VariableLabel("b")
- val x = VariableLabel("x")
- val x1 = VariableLabel("x1")
- val x_ = SchematicFunctionLabel("x", 0)
- val y_ = SchematicFunctionLabel("y", 0)
- 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)
+ THEOREM("mapTwoArguments") of
+ "∀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)" PROOF {
+ val a = VariableLabel("a")
+ val b = VariableLabel("b")
+ val x = VariableLabel("x")
+ val x1 = VariableLabel("x1")
+ val y = VariableLabel("y")
+ val F = SchematicFunctionLabel("F", 1)
+ val A = VariableLabel("A")
+ val B = VariableLabel("B")
+ val phi = SchematicPredicateLabel("phi", 1)
+ val psi = SchematicPredicateLabel("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 s2 = Cut(i1.left |- seq1.right, -1, 1, seq1.left.head)
- Proof(steps(s0, s1, s2), imports(i1, i2))
+ 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 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
+ show
- val A = SchematicFunctionLabel("A", 0)
- val B = SchematicFunctionLabel("B", 0)
- private val sz = SchematicFunctionLabel("z", 0)
- val cartesianProduct: ConstantFunctionLabel =
- DEFINE("cartProd", A, B) asThe sz 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)))))))
- } PROOF {
- def makeFunctional(t: Term): Proof = {
- val x = VariableLabel(freshId(t.freeVariables.map(_.id), "x"))
- val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
- val s0 = RightRefl(() |- t === t, t === t)
- val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
- val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
- val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
- val s4 = Rewrite(() |- existsOne(x, x === t), 3)
- Proof(s0, s1, s2, s3, s4)
- }
+ val A = VariableLabel("A")
+ val B = VariableLabel("B")
+ private val z = VariableLabel("z")
+ val cartesianProduct: ConstantFunctionLabel =
+ 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 = 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"))
+ val y = VariableLabel(freshId(t.freeVariables.map(_.id), "y"))
+ val s0 = RightRefl(() |- t === t, t === t)
+ val s1 = Rewrite(() |- (x === t) <=> (x === t), 0)
+ val s2 = RightForall(() |- forall(x, (x === t) <=> (x === t)), 1, (x === t) <=> (x === t), x)
+ val s3 = RightExists(() |- exists(y, forall(x, (x === y) <=> (x === t))), 2, forall(x, (x === y) <=> (x === t)), y, t)
+ val s4 = Rewrite(() |- existsOne(x, x === t), 3)
+ Proof(s0, s1, s2, s3, s4)
+ }
- 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 x = VariableLabel("x")
+ val A = VariableLabel("A")
+ val B = VariableLabel("B")
+ val psi = SchematicPredicateLabel("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)
+ 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)
- val s0 = SCSubproof({
- val s0 = SCSubproof(makeFunctional(oPair(a, b)))
- val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
- val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
- val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
- val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
- val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
- Proof(steps(s0, s1, s2, s3, s4, s5))
- }) // ∀b. (b ∈ ?B) ⇒ ∀a. (a ∈ ?A) ⇒ ∃!x. x= (a, b)
+ val s0 = SCSubproof({
+ val s0 = SCSubproof(makeFunctional(oPair(a, b)))
+ val s1 = Weakening((in(b, B), in(a, A)) |- s0.bot.right, 0)
+ val s2 = Rewrite(in(b, B) |- in(a, A) ==> s0.bot.right.head, 1)
+ val s3 = RightForall(in(b, B) |- forall(a, in(a, A) ==> s0.bot.right.head), 2, in(a, A) ==> s0.bot.right.head, a)
+ val s4 = Rewrite(() |- in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), 3)
+ val s5 = RightForall(() |- forall(b, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head)), 4, in(b, B) ==> forall(a, in(a, A) ==> s0.bot.right.head), b)
+ Proof(steps(s0, s1, s2, s3, s4, s5))
+ }) // ∀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_)))),
- -1,
- 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))
- } using (thm"mapTwoArguments")
- show
+ 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)
+ Proof(steps(s0, s1, s2), imports(i1))
+ } using (thm"mapTwoArguments")
+ show
}
diff --git a/src/main/scala/lisa/proven/mathematics/SetTheory.scala b/src/main/scala/lisa/proven/mathematics/SetTheory.scala
index 22822eb716ee39a060abd33cc3a0992ff657d4d4..21dffc61297a36b62bee9b16d4541905391b6208 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
@@ -80,7 +80,7 @@ object SetTheory extends lisa.proven.Main {
val x1 = VariableLabel("x'")
val y1 = VariableLabel("y'")
val z = VariableLabel("z")
- val g = SchematicFunctionLabel("g", 0)
+ val g = VariableLabel("g")
val h = SchematicPredicateLabel("h", 0)
val pxy = pair(x, y)
val pxy1 = pair(x1, y1)
@@ -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,7 +119,7 @@ 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))),
@@ -166,7 +166,7 @@ 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))),
@@ -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,
@@ -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 x = VariableLabel("x")
+ val y = VariableLabel("y")
+ val z = VariableLabel("z")
val h = SchematicPredicateLabel("h", 0)
val sPhi = SchematicPredicateLabel("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
}