Skip to content

Commit d83b952

Browse files
augustepoirouxaugustepoiroux
committed
Add standalone file generator for theorems and proofs + cleanup
1 parent 1608480 commit d83b952

File tree

3 files changed

+93
-72
lines changed

3 files changed

+93
-72
lines changed

‎lisa-examples/src/main/scala/Kernel2Code.scala‎

Lines changed: 8 additions & 14 deletions
Original file line numberDiff line numberDiff line change
@@ -8,9 +8,7 @@ object Kernel2Code extends lisa.Main {
88

99
val x = variable
1010
val y = variable
11-
val z = variable
1211
val f = function[1]
13-
val P = formulaVariable
1412
val Q = predicate[1]
1513
val R = predicate[1]
1614
val S = predicate[2]
@@ -29,9 +27,8 @@ object Kernel2Code extends lisa.Main {
2927
thenHave(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) by RightForall
3028
}
3129

32-
// println(generateTheoremCode("thm1_raw", thm1.statement.underlying, thm1.kernelProof.get))
33-
// println()
34-
// println(generateTheoremCode("thm1_optimized", thm1.statement.underlying, optimizeProofIteratively(thm1.kernelProof.get)))
30+
// println(generateStandaloneTheoremFileContent("thm1_raw", thm1.statement.underlying, thm1.kernelProof.get))
31+
// println(generateStandaloneTheoremFileContent("thm1_optimized", thm1.statement.underlying, optimizeProofIteratively(thm1.kernelProof.get)))
3532

3633
val thm1_raw = Theorem(
3734
∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
@@ -88,9 +85,8 @@ object Kernel2Code extends lisa.Main {
8885
have(thesis) by Tautology.from(forward, backward)
8986
}
9087

91-
// println(generateTheoremCode("thm2_raw", thm2.statement.underlying, thm2.kernelProof.get))
92-
// println()
93-
// println(generateTheoremCode("thm2_optimized", thm2.statement.underlying, optimizeProofIteratively(thm2.kernelProof.get)))
88+
// println(generateStandaloneTheoremFileContent("thm2_raw", thm2.statement.underlying, thm2.kernelProof.get))
89+
// println(generateStandaloneTheoremFileContent("thm2_optimized", thm2.statement.underlying, optimizeProofIteratively(thm2.kernelProof.get)))
9490

9591
val thm2_raw = Theorem(
9692
((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))
@@ -196,9 +192,8 @@ object Kernel2Code extends lisa.Main {
196192
have(thesis) by Tautology.from(step1, step1 of (x := f(x)))
197193
}
198194

199-
// println(generateTheoremCode("thm3_raw", thm3.statement.underlying, thm3.kernelProof.get))
200-
// println()
201-
// println(generateTheoremCode("thm3_optimized", thm3.statement.underlying, optimizeProofIteratively(thm3.kernelProof.get)))
195+
// println(generateStandaloneTheoremFileContent("thm3_raw", thm3.statement.underlying, thm3.kernelProof.get))
196+
// println(generateStandaloneTheoremFileContent("thm3_optimized", thm3.statement.underlying, optimizeProofIteratively(thm3.kernelProof.get)))
202197

203198
val thm3_raw = Theorem(
204199
∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))
@@ -301,9 +296,8 @@ object Kernel2Code extends lisa.Main {
301296
have(thesis) by Tableau
302297
}
303298

304-
// println(generateTheoremCode("thm1bis_raw", thm1bis.statement.underlying, thm1bis.kernelProof.get))
305-
// println()
306-
// println(generateTheoremCode("thm1bis_optimized", thm1bis.statement.underlying, optimizeProofIteratively(thm1bis.kernelProof.get)))
299+
// println(generateStandaloneTheoremFileContent("thm1bis_raw", thm1bis.statement.underlying, thm1bis.kernelProof.get))
300+
// println(generateStandaloneTheoremFileContent("thm1bis_optimized", thm1bis.statement.underlying, optimizeProofIteratively(thm1bis.kernelProof.get)))
307301

308302
val thm1bis_raw = Theorem(
309303
∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))

‎lisa-examples/src/main/scala/TPTPSolver.scala‎

Lines changed: 2 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -86,10 +86,9 @@ object TPTPSolver extends lisa.Main {
8686
}
8787

8888
def writeProof(problem: Problem, proof: SCProof, path: String): Unit = {
89-
// TODO
9089
val file = new File(path + problem.name + ".sc")
9190
val bw = new FileWriter(file)
92-
val proofCode = scproof2code(proof)
93-
bw.write(proof.toString)
91+
val fileContent = generateStandaloneTheoremFileContent(problem.name, problemToSequent(problem), proof)
92+
bw.write(fileContent)
9493
bw.close()
9594
}

‎lisa-utils/src/main/scala/lisa/utils/ProofsConverter.scala‎

Lines changed: 83 additions & 55 deletions
Original file line numberDiff line numberDiff line change
@@ -9,9 +9,8 @@ import lisa.fol.FOLHelpers.*
99

1010
object ProofsConverter {
1111

12-
// TODO: remove unnecessary variables "val s_..." in generated proofs -> need to keep track of which steps are used in other steps
12+
// TODO: remove unnecessary variables "val s_..." in generated proofs -> need to detect which steps are used later in other steps
1313
// TODO: generate more realistic variable names
14-
// TODO: handle automatic global variable declaration before theorems/proofs
1514

1615
private def indent(s: String, indent: Int = 2): String = s.split("\n").map(" " * indent + _).mkString("\n")
1716
private def unindent(s: String, indent: Int = 2): String = s.split("\n").map(_.drop(indent)).mkString("\n")
@@ -22,13 +21,13 @@ object ProofsConverter {
2221
case term: K.Term => asFront(term)
2322
).toString.replace("⇒", "==>").replace("⇔", "<=>")
2423

25-
def scproof2code(p: K.SCProof): String = {
26-
def scproof2codeAux(p: K.SCProof, varPrefix: String = "s", premises: Seq[String] = Seq.empty): String = {
27-
def scproofstep2code(ps: SCProofStep, stepNum: Int, premises: Seq[String], varPrefix: String): String = {
24+
private def scproof2code(p: K.SCProof): String = {
25+
def scproof2codeAux(p: K.SCProof, varPrefix: String = "s", implicitPremises: Seq[String] = Seq.empty): String = {
26+
def scproofstep2code(ps: SCProofStep, stepNum: Int, implicitPremises: Seq[String], varPrefix: String): String = {
2827

2928
def index2stepvar(i: Int): String =
30-
if i < -premises.size then throw new Exception(s"step $i is not defined")
31-
else if i < 0 then premises(-i - 1)
29+
if i < -implicitPremises.size then throw new Exception(s"step $i is not defined")
30+
else if i < 0 then implicitPremises(-i - 1)
3231
else s"${varPrefix}_$i"
3332

3433
ps match
@@ -43,93 +42,122 @@ object ProofsConverter {
4342
var tacticName = ps.getClass.getSimpleName
4443
var opening = "("
4544
var closing = ")"
46-
val (bot_, step_ref_seq) = (ps match
47-
case Restate(bot, t1) =>
48-
opening = ".from("
49-
(bot, Seq(t1))
50-
case RestateTrue(bot) =>
51-
tacticName = "Restate"
52-
(bot, null)
53-
case Hypothesis(bot, phi) => (bot, null)
54-
case Cut(bot, t1, t2, phi) => (bot, Seq(t1, t2))
55-
case LeftAnd(bot, t1, phi, psi) => (bot, Seq(t1))
56-
case LeftOr(bot, t, disjuncts) => (bot, t)
57-
case LeftImplies(bot, t1, t2, phi, psi) => (bot, Seq(t1, t2))
58-
case LeftIff(bot, t1, phi, psi) => (bot, Seq(t1))
59-
case LeftNot(bot, t1, phi) => (bot, Seq(t1))
60-
case LeftForall(bot, t1, phi, x, t) => (bot, Seq(t1))
61-
case LeftExists(bot, t1, phi, x) => (bot, Seq(t1))
62-
case LeftExistsOne(bot, t1, phi, x) => (bot, Seq(t1))
63-
case RightAnd(bot, t, conjuncts) => (bot, t)
64-
case RightOr(bot, t1, phi, psi) => (bot, Seq(t1))
65-
case RightImplies(bot, t1, phi, psi) => (bot, Seq(t1))
66-
case RightIff(bot, t1, t2, phi, psi) => (bot, Seq(t1, t2))
67-
case RightNot(bot, t1, phi) => (bot, Seq(t1))
68-
case RightForall(bot, t1, phi, x) => (bot, Seq(t1))
69-
case RightExists(bot, t1, phi, x, t) => (bot, Seq(t1))
70-
case RightExistsOne(bot, t1, phi, x) => (bot, Seq(t1))
71-
case Weakening(bot, t1) => (bot, Seq(t1))
72-
case LeftRefl(bot, t1, phi) => (bot, Seq(t1))
73-
case RightRefl(bot, phi) => (bot, null)
74-
case LeftSubstEq(bot, t1, equals, lambdaPhi) =>
45+
ps match
46+
case Restate(_, _) => opening = ".from("
47+
case RestateTrue(_) => tacticName = "Restate"
48+
case LeftSubstEq(_, _, equals, lambdaPhi) =>
7549
tacticName = s"LeftSubstEq.withParametersSimple(List(${equals
7650
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
7751
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
78-
(bot, Seq(t1))
79-
case RightSubstEq(bot, t1, equals, lambdaPhi) =>
52+
case RightSubstEq(_, _, equals, lambdaPhi) =>
8053
tacticName = s"RightSubstEq.withParametersSimple(List(${equals
8154
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
8255
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
83-
(bot, Seq(t1))
84-
case LeftSubstIff(bot, t1, equals, lambdaPhi) =>
56+
case LeftSubstIff(_, _, equals, lambdaPhi) =>
8557
tacticName = s"LeftSubstIff.withParametersSimple(List(${equals
8658
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
8759
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
88-
(bot, Seq(t1))
89-
case RightSubstIff(bot, t1, equals, lambdaPhi) =>
60+
case RightSubstIff(_, _, equals, lambdaPhi) =>
9061
tacticName = s"RightSubstIff.withParametersSimple(List(${equals
9162
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
9263
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
93-
(bot, Seq(t1))
94-
case InstSchema(bot, t1, mCon, mPred, mTerm) =>
64+
case InstSchema(_, _, mCon, mPred, mTerm) =>
9565
if mCon.isEmpty && mPred.isEmpty then
9666
tacticName = s"InstFunSchema(Map(${mTerm.toList
9767
.map((k, v) => s"${asFrontLabel(k)} -> ${any2code(v.body)}")
9868
.mkString(", ")}))"
99-
(bot, Seq(t1))
10069
else if mCon.isEmpty && mTerm.isEmpty then
10170
tacticName = s"InstPredSchema(Map(${mPred.toList
10271
.map((k, v) => s"${asFrontLabel(k)} -> ${any2code(v.body)}")
10372
.mkString(", ")}))"
104-
(bot, Seq(t1))
10573
else throw new Exception("InstSchema not implemented")
106-
case _ => throw new Exception(s"Tactic ${ps.getClass.getName} not implemented")
107-
)
74+
case _ => ()
10875

10976
indent(
11077
s"val ${varPrefix}_$stepNum = " + (
111-
if (step_ref_seq != null && step_ref_seq.size == 1 && stepNum > 0 && step_ref_seq.head + 1 == stepNum)
112-
then s"thenHave(${any2code(bot_)}) by $tacticName"
78+
if (ps.premises.size == 1 && ps.premises.head + 1 == stepNum && stepNum > 0)
79+
then s"thenHave(${any2code(ps.bot)}) by $tacticName"
11380
else
114-
s"have(${any2code(bot_)}) by $tacticName" + (
115-
if step_ref_seq == null then ""
116-
else s"$opening${step_ref_seq.map(index2stepvar).mkString(", ")}$closing"
81+
s"have(${any2code(ps.bot)}) by $tacticName" + (
82+
if ps.premises.size == 0 then ""
83+
else s"$opening${ps.premises.map(index2stepvar).mkString(", ")}$closing"
11784
)
11885
)
11986
)
12087
}
12188

122-
p.steps.zipWithIndex.map((ps, i) => scproofstep2code(ps, i, premises, varPrefix)).mkString("\n")
89+
p.steps.zipWithIndex.map((ps, i) => scproofstep2code(ps, i, implicitPremises, varPrefix)).mkString("\n")
12390
}
12491
unindent(scproof2codeAux(p))
12592
}
12693

127-
def generateTheoremCode(name: String, statement: K.Sequent, proof: K.SCProof): String = {
94+
private def extractFormulasFromProof(proof: K.SCProof): Set[K.Formula] =
95+
proof.steps.foldLeft(Set.empty[K.Formula])((prev, next) => {
96+
prev ++ (next match
97+
case sp @ SCSubproof(subproof, _) => extractFormulasFromProof(subproof)
98+
case LeftSubstEq(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
99+
case RightSubstEq(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
100+
case LeftSubstIff(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
101+
case RightSubstIff(_, _, _, lambdaPhi) => Seq(lambdaPhi._2, K.sequentToFormula(next.bot))
102+
case _ => Seq(K.sequentToFormula(next.bot))
103+
)
104+
})
105+
106+
private def extractVariables(
107+
formulas: Set[K.Formula]
108+
): (Set[K.VariableLabel], Set[K.SchematicFunctionLabel], Set[K.VariableFormulaLabel], Set[K.SchematicPredicateLabel], Set[K.SchematicConnectorLabel]) =
109+
def extractVariablesAux(
110+
formula: K.Formula
111+
): (Set[K.VariableLabel], Set[K.SchematicFunctionLabel], Set[K.VariableFormulaLabel], Set[K.SchematicPredicateLabel], Set[K.SchematicConnectorLabel]) =
112+
var variableSet = formula.schematicTermLabels.collect { case v: K.VariableLabel => v }
113+
var functionSet = formula.schematicTermLabels.collect { case f: K.SchematicFunctionLabel => f }
114+
var formulaVariableSet = formula.schematicAtomicLabels.collect { case v: K.VariableFormulaLabel => v }
115+
var predicateSet = formula.schematicAtomicLabels.collect { case p: K.SchematicPredicateLabel => p }
116+
var connectorSet = formula.schematicConnectorLabels.collect { case c: K.SchematicConnectorLabel => c }
117+
(variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet)
118+
119+
formulas.foldLeft(
120+
(Set.empty[K.VariableLabel], Set.empty[K.SchematicFunctionLabel], Set.empty[K.VariableFormulaLabel], Set.empty[K.SchematicPredicateLabel], Set.empty[K.SchematicConnectorLabel])
121+
)((prev, next) => {
122+
val (variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet) = prev
123+
val (variableSet_, functionSet_, formulaVariableSet_, predicateSet_, connectorSet_) = extractVariablesAux(next)
124+
(
125+
variableSet ++ variableSet_,
126+
functionSet ++ functionSet_,
127+
formulaVariableSet ++ formulaVariableSet_,
128+
predicateSet ++ predicateSet_,
129+
connectorSet ++ connectorSet_
130+
)
131+
})
132+
133+
private def generateVariablesCode(formulas: Set[K.Formula], accessibility: String): String =
134+
val (variableSet, functionSet, formulaVariableSet, predicateSet, connectorSet) = extractVariables(formulas)
135+
val access = if accessibility != "" then accessibility.strip() + " " else ""
136+
(variableSet.map(v => access + s"val ${v.id} = variable").toList.sorted ++
137+
functionSet.map(f => access + s"val ${f.id} = function[${f.arity}]").toList.sorted ++
138+
formulaVariableSet.map(v => access + s"val ${v.id} = formulaVariable").toList.sorted ++
139+
predicateSet.map(p => access + s"val ${p.id} = predicate[${p.arity}]").toList.sorted ++
140+
connectorSet.map(c => access + s"val ${c.id} = connector[${c.arity}]").toList.sorted).mkString("\n")
141+
142+
private def generateVariablesCode(statement: K.Sequent, proof: K.SCProof, accessibility: String = "private"): String =
143+
generateVariablesCode(extractFormulasFromProof(proof) + K.sequentToFormula(statement), accessibility)
144+
145+
private def generateTheoremCode(name: String, statement: K.Sequent, proof: K.SCProof): String = {
128146
s"val $name = Theorem(\n" +
129147
indent(any2code(statement)) +
130148
s"\n) {\n" +
131149
indent(scproof2code(proof)) +
132150
s"\n}"
133151
}
134152

153+
def generateStandaloneTheoremFileContent(name: String, statement: K.Sequent, proof: K.SCProof): String =
154+
val camelName = "[A-Za-z0-9]+".r.findAllIn(name).map(_.capitalize).mkString
155+
s"object $camelName extends lisa.Main {\n\n" +
156+
indent(
157+
generateVariablesCode(statement, proof) +
158+
"\n\n" +
159+
generateTheoremCode(name, statement, proof)
160+
) +
161+
"\n}"
162+
135163
}

0 commit comments

Comments
 (0)