From eab5e80a995853c0e0685d3e6a37dec5d18a14f2 Mon Sep 17 00:00:00 2001
From: SimonGuilloud <sim-guilloud@bluewin.ch>
Date: Wed, 13 Jul 2022 00:20:13 +0200
Subject: [PATCH] Changed the whole project to remove 0-arity schematic
variables and replace them by variables. It compiles, but at least one proof
doesn't go through.
---
.../lisa/kernel/fol/CommonDefinitions.scala | 1 +
.../lisa/kernel/fol/FormulaDefinitions.scala | 8 +-
.../kernel/fol/FormulaLabelDefinitions.scala | 4 +-
.../scala/lisa/kernel/fol/Substitutions.scala | 77 +-
.../lisa/kernel/fol/TermDefinitions.scala | 20 +-
.../kernel/fol/TermLabelDefinitions.scala | 23 +-
.../lisa/kernel/proof/RunningTheory.scala | 12 +-
.../scala/lisa/kernel/proof/SCProof.scala | 1 -
.../lisa/kernel/proof/SCProofChecker.scala | 2 +-
.../lisa/kernel/proof/SequentCalculus.scala | 3 +-
.../main/scala/lisa/utils/KernelHelpers.scala | 4 +-
.../src/main/scala/lisa/utils/Library.scala | 34 +-
.../scala/lisa/utils/TheoriesHelpers.scala | 14 +-
.../test/scala/lisa/kernel/ProofTests.scala | 4 +-
.../scala/lisa/test/ProofCheckerSuite.scala | 87 +-
src/main/scala/lisa/proven/Main.scala | 4 +
.../lisa/proven/mathematics/Mapping.scala | 802 +++++++++---------
.../lisa/proven/mathematics/SetTheory.scala | 62 +-
18 files changed, 565 insertions(+), 597 deletions(-)
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 f1d01c42..901989ed 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 0a19f260..2290bb7b 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 b1d14331..c8f99beb 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 0f2fe1f4..cf919863 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 e98ca824..23359f10 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 c2691946..c456cc47 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 ce544cf2..5d17880e 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 0892ef5d..de5b860c 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 a2ff683d..b11218c3 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 15d677b9..faaec02d 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 e372a02e..d574cd63 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 3863a9b6..88baf194 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 58678892..12629781 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 53fa5f17..d00afd89 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 6765e70a..7f5c4e7a 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 e69a7102..bf01e93e 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 7267e0c7..a7007967 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 22822eb7..21dffc61 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
}
--
GitLab