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