diff --git a/CHANGES.md b/CHANGES.md
index 25595adeac000dbf32e2c6ba67155f2dffcbe56d..8907b3058da95a3c484ac99aac1d076a3973ace2 100644
--- a/CHANGES.md
+++ b/CHANGES.md
@@ -1,5 +1,16 @@
# Change List
+
+## 2024-01-02
+The of keyword can now be used to instantiate quantified variables in facts whose right hand side is a single universaly quantified formula. This can be combined freely with instantiation of ffree schematic symbols. Manual and tests update.
+
+
+## 2023-12-31
+Expanded the Substitution rules to allow substitution under quantifiers when a statement of the form $\forall x. f(x) = g(x)$ is given.
+
+## 2023-12-29
+Update to the user manual, change format to B5 and more improvements.
+
## 2023-12-19
Introduction of local definitions, with methods `witness`, `t.replace`, `t.collect`, `t.map` and `t.filter`. Update of the manual, describing how those work, along with some corrections to the statement of axioms ot match LISA's presentation. Include test cases using each, and proved some required theorems. Fix an error in the reconstruction of OL-normalized formulas used in some tactics.
diff --git a/lisa-examples/src/main/scala/Test.scala b/lisa-examples/src/main/scala/Test.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b65c3c6c2856115278ef9fd926b786a5f706b0a9
--- /dev/null
+++ b/lisa-examples/src/main/scala/Test.scala
@@ -0,0 +1,58 @@
+
+object Test extends lisa.Main {
+
+ val u = variable
+ val v = variable
+ val w = variable
+ val x = variable
+ val y = variable
+ val z = variable
+ val a = variable
+ val c = variable
+ val d = variable
+
+ val f = function[1]
+ val g = function[1]
+ val h = function[2]
+
+ val E = predicate[2]
+ val P = predicate[2]
+
+ val assump1 = ∀(u, ∀(v, ∀(w, E(u, v) ==> (E(v, w) ==> E(u, w)))))
+ val assump2 = ∀(x, ∀(y, E(x, y) ==> (E(f(x), f(y)))))
+ val assump3 = ∀(z, E(f(g(z)), g(f(z))))
+
+ val goal = E(f(f(g(a))), g(f(f(a))))
+
+
+
+ val thm = Theorem((assump1, assump2, assump3) |- goal) {
+ have(thesis) by Tableau
+ }
+
+ val thm1 = Theorem(∀(x, E(x, x)) |- ∀(x, E(f(x), f(x)))) {
+ val s1 = assume(∀(x, E(x, x)))
+ have(thesis) by RightForall(s1 of f(x))
+ }
+
+ val thm2 = Theorem(∀(y, ∀(x, E(x, y))) |- ∀(y, ∀(x, E(f(x), h(x, y))))) {
+ val s1 = assume(∀(y, ∀(x, E(x, y))))
+ println((s1 of (h(x, y), f(x))).result)
+ have(∀(x, E(f(x), h(x, y)))) by RightForall(s1 of (h(x, y), f(x)))
+ thenHave(thesis) by RightForall
+ }
+
+ val thm3 = Theorem(∀(y, ∀(x, E(x, y))) |- E(f(x), y) /\ E(x, h(x, y))) {
+ val s1 = assume (∀(y, ∀(x, E(x, y))))
+ val s2 = have(∀(x, E(x, y))) by Restate.from(s1 of y)
+ have(thesis) by Tautology.from(s2 of f(x), s2 of (x, y := h(x, y)))
+
+ }
+
+ val ax = Axiom(∀(x, ∀(y, P(x, y))))
+ val thm4 = Theorem(c === d) {
+ have(thesis) by Restate.from(ax of (c, d, P := ===))
+ showCurrentProof()
+ }
+
+}
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 f3f04bc26dde398a1c1b3b6793383dfa46cab02a..51bfb465488256921e68dfd91e02f888b411e637 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/fol/Substitutions.scala
@@ -136,7 +136,7 @@ trait Substitutions extends FormulaDefinitions {
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiateTermSchemas(_, m)))
case BinderFormula(label, bound, inner) =>
val newSubst = m - bound
- val fv: Set[VariableLabel] = newSubst.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }.toSet
+ val fv: Set[VariableLabel] = newSubst.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }.toSet ++ inner.freeVariables
if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ m.keys.map(_.id), bound.name))
val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
@@ -162,7 +162,7 @@ trait Substitutions extends FormulaDefinitions {
}
case ConnectorFormula(label, args) => ConnectorFormula(label, args.map(instantiatePredicateSchemas(_, m)))
case BinderFormula(label, bound, inner) =>
- val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet
+ val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet ++ inner.freeVariables
if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
@@ -189,7 +189,7 @@ trait Substitutions extends FormulaDefinitions {
case _ => ConnectorFormula(label, newArgs)
}
case BinderFormula(label, bound, inner) =>
- val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaFormulaFormula(arguments, body)) => body.freeVariables }).toSet
+ val fv: Set[VariableLabel] = (m.flatMap { case (symbol, LambdaFormulaFormula(arguments, body)) => body.freeVariables }).toSet ++ inner.freeVariables
if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name), bound.name))
val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
@@ -232,7 +232,7 @@ trait Substitutions extends FormulaDefinitions {
val fv: Set[VariableLabel] =
(mCon.flatMap { case (symbol, LambdaFormulaFormula(arguments, body)) => body.freeVariables }).toSet ++
(mPred.flatMap { case (symbol, LambdaTermFormula(arguments, body)) => body.freeVariables }).toSet ++
- (mTerm.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet
+ (mTerm.flatMap { case (symbol, LambdaTermTerm(arguments, body)) => body.freeVariables }).toSet ++ inner.freeVariables
if (fv.contains(bound)) {
val newBoundVariable = VariableLabel(freshId(fv.map(_.name) ++ mTerm.keys.map(_.id), bound.name))
val newInner = substituteVariablesInFormula(inner, Map(bound -> VariableTerm(newBoundVariable)))
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 a4c89b54bef12937c5f6165e31d543298eeba909..bf7c711474432520bd550e044aa834a2487fb4db 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SCProofChecker.scala
@@ -356,23 +356,35 @@ object SCProofChecker {
*/
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) => AtomicFormula(equality, Seq(s, t)) }
+ val (phi_args, phi_body) = lambdaPhi
+ if (phi_args.size != s_es.size) // Not strictly necessary, but it's a good sanity check. To reactivate when tactics have been modified.
+ SCInvalidProof(SCProof(step), Nil, "The number of arguments of φ must be the same as the number of equalities.")
+ else if (equals.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ SCInvalidProof(SCProof(step), Nil, "The arities of symbols in φ must be the same as the arities of equalities.")
+ else {
+ val phi_s_for_f = instantiateTermSchemas(phi_body, (phi_args zip s_es).toMap)
+ val phi_t_for_f = instantiateTermSchemas(phi_body, (phi_args zip t_es).toMap)
+ val sEqT_es = equals map {
+ case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = AtomicFormula(equality, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(VariableTerm))))
+ (s.vars).foldLeft(base: Formula) { case (acc, s_arg) => BinderFormula(Forall, s_arg, acc) }
+ }
- 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(SCProof(step))
- else
- SCInvalidProof(
- SCProof(step),
- 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)."
+ 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)
)
- else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ 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(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ }
/*
* Γ |- φ(s_), Δ
@@ -380,46 +392,73 @@ object SCProofChecker {
* Γ, (s=t)_ |- φ(t_), Δ
*/
case RightSubstEq(b, t1, equals, lambdaPhi) =>
- val sEqT_es = equals map { case (s, t) => AtomicFormula(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(SCProof(step))
- else
- SCInvalidProof(
- SCProof(step),
- 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."
+ val (s_es, t_es) = equals.unzip
+ val (phi_args, phi_body) = lambdaPhi
+ if (phi_args.size != equals.size) // Not strictly necessary, but it's a good sanity check. To reactivate when tactics have been modified.
+ SCInvalidProof(SCProof(step), Nil, "The number of arguments of φ must be the same as the number of equalities.")
+ else if (equals.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ SCInvalidProof(SCProof(step), Nil, "The arities of symbols in φ must be the same as the arities of equalities.")
+ else {
+ val phi_s_for_f = instantiateTermSchemas(phi_body, (phi_args zip s_es).toMap)
+ val phi_t_for_f = instantiateTermSchemas(phi_body, (phi_args zip t_es).toMap)
+ val sEqT_es = equals map {
+ case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = AtomicFormula(equality, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(VariableTerm))))
+ (s.vars).foldLeft(base: Formula) { case (acc, s_arg) => BinderFormula(Forall, s_arg, acc) }
+ }
+
+ if (isSameSet(ref(t1).left ++ sEqT_es, b.left))
+ 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)
)
- } else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ "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(SCProof(step), Nil, "Left-hand sides of the premise + (s=t)_ must be the same as left-hand side of the premise.")
+ }
+
/*
* Γ, φ(ψ_) |- Δ
* ---------------------
* Γ, ψ⇔τ, φ(τ) |- Δ
*/
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(SCProof(step))
- else
- SCInvalidProof(
- SCProof(step),
- Nil,
- "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ⇔τ)_ + φ(τ_) (or with ψ and τ swapped)."
+ val (phi_args, phi_body) = lambdaPhi
+ if (phi_args.size != phi_s.size) // Not strictly necessary, but it's a good sanity check. To reactivate when tactics have been modified.
+ SCInvalidProof(SCProof(step), Nil, "The number of arguments of φ must be the same as the number of equalities.")
+ else if (equals.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ SCInvalidProof(SCProof(step), Nil, "The arities of symbols in φ must be the same as the arities of equalities.")
+ else {
+ val phi_psi_for_q = instantiatePredicateSchemas(phi_body, (phi_args zip phi_s).toMap)
+ val phi_tau_for_q = instantiatePredicateSchemas(phi_body, (phi_args zip tau_s).toMap)
+ val psiIffTau = equals map {
+ case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = ConnectorFormula(Iff, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(VariableTerm))))
+ (s.vars).foldLeft(base: Formula) { case (acc, s_arg) => BinderFormula(Forall, s_arg, acc) }
+ }
+
+ if (isSameSet(b.right, ref(t1).right))
+ if (
+ isSameSet(b.left + phi_tau_for_q, ref(t1).left ++ psiIffTau + phi_psi_for_q) ||
+ isSameSet(b.left + phi_psi_for_q, ref(t1).left ++ psiIffTau + phi_tau_for_q)
)
- else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ "Left-hand sides of the conclusion + φ(ψ_) must be the same as left-hand side of the premise + (ψ⇔τ)_ + φ(τ_) (or with ψ and τ swapped)."
+ )
+ else SCInvalidProof(SCProof(step), Nil, "Right-hand sides of the premise and the conclusion aren't the same.")
+ }
/*
* Γ |- φ[ψ/?p], Δ
@@ -427,23 +466,38 @@ object SCProofChecker {
* Γ, ψ⇔τ |- φ[τ/?p], Δ
*/
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(SCProof(step))
- else
- SCInvalidProof(
- SCProof(step),
- 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."
+ val (psi_s, tau_s) = equals.unzip
+ val (phi_args, phi_body) = lambdaPhi
+ if (phi_args.size != psi_s.size)
+ SCInvalidProof(SCProof(step), Nil, "The number of arguments of φ must be the same as the number of equalities.")
+ else if (equals.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ SCInvalidProof(SCProof(step), Nil, "The arities of symbols in φ must be the same as the arities of equalities.")
+ else {
+ val phi_psi_for_q = instantiatePredicateSchemas(phi_body, (phi_args zip psi_s).toMap)
+ val phi_tau_for_q = instantiatePredicateSchemas(phi_body, (phi_args zip tau_s).toMap)
+ val psiIffTau = equals map {
+ case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = ConnectorFormula(Iff, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(VariableTerm))))
+ (s.vars).foldLeft(base: Formula) { case (acc, s_arg) => BinderFormula(Forall, s_arg, acc) }
+ }
+
+ 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)
)
- else SCInvalidProof(SCProof(step), Nil, "Left-hand sides of the premise + ψ⇔τ must be the same as left-hand side of the premise.")
+ SCValidProof(SCProof(step))
+ else
+ SCInvalidProof(
+ SCProof(step),
+ Nil,
+ "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(SCProof(step), Nil, "Left-hand sides of the premise + ψ⇔τ must be the same as left-hand side of the premise.")
+ }
+
+
/**
* <pre>
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 d089f29a421214a61b5c4c3449a4a1a238c1eb60..b84d84b443ef507c522ffb137b8318c16d66a7a4 100644
--- a/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
+++ b/lisa-kernel/src/main/scala/lisa/kernel/proof/SequentCalculus.scala
@@ -282,7 +282,7 @@ object SequentCalculus {
* Γ, s1=t1, ..., sn=tn, φ(t1,...tn) |- Δ
* </pre>
*/
- case class LeftSubstEq(bot: Sequent, t1: Int, equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends SCProofStep { val premises = Seq(t1) }
+ case class LeftSubstEq(bot: Sequent, t1: Int, equals: List[(LambdaTermTerm, LambdaTermTerm)], lambdaPhi: (Seq[SchematicTermLabel], Formula)) extends SCProofStep { val premises = Seq(t1) }
/**
* <pre>
@@ -291,7 +291,7 @@ object SequentCalculus {
* Γ, s1=t1, ..., sn=tn |- φ(t1,...tn), Δ
* </pre>
*/
- case class RightSubstEq(bot: Sequent, t1: Int, equals: List[(Term, Term)], lambdaPhi: LambdaTermFormula) extends SCProofStep { val premises = Seq(t1) }
+ case class RightSubstEq(bot: Sequent, t1: Int, equals: List[(LambdaTermTerm, LambdaTermTerm)], lambdaPhi: (Seq[SchematicTermLabel], Formula)) extends SCProofStep { val premises = Seq(t1) }
/**
* <pre>
@@ -300,7 +300,7 @@ object SequentCalculus {
* Γ, a1⇔b1, ..., an⇔bn, φ(b1,...bn) |- Δ
* </pre>
*/
- case class LeftSubstIff(bot: Sequent, t1: Int, equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends SCProofStep { val premises = Seq(t1) }
+ case class LeftSubstIff(bot: Sequent, t1: Int, equals: List[(LambdaTermFormula, LambdaTermFormula)], lambdaPhi: (Seq[SchematicAtomicLabel], Formula)) extends SCProofStep { val premises = Seq(t1) }
/**
* <pre>
@@ -309,7 +309,8 @@ object SequentCalculus {
* Γ, a1⇔b1, ..., an⇔bn |- φ(b1,...bn), Δ
* </pre>
*/
- case class RightSubstIff(bot: Sequent, t1: Int, equals: List[(Formula, Formula)], lambdaPhi: LambdaFormulaFormula) extends SCProofStep { val premises = Seq(t1) }
+
+ case class RightSubstIff(bot: Sequent, t1: Int, equals: List[(LambdaTermFormula, LambdaTermFormula)], lambdaPhi: (Seq[SchematicAtomicLabel], Formula)) extends SCProofStep { val premises = Seq(t1) }
// Rule for schemas
diff --git a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
index 383ed4f865a310e5e7226ec1530c780000063f5f..9430195a14705a74d000832a122f3cc707b9e963 100644
--- a/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/CommonTactics.scala
@@ -65,7 +65,7 @@ object CommonTactics {
val forward = lib.have(phi |- ((x === y) ==> substPhi)) subproof {
lib.assume(phi)
- lib.thenHave((x === y) |- substPhi) by RightSubstEq.withParameters(List((x, y)), F.lambda(x, phi))
+ lib.thenHave((x === y) |- substPhi) by RightSubstEq.withParametersSimple(List((x, y)), F.lambda(x, phi))
lib.thenHave((x === y) ==> substPhi) by Restate
}
diff --git a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
index fc7a0e2f52cd6b96401f4c6ea18eb74bcc7a000b..fcc4564297b0e76faef9198a100a05ec63d463d3 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Substitution.scala
@@ -154,27 +154,39 @@ object Substitution {
takenFormulaVars
)
- lazy val rightPairs = premiseSequent.right zip premiseSequent.right.map(x => bot.right.find(y => UnificationUtils.getContextFormula(
- x,
- y,
- freeEqualities,
- freeIffs,
- confinedEqualities,
- takenTermVars,
- confinedIffs,
- takenFormulaVars
- ).isDefined))
+ lazy val rightPairs = premiseSequent.right zip premiseSequent.right.map(x =>
+ bot.right.find(y =>
+ UnificationUtils
+ .getContextFormula(
+ x,
+ y,
+ freeEqualities,
+ freeIffs,
+ confinedEqualities,
+ takenTermVars,
+ confinedIffs,
+ takenFormulaVars
+ )
+ .isDefined
+ )
+ )
- lazy val leftPairs = filteredPrem zip filteredPrem.map(x => filteredBot.find(y => UnificationUtils.getContextFormula(
- x,
- y,
- freeEqualities,
- freeIffs,
- confinedEqualities,
- takenTermVars,
- confinedIffs,
- takenFormulaVars
- ).isDefined))
+ lazy val leftPairs = filteredPrem zip filteredPrem.map(x =>
+ filteredBot.find(y =>
+ UnificationUtils
+ .getContextFormula(
+ x,
+ y,
+ freeEqualities,
+ freeIffs,
+ confinedEqualities,
+ takenTermVars,
+ confinedIffs,
+ takenFormulaVars
+ )
+ .isDefined
+ )
+ )
lazy val violatingFormulaLeft = leftPairs.find(_._2.isEmpty)
lazy val violatingFormulaRight = rightPairs.find(_._2.isEmpty)
@@ -308,7 +320,7 @@ object Substitution {
val sequentAfterEq = sequentAfterEqPre ++<< (eqs |- ()) ++<< (iffs |- ())
// this uses the "lambda" (λx. Λp. body) (p = left formulas)
- lib.thenHave(sequentAfterEq) by BasicStepTactic.LeftSubstEq.withParameters(termInputs.toList, lambda(termVars, ctx.body.substituteUnsafe2(formSubstL)))
+ lib.thenHave(sequentAfterEq) by BasicStepTactic.LeftSubstEq.withParametersSimple(termInputs.toList, lambda(termVars, ctx.body.substituteUnsafe2(formSubstL)))
// left <=>
val formSubstR = Map((formulaVars zip formulaInputsR)*)
@@ -317,7 +329,7 @@ object Substitution {
val sequentAfterIff = sequentAfterIffPre ++<< (eqs |- ()) ++<< (iffs |- ())
// this uses the "lambda" (λx. Λp. body) (x = right terms)
- lib.thenHave(sequentAfterIff) by BasicStepTactic.LeftSubstIff(formulaInputs.toList, lambda(formulaVars, ctx.body.substituteUnsafe2(eqSubst)))
+ lib.thenHave(sequentAfterIff) by BasicStepTactic.LeftSubstIff.withParametersSimple(formulaInputs.toList, lambda(formulaVars, ctx.body.substituteUnsafe2(eqSubst)))
sequentAfterIff
}
@@ -365,7 +377,7 @@ object Substitution {
val sequentAfterEq = sequentAfterEqPre ++<< (eqs |- ()) ++<< (iffs |- ())
// this uses the "lambda" (λx. Λp. body) (p = left formulas)
- lib.thenHave(sequentAfterEq) by BasicStepTactic.RightSubstEq.withParameters(termInputs.toList, lambda(termVars, ctx.body.substituteUnsafe2(formSubstL)))
+ lib.thenHave(sequentAfterEq) by BasicStepTactic.RightSubstEq.withParametersSimple(termInputs.toList, lambda(termVars, ctx.body.substituteUnsafe2(formSubstL)))
// right <=>
val formSubstR = Map((formulaVars zip formulaInputsR)*)
@@ -374,7 +386,7 @@ object Substitution {
val sequentAfterIff = sequentAfterIffPre ++<< (eqs |- ()) ++<< (iffs |- ())
// this uses the "lambda" (λx. Λp. body) (x = right terms)
- lib.thenHave(sequentAfterIff) by BasicStepTactic.RightSubstIff(formulaInputs.toList, lambda(formulaVars, ctx.body.substituteUnsafe2(eqSubst)))
+ lib.thenHave(sequentAfterIff) by BasicStepTactic.RightSubstIff.withParametersSimple(formulaInputs.toList, lambda(formulaVars, ctx.body.substituteUnsafe2(eqSubst)))
}
// discharge any assumptions
@@ -519,9 +531,19 @@ object Substitution {
val result2: Sequent = result1.left |- AppliedConnector(Or, newright.toSeq)
var scproof: Seq[K.SCProofStep] = Seq(K.Restate((leftOrigin |- rightOrigin).underlying, -1))
if (toLeft)
- scproof = scproof :+ K.LeftSubstEq(result1.underlying, scproof.length - 1, List(left.underlying -> right.underlying), K.LambdaTermFormula(Seq(v.underlyingLabel), leftForm.underlying))
+ scproof = scproof :+ K.LeftSubstEq(
+ result1.underlying,
+ scproof.length - 1,
+ List(K.LambdaTermTerm(Seq(), left.underlying) -> (K.LambdaTermTerm(Seq(), right.underlying))),
+ (Seq(v.underlyingLabel), leftForm.underlying)
+ )
if (toRight)
- scproof = scproof :+ K.RightSubstEq(result2.underlying, scproof.length - 1, List(left.underlying -> right.underlying), K.LambdaTermFormula(Seq(v.underlyingLabel), rightForm.underlying))
+ scproof = scproof :+ K.RightSubstEq(
+ result2.underlying,
+ scproof.length - 1,
+ List(K.LambdaTermTerm(Seq(), left.underlying) -> (K.LambdaTermTerm(Seq(), right.underlying))),
+ (Seq(v.underlyingLabel), rightForm.underlying)
+ )
val bot = newleft + phi |- newright
scproof = scproof :+ K.Restate(bot.underlying, scproof.length - 1)
@@ -556,10 +578,19 @@ object Substitution {
var scproof: Seq[K.SCProofStep] = Seq(K.Restate((leftOrigin |- rightOrigin).underlying, -1))
if (toLeft)
- scproof = scproof :+ K.LeftSubstIff(result1.underlying, scproof.length - 1, List(left.underlying -> right.underlying), K.LambdaFormulaFormula(Seq(H.underlyingLabel), leftForm.underlying))
+ scproof = scproof :+ K.LeftSubstIff(
+ result1.underlying,
+ scproof.length - 1,
+ List(K.LambdaTermFormula(Seq(), left.underlying) -> (K.LambdaTermFormula(Seq(), right.underlying))),
+ (Seq(H.underlyingLabel), leftForm.underlying)
+ )
if (toRight)
- scproof =
- scproof :+ K.RightSubstIff(result2.underlying, scproof.length - 1, List(left.underlying -> right.underlying), K.LambdaFormulaFormula(Seq(H.underlyingLabel), rightForm.underlying))
+ scproof = scproof :+ K.RightSubstIff(
+ result2.underlying,
+ scproof.length - 1,
+ List(K.LambdaTermFormula(Seq(), left.underlying) -> (K.LambdaTermFormula(Seq(), right.underlying))),
+ (Seq(H.underlyingLabel), rightForm.underlying)
+ )
val bot = newleft + phi |- newright
scproof = scproof :+ K.Restate(bot.underlying, scproof.length - 1)
diff --git a/lisa-sets/src/main/scala/lisa/automation/Tableau.scala b/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
index 1ab6e0673eefaa2a52b8d34e7505fffab66412ac..de6f6bcbd48a6d008c4b836c58d71eb95ca1a80b 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Tableau.scala
@@ -24,6 +24,9 @@ import scala.collection.immutable.HashSet
object Tableau extends ProofTactic with ProofSequentTactic with ProofFactSequentTactic {
+ var debug = true
+ def pr(s: Object) = if debug then println(s)
+
def apply(using lib: Library, proof: lib.Proof)(bot: F.Sequent): proof.ProofTacticJudgement = {
solve(bot) match {
case Some(value) => proof.ValidProofTactic(bot, value.steps, Seq())
diff --git a/lisa-sets/src/main/scala/lisa/automation/Tautology.scala b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
index f217058c289448d9fa29d215c0147d3fbc01e29f..476df8a588f235fb31935088ec0d932710bffe17 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
@@ -144,10 +144,20 @@ object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSeque
val seq1 = AugSequent((atom :: s.decisions._1, s.decisions._2), lambdaF(Seq(top())))
val proof1 = solveAugSequent(seq1, offset)
- val subst1 = RightSubstIff(atom :: s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- redF, offset + proof1.length - 1, List((atom, top())), lambdaF)
+ val subst1 = RightSubstIff(
+ atom :: s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- redF,
+ offset + proof1.length - 1,
+ List((LambdaTermFormula(Seq(), atom), LambdaTermFormula(Seq(), top()))),
+ (lambdaF.vars, lambdaF.body)
+ )
val seq2 = AugSequent((s.decisions._1, atom :: s.decisions._2), lambdaF(Seq(bot())))
val proof2 = solveAugSequent(seq2, offset + proof1.length + 1)
- val subst2 = RightSubstIff(Neg(atom) :: s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- redF, offset + proof1.length + proof2.length - 1 + 1, List((atom, bot())), lambdaF)
+ val subst2 = RightSubstIff(
+ Neg(atom) :: s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- redF,
+ offset + proof1.length + proof2.length - 1 + 1,
+ List((LambdaTermFormula(Seq(), atom), LambdaTermFormula(Seq(), bot()))),
+ (lambdaF.vars, lambdaF.body)
+ )
val red2 = Restate(s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- (redF, atom), offset + proof1.length + proof2.length + 2 - 1)
val cutStep = Cut(s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- redF, offset + proof1.length + proof2.length + 3 - 1, offset + proof1.length + 1 - 1, atom)
val redStep = Restate(s.decisions._1 ++ s.decisions._2.map((f: Formula) => Neg(f)) |- s.formula, offset + proof1.length + proof2.length + 4 - 1)
diff --git a/lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala b/lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala
index 67a1e6aa2bbab0796317b531360e273dc7be8bc2..1aeaf55ac25e1ea01d529e764bd0f547640611bb 100644
--- a/lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/Quantifiers.scala
@@ -55,7 +55,7 @@ object Quantifiers extends lisa.Main {
(x === y) /\ (y === z) |- (x === z)
) {
have((x === y) |- (x === y)) by Hypothesis
- thenHave(((x === y), (y === z)) |- (x === z)) by RightSubstEq.apply2
+ thenHave(((x === y), (y === z)) |- (x === z)) by RightSubstEq.withParametersSimple(List((y, z)), lambda(y, x === y))
thenHave(thesis) by Restate
}
@@ -95,7 +95,7 @@ object Quantifiers extends lisa.Main {
) {
have(exists(x, P(x) /\ (y === x)) |- P(y)) subproof {
have(P(x) |- P(x)) by Hypothesis
- thenHave((P(x), y === x) |- P(y)) by RightSubstEq.withParameters(List((y, x)), lambda(y, P(y)))
+ thenHave((P(x), y === x) |- P(y)) by RightSubstEq.withParametersSimple(List((y, x)), lambda(y, P(y)))
thenHave(P(x) /\ (y === x) |- P(y)) by Restate
thenHave(thesis) by LeftExists
}
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
index 996d55eea3ee24a4ed3480f6a4271283a2f2ccef..cbc135a146dbfdf02b470d360b36e318f69aaa0a 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/InductiveSets.scala
@@ -115,7 +115,7 @@ object InductiveSets extends lisa.Main {
val form = formulaVariable
val inductIff = thenHave(
(∀(t, in(t, z) <=> (∀(x, inductive(x) ==> in(t, x)))), inductive(z) <=> (in(∅, z) /\ ∀(y, in(y, z) ==> in(successor(y), z)))) |- inductive(z)
- ) by RightSubstIff(List((inductive(z), in(∅, z) /\ ∀(y, in(y, z) ==> in(successor(y), z)))), lambda(form, form))
+ ) by RightSubstIff.withParametersSimple(List((inductive(z), in(∅, z) /\ ∀(y, in(y, z) ==> in(successor(y), z)))), lambda(form, form))
val inductDef = have(inductive(z) <=> (in(∅, z) /\ ∀(y, in(y, z) ==> in(successor(y), z)))) by InstFunSchema(Map(x -> z))(inductive.definition)
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala
index 34737dbb5bdc1b526af55fd2aa1b3ac5fa3925f1..069d23d776c13387011e78d2979a10038c638573 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory.scala
@@ -97,7 +97,7 @@ object SetTheory extends lisa.Main {
// forward direction
have(fprop(z) |- fprop(z)) by Hypothesis
thenHave(fprop(z) /\ (z === a) |- fprop(z)) by Weakening
- thenHave((fprop(z) /\ (z === a), (z === a)) |- fprop(a)) by RightSubstEq.withParameters(List((z, a)), lambda(Seq(z), fprop(z)))
+ thenHave((fprop(z) /\ (z === a), (z === a)) |- fprop(a)) by RightSubstEq.withParametersSimple(List((z, a)), lambda(Seq(z), fprop(z)))
val forward = thenHave(fprop(z) |- (z === a) ==> fprop(a)) by Restate
// backward direction
@@ -177,10 +177,10 @@ object SetTheory extends lisa.Main {
val fwd = have(∃(a, in(z, a) /\ in(a, unorderedPair(x, y))) ==> (in(z, x) \/ in(z, y))) subproof {
have((in(z, a), a === x) |- in(z, a)) by Hypothesis
- val tax = thenHave((in(z, a), a === x) |- in(z, x)) by RightSubstEq.withParameters(List((a, x)), lambda(a, in(z, a)))
+ val tax = thenHave((in(z, a), a === x) |- in(z, x)) by RightSubstEq.withParametersSimple(List((a, x)), lambda(a, in(z, a)))
have((in(z, a), a === y) |- in(z, a)) by Hypothesis
- val tay = thenHave((in(z, a), a === y) |- in(z, y)) by RightSubstEq.withParameters(List((a, y)), lambda(a, in(z, a)))
+ val tay = thenHave((in(z, a), a === y) |- in(z, y)) by RightSubstEq.withParametersSimple(List((a, y)), lambda(a, in(z, a)))
have((in(z, a), (a === x) \/ (a === y)) |- (in(z, x), in(z, y))) by LeftOr(tax, tay)
thenHave((in(z, a), in(a, unorderedPair(x, y))) |- (in(z, x), in(z, y))) by Substitution.ApplyRules(upairax)
@@ -191,7 +191,7 @@ object SetTheory extends lisa.Main {
val bwd = have(((in(z, x) \/ in(z, y)) ==> ∃(a, in(z, a) /\ in(a, unorderedPair(x, y))))) subproof {
have((in(z, x), (a === x)) |- in(z, x)) by Hypothesis
- thenHave((in(z, x), (a === x)) |- in(z, a)) by RightSubstEq.withParameters(List((a, x)), lambda(a, in(z, a)))
+ thenHave((in(z, x), (a === x)) |- in(z, a)) by RightSubstEq.withParametersSimple(List((a, x)), lambda(a, in(z, a)))
thenHave((in(z, x), (a === x)) |- in(z, a) /\ ((a === x) \/ (a === y))) by Tautology
andThen(Substitution.applySubst(upairax, false))
thenHave((in(z, x), (a === x)) |- ∃(a, in(z, a) /\ in(a, unorderedPair(x, y)))) by RightExists
@@ -199,7 +199,7 @@ object SetTheory extends lisa.Main {
val tax = thenHave((in(z, x)) |- ∃(a, in(z, a) /\ in(a, unorderedPair(x, y)))) by Restate
have((in(z, y), (a === y)) |- in(z, y)) by Hypothesis
- thenHave((in(z, y), (a === y)) |- in(z, a)) by RightSubstEq.withParameters(List((a, y)), lambda(a, in(z, a)))
+ thenHave((in(z, y), (a === y)) |- in(z, a)) by RightSubstEq.withParametersSimple(List((a, y)), lambda(a, in(z, a)))
thenHave((in(z, y), (a === y)) |- in(z, a) /\ ((a === x) \/ (a === y))) by Tautology
andThen(Substitution.applySubst(upairax, false))
thenHave((in(z, y), (a === y)) |- ∃(a, in(z, a) /\ in(a, unorderedPair(x, y)))) by RightExists
@@ -260,7 +260,7 @@ object SetTheory extends lisa.Main {
have((in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)) <=> (in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x))) by Restate
val succEq = thenHave(
(successor(y) === union(unorderedPair(y, unorderedPair(y, y)))) |- (in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)) <=> (in(y, x) ==> in(successor(y), x))
- ) by RightSubstEq.withParameters(
+ ) by RightSubstEq.withParametersSimple(
List((successor(y), union(unorderedPair(y, unorderedPair(y, y))))),
lambda(z, (in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)) <=> (in(y, x) ==> in(z, x)))
)
@@ -291,7 +291,7 @@ object SetTheory extends lisa.Main {
∀(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)) <=> ∀(y, in(y, x) ==> in(successor(y), x)),
in(∅, x) /\ ∀(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x))
) |- in(∅, x) /\ ∀(y, in(y, x) ==> in(successor(y), x))
- ) by RightSubstIff(
+ ) by RightSubstIff.withParametersSimple(
List((∀(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)), ∀(y, in(y, x) ==> in(successor(y), x)))),
lambda(form, in(∅, x) /\ form)
)
@@ -301,7 +301,7 @@ object SetTheory extends lisa.Main {
∀(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)) <=> ∀(y, in(y, x) ==> in(successor(y), x)),
in(∅, x) /\ ∀(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x))
) |- inductive(x)
- ) by RightSubstIff(List((inductive(x), in(∅, x) /\ ∀(y, in(y, x) ==> in(successor(y), x)))), lambda(form, form))
+ ) by RightSubstIff.withParametersSimple(List((inductive(x), in(∅, x) /\ ∀(y, in(y, x) ==> in(successor(y), x)))), lambda(form, form))
val cut1 = have(
(
∀(y, in(y, x) ==> in(union(unorderedPair(y, unorderedPair(y, y))), x)) <=> ∀(y, in(y, x) ==> in(successor(y), x)),
@@ -532,11 +532,17 @@ object SetTheory extends lisa.Main {
// backward direction
// a = c and b = d => up ab = up cd (and the other case)
have(unorderedPair(a, b) === unorderedPair(a, b)) by RightRefl
- thenHave((a === c, b === d) |- unorderedPair(a, b) === unorderedPair(c, d)) by RightSubstEq.withParameters(List((a, c), (b, d)), lambda(Seq(x, y), unorderedPair(a, b) === unorderedPair(x, y)))
+ thenHave((a === c, b === d) |- unorderedPair(a, b) === unorderedPair(c, d)) by RightSubstEq.withParametersSimple(
+ List((a, c), (b, d)),
+ lambda(Seq(x, y), unorderedPair(a, b) === unorderedPair(x, y))
+ )
val lhs = thenHave(Set((a === c) /\ (b === d)) |- unorderedPair(a, b) === unorderedPair(c, d)) by Restate
have(unorderedPair(a, b) === unorderedPair(b, a)) by InstFunSchema(ScalaMap(x -> a, y -> b))(unorderedPairSymmetry)
- thenHave((a === d, b === c) |- (unorderedPair(a, b) === unorderedPair(c, d))) by RightSubstEq.withParameters(List((a, d), (b, c)), lambda(Seq(x, y), unorderedPair(a, b) === unorderedPair(y, x)))
+ thenHave((a === d, b === c) |- (unorderedPair(a, b) === unorderedPair(c, d))) by RightSubstEq.withParametersSimple(
+ List((a, d), (b, c)),
+ lambda(Seq(x, y), unorderedPair(a, b) === unorderedPair(y, x))
+ )
val rhs = thenHave(Set((a === d) /\ (b === c)) |- (unorderedPair(a, b) === unorderedPair(c, d))) by Restate
have((((a === d) /\ (b === c)) \/ ((a === c) /\ (b === d))) |- (unorderedPair(a, b) === unorderedPair(c, d))) by LeftOr(lhs, rhs)
@@ -593,7 +599,7 @@ object SetTheory extends lisa.Main {
// backward direction
// x === y |- {x} === {y}
have(singleton(x) === singleton(x)) by RightRefl
- thenHave((x === y) |- singleton(x) === singleton(y)) by RightSubstEq.withParameters(List((x, y)), lambda(a, singleton(x) === singleton(a)))
+ thenHave((x === y) |- singleton(x) === singleton(y)) by RightSubstEq.withParametersSimple(List((x, y)), lambda(a, singleton(x) === singleton(a)))
val bwd = thenHave((x === y) ==> (singleton(x) === singleton(y))) by Restate
have((singleton(x) === singleton(y)) <=> (x === y)) by RightIff(fwd, bwd)
@@ -619,9 +625,9 @@ object SetTheory extends lisa.Main {
val pairAxab = have(in(z, unorderedPair(a, b)) |- (z === a) \/ (z === b)) by Tautology.from(pairAxiom of (x -> a, y -> b))
have(in(a, x) /\ in(b, x) |- in(a, x)) by Restate
- val za = thenHave((in(a, x) /\ in(b, x), (z === a)) |- in(z, x)) by RightSubstEq.withParameters(List((z, a)), lambda(a, in(a, x)))
+ val za = thenHave((in(a, x) /\ in(b, x), (z === a)) |- in(z, x)) by RightSubstEq.withParametersSimple(List((z, a)), lambda(a, in(a, x)))
have(in(a, x) /\ in(b, x) |- in(b, x)) by Restate
- val zb = thenHave((in(a, x) /\ in(b, x), (z === b)) |- in(z, x)) by RightSubstEq.withParameters(List((z, b)), lambda(a, in(a, x)))
+ val zb = thenHave((in(a, x) /\ in(b, x), (z === b)) |- in(z, x)) by RightSubstEq.withParametersSimple(List((z, b)), lambda(a, in(a, x)))
val zab = have((in(a, x) /\ in(b, x), (z === a) \/ (z === b)) |- in(z, x)) by LeftOr(za, zb)
@@ -665,7 +671,7 @@ object SetTheory extends lisa.Main {
// (a === c) /\ (b === d) ==> pair a b === pair c d
val fwd = have(((a === c) /\ (b === d)) ==> (pair(a, b) === pair(c, d))) subproof {
have((pair(a, b) === pair(a, b))) by RightRefl
- thenHave(Set((a === c), (b === d)) |- (pair(a, b) === pair(c, d))) by RightSubstEq.withParameters(List((a, c), (b, d)), lambda(Seq(x, y), pair(a, b) === pair(x, y)))
+ thenHave(Set((a === c), (b === d)) |- (pair(a, b) === pair(c, d))) by RightSubstEq.withParametersSimple(List((a, c), (b, d)), lambda(Seq(x, y), pair(a, b) === pair(x, y)))
thenHave(thesis) by Restate
}
@@ -680,7 +686,7 @@ object SetTheory extends lisa.Main {
c
))) \/ ((unorderedPair(a, b) === singleton(c)) /\ (singleton(a) === unorderedPair(c, d))))
) |- (((unorderedPair(a, b) === unorderedPair(c, d)) /\ (singleton(a) === singleton(c))) \/ ((unorderedPair(a, b) === singleton(c)) /\ (singleton(a) === unorderedPair(c, d))))
- ) by RightSubstIff(
+ ) by RightSubstIff.withParametersSimple(
List(
(
(unorderedPair(unorderedPair(a, b), singleton(a)) === unorderedPair(unorderedPair(c, d), singleton(c))),
@@ -749,7 +755,7 @@ object SetTheory extends lisa.Main {
// now we need to show that the assumption is indeed true
// this requires destruction of the existential quantifier in lhs
have(in(x, X) /\ ∀(z, in(z, X) ==> !in(z, x)) |- in(x, X) /\ ∀(z, in(z, X) ==> !in(z, x))) by Hypothesis
- val innerRhs2 = thenHave((in(y, X) /\ ∀(z, in(z, X) ==> !in(z, y)), x === y) |- in(x, X) /\ ∀(z, in(z, X) ==> !in(z, x))) by LeftSubstEq.withParameters(
+ val innerRhs2 = thenHave((in(y, X) /\ ∀(z, in(z, X) ==> !in(z, y)), x === y) |- in(x, X) /\ ∀(z, in(z, X) ==> !in(z, x))) by LeftSubstEq.withParametersSimple(
List((x, y)),
lambda(Seq(y), in(y, X) /\ ∀(z, in(z, X) ==> !in(z, y)))
)
@@ -1010,7 +1016,7 @@ object SetTheory extends lisa.Main {
have((in(t, z) <=> (in(t, x) /\ ∀(y, P(y) ==> in(t, y)))) |- in(t, z) <=> (in(t, x) /\ ∀(y, P(y) ==> in(t, y)))) by Hypothesis
val rhs = thenHave(
Set((in(t, z) <=> (in(t, x) /\ ∀(y, P(y) ==> in(t, y)))), (∀(y, P(y) ==> in(t, y)) <=> (in(t, x) /\ ∀(y, P(y) ==> in(t, y))))) |- (in(t, z) <=> (∀(y, P(y) ==> in(t, y))))
- ) by RightSubstIff(List((∀(y, P(y) ==> in(t, y)), (in(t, x) /\ ∀(y, P(y) ==> in(t, y))))), lambda(form, in(t, z) <=> (form)))
+ ) by RightSubstIff.withParametersSimple(List((∀(y, P(y) ==> in(t, y)), (in(t, x) /\ ∀(y, P(y) ==> in(t, y))))), lambda(form, in(t, z) <=> (form)))
have((P(x), (in(t, z) <=> (in(t, x) /\ ∀(y, P(y) ==> in(t, y))))) |- in(t, z) <=> (∀(y, P(y) ==> in(t, y)))) by Cut(lhs, rhs)
thenHave((P(x), ∀(t, (in(t, z) <=> (in(t, x) /\ ∀(y, P(y) ==> in(t, y)))))) |- in(t, z) <=> (∀(y, P(y) ==> in(t, y)))) by LeftForall
@@ -1458,7 +1464,7 @@ object SetTheory extends lisa.Main {
// (a, b) \in x * y ⟹ a ∈ x ∧ b ∈ y
val fwd = have(in(pair(a, b), cartesianProduct(x, y)) ==> (in(a, x) /\ in(b, y))) subproof {
have((a === c, b === d, in(c, x) /\ in(d, y)) |- in(c, x) /\ in(d, y)) by Hypothesis
- thenHave((a === c, b === d, in(c, x) /\ in(d, y)) |- in(a, x) /\ in(b, y)) by RightSubstEq.withParameters(List((a, c), (b, d)), lambda(Seq(a, b), in(a, x) /\ in(b, y)))
+ thenHave((a === c, b === d, in(c, x) /\ in(d, y)) |- in(a, x) /\ in(b, y)) by RightSubstEq.withParametersSimple(List((a, c), (b, d)), lambda(Seq(a, b), in(a, x) /\ in(b, y)))
thenHave(Set((a === c) /\ (b === d), in(c, x) /\ in(d, y)) |- in(a, x) /\ in(b, y)) by Restate
andThen(Substitution.applySubst(pairExtensionality))
thenHave((pair(a, b) === pair(c, d)) /\ in(c, x) /\ in(d, y) |- in(a, x) /\ in(b, y)) by Restate
@@ -1485,10 +1491,16 @@ object SetTheory extends lisa.Main {
have(prem |- in(unorderedPair(a, b), powerSet(setUnion(x, y)))) by Weakening(unorderedPairInPowerSet of (x -> setUnion(x, y)))
val zab =
- thenHave((prem, (z === unorderedPair(a, b))) |- in(z, powerSet(setUnion(x, y)))) by RightSubstEq.withParameters(List((z, unorderedPair(a, b))), lambda(a, in(a, powerSet(setUnion(x, y)))))
+ thenHave((prem, (z === unorderedPair(a, b))) |- in(z, powerSet(setUnion(x, y)))) by RightSubstEq.withParametersSimple(
+ List((z, unorderedPair(a, b))),
+ lambda(a, in(a, powerSet(setUnion(x, y))))
+ )
have(prem |- in(unorderedPair(a, a), powerSet(setUnion(x, y)))) by Weakening(unorderedPairInPowerSet of (x -> setUnion(x, y), b -> a))
val zaa =
- thenHave((prem, (z === unorderedPair(a, a))) |- in(z, powerSet(setUnion(x, y)))) by RightSubstEq.withParameters(List((z, unorderedPair(a, a))), lambda(a, in(a, powerSet(setUnion(x, y)))))
+ thenHave((prem, (z === unorderedPair(a, a))) |- in(z, powerSet(setUnion(x, y)))) by RightSubstEq.withParametersSimple(
+ List((z, unorderedPair(a, a))),
+ lambda(a, in(a, powerSet(setUnion(x, y))))
+ )
val cutRhs = have((prem, (z === unorderedPair(a, b)) \/ (z === singleton(a))) |- in(z, powerSet(setUnion(x, y)))) by LeftOr(zab, zaa)
@@ -1849,7 +1861,7 @@ object SetTheory extends lisa.Main {
a,
in(pair(t, a), r)
))
- ) by RightSubstIff(List((∃(a, in(pair(t, a), r)), in(t, union(union(r))) /\ ∃(a, in(pair(t, a), r)))), lambda(h, in(t, z) <=> h))
+ ) by RightSubstIff.withParametersSimple(List((∃(a, in(pair(t, a), r)), in(t, union(union(r))) /\ ∃(a, in(pair(t, a), r)))), lambda(h, in(t, z) <=> h))
have((in(t, z) <=> (in(t, union(union(r))) /\ ∃(a, in(pair(t, a), r)))) |- in(t, z) <=> (∃(a, in(pair(t, a), r)))) by Cut(subst, cutRhs)
thenHave(∀(t, in(t, z) <=> (in(t, union(union(r))) /\ ∃(a, in(pair(t, a), r)))) |- in(t, z) <=> (∃(a, in(pair(t, a), r)))) by LeftForall
thenHave(∀(t, in(t, z) <=> (in(t, union(union(r))) /\ ∃(a, in(pair(t, a), r)))) |- ∀(t, in(t, z) <=> (∃(a, in(pair(t, a), r))))) by RightForall
@@ -1917,7 +1929,7 @@ object SetTheory extends lisa.Main {
a,
in(pair(a, t), r)
))
- ) by RightSubstIff(List((∃(a, in(pair(a, t), r)), in(t, union(union(r))) /\ ∃(a, in(pair(a, t), r)))), lambda(h, in(t, z) <=> h))
+ ) by RightSubstIff.withParametersSimple(List((∃(a, in(pair(a, t), r)), in(t, union(union(r))) /\ ∃(a, in(pair(a, t), r)))), lambda(h, in(t, z) <=> h))
have((in(t, z) <=> (in(t, union(union(r))) /\ ∃(a, in(pair(a, t), r)))) |- in(t, z) <=> (∃(a, in(pair(a, t), r)))) by Cut(subst, cutRhs)
thenHave(∀(t, in(t, z) <=> (in(t, union(union(r))) /\ ∃(a, in(pair(a, t), r)))) |- in(t, z) <=> (∃(a, in(pair(a, t), r)))) by LeftForall
thenHave(∀(t, in(t, z) <=> (in(t, union(union(r))) /\ ∃(a, in(pair(a, t), r)))) |- ∀(t, in(t, z) <=> (∃(a, in(pair(a, t), r))))) by RightForall
@@ -2373,10 +2385,11 @@ object SetTheory extends lisa.Main {
val lhs = have(prem /\ ((z === y) <=> in(pair(x, y), f)) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ ⊤))) subproof {
val iff = have(prem |- (in(pair(x, y), f)) <=> (prem ==> in(pair(x, y), f))) by Restate
have(prem /\ ((z === y) <=> in(pair(x, y), f)) |- ((z === y) <=> in(pair(x, y), f))) by Restate
- val subst = thenHave((prem /\ ((z === y) <=> in(pair(x, y), f)), (in(pair(x, y), f)) <=> (prem ==> in(pair(x, y), f))) |- ((z === y) <=> (prem ==> in(pair(x, y), f)))) by RightSubstIff(
- List(((in(pair(x, y), f)), (prem ==> in(pair(x, y), f)))),
- lambda(h, ((z === y) <=> h))
- )
+ val subst = thenHave((prem /\ ((z === y) <=> in(pair(x, y), f)), (in(pair(x, y), f)) <=> (prem ==> in(pair(x, y), f))) |- ((z === y) <=> (prem ==> in(pair(x, y), f)))) by RightSubstIff
+ .withParametersSimple(
+ List(((in(pair(x, y), f)), (prem ==> in(pair(x, y), f)))),
+ lambda(h, ((z === y) <=> h))
+ )
have((prem /\ ((z === y) <=> in(pair(x, y), f)), prem) |- ((z === y) <=> (prem ==> in(pair(x, y), f)))) by Cut(iff, subst)
thenHave(thesis) by Restate
@@ -2386,7 +2399,7 @@ object SetTheory extends lisa.Main {
val topIff = have(prem |- (!prem ==> (y === ∅)) <=> ⊤) by Restate
val topSubst = have(
(prem /\ ((z === y) <=> in(pair(x, y), f)), ((!prem ==> (y === ∅)) <=> ⊤)) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ (!prem ==> (y === ∅))))
- ) by RightSubstIff(List(((!prem ==> (y === ∅)), ⊤)), lambda(h, ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ h))))(lhs)
+ ) by RightSubstIff.withParametersSimple(List(((!prem ==> (y === ∅)), ⊤)), lambda(h, ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ h))))(lhs)
have((prem /\ ((z === y) <=> in(pair(x, y), f)), prem) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ (!prem ==> (y === ∅))))) by Cut(topIff, topSubst)
thenHave((prem, ((z === y) <=> in(pair(x, y), f))) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ (!prem ==> (y === ∅))))) by Restate
@@ -2417,7 +2430,7 @@ object SetTheory extends lisa.Main {
have(!prem /\ ((z === y) <=> (y === ∅)) |- ((z === y) <=> (y === ∅))) by Restate
val subst = thenHave(
(!prem /\ ((z === y) <=> (y === ∅)), ((y === ∅)) <=> (!prem ==> (y === ∅))) |- ((z === y) <=> (!prem ==> (y === ∅)))
- ) by RightSubstIff(List((((y === ∅)), (!prem ==> (y === ∅)))), lambda(h, ((z === y) <=> h)))
+ ) by RightSubstIff.withParametersSimple(List((((y === ∅)), (!prem ==> (y === ∅)))), lambda(h, ((z === y) <=> h)))
have((!prem /\ ((z === y) <=> (y === ∅)), !prem) |- ((z === y) <=> (!prem ==> (y === ∅)))) by Cut(iff, subst)
thenHave(thesis) by Restate
@@ -2427,7 +2440,7 @@ object SetTheory extends lisa.Main {
val topIff = have(!prem |- (prem ==> in(pair(x, y), f)) <=> ⊤) by Restate
val topSubst = have(
(!prem /\ ((z === y) <=> (y === ∅)), ((prem ==> in(pair(x, y), f)) <=> ⊤)) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ (!prem ==> (y === ∅))))
- ) by RightSubstIff(List(((prem ==> in(pair(x, y), f)), ⊤)), lambda(h, ((z === y) <=> ((!prem ==> (y === ∅)) /\ h))))(lhs)
+ ) by RightSubstIff.withParametersSimple(List(((prem ==> in(pair(x, y), f)), ⊤)), lambda(h, ((z === y) <=> ((!prem ==> (y === ∅)) /\ h))))(lhs)
have((!prem /\ ((z === y) <=> (y === ∅)), !prem) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ (!prem ==> (y === ∅))))) by Cut(topIff, topSubst)
thenHave((!prem, ((z === y) <=> (y === ∅))) |- ((z === y) <=> ((prem ==> in(pair(x, y), f)) /\ (!prem ==> (y === ∅))))) by Restate
@@ -3216,7 +3229,7 @@ object SetTheory extends lisa.Main {
inRangeImpliesPullbackExists of (z -> y),
functionFromImpliesFunctional of (y -> powerSet(x))
)
- val xeqdom = thenHave((ydef, surjective(f, x, powerSet(x)), (relationDomain(f) === x)) |- ∃(z, in(z, x) /\ (app(f, z) === y))) by RightSubstEq.withParameters(
+ val xeqdom = thenHave((ydef, surjective(f, x, powerSet(x)), (relationDomain(f) === x)) |- ∃(z, in(z, x) /\ (app(f, z) === y))) by RightSubstEq.withParametersSimple(
List((x, relationDomain(f))),
lambda(x, ∃(z, in(z, x) /\ (app(f, z) === y)))
)
@@ -3231,7 +3244,7 @@ object SetTheory extends lisa.Main {
have(ydef |- ydef) by Hypothesis
thenHave(ydef |- in(z, y) <=> (in(z, x) /\ !in(z, app(f, z)))) by InstantiateForall(z)
thenHave((ydef, in(z, x), (app(f, z) === y)) |- in(z, y) <=> (in(z, x) /\ !in(z, app(f, z)))) by Weakening
- thenHave((ydef, in(z, x), (app(f, z) === y)) |- in(z, app(f, z)) <=> (in(z, x) /\ !in(z, app(f, z)))) by RightSubstEq.withParameters(
+ thenHave((ydef, in(z, x), (app(f, z) === y)) |- in(z, app(f, z)) <=> (in(z, x) /\ !in(z, app(f, z)))) by RightSubstEq.withParametersSimple(
List((y, app(f, z))),
lambda(y, in(z, y) <=> (in(z, x) /\ !in(z, app(f, z))))
)
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory2.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory2.scala
index 55690ed41e297ffeaa96adfc1cad0b480716960e..b3d69dcc607dc99de300992e3a9df47510825929 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory2.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/SetTheory2.scala
@@ -1,5 +1,9 @@
package lisa.maths.settheory
+/**
+ * Revamp of the set theory library from scratch, since most of the current one is severely outdated.
+ * We can make a better presentation and organisation of theorems, better automation, uniform comments/latex tags, etc.
+ */
object SetTheory2 extends lisa.Main {
import lisa.maths.settheory.SetTheory.*
// import Comprehensions.*
diff --git a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
index 3e4d406f2931f1ac5056726358b8631d908b8419..4ca6df8a3c4bfc473835d925676d2776e2324472 100644
--- a/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
+++ b/lisa-sets/src/main/scala/lisa/maths/settheory/orderings/Recursion.scala
@@ -1873,8 +1873,6 @@ object Recursion extends lisa.Main {
val sPsi = SchematicPredicateLabel("P", 3)
have(forall(y, in(y, initialSegment(p, x)) ==> existsOne(g, fun(g, y)))) by Restate
- println(existsOne(g, fun(g, y)))
- println(lastStep.bot)
have(exists(w, forall(t, in(t, w) <=> exists(y, in(y, initialSegment(p, x)) /\ fun(t, y))))) by Tautology.from(
lastStep,
strictReplacementSchema of (A -> initialSegment(p, x), R -> lambda((y, g), fun(g, y)))
@@ -1882,8 +1880,6 @@ object Recursion extends lisa.Main {
}
have(thesis) by Tautology.from(lastStep, funExists)
- println("thesis")
- println(lastStep.bot)
}
/**
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index 39bdc5df9e9b778e4a2cde5501d2e3e423d53b46..356b95d845b0c0a1407103759dee0fd0007a695e 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -480,6 +480,7 @@ trait Common {
*/
sealed trait SchematicAtomicLabel[A <: (Formula | (Seq[Term] |-> Formula)) & LisaObject[A]] extends AtomicLabel[A] with SchematicLabel[A] {
this: A & LisaObject[A] =>
+ val underlyingLabel: K.SchematicAtomicLabel
override def rename(newid: Identifier): SchematicAtomicLabel[A]
def freshRename(taken: Iterable[Identifier]): SchematicAtomicLabel[A]
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index 44eb047b503149b85d5c06aafbee1f6044758cb4..bd6bc96696d4b4f178c4d6936a53c1965f557dc9 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -10,7 +10,7 @@ import lisa.utils.K
import scala.annotation.showAsInfix
-trait Sequents extends Common with lisa.fol.Lambdas {
+trait Sequents extends Common with lisa.fol.Lambdas with Predef {
object SequentInstantiationRule extends ProofTactic
given ProofTactic = SequentInstantiationRule
@@ -30,7 +30,7 @@ trait Sequents extends Common with lisa.fol.Lambdas {
* @param map
* @return
*/
- def substituteWithProof(map: Map[SchematicLabel[_], _ <: LisaObject[_]]): (Sequent, Seq[K.SCProofStep]) = {
+ def instantiateWithProof(map: Map[SchematicLabel[_], _ <: LisaObject[_]], index: Int): (Sequent, Seq[K.SCProofStep]) = {
val mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]] =
map.collect[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]](p =>
@@ -70,7 +70,27 @@ trait Sequents extends Common with lisa.fol.Lambdas {
}
}
)
- (substituteUnsafe(map), substituteWithProofLikeKernel(mConn, mPred, mTerm))
+ (substituteUnsafe(map), instantiateWithProofLikeKernel(mConn, mPred, mTerm, index))
+
+ }
+
+ def instantiateForallWithProof(args: Seq[Term], index: Int): (Sequent, Seq[K.SCProofStep]) = {
+ if this.right.size != 1 then throw new IllegalArgumentException("Right side of sequent must be a single universally quantified formula")
+ this.right.head match {
+ case r @ Forall(x, f) =>
+ val t = args.head
+ val newf = f.substitute(x := t)
+ val s0 = K.Hypothesis((newf |- newf).underlying, newf.underlying)
+ val s1 = K.LeftForall((r |- newf).underlying, index + 1, f.underlying, x.underlyingLabel, t.underlying)
+ val s2 = K.Cut((this.left |- newf).underlying, index, index + 2, r.underlying)
+ if args.tail.isEmpty then (this.left |- newf, Seq(s0, s1, s2))
+ else
+ (this.left |- newf).instantiateForallWithProof(args.tail, index + 3) match {
+ case (s, p) => (s, Seq(s0, s1, s2) ++ p)
+ }
+
+ case _ => throw new IllegalArgumentException("Right side of sequent must be a single universaly quantified formula")
+ }
}
@@ -83,10 +103,11 @@ trait Sequents extends Common with lisa.fol.Lambdas {
* @param mTerm The substitution of function schemas
* @return
*/
- def substituteWithProofLikeKernel(
+ def instantiateWithProofLikeKernel(
mCon: Map[SchematicConnectorLabel[?], LambdaExpression[Formula, Formula, ?]],
mPred: Map[SchematicPredicateLabel[?] | VariableFormula, LambdaExpression[Term, Formula, ?]],
- mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]]
+ mTerm: Map[SchematicFunctionLabel[?] | Variable, LambdaExpression[Term, Term, ?]],
+ index: Int
): Seq[K.SCProofStep] = {
val premiseSequent = this.underlying
val mConK = mCon.map((sl, le) => (sl.underlyingLabel, underlyingLFF(le)))
@@ -104,7 +125,7 @@ trait Sequents extends Common with lisa.fol.Lambdas {
)
val botK = lisa.utils.KernelHelpers.instantiateSchemaInSequent(premiseSequent, mConK, mPredK, mTermK)
val smap = Map[SchematicLabel[?], LisaObject[?]]() ++ mCon ++ mPred ++ mTerm
- Seq(K.InstSchema(botK, -1, mConK, mPredK, mTermK))
+ Seq(K.InstSchema(botK, index, mConK, mPredK, mTermK))
}
infix def +<<(f: Formula): Sequent = this.copy(left = this.left + f)
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
index 320ea5a6e74496b10f24e49dfca4c0c5f3376d43..678cd18cd1f32ad499c04558e0ae76c6d3759069 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/BasicStepTactic.scala
@@ -1111,26 +1111,43 @@ object BasicStepTactic {
* </pre>
*/
object LeftSubstEq extends ProofTactic {
- def withParameters(using lib: Library, proof: lib.Proof)(
+
+ def withParametersSimple(using lib: Library, proof: lib.Proof)(
equals: List[(F.Term, F.Term)],
lambdaPhi: F.LambdaExpression[F.Term, F.Formula, ?]
)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
+ withParameters(equals.map { case (a, b) => (F.lambda(Seq(), a), F.lambda(Seq(), b)) }, (lambdaPhi.bounds.asInstanceOf[Seq[F.SchematicTermLabel[?]]], lambdaPhi.body))(premise)(bot)
+ }
+ def withParameters(using lib: Library, proof: lib.Proof)(
+ equals: List[(F.LambdaExpression[F.Term, F.Term, ?], F.LambdaExpression[F.Term, F.Term, ?])],
+ lambdaPhi: (Seq[F.SchematicTermLabel[?]], F.Formula)
+ )(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
lazy val premiseSequent = proof.getSequent(premise).underlying
lazy val botK = bot.underlying
- lazy val equalsK = equals.map((p: (F.Term, F.Term)) => (p._1.underlying, p._2.underlying))
-
- lazy val lambdaPhiK = F.underlyingLTF(lambdaPhi)
- lazy val (s_es, t_es) = equalsK.unzip
- lazy val phi_s = lambdaPhiK(s_es)
- lazy val phi_t = lambdaPhiK(t_es)
- lazy val equalities = equalsK map { case (s, t) => K.AtomicFormula(K.equality, Seq(s, t)) }
+ lazy val equalsK = equals.map(p => (p._1.underlyingLTT, p._2.underlyingLTT))
+ lazy val lambdaPhiK = (lambdaPhi._1.map(_.underlyingLabel), lambdaPhi._2.underlying)
+
+ val (s_es, t_es) = equalsK.unzip
+ val (phi_args, phi_body) = lambdaPhiK
+ if (phi_args.size != s_es.size)
+ return proof.InvalidProofTactic("The number of arguments of φ must be the same as the number of equalities.")
+ else if (equalsK.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ return proof.InvalidProofTactic("The arities of symbols in φ must be the same as the arities of equalities.")
+
+ val phi_s = K.instantiateTermSchemas(phi_body, (phi_args zip s_es).toMap)
+ val phi_t = K.instantiateTermSchemas(phi_body, (phi_args zip t_es).toMap)
+ val sEqT_es = equalsK map { case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = K.AtomicFormula(K.equality, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(K.VariableTerm))))
+ (s.vars).foldLeft(base: K.Formula) { case (acc, s_arg) => K.BinderFormula(K.Forall, s_arg, acc) }
+ }
if (!K.isSameSet(botK.right, premiseSequent.right))
proof.InvalidProofTactic("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
else if (
- !K.isSameSet(botK.left + phi_s, premiseSequent.left ++ equalities + phi_t) &&
- !K.isSameSet(botK.left + phi_t, premiseSequent.left ++ equalities + phi_s)
+ !K.isSameSet(botK.left + phi_s, premiseSequent.left ++ sEqT_es + phi_t) &&
+ !K.isSameSet(botK.left + phi_t, premiseSequent.left ++ sEqT_es + phi_s)
)
proof.InvalidProofTactic("Left-hand side of the conclusion + φ(s_) is not the same as left-hand side of the premise + (s=t)_ + φ(t_) (or with s_ and t_ swapped).")
else
@@ -1146,22 +1163,38 @@ object BasicStepTactic {
* </pre>
*/
object RightSubstEq extends ProofTactic {
- def withParameters(using lib: Library, proof: lib.Proof)(
+ def withParametersSimple(using lib: Library, proof: lib.Proof)(
equals: List[(F.Term, F.Term)],
lambdaPhi: F.LambdaExpression[F.Term, F.Formula, ?]
)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
+ withParameters(equals.map { case (a, b) => (F.lambda(Seq(), a), F.lambda(Seq(), b)) }, (lambdaPhi.bounds.asInstanceOf[Seq[F.SchematicTermLabel[?]]], lambdaPhi.body))(premise)(bot)
+ }
- lazy val lambdaPhiK = F.underlyingLTF(lambdaPhi)
+ def withParameters(using lib: Library, proof: lib.Proof)(
+ equals: List[(F.LambdaExpression[F.Term, F.Term, ?], F.LambdaExpression[F.Term, F.Term, ?])],
+ lambdaPhi: (Seq[F.SchematicTermLabel[?]], F.Formula)
+ )(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
lazy val premiseSequent = proof.getSequent(premise).underlying
lazy val botK = bot.underlying
- lazy val equalsK = equals.map((p: (F.Term, F.Term)) => (p._1.underlying, p._2.underlying))
-
- lazy val (s_es, t_es) = equalsK.unzip
- lazy val phi_s = lambdaPhiK(s_es)
- lazy val phi_t = lambdaPhiK(t_es)
- lazy val equalities = equalsK map { case (s, t) => K.AtomicFormula(K.equality, Seq(s, t)) }
+ lazy val equalsK = equals.map(p => (p._1.underlyingLTT, p._2.underlyingLTT))
+ lazy val lambdaPhiK = (lambdaPhi._1.map(_.underlyingLabel), lambdaPhi._2.underlying)
+
+ val (s_es, t_es) = equalsK.unzip
+ val (phi_args, phi_body) = lambdaPhiK
+ if (phi_args.size != s_es.size)
+ return proof.InvalidProofTactic("The number of arguments of φ must be the same as the number of equalities.")
+ else if (equalsK.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ return proof.InvalidProofTactic("The arities of symbols in φ must be the same as the arities of equalities.")
+
+ val phi_s = K.instantiateTermSchemas(phi_body, (phi_args zip s_es).toMap)
+ val phi_t = K.instantiateTermSchemas(phi_body, (phi_args zip t_es).toMap)
+ val sEqT_es = equalsK map { case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = K.AtomicFormula(K.equality, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(K.VariableTerm))))
+ (s.vars).foldLeft(base: K.Formula) { case (acc, s_arg) => K.BinderFormula(K.Forall, s_arg, acc) }
+ }
- if (!K.isSameSet(botK.left, premiseSequent.left ++ equalities))
+ if (!K.isSameSet(botK.left, premiseSequent.left ++ sEqT_es))
proof.InvalidProofTactic("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (s=t)_.")
else if (
!K.isSameSet(botK.right + phi_s, premiseSequent.right + phi_t) &&
@@ -1173,26 +1206,6 @@ object BasicStepTactic {
}
- def apply2(using lib: Library, proof: lib.Proof)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
- lazy val premiseSequent = proof.getSequent(premise)
- val premRight = F.AppliedConnector(F.Or, premiseSequent.right.toSeq)
- val botRight = F.AppliedConnector(F.Or, bot.right.toSeq)
-
- val equalities = bot.left.toSeq.collect { case F.AppliedPredicate(F.equality, Seq(l, r)) => (l, r) }
- val undereqs = equalities.toList.map(p => (p._1.underlying, p._2.underlying))
- val canReach = UnificationUtils.getContextFormula(
- first = premRight,
- second = botRight,
- confinedTermRules = equalities,
- takenTermVariables = equalities.flatMap(e => e._1.freeVariables ++ e._2.freeVariables).toSet
- )
-
- if (canReach.isEmpty) proof.InvalidProofTactic("Could not find a set of equalities to rewrite premise into conclusion successfully.")
- else
- val termLambda = canReach.get.toLambdaTF
- withParameters(equalities.toList, termLambda)(premise)(bot)
-
- }
}
/**
@@ -1203,26 +1216,43 @@ object BasicStepTactic {
* </pre>
*/
object LeftSubstIff extends ProofTactic {
- def apply(using lib: Library, proof: lib.Proof)(
+ def withParametersSimple(using lib: Library, proof: lib.Proof)(
equals: List[(F.Formula, F.Formula)],
lambdaPhi: F.LambdaExpression[F.Formula, F.Formula, ?]
)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
+ withParameters(equals.map { case (a, b) => (F.lambda(Seq(), a), F.lambda(Seq(), b)) }, (lambdaPhi.bounds.asInstanceOf[Seq[F.SchematicAtomicLabel[?]]], lambdaPhi.body))(premise)(bot)
+ }
+
+ def withParameters(using lib: Library, proof: lib.Proof)(
+ equals: List[(F.LambdaExpression[F.Term, F.Formula, ?], F.LambdaExpression[F.Term, F.Formula, ?])],
+ lambdaPhi: (Seq[F.SchematicAtomicLabel[?]], F.Formula)
+ )(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
lazy val premiseSequent = proof.getSequent(premise).underlying
lazy val botK = bot.underlying
- lazy val equalsK = equals.map((p: (F.Formula, F.Formula)) => (p._1.underlying, p._2.underlying))
- lazy val lambdaPhiK = F.underlyingLFF(lambdaPhi)
-
- lazy val (psi_es, tau_es) = equalsK.unzip
- lazy val phi_psi = lambdaPhiK(psi_es)
- lazy val phi_tau = lambdaPhiK(tau_es)
- lazy val implications = equalsK map { case (s, t) => K.ConnectorFormula(K.Iff, Seq(s, t)) }
+ lazy val equalsK = equals.map(p => (p._1.underlyingLTF, p._2.underlyingLTF))
+ lazy val lambdaPhiK = (lambdaPhi._1.map(_.underlyingLabel), lambdaPhi._2.underlying)
+
+ val (psi_s, tau_s) = equalsK.unzip
+ val (phi_args, phi_body) = lambdaPhiK
+ if (phi_args.size != psi_s.size)
+ return proof.InvalidProofTactic("The number of arguments of φ must be the same as the number of equalities.")
+ else if (equalsK.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ return proof.InvalidProofTactic("The arities of symbols in φ must be the same as the arities of equalities.")
+
+ val phi_psi = K.instantiatePredicateSchemas(phi_body, (phi_args zip psi_s).toMap)
+ val phi_tau = K.instantiatePredicateSchemas(phi_body, (phi_args zip tau_s).toMap)
+ val psiIffTau = equalsK map { case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = K.ConnectorFormula(K.Iff, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(K.VariableTerm))))
+ (s.vars).foldLeft(base: K.Formula) { case (acc, s_arg) => K.BinderFormula(K.Forall, s_arg, acc) }
+ }
if (!K.isSameSet(botK.right, premiseSequent.right))
proof.InvalidProofTactic("Right-hand side of the premise is not the same as the right-hand side of the conclusion.")
else if (
- !K.isSameSet(botK.left + phi_psi, premiseSequent.left ++ implications + phi_tau) &&
- !K.isSameSet(botK.left + phi_tau, premiseSequent.left ++ implications + phi_psi)
+ !K.isSameSet(botK.left + phi_psi, premiseSequent.left ++ psiIffTau + phi_tau) &&
+ !K.isSameSet(botK.left + phi_tau, premiseSequent.left ++ psiIffTau + phi_psi)
)
proof.InvalidProofTactic("Left-hand side of the conclusion + φ(ψ_) is not the same as left-hand side of the premise + (ψ ⇔ τ)_ + φ(τ_) (or with ψ_ and τ_ swapped).")
else
@@ -1238,22 +1268,39 @@ object BasicStepTactic {
* </pre>
*/
object RightSubstIff extends ProofTactic {
- def apply(using lib: Library, proof: lib.Proof)(
+ def withParametersSimple(using lib: Library, proof: lib.Proof)(
equals: List[(F.Formula, F.Formula)],
lambdaPhi: F.LambdaExpression[F.Formula, F.Formula, ?]
)(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
+ withParameters(equals.map { case (a, b) => (F.lambda(Seq(), a), F.lambda(Seq(), b)) }, (lambdaPhi.bounds.asInstanceOf[Seq[F.SchematicAtomicLabel[?]]], lambdaPhi.body))(premise)(bot)
+ }
+
+ def withParameters(using lib: Library, proof: lib.Proof)(
+ equals: List[(F.LambdaExpression[F.Term, F.Formula, ?], F.LambdaExpression[F.Term, F.Formula, ?])],
+ lambdaPhi: (Seq[F.SchematicAtomicLabel[?]], F.Formula)
+ )(premise: proof.Fact)(bot: F.Sequent): proof.ProofTacticJudgement = {
lazy val premiseSequent = proof.getSequent(premise).underlying
lazy val botK = bot.underlying
- lazy val equalsK = equals.map((p: (F.Formula, F.Formula)) => (p._1.underlying, p._2.underlying))
- lazy val lambdaPhiK = F.underlyingLFF(lambdaPhi)
-
- lazy val (psi_es, tau_es) = equalsK.unzip
- lazy val phi_psi = lambdaPhiK(psi_es)
- lazy val phi_tau = lambdaPhiK(tau_es)
- lazy val implications = equalsK map { case (s, t) => K.ConnectorFormula(K.Iff, Seq(s, t)) }
+ lazy val equalsK = equals.map(p => (p._1.underlyingLTF, p._2.underlyingLTF))
+ lazy val lambdaPhiK = (lambdaPhi._1.map(_.underlyingLabel), lambdaPhi._2.underlying)
+
+ val (psi_s, tau_s) = equalsK.unzip
+ val (phi_args, phi_body) = lambdaPhiK
+ if (phi_args.size != psi_s.size)
+ return proof.InvalidProofTactic("The number of arguments of φ must be the same as the number of equalities.")
+ else if (equalsK.zip(phi_args).exists { case ((s, t), arg) => s.vars.size != arg.arity || t.vars.size != arg.arity })
+ return proof.InvalidProofTactic("The arities of symbols in φ must be the same as the arities of equalities.")
+
+ val phi_psi = K.instantiatePredicateSchemas(phi_body, (phi_args zip psi_s).toMap)
+ val phi_tau = K.instantiatePredicateSchemas(phi_body, (phi_args zip tau_s).toMap)
+ val psiIffTau = equalsK map { case (s, t) =>
+ assert(s.vars.size == t.vars.size)
+ val base = K.ConnectorFormula(K.Iff, Seq(s.body, if (s.vars == t.vars) t.body else t(s.vars.map(K.VariableTerm))))
+ (s.vars).foldLeft(base: K.Formula) { case (acc, s_arg) => K.BinderFormula(K.Forall, s_arg, acc) }
+ }
- if (!K.isSameSet(botK.left, premiseSequent.left ++ implications)) {
+ if (!K.isSameSet(botK.left, premiseSequent.left ++ psiIffTau)) {
proof.InvalidProofTactic("Left-hand side of the conclusion is not the same as the left-hand side of the premise + (ψ ⇔ τ)_.")
} else if (
!K.isSameSet(botK.right + phi_psi, premiseSequent.right + phi_tau) &&
@@ -1261,7 +1308,7 @@ object BasicStepTactic {
)
proof.InvalidProofTactic("Right-hand side of the conclusion + φ(ψ_) is not the same as right-hand side of the premise + φ(τ_) (or with ψ_ and τ_ swapped).")
else
- proof.ValidProofTactic(bot, Seq(K.RightSubstIff(botK, -1, equalsK, F.underlyingLFF(lambdaPhi))), Seq(premise))
+ proof.ValidProofTactic(bot, Seq(K.RightSubstIff(botK, -1, equalsK, lambdaPhiK)), Seq(premise))
}
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
index da97d5e35cf44d3b5ccb3fc7228a3a0a1d69df65..e612d0ebae89addeca813a9e4f8adbf38508a0bc 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/ProofsHelpers.scala
@@ -121,7 +121,7 @@ trait ProofsHelpers {
}
extension (using proof: library.Proof)(fact: proof.Fact) {
- def of(insts: F.SubstPair*): proof.InstantiatedFact = {
+ def of(insts: (F.SubstPair | F.Term)*): proof.InstantiatedFact = {
proof.InstantiatedFact(fact, insts)
}
def statement: F.Sequent = proof.sequentOfFact(fact)
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index 98f077eb0a66003faeb4cddb24eb68b916b93b66..49349ce973650803707afa2be9ccd63a321cef3a 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -43,13 +43,19 @@ trait WithTheorems {
*/
case class InstantiatedFact(
fact: Fact,
- insts: Seq[F.SubstPair] /*,
- instsConn: Map[K.SchematicConnectorLabel, K.LambdaFormulaFormula],
- instsPred: Map[K.SchematicAtomicLabel, K.LambdaTermFormula],
- instsTerm: Map[K.SchematicTermLabel, K.LambdaTermTerm]*/
+ insts: Seq[F.SubstPair | F.Term]
) {
val baseFormula: F.Sequent = sequentOfFact(fact)
- val result: F.Sequent = baseFormula.substitute(insts*)
+ val (result, proof) = {
+ val (terms, substPairs) = insts.partitionMap {
+ case t: F.Term => Left(t)
+ case sp: F.SubstPair => Right(sp)
+ }
+
+ val (s1, p1) = if substPairs.isEmpty then (baseFormula, Seq()) else baseFormula.instantiateWithProof(substPairs.map(sp => (sp._1, sp._2)).toMap, -1)
+ val (s2, p2) = if terms.isEmpty then (s1, p1) else s1.instantiateForallWithProof(terms, p1.length - 1)
+ (s2, p1 ++ p2)
+ }
}
@@ -112,16 +118,8 @@ trait WithTheorems {
}
private def addInstantiatedFact(instFact: InstantiatedFact): Unit = {
- val (s, i) = sequentAndIntOfFact(instFact.fact)
- // newProofStep(BasicStepTactic.InstSchema(using library, this)(instFact.instsConn, instFact.instsPred, instFact.instsTerm)(i).asInstanceOf[ValidProofTactic])
- // newProofStep(BasicStepTactic.InstSchema(using library, this)(instFact.insts)(i).asInstanceOf[ValidProofTactic])
- val instMap = Map(instFact.insts.map(s => (s._1, (s._2.asInstanceOf: F.LisaObject[_])))*)
- val instStep = {
- val res = s.substituteWithProof(instMap)
-
- ValidProofTactic(res._1, res._2, Seq(instFact.fact))(using F.SequentInstantiationRule)
- }
- newProofStep(instStep)
+ val step = ValidProofTactic(instFact.result, instFact.proof, Seq(instFact.fact))(using F.SequentInstantiationRule)
+ newProofStep(step)
instantiatedFacts = (instFact, steps.length - 1) :: instantiatedFacts
}
diff --git a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
index 88e0e8dbda4a67ab4e15612b9ce9ff227d8d281f..3b934506a166849c7de4d557163081f4a223ecb6 100644
--- a/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
+++ b/lisa-utils/src/main/scala/lisa/utils/Serialization.scala
@@ -1,6 +1,7 @@
package lisa.utils
-import lisa.utils.K.*
+import lisa.kernel.proof.SequentCalculus.*
+import lisa.utils.K.{LeftSubstEq => _, LeftSubstIff => _, RightSubstEq => _, RightSubstIff => _, _}
import lisa.utils.ProofsShrink.*
import java.io._
@@ -320,41 +321,49 @@ object Serialization {
sequentToProofDOS(bot)
proofDOS.writeInt(t1)
proofDOS.writeShort(equals.size)
- equals.foreach(t =>
- proofDOS.writeInt(lineOfTerm(t._1))
- proofDOS.writeInt(lineOfTerm(t._2))
+ equals.foreach(ltts =>
+ lttToProofDOS(ltts._1)
+ lttToProofDOS(ltts._2)
)
- ltfToProofDOS(lambdaPhi)
+ proofDOS.writeShort(lambdaPhi._1.size)
+ lambdaPhi._1.foreach(stl => termLabelToDOS(stl, proofDOS))
+ proofDOS.writeInt(lineOfFormula(lambdaPhi._2))
case RightSubstEq(bot, t1, equals, lambdaPhi) =>
proofDOS.writeByte(rightSubstEq)
sequentToProofDOS(bot)
proofDOS.writeInt(t1)
proofDOS.writeShort(equals.size)
- equals.foreach(t =>
- proofDOS.writeInt(lineOfTerm(t._1))
- proofDOS.writeInt(lineOfTerm(t._2))
+ equals.foreach(ltts =>
+ lttToProofDOS(ltts._1)
+ lttToProofDOS(ltts._2)
)
- ltfToProofDOS(lambdaPhi)
+ proofDOS.writeShort(lambdaPhi._1.size)
+ lambdaPhi._1.foreach(stl => termLabelToDOS(stl, proofDOS))
+ proofDOS.writeInt(lineOfFormula(lambdaPhi._2))
case LeftSubstIff(bot, t1, equals, lambdaPhi) =>
proofDOS.writeByte(leftSubstIff)
sequentToProofDOS(bot)
proofDOS.writeInt(t1)
proofDOS.writeShort(equals.size)
- equals.foreach(t =>
- proofDOS.writeInt(lineOfFormula(t._1))
- proofDOS.writeInt(lineOfFormula(t._2))
+ equals.foreach(ltts =>
+ ltfToProofDOS(ltts._1)
+ ltfToProofDOS(ltts._2)
)
- lffToProofDOS(lambdaPhi)
+ proofDOS.writeShort(lambdaPhi._1.size)
+ lambdaPhi._1.foreach(stl => formulaLabelToDOS(stl, proofDOS))
+ proofDOS.writeInt(lineOfFormula(lambdaPhi._2))
case RightSubstIff(bot, t1, equals, lambdaPhi) =>
proofDOS.writeByte(rightSubstIff)
sequentToProofDOS(bot)
proofDOS.writeInt(t1)
proofDOS.writeShort(equals.size)
- equals.foreach(t =>
- proofDOS.writeInt(lineOfFormula(t._1))
- proofDOS.writeInt(lineOfFormula(t._2))
+ equals.foreach(ltts =>
+ ltfToProofDOS(ltts._1)
+ ltfToProofDOS(ltts._2)
)
- lffToProofDOS(lambdaPhi)
+ proofDOS.writeShort(lambdaPhi._1.size)
+ lambdaPhi._1.foreach(stl => formulaLabelToDOS(stl, proofDOS))
+ proofDOS.writeInt(lineOfFormula(lambdaPhi._2))
case InstSchema(bot, t1, mCon, mPred, mTerm) =>
proofDOS.writeByte(instSchema)
sequentToProofDOS(bot)
@@ -561,29 +570,29 @@ object Serialization {
LeftSubstEq(
sequentFromProofDIS(),
proofDIS.readInt(),
- (1 to proofDIS.readShort()).map(_ => (termMap(proofDIS.readInt()), termMap(proofDIS.readInt()))).toList,
- ltfFromProofDIS()
+ (1 to proofDIS.readShort()).map(_ => (lttFromProofDIS(), lttFromProofDIS())).toList,
+ ((1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[SchematicTermLabel]).toList, formulaMap(proofDIS.readInt()))
)
else if (psType == rightSubstEq)
RightSubstEq(
sequentFromProofDIS(),
proofDIS.readInt(),
- (1 to proofDIS.readShort()).map(_ => (termMap(proofDIS.readInt()), termMap(proofDIS.readInt()))).toList,
- ltfFromProofDIS()
+ (1 to proofDIS.readShort()).map(_ => (lttFromProofDIS(), lttFromProofDIS())).toList,
+ ((1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[SchematicTermLabel]).toList, formulaMap(proofDIS.readInt()))
)
else if (psType == leftSubstIff)
LeftSubstIff(
sequentFromProofDIS(),
proofDIS.readInt(),
- (1 to proofDIS.readShort()).map(_ => (formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))).toList,
- lffFromProofDIS()
+ (1 to proofDIS.readShort()).map(_ => (ltfFromProofDIS(), ltfFromProofDIS())).toList,
+ ((1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[SchematicAtomicLabel]).toList, formulaMap(proofDIS.readInt()))
)
else if (psType == rightSubstIff)
RightSubstIff(
sequentFromProofDIS(),
proofDIS.readInt(),
- (1 to proofDIS.readShort()).map(_ => (formulaMap(proofDIS.readInt()), formulaMap(proofDIS.readInt()))).toList,
- lffFromProofDIS()
+ (1 to proofDIS.readShort()).map(_ => (ltfFromProofDIS(), ltfFromProofDIS())).toList,
+ ((1 to proofDIS.readShort()).map(_ => labelFromInputStream(proofDIS).asInstanceOf[SchematicAtomicLabel]).toList, formulaMap(proofDIS.readInt()))
)
else if (psType == instSchema)
InstSchema(
diff --git a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
index 05933f01b6ae3f045c9be6bfe99d808cb522d762..8a9ba63a1a5c25ab4e4f3bef991ef663f2d73531 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/IncorrectProofsTests.scala
@@ -40,23 +40,23 @@ class IncorrectProofsTests extends ProofCheckerSuite {
SCProof(
Hypothesis(emptySeq +<< (x === y) +>> (x === y), x === y),
- RightSubstEq(emptySeq +<< (x === y) +<< (x === z) +>> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y)) // wrong variable replaced
+ RightSubstEq(emptySeq +<< (x === y) +<< (x === z) +>> (z === y), 0, List(((LambdaTermTerm(Seq(), x), LambdaTermTerm(Seq(), z)))), (Seq(yl), x === y)) // wrong variable replaced
),
SCProof(
Hypothesis(emptySeq +<< (x === y) +>> (x === y), x === y),
- RightSubstEq(emptySeq +<< (x === y) +>> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === y)) // missing hypothesis
+ RightSubstEq(emptySeq +<< (x === y) +>> (z === y), 0, List(((LambdaTermTerm(Seq(), x), LambdaTermTerm(Seq(), z)))), (Seq(xl), x === y)) // missing hypothesis
),
SCProof(
Hypothesis(emptySeq +<< (x === y) +>> (x === y), x === y),
- RightSubstEq(emptySeq +<< (x === y) +<< (x === z) +>> (z === y), 0, List((x, z)), LambdaTermFormula(Seq(xl), x === z)) // replacement mismatch
+ RightSubstEq(emptySeq +<< (x === y) +<< (x === z) +>> (z === y), 0, List(((LambdaTermTerm(Seq(), x), LambdaTermTerm(Seq(), z)))), (Seq(xl), x === z)) // replacement mismatch
),
SCProof(
Hypothesis(emptySeq +<< (x === y) +>> (x === y), x === y),
- LeftSubstEq(emptySeq +<< (z === y) +<< (x === z) +>> (x === y), 0, List((x, z)), LambdaTermFormula(Seq(yl), x === y))
+ LeftSubstEq(emptySeq +<< (z === y) +<< (x === z) +>> (x === y), 0, List(((LambdaTermTerm(Seq(), x), LambdaTermTerm(Seq(), z)))), (Seq(yl), x === y))
),
SCProof(
Hypothesis(emptySeq +<< (f <=> g) +>> (f <=> g), f <=> g),
- LeftSubstIff(emptySeq +<< (h <=> g) +<< (f <=> h) +>> (f <=> g), 0, List((f, h)), LambdaFormulaFormula(Seq(gl), f <=> g))
+ LeftSubstIff(emptySeq +<< (h <=> g) +<< (f <=> h) +>> (f <=> g), 0, List(((LambdaTermFormula(Seq(), f), LambdaTermFormula(Seq(), h)))), (Seq(gl), f <=> g))
),
SCProof(
Hypothesis(emptySeq +<< f +>> f, f),
diff --git a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
index 474f4fee9052d1b7fe9407819df244f656c6e325..f86a181379c91093a835aacc6b114319a9387cfd 100644
--- a/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
+++ b/lisa-utils/src/test/scala/lisa/kernel/ProofTests.scala
@@ -5,6 +5,7 @@ import lisa.kernel.proof.RunningTheory
import lisa.kernel.proof.RunningTheory.*
import lisa.kernel.proof.SCProof
import lisa.kernel.proof.SCProofChecker
+import lisa.kernel.proof.SCProofChecker.checkSCProof
import lisa.kernel.proof.SequentCalculus.*
import lisa.utils.KernelHelpers.{_, given}
import lisa.utils.Printer
@@ -14,16 +15,25 @@ import scala.language.adhocExtensions
import scala.util.Random
class ProofTests extends AnyFunSuite {
- val predicateVerifier = SCProofChecker.checkSCProof
private val x = VariableLabel("x")
private val y = VariableLabel("y")
private val z = VariableLabel("z")
+ val f = SchematicFunctionLabel("f", 1)
+ val f2 = SchematicFunctionLabel("f2", 1)
+ val g = ConstantFunctionLabel("g", 2)
+ val g2 = SchematicFunctionLabel("g2", 2)
private val a = AtomicFormula(ConstantAtomicLabel("A", 0), Seq())
private val b = AtomicFormula(ConstantAtomicLabel("B", 0), Seq())
private val fp = ConstantAtomicLabel("F", 1)
val sT = VariableLabel("t")
+ val X = VariableFormulaLabel("X")
+ val P = SchematicPredicateLabel("f", 1)
+ val P2 = SchematicPredicateLabel("f2", 1)
+ val Q = ConstantAtomicLabel("g", 2)
+ val Q2 = SchematicPredicateLabel("g2", 2)
+
test("Verification of Pierce law") {
val s0 = Hypothesis(a |- a, a)
val s1 = Weakening(a |- Set(a, b), 0)
@@ -31,14 +41,203 @@ class ProofTests extends AnyFunSuite {
val s3 = LeftImplies((a ==> b) ==> a |- a, 2, 0, a ==> b, a)
val s4 = RightImplies(() |- (a ==> b) ==> a ==> a, 3, (a ==> b) ==> a, a)
val ppl: SCProof = SCProof(IndexedSeq(s0, s1, s2, s3, s4))
- assert(predicateVerifier(ppl).isValid)
+ assert(checkSCProof(ppl).isValid)
}
- 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 pr = new SCProof(IndexedSeq(t0, t1))
- assert(predicateVerifier(pr).isValid)
+ test("Verification of LeftSubstEq") {
+ {
+ val t0 = Hypothesis(fp(x) |- fp(x), fp(x))
+ val t1 = LeftSubstEq(Set(fp(y), x === y) |- fp(x), 0, List(((LambdaTermTerm(Seq(), x), LambdaTermTerm(Seq(), y)))), (Seq(sT), fp(sT)))
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, fp(f(x))) |- exists(x, fp(f(x))), exists(x, fp(f(x))))
+ val t1 = LeftSubstEq(
+ Set(exists(x, fp(g(x, x))), forall(y, f(y) === g(y, y))) |- exists(x, fp(f(x))),
+ 0,
+ List((LambdaTermTerm(Seq(x), f(x)), LambdaTermTerm(Seq(x), g(x, x)))),
+ (Seq(f2), exists(x, fp(f2(x))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, fp(f(x))) |- exists(x, fp(f(x))), exists(x, fp(f(x))))
+ val t1 = LeftSubstEq(
+ Set(exists(x, fp(g(x, x))), forall(y, f(y) === g(y, y))) |- exists(x, fp(f(x))),
+ 0,
+ List((LambdaTermTerm(Seq(y), f(y)), LambdaTermTerm(Seq(z), g(z, z)))),
+ (Seq(f2), exists(x, fp(f2(x))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, fp(g(y, g(x, z))))) |- exists(x, forall(y, fp(g(y, g(x, z))))), exists(x, forall(y, fp(g(y, g(x, z))))))
+ val t1 = LeftSubstEq(
+ Set(exists(x, forall(y, fp(g(g(x, z), y)))), forall(y, forall(z, g(y, z) === g(z, y)))) |- exists(x, forall(y, fp(g(y, g(x, z))))),
+ 0,
+ List((LambdaTermTerm(Seq(y, z), g(y, z)), LambdaTermTerm(Seq(y, z), g(z, y)))),
+ (Seq(g2), exists(x, forall(y, fp(g2(y, g(x, z))))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, fp(g(y, g(x, z))))) |- exists(x, forall(y, fp(g(y, g(x, z))))), exists(x, forall(y, fp(g(y, g(x, z))))))
+ val t1 = LeftSubstEq(
+ Set(exists(x, forall(y, fp(g(g(z, x), y)))), forall(y, forall(z, g(y, z) === g(z, y)))) |- exists(x, forall(y, fp(g(y, g(x, z))))),
+ 0,
+ List((LambdaTermTerm(Seq(y, z), g(y, z)), LambdaTermTerm(Seq(y, z), g(z, y)))),
+ (Seq(g2), exists(x, forall(y, fp(g2(y, g2(x, z))))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, fp(g(y, g(x, f(z)))))) |- exists(x, forall(y, fp(g(y, g(x, f(z)))))), exists(x, forall(y, fp(g(y, g(x, f(z)))))))
+ val t1 = LeftSubstEq(
+ Set(exists(x, forall(y, fp(g(g(g(z, z), x), y)))), forall(y, f(y) === g(y, y)), forall(y, forall(z, g(y, z) === g(z, y)))) |- exists(x, forall(y, fp(g(y, g(x, f(z)))))),
+ 0,
+ List((LambdaTermTerm(Seq(y, z), g(y, z)), LambdaTermTerm(Seq(y, z), g(z, y))), (LambdaTermTerm(Seq(y), f(y)), LambdaTermTerm(Seq(z), g(z, z)))),
+ (Seq(g2, f2), exists(x, forall(y, fp(g2(y, g2(x, f2(z)))))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ }
+
+ test("Verification of RightSubstEq") {
+ {
+ val t0 = Hypothesis(fp(x) |- fp(x), fp(x))
+ val t1 = RightSubstEq(Set(fp(x), x === y) |- fp(y), 0, List(((LambdaTermTerm(Seq(), x), LambdaTermTerm(Seq(), y)))), (Seq(sT), fp(sT)))
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, fp(f(x))) |- exists(x, fp(f(x))), exists(x, fp(f(x))))
+ val t1 = RightSubstEq(
+ Set(exists(x, fp(f(x))), forall(y, f(y) === g(y, y))) |- exists(x, fp(g(x, x))),
+ 0,
+ List((LambdaTermTerm(Seq(x), f(x)), LambdaTermTerm(Seq(x), g(x, x)))),
+ (Seq(f2), exists(x, fp(f2(x))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, fp(f(x))) |- exists(x, fp(f(x))), exists(x, fp(f(x))))
+ val t1 = RightSubstEq(
+ Set(exists(x, fp(f(x))), forall(y, f(y) === g(y, y))) |- exists(x, fp(g(x, x))),
+ 0,
+ List((LambdaTermTerm(Seq(y), f(y)), LambdaTermTerm(Seq(z), g(z, z)))),
+ (Seq(f2), exists(x, fp(f2(x))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, fp(g(y, g(x, z))))) |- exists(x, forall(y, fp(g(y, g(x, z))))), exists(x, forall(y, fp(g(y, g(x, z))))))
+ val t1 = RightSubstEq(
+ Set(exists(x, forall(y, fp(g(y, g(x, z))))), forall(y, forall(z, g(y, z) === g(z, y)))) |- exists(x, forall(y, fp(g(g(x, z), y)))),
+ 0,
+ List((LambdaTermTerm(Seq(y, z), g(y, z)), LambdaTermTerm(Seq(y, z), g(z, y)))),
+ (Seq(g2), exists(x, forall(y, fp(g2(y, g(x, z))))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, fp(g(y, g(x, z))))) |- exists(x, forall(y, fp(g(y, g(x, z))))), exists(x, forall(y, fp(g(y, g(x, z))))))
+ val t1 = RightSubstEq(
+ Set(exists(x, forall(y, fp(g(y, g(x, z))))), forall(y, forall(z, g(y, z) === g(z, y)))) |- exists(x, forall(y, fp(g(g(z, x), y)))),
+ 0,
+ List((LambdaTermTerm(Seq(y, z), g(y, z)), LambdaTermTerm(Seq(y, z), g(z, y)))),
+ (Seq(g2), exists(x, forall(y, fp(g2(y, g2(x, z))))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, fp(g(y, g(x, f(z)))))) |- exists(x, forall(y, fp(g(y, g(x, f(z)))))), exists(x, forall(y, fp(g(y, g(x, f(z)))))))
+ val t1 = RightSubstEq(
+ Set(exists(x, forall(y, fp(g(y, g(x, f(z)))))), forall(y, f(y) === g(y, y)), forall(y, forall(z, g(y, z) === g(z, y)))) |- exists(x, forall(y, fp(g(g(g(z, z), x), y)))),
+ 0,
+ List((LambdaTermTerm(Seq(y, z), g(y, z)), LambdaTermTerm(Seq(y, z), g(z, y))), (LambdaTermTerm(Seq(y), f(y)), LambdaTermTerm(Seq(z), g(z, z)))),
+ (Seq(g2, f2), exists(x, forall(y, fp(g2(y, g2(x, f2(z)))))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+
+ }
+
+ test("Verification of LeftSubstIff") {
+ {
+ val t0 = Hypothesis(P(x) |- P(x), P(x))
+ val t1 = LeftSubstIff(Set(P(y), P(x) <=> P(y)) |- P(x), 0, List(((LambdaTermFormula(Seq(), P(x)), LambdaTermFormula(Seq(), P(y))))), (Seq(X), X))
+ val pr = new SCProof(IndexedSeq(t0, t1))
+ assert(checkSCProof(pr).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, P(x)) |- exists(x, P(x)), exists(x, P(x)))
+ val t1 = LeftSubstIff(
+ Set(exists(x, Q(x, x)), forall(y, P(y) <=> Q(y, y))) |- exists(x, P(x)),
+ 0,
+ List((LambdaTermFormula(Seq(x), P(x)), LambdaTermFormula(Seq(x), Q(x, x)))),
+ (Seq(P2), exists(x, P2(x)))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, P(x)) |- exists(x, P(x)), exists(x, P(x)))
+ val t1 = LeftSubstIff(
+ Set(exists(x, Q(x, x)), forall(y, P(y) <=> Q(y, y))) |- exists(x, P(x)),
+ 0,
+ List((LambdaTermFormula(Seq(y), P(y)), LambdaTermFormula(Seq(z), Q(z, z)))),
+ (Seq(P2), exists(x, P2(x)))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, Q(y, g(x, z)))) |- exists(x, forall(y, Q(y, g(x, z)))), exists(x, forall(y, Q(y, g(x, z)))))
+ val t1 = LeftSubstIff(
+ Set(exists(x, forall(y, Q(g(x, z), y))), forall(x, forall(y, Q(x, y) <=> Q(y, x)))) |- exists(x, forall(y, Q(y, g(x, z)))),
+ 0,
+ List((LambdaTermFormula(Seq(y, z), Q(y, z)), LambdaTermFormula(Seq(y, z), Q(z, y)))),
+ (Seq(Q2), exists(x, forall(y, Q2(y, g(x, z)))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+
+ }
+
+ test("Verification of RightSubstIff") {
+ {
+ val t0 = Hypothesis(P(x) |- P(x), P(x))
+ val t1 = RightSubstIff(Set(P(x), P(x) <=> P(y)) |- P(y), 0, List(((LambdaTermFormula(Seq(), P(x)), LambdaTermFormula(Seq(), P(y))))), (Seq(X), X))
+ val pr = new SCProof(IndexedSeq(t0, t1))
+ assert(checkSCProof(pr).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, P(x)) |- exists(x, P(x)), exists(x, P(x)))
+ val t1 = RightSubstIff(
+ Set(exists(x, P(x)), forall(y, P(y) <=> Q(y, y))) |- exists(x, Q(x, x)),
+ 0,
+ List((LambdaTermFormula(Seq(x), P(x)), LambdaTermFormula(Seq(x), Q(x, x)))),
+ (Seq(P2), exists(x, P2(x)))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, P(x)) |- exists(x, P(x)), exists(x, P(x)))
+ val t1 = RightSubstIff(
+ Set(exists(x, P(x)), forall(y, P(y) <=> Q(y, y))) |- exists(x, Q(x, x)),
+ 0,
+ List((LambdaTermFormula(Seq(y), P(y)), LambdaTermFormula(Seq(z), Q(z, z)))),
+ (Seq(P2), exists(x, P2(x)))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
+ {
+ val t0 = Hypothesis(exists(x, forall(y, Q(y, g(x, z)))) |- exists(x, forall(y, Q(y, g(x, z)))), exists(x, forall(y, Q(y, g(x, z)))))
+ val t1 = RightSubstIff(
+ Set(exists(x, forall(y, Q(y, g(x, z)))), forall(x, forall(y, Q(x, y) <=> Q(y, x)))) |- exists(x, forall(y, Q(g(x, z), y))),
+ 0,
+ List((LambdaTermFormula(Seq(y, z), Q(y, z)), LambdaTermFormula(Seq(y, z), Q(z, y)))),
+ (Seq(Q2), exists(x, forall(y, Q2(g(x, z), y))))
+ )
+ assert(checkSCProof(SCProof(IndexedSeq(t0, t1))).isValid)
+ }
}
test("Commutativity on a random large formula") {
@@ -58,6 +257,6 @@ class ProofTests extends AnyFunSuite {
val orig = subformulas.next().head
val swapped = subformulasSwapped.next().head
val prf = SCProof(Vector(Hypothesis(Sequent(Set(orig), Set(orig)), orig), Restate(Sequent(Set(orig), Set(swapped)), 0)))
- assert(predicateVerifier(prf).isValid)
+ assert(checkSCProof(prf).isValid)
}
}
diff --git a/refman/kernel.tex b/refman/kernel.tex
index 5d5aeb1913f3785f25c0c32d901ceed471883fcf..340d278cbb8609f51cdd0800d4d7cb457ed6fcde 100644
--- a/refman/kernel.tex
+++ b/refman/kernel.tex
@@ -507,26 +507,39 @@ Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
\RightLabel{\text{ InstSchema}}
\UnaryInfC{$\Gamma[\psi(\vec{v}) := {\schem{p}(\vec{v})}] \vdash \Delta[\psi(\vec{v}) := {\schem{p}(\vec{v})}]$}
\DisplayProof
- } \\[5ex]
+ }
+ \\[5ex]
- \AxiomC{$\Gamma, \phi[\schem{f} := s] \vdash \Delta$}
- \RightLabel{\text{ LeftSubstEq}}
- \UnaryInfC{$\Gamma, s = t, \phi[\schem{f} := t] \vdash \Delta$}
- \DisplayProof &
- \AxiomC{$\Gamma \vdash \phi[\schem{f} := s], \Delta$}
- \RightLabel{\text{ RightSubstEq}}
- \UnaryInfC{$\Gamma, s = t \vdash \phi[\schem{f} := t], \Delta$}
- \DisplayProof
+ \multicolumn{2}{c}{
+ \AxiomC{$\Gamma, \phi[\schem{f} := s] \vdash \Delta$}
+ \RightLabel{\text{ LeftSubstEq}}
+ \UnaryInfC{$\Gamma, \forall \vec x. s(\vec x) = t(\vec x), \phi[\schem{f} := t] \vdash \Delta$}
+ \DisplayProof
+ }
\\[5ex]
- \AxiomC{$\Gamma, \phi[{\schem{p}} := a] \vdash \Delta$}
- \RightLabel{\text{ LeftSubstIff}}
- \UnaryInfC{$\Gamma, a \leftrightarrow b, \phi[{\schem{p}} = b] \vdash \Delta$}
- \DisplayProof &
- \AxiomC{$\Gamma \vdash \phi[{\schem{p}} := a], \Delta$}
- \RightLabel{\text{ RightSubstIff}}
- \UnaryInfC{$\Gamma, a \leftrightarrow b \vdash \phi[{\schem{p}} := b], \Delta$}
- \DisplayProof
+ \multicolumn{2}{c}{
+ \AxiomC{$\Gamma \vdash \phi[\schem{f} := s], \Delta$}
+ \RightLabel{\text{ RightSubstEq}}
+ \UnaryInfC{$\Gamma, \forall \vec x. s(\vec x) = t(\vec x) \vdash \phi[\schem{f} := t], \Delta$}
+ \DisplayProof
+ }
+ \\[5ex]
+
+ \multicolumn{2}{c}{
+ \AxiomC{$\Gamma, \phi[{\schem{p}} := a] \vdash \Delta$}
+ \RightLabel{\text{ LeftSubstIff}}
+ \UnaryInfC{$\Gamma, \forall \vec x. a(\vec x) \leftrightarrow b(\vec x), \phi[{\schem{p}} = b] \vdash \Delta$}
+ \DisplayProof
+ }
+ \\[5ex]
+
+ \multicolumn{2}{c}{
+ \AxiomC{$\Gamma \vdash \phi[{\schem{p}} := a], \Delta$}
+ \RightLabel{\text{ RightSubstIff}}
+ \UnaryInfC{$\Gamma, \forall \vec x. a(\vec x) \leftrightarrow b(\vec x) \vdash \phi[{\schem{p}} := b], \Delta$}
+ \DisplayProof
+ }
\\[5ex]
\AxiomC{$\Gamma, t = t \vdash \Delta$}
@@ -562,7 +575,7 @@ Finally, the two rules Restate and Weakening leverage the $\FOLalg$ algorithm.
\multicolumn{2}{c}{
\AxiomC{}
- \RightLabel{\text { Sorry: admit a statement as axiom. Usage transitively tracked.}}
+ \RightLabel{\text { Sorry: admit a statement without proof. Usage transitively tracked.}}
\UnaryInfC{$\Gamma \vdash \Delta$}
\DisplayProof
}
diff --git a/refman/lisa.pdf b/refman/lisa.pdf
index 485feaa4cc5206b5d66d69b6b1a9edad2fb916cf..ab0dec1fa62604d7969a3358bec28f10bb5b1a9c 100644
Binary files a/refman/lisa.pdf and b/refman/lisa.pdf differ
diff --git a/refman/macro.tex b/refman/macro.tex
index 2919e649c00daa150ead14152c8fc1e3c8cbe366..c3f2863345317398d2aaf140466c6527efbe240e 100644
--- a/refman/macro.tex
+++ b/refman/macro.tex
@@ -96,6 +96,7 @@
\definecolor{comments}{RGB}{80,0,110}
\lstdefinelanguage{scala}{
+ keepspaces=true,
extendedchars = true,
inputencoding = utf8,
alsoletter={@,=,>},
@@ -119,7 +120,9 @@
otherkeywords = {;,<<,>>,++},
}
+
\lstdefinelanguage{lisa}{
+ keepspaces=true,
extendedchars = true,
inputencoding = utf8,
alsoletter={@,=,>},
@@ -151,6 +154,7 @@
\definecolor{bluishlightgray}{rgb}{0.94, 0.96, 0.98}
\lstdefinelanguage{console}{
+ keepspaces=true,
extendedchars = true,
inputencoding = utf8,
backgroundcolor = \color{bluishlightgray},
@@ -164,6 +168,7 @@
}
\lstset{
+ keepspaces=true,
extendedchars = true,
inputencoding = utf8,
extendedchars = \true,
diff --git a/refman/prooflib.tex b/refman/prooflib.tex
index b338295ac7ad4dca2d9a68f5349f0c890bb557b2..08853d820579d128022a255a9ffaddce69158872 100644
--- a/refman/prooflib.tex
+++ b/refman/prooflib.tex
@@ -93,10 +93,38 @@ This simulation is provided by Lisa through the \lstinline|witness|{} method. It
\section{DSL}
-%It is important to note that when multiple such files are developed, they all use the same underlying \lstinline|RunningTheory|{}. This makes it possible to use results proved previously by means of a simple \lstinline|import|{} statement as one would import a regular object. Similarly, one should also import as usual automation and tactics developed alongside. It is expected in the medium term that \lstinline|lisa.Main|{} will come with basic automation.
-%All imported theory objects will be run through as well, but only the result of the selected one will be printed.
+\subsection{Instantiations with ``of''}
+With lisa's kernel, it is possible to instantiate a theorem proving $P(x)$ to obtain a proof of $P(t)$, for any term $t$, using the \texttt{Inst} rule from \autoref{fig:deduct_rules_1}. Lisa's DSL provides a more convenient way to do so, using the \lstinline|of| keyword. It is used like so:
+\begin{lstlisting}[language=lisa, frame=single]
+ val ax = Axiom(P(x))
+ val falso = Theorem(P(c) /\ P(d)) {
+ have(thesis) by RightAnd(ax of (x := c), ax of (x := d))
+ }
+\end{lstlisting}
+\lstinline|x := d| is called a substitution pair, and is equivalent to the tuple \lstinline|(x, d)|. Arbitrarily many substitution pairs can be given as argument to \lstinline|of|, and the instantiations are done simultaneously. \lstinline|ax of (x := c)| is called an \lstinline|InstantiatedFact|, whose statement is $P(c)$, and which can be used exactly like theorems, axioms and intermediate steps in the proof. Internally, Lisa produces a proof step corresponding to the instantiation using the \texttt{Inst} rule.
+The \lstinline|of| keyword can also instantiate universaly quantified formulas of a fact, when it contains a single formula. For example, the following code is valid:
+\begin{lstlisting}[language=lisa, frame=single]
+ val ax = Axiom(∀(x, P(x)))
+ val thm = Theorem(P(c) /\ P(d)) {
+ have(thesis) by RightAnd(ax of c, ax of d)
+ }
+\end{lstlisting}
+Here, \lstinline|ax of c| is a fact whose proven statement is again $P(c)$. It is possible to instantiate multiple $\forall$ quantifiers at once. For example if \lstinline|ax| is an axiom of the form $\forall x, \forall y, P(x, y)$, then \lstinline|ax of (c, d)| is a fact whose proven statement is $P(c, d)$. It is also possible to combine instantiation of free symbols and quantified variables. For example, if \lstinline|ax| is an axiom of the form $\forall x, \forall y, P(x, y)$, then \lstinline|ax of (c, y, P := ===)| is a fact whose proven statement is $(c = y)$.
+Formally, the \lstinline|of| keyword takes as argument arbitrarily many terms and substitution pairs. If there is at least on term given as argument, the base fact must have a single universaly quantified formula on the right (an arbitrarily many formulas on the left). The number of given terms must be at most the number of leading universal quantifiers. Moreover, a substitution cannot instantiate any locked symbol (i.e. a symbol part of an assumption or definition). The ordering of substitution pairs does not matter, but the ordering of terms does. The resulting fact is obtained by firstreplacing the free symbols in the formula by the given substitution pairs, and then instantiating the quantified variables in the formula by the given terms
+In general, for the following proof
+\begin{lstlisting}[language=lisa, frame=single]
+ val ax = Axiom(∀(x, ∀(y, P(x, y))))
+ val thm = Theorem(c == d) {
+ have(thesis) by Restate.from(ax of (c, d, P := ===))
+ }
+\end{lstlisting}
+Lisa will produce the following inner statements:
+\begin{lstlisting}
+ -1 Import 0 ( ) ⊢ ∀(x, ∀(y, P(x, y)))
+ 0 SequentInstantiationRule ( ) ⊢ c === d
+\end{lstlisting}