diff --git a/lisa-examples/src/main/scala/Example.scala b/lisa-examples/src/main/scala/Example.scala
index 28b78f657614e16d12f4ef651bbc70500be17582..74465308c6ad2e9142ed75d100bc04b37058124e 100644
--- a/lisa-examples/src/main/scala/Example.scala
+++ b/lisa-examples/src/main/scala/Example.scala
@@ -9,10 +9,8 @@ object Example extends lisa.Main {
// Simple proof with LISA's DSL
val fixedPointDoubleApplication = Theorem(∀(x, P(x) ==> P(f(x))) |- P(x) ==> P(f(f(x)))) {
- assume(∀(x, P(x) ==> P(f(x))))
- val step1 = have(P(x) ==> P(f(x))) by InstantiateForall
- val step2 = have(P(f(x)) ==> P(f(f(x)))) by InstantiateForall
- have(thesis) by Tautology.from(step1, step2)
+ val a1 = assume(∀(x, P(x) ==> P(f(x))))
+ have(thesis) by Tautology.from(a1 of x, a1 of f(x))
}
// Example of set theoretic development
diff --git a/lisa-examples/src/main/scala/Lattices.scala b/lisa-examples/src/main/scala/Lattices.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5a467b30b4571d07b26dec4561dbdb6bb1bb60a4
--- /dev/null
+++ b/lisa-examples/src/main/scala/Lattices.scala
@@ -0,0 +1,186 @@
+object Lattices extends lisa.Main {
+ // We introduce the signature of lattices
+ val <= = ConstantPredicateLabel.infix("<=", 2)
+ addSymbol(<=)
+ val u = ConstantFunctionLabel.infix("u", 2) // join (union for sets, disjunction in boolean algebras)
+ addSymbol(u)
+ val n = ConstantFunctionLabel.infix("n", 2) // meet (interestion for sets, conjunction in boolean algebras)
+ addSymbol(n)
+
+ // Enables infix notation
+ extension (left: Term) {
+ def <=(right: Term): Formula = Lattices.<=.applyUnsafe(Seq(left, right))
+ def u(right: Term): Term = Lattices.u.applyUnsafe(Seq(left, right))
+ def n(right: Term): Term = Lattices.n.applyUnsafe(Seq(left, right))
+ }
+
+ // We now states the axioms of lattices
+
+ val x = variable
+ val y = variable
+ val z = variable
+
+ val reflexivity = Axiom(x <= x)
+ val antisymmetry = Axiom(((x <= y) /\ (y <= x)) ==> (x === y))
+ val transitivity = Axiom(((x <= y) /\ (y <= z)) ==> (x <= z))
+ val lub = Axiom(((x <= z) /\ (y <= z)) <=> ((x u y) <= z))
+ val glb = Axiom(((z <= x) /\ (z <= y)) <=> (z <= (x n y)))
+
+ // Let's prove some properties !
+
+ val joinLowerBound = Theorem((x <= (x u y)) /\ (y <= (x u y))) {
+ have(thesis) by Tautology.from(lub of (z := (x u y)), reflexivity of (x := (x u y)))
+ }
+
+
+ val meetUpperBound = Theorem(((x n y) <= x) /\ ((x n y) <= y)) {
+ sorry
+ }
+ val joinCommutative = Theorem((x u y) === (y u x)) {
+ val s1 = have((x u y) <= (y u x)) by Tautology.from(lub of (z := (y u x)), joinLowerBound of (x := y, y := x))
+ have(thesis) by Tautology.from(s1, s1 of (x := y, y := x), antisymmetry of (x := x u y, y := y u x))
+ }
+
+
+ val meetCommutative = Theorem((x n y) === (y n x)) {
+ sorry
+ }
+ val joinAbsorption = Theorem((x <= y) |- (x u y) === y) {
+ sorry
+ }
+
+ val meetAbsorption = Theorem((x <= y) |- (x n y) === x) {
+ sorry
+ }
+
+ val joinAssociative = Theorem((x u (y u z)) === ((x u y) u z)) {
+ sorry
+ }
+
+ // Tedious, isn't it
+ // Can we automate this?
+ // Yes, we can!
+
+ import lisa.prooflib.ProofTacticLib.ProofTactic
+ import lisa.prooflib.Library
+
+ object Whitman extends ProofTactic {
+ def solve(using lib: library.type, proof: lib.Proof)(goal: Sequent): proof.ProofTacticJudgement = {
+ TacticSubproof { // Starting the proof of `goal`
+
+ if goal.left.nonEmpty || goal.right.size != 1 then proof.InvalidProofTactic("Whitman can only be applied to solve goals of the form () |- s <= t")
+ else
+ goal.right.head match {
+ case <=(left: Term, right: Term) => {
+ // We have different cases to consider
+ (left, right) match {
+ // 1. left is a join. In that case, lub gives us the decomposition
+ case (u(a: Term, b: Term), _) =>
+ val s1 = solve(a <= right)
+ val s2 = solve(b <= right)
+ if s1.isValid & s2.isValid then
+ have(left <= right) by Tautology.from(lub of (x := a, y := b, z := right), have(s1), have(s2))
+ else return proof.InvalidProofTactic("The inequality is not true in general ")
+
+ // 2. right is a meet. In that case, glb gives us the decomposition
+ case (_, n(a: Term, b: Term)) =>
+ ???
+
+ // 3. left is a meet, right is a join. In that case, we try all pairs.
+ case (n(a: Term, b: Term), u(c: Term, d: Term)) =>
+ val result = LazyList(a, b)
+ .map { e => (e, solve(e <= right)) }
+ .find { _._2.isValid }
+ .map { case (e, step) =>
+ have(left <= right) by Tautology.from(
+ have(step),
+ meetUpperBound of (x := a, y := b),
+ transitivity of (x := left, y := e, z := right)
+ )
+ } orElse {
+ LazyList(c, d)
+ .map { e => (e, solve(left <= e)) }
+ .find { _._2.isValid }
+ .map { case (e, step) =>
+ have(left <= right) by Tautology.from(
+ have(step),
+ joinLowerBound of (x := c, y := d),
+ transitivity of (x := left, y := e, z := right)
+ )
+ }
+ }
+ if result.isEmpty then return proof.InvalidProofTactic("The inequality is not true in general 3")
+
+
+ // 4. left is a meet, right is a variable or unknown term.
+ case (n(a: Term, b: Term), _) =>
+ val result = LazyList(a, b)
+ .map { e => (e, solve(e <= right)) }
+ .find { _._2.isValid }
+ .map { case (e, step) =>
+ have(left <= right) by Tautology.from(
+ have(step),
+ meetUpperBound of (x := a, y := b),
+ transitivity of (x := left, y := e, z := right)
+ )
+
+ }
+ if result.isEmpty then return proof.InvalidProofTactic("The inequality is not true in general")
+
+ // 5. left is a variable or unknown term, right is a join.
+ case (_, u(c: Term, d: Term)) =>
+ ???
+
+ // 6. left and right are variables or unknown terms.
+ case _ =>
+ if !(left == right) then return proof.InvalidProofTactic("The inequality is not true in general 6")
+ else ???
+
+ }
+ }
+
+ case ===(left: Term, right: Term) =>
+ val s1 = solve(left <= right)
+ val s2 = solve(right <= left)
+ if !(s1.isValid && s2.isValid) then return proof.InvalidProofTactic("The equality is not true in general")
+ else
+ have(left === right) by Tautology.from(
+ have(s1),
+ have(s2),
+ antisymmetry of (x := left, y := right)
+ )
+ case _ => return proof.InvalidProofTactic("Whitman can only be applied to solve goals of the form () |- s <= t")
+ }
+ }
+ }
+ }
+
+
+ // uncomment when the tactic is implemented
+
+ /*
+ val test1 = Theorem(x <= x) {
+ have(thesis) by Whitman.solve
+ }
+ val test2 = Theorem(x <= (x u y)) {
+ have(thesis) by Whitman.solve
+ }
+ val test3 = Theorem((y n x) <= x) {
+ have(thesis) by Whitman.solve
+ }
+ val test4 = Theorem((x n y) <= (y u z)) {
+ have(thesis) by Whitman.solve
+ }
+ val idempotence = Theorem((x u x) === x) {
+ have(thesis) by Whitman.solve
+ }
+ val meetAssociative = Theorem((x n (y n z)) === ((x n y) n z)) {
+ have(thesis) by Whitman.solve
+ }
+ val semiDistributivity = Theorem((x u (y n z)) <= ((x u y) n (x u z))) {
+ have(thesis) by Whitman.solve
+ }
+ */
+
+
+}
diff --git a/lisa-examples/src/main/scala/Test.scala b/lisa-examples/src/main/scala/Test.scala
index b65c3c6c2856115278ef9fd926b786a5f706b0a9..026a3761a4610362f2a41b69b7a4c45ea5a536db 100644
--- a/lisa-examples/src/main/scala/Test.scala
+++ b/lisa-examples/src/main/scala/Test.scala
@@ -25,7 +25,6 @@ object Test extends lisa.Main {
val goal = E(f(f(g(a))), g(f(f(a))))
-
val thm = Theorem((assump1, assump2, assump3) |- goal) {
have(thesis) by Tableau
}
@@ -43,7 +42,7 @@ object Test extends lisa.Main {
}
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 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)))
diff --git a/lisa-sets/src/main/scala/lisa/automation/Tautology.scala b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
index 476df8a588f235fb31935088ec0d932710bffe17..d1367feebb32cd151a00958f8b7ec191a42b53bb 100644
--- a/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
+++ b/lisa-sets/src/main/scala/lisa/automation/Tautology.scala
@@ -48,7 +48,8 @@ object Tautology extends ProofTactic with ProofSequentTactic with ProofFactSeque
val subpr = SCSubproof(value)
val stepsList = premsFormulas.foldLeft[List[SCProofStep]](List(subpr))((prev: List[SCProofStep], cur) => {
val ((prem, form), position) = cur
- Cut(prev.head.bot -<< form, position, initProof.length + prev.length - 1, form) :: prev
+ if prev.head.bot.left.contains(form) then Cut(prev.head.bot -<< form, position, initProof.length + prev.length - 1, form) :: prev
+ else prev
})
val steps = (initProof ++ stepsList.reverse).toIndexedSeq
proof.ValidProofTactic(bot, steps, premises)
diff --git a/lisa-utils/src/main/scala/lisa/fol/Common.scala b/lisa-utils/src/main/scala/lisa/fol/Common.scala
index 356b95d845b0c0a1407103759dee0fd0007a695e..cb1ca1eeb7290babfdc96545e97397f989bebc1b 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Common.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Common.scala
@@ -377,7 +377,7 @@ trait Common {
def rename(newid: Identifier): ConstantFunctionLabel[N] = ConstantFunctionLabel(newid, arity)
def freshRename(taken: Iterable[Identifier]): ConstantFunctionLabel[N] = rename(K.freshId(taken, id))
override def toString(): String = id
- def mkString(args: Seq[Term]): String = if (infix) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")"
+ def mkString(args: Seq[Term]): String = if (infix) (args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated()) else toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Term]): String = if (infix) "(" + mkString(args) + ")" else mkString(args)
}
object ConstantFunctionLabel {
@@ -398,7 +398,7 @@ trait Common {
def freeSchematicLabels: Set[SchematicLabel[?]] = label.freeSchematicLabels ++ args.flatMap(_.freeSchematicLabels)
def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.flatMap(_.allSchematicLabels)
override def toString: String = label.mkString(args)
- override def toStringSeparated(): String = label.mkString(args)
+ override def toStringSeparated(): String = label.mkStringSeparated(args)
}
//////////////////////////////////////
@@ -610,7 +610,7 @@ trait Common {
def rename(newid: Identifier): ConstantPredicateLabel[N] = ConstantPredicateLabel(newid, arity)
def freshRename(taken: Iterable[Identifier]): ConstantPredicateLabel[N] = rename(K.freshId(taken, id))
override def toString(): String = id
- def mkString(args: Seq[Term]): String = if (infix) (args(0).toString() + " " + toString() + " " + args(1).toString()) else toString() + "(" + args.mkString(", ") + ")"
+ def mkString(args: Seq[Term]): String = if (infix) (args(0).toStringSeparated() + " " + toString() + " " + args(1).toStringSeparated()) else toString() + "(" + args.mkString(", ") + ")"
override def mkStringSeparated(args: Seq[Term]): String = if (infix) "(" + mkString(args) + ")" else mkString(args)
}
object ConstantPredicateLabel {
@@ -632,7 +632,7 @@ trait Common {
def allSchematicLabels: Set[SchematicLabel[?]] = label.allSchematicLabels ++ args.toSeq.flatMap(_.allSchematicLabels)
override def toString: String = label.mkString(args)
- override def toStringSeparated(): String = label.mkString(args)
+ override def toStringSeparated(): String = label.mkStringSeparated(args)
}
////////////////
diff --git a/lisa-utils/src/main/scala/lisa/fol/Predef.scala b/lisa-utils/src/main/scala/lisa/fol/Predef.scala
index c5cd8d3a7ab827e88796cb542cdfb31d62ad372f..5d53b6a92040ae45e08e614127cedb8ee3886c98 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Predef.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Predef.scala
@@ -4,7 +4,7 @@ import lisa.utils.K
trait Predef extends Common {
- val equality: ConstantPredicateLabel[2] = ConstantPredicateLabel[2](K.Identifier("="), 2)
+ val equality: ConstantPredicateLabel[2] = ConstantPredicateLabel.infix(K.Identifier("="), 2)
val === = equality
val ＝ = equality
diff --git a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
index bd6bc96696d4b4f178c4d6936a53c1965f557dc9..1f13bf8498f0eb2b309d746687cc6e6f88070e8a 100644
--- a/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
+++ b/lisa-utils/src/main/scala/lisa/fol/Sequents.scala
@@ -168,9 +168,9 @@ trait Sequents extends Common with lisa.fol.Lambdas with Predef {
infix def ++?(s1: Sequent): Sequent = this addAllIfNotExists s1
override def toString =
- (if left.size == 1 then left.head.toString else "( " + left.mkString(", ") + " )") +
+ (if left.size == 0 then "" else if left.size == 1 then left.head.toString else "( " + left.mkString(", ") + " )") +
" ⊢ " +
- (if right.size == 1 then right.head.toString else "( " + right.mkString(", ") + " )")
+ (if right.size == 0 then "" else if right.size == 1 then right.head.toString else "( " + right.mkString(", ") + " )")
}
diff --git a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
index 49349ce973650803707afa2be9ccd63a321cef3a..45cab01d15b300afb2e0e438eb659db769966ad4 100644
--- a/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
+++ b/lisa-utils/src/main/scala/lisa/prooflib/WithTheorems.scala
@@ -451,6 +451,8 @@ trait WithTheorems {
* A proven, reusable statement. A justification corresponding to [[K.Theorem]].
*/
sealed abstract class THM extends JUSTIFICATION {
+ def repr: String =
+ s" Theorem ${name} := ${statement}${if (withSorry) " (!! Relies on Sorry)" else ""}"
/**
* The underlying Kernel proof [[K.SCProof]], if it is still available. Proofs are not kept in memory for efficiency.
@@ -533,7 +535,6 @@ trait WithTheorems {
*/
class THMFromKernel(using om: OutputManager)(val statement: F.Sequent, val fullName: String, val kind: TheoremKind, innerThm: theory.Theorem, getProof: () => Option[K.SCProof]) extends THM {
- def repr: String = innerJustification.repr
val innerJustification: theory.Theorem = innerThm
assert(innerThm.name == fullName)
def kernelProof: Option[K.SCProof] = getProof()
@@ -567,7 +568,6 @@ trait WithTheorems {
thm
}
else prove(computeProof)._1
- def repr: String = innerJustification.repr
library.last = Some(this)
private def prove(computeProof: Proof ?=> Unit): (theory.Theorem, SCProof, List[(String, theory.Justification)]) = {