Skip to content

Commit 1608480

Browse files
augustepoirouxaugustepoiroux
committed
Improve conversion from kernel to code
1 parent 860fc1f commit 1608480

File tree

2 files changed

+147
-105
lines changed

2 files changed

+147
-105
lines changed

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

Lines changed: 36 additions & 24 deletions
Original file line numberDiff line numberDiff line change
@@ -29,12 +29,13 @@ object Kernel2Code extends lisa.Main {
2929
thenHave(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) by RightForall
3030
}
3131

32-
// println(prettyProof(thm1.highProof.get))
33-
// println(prettySCProof(thm1.kernelProof.get))
34-
// println(scproof2code(thm1.kernelProof.get))
35-
// println(scproof2code(optimizeProofIteratively(thm1.kernelProof.get)))
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)))
3635

37-
val thm1_raw = Theorem(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) {
36+
val thm1_raw = Theorem(
37+
∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
38+
) {
3839
val s_0 = have(S(x, y) ⊢ S(x, y)) subproof {
3940
val s_0_0 = have(S(x, y) ⊢ S(x, y)) by Restate
4041
}
@@ -52,7 +53,9 @@ object Kernel2Code extends lisa.Main {
5253
}
5354
}
5455

55-
val thm1_optimized = Theorem(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) {
56+
val thm1_optimized = Theorem(
57+
∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
58+
) {
5659
val s_0 = have(S(x, y) ⊢ S(x, y)) by Restate
5760
val s_1 = thenHave(∀(y, S(x, y)) ⊢ S(x, y)) by LeftForall
5861
val s_2 = thenHave(∀(y, S(x, y)) ⊢ ∃(x, S(x, y))) by RightExists
@@ -85,12 +88,13 @@ object Kernel2Code extends lisa.Main {
8588
have(thesis) by Tautology.from(forward, backward)
8689
}
8790

88-
// println(prettyProof(thm2.highProof.get))
89-
// println(prettySCProof(thm2.kernelProof.get))
90-
// println(scproof2code(thm2.kernelProof.get))
91-
// println(scproof2code(optimizeProofIteratively(thm2.kernelProof.get)))
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)))
9294

93-
val thm2_raw = Theorem((∀(x, Q(x)) /\ ∀(x, R(x))) <=> ∀(x, Q(x) /\ R(x))) {
95+
val thm2_raw = Theorem(
96+
((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))
97+
) {
9498
val s_0 = have((∀(x, R(x)), ∀(x, Q(x))) ⊢ ∀(x, (Q(x) ∧ R(x)))) subproof {
9599
val s_0_0 = have((R(x), Q(x)) ⊢ (Q(x) ∧ R(x))) subproof {
96100
val s_0_0_0 = have((R(x), Q(x)) ⊢ (Q(x) ∧ R(x))) by Restate
@@ -155,7 +159,9 @@ object Kernel2Code extends lisa.Main {
155159
}
156160
}
157161

158-
val thm2_optimized = Theorem((∀(x, Q(x)) /\ ∀(x, R(x))) <=> ∀(x, Q(x) /\ R(x))) {
162+
val thm2_optimized = Theorem(
163+
((∀(x, Q(x)) ∧ ∀(x, R(x))) <=> ∀(x, (Q(x) ∧ R(x))))
164+
) {
159165
val s_0 = have((R(x), Q(x)) ⊢ (Q(x) ∧ R(x))) by Restate
160166
val s_1 = thenHave((R(x), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall
161167
val s_2 = thenHave((∀(x, R(x)), ∀(x, Q(x))) ⊢ (Q(x) ∧ R(x))) by LeftForall
@@ -190,12 +196,13 @@ object Kernel2Code extends lisa.Main {
190196
have(thesis) by Tautology.from(step1, step1 of (x := f(x)))
191197
}
192198

193-
// println(prettyProof(thm3.highProof.get))
194-
// println(prettySCProof(thm3.kernelProof.get))
195-
// println(scproof2code(thm3.kernelProof.get))
196-
// println(scproof2code(optimizeProofIteratively(thm3.kernelProof.get)))
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)))
197202

198-
val thm3_raw = Theorem(∀(x, Q(x) ==> Q(f(x))) |- (Q(x) ==> Q(f(f(x))))) {
203+
val thm3_raw = Theorem(
204+
∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))
205+
) {
199206
val s_0 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ ∀(x, (Q(x) ==> Q(f(x))))) subproof {
200207
val s_0_0 = have(∀(x, (Q(x) ==> Q(f(x)))) ⊢ ∀(x, (Q(x) ==> Q(f(x))))) by Hypothesis
201208
}
@@ -260,7 +267,9 @@ object Kernel2Code extends lisa.Main {
260267
}
261268
}
262269

263-
val thm3_optimized = Theorem(∀(x, Q(x) ==> Q(f(x))) |- (Q(x) ==> Q(f(f(x))))) {
270+
val thm3_optimized = Theorem(
271+
∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(f(x))))
272+
) {
264273
val s_0 = have((∀(x, (Q(x) ==> Q(f(x)))), (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) by Restate
265274
val s_1 = thenHave(∀(x, (Q(x) ==> Q(f(x)))) ⊢ (Q(x) ==> Q(f(x)))) by LeftForall
266275
val s_2 = thenHave(∀(x_1, (Q(x_1) ==> Q(f(x_1)))) ⊢ (Q(f(x)) ==> Q(f(f(x))))) by InstFunSchema(Map(x -> f(x)))
@@ -292,12 +301,13 @@ object Kernel2Code extends lisa.Main {
292301
have(thesis) by Tableau
293302
}
294303

295-
// println(prettyProof(thm1bis.highProof.get))
296-
// println(prettySCProof(thm1bis.kernelProof.get))
297-
// println(scproof2code(thm1bis.kernelProof.get))
298-
// println(scproof2code(optimizeProofIteratively(thm1bis.kernelProof.get)))
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)))
299307

300-
val thm1bis_raw = Theorem(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) {
308+
val thm1bis_raw = Theorem(
309+
∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
310+
) {
301311
val s_0 = have(∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))) subproof {
302312
val s_0_0 = have((S(x, y_1), ¬(S(x, y_1))) ⊢ ()) by Restate
303313
val s_0_1 = thenHave((S(x, y_1), ∀(x_2, ¬(S(x_2, y_1)))) ⊢ ()) by LeftForall
@@ -310,7 +320,9 @@ object Kernel2Code extends lisa.Main {
310320
}
311321
}
312322

313-
val thm1bis_optimized = Theorem(∃(x, ∀(y, S(x, y))) |- ∀(y, ∃(x, S(x, y)))) {
323+
val thm1bis_optimized = Theorem(
324+
∃(x, ∀(y, S(x, y))) ⊢ ∀(y, ∃(x, S(x, y)))
325+
) {
314326
val s_0 = have((S(x, y_1), ¬(S(x, y_1))) ⊢ ()) by Restate
315327
val s_1 = thenHave((S(x, y_1), ∀(x_2, ¬(S(x_2, y_1)))) ⊢ ()) by LeftForall
316328
val s_2 = thenHave((∀(x_2, ¬(S(x_2, y_1))), ∀(y, S(x, y))) ⊢ ()) by LeftForall

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

Lines changed: 111 additions & 81 deletions
Original file line numberDiff line numberDiff line change
@@ -2,104 +2,134 @@ package lisa.utils
22

33
import lisa.kernel.proof.SequentCalculus.*
44
import lisa.utils.K
5+
import lisa.utils.KernelHelpers.lambda
56
import lisa.prooflib.ProofTacticLib.*
6-
import lisa.fol.FOLHelpers.*
77
import lisa.fol.FOL as F
8-
import lisa.utils.KernelHelpers.lambda
8+
import lisa.fol.FOLHelpers.*
99

1010
object ProofsConverter {
1111

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

16-
def scproof2code(p: K.SCProof, premises: Seq[String] = Seq.empty, indent: Int = 0, varPrefix: String = "s"): String = {
17-
def scproofstep2line(ps: SCProofStep, stepNum: Int, premises: Seq[String], indent: Int, varPrefix: String): String = {
18-
def sequent2code(sq: Sequent): String = asFront(sq).toString.replace("⇒", "==>").replace("⇔", "<=>")
19-
def formula2code(form: K.Formula): String = asFront(form).toString.replace("⇒", "==>").replace("⇔", "<=>")
20-
def term2code(term: K.Term): String = asFront(term).toString.replace("⇒", "==>").replace("⇔", "<=>")
16+
private def indent(s: String, indent: Int = 2): String = s.split("\n").map(" " * indent + _).mkString("\n")
17+
private def unindent(s: String, indent: Int = 2): String = s.split("\n").map(_.drop(indent)).mkString("\n")
18+
19+
private def any2code(a: K.Sequent | K.Formula | K.Term): String = (a match
20+
case sq: K.Sequent => asFront(sq)
21+
case form: K.Formula => asFront(form)
22+
case term: K.Term => asFront(term)
23+
).toString.replace("⇒", "==>").replace("⇔", "<=>")
24+
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 = {
2128

22-
def index2stepvar(i: Int): String =
23-
if i < -premises.size then throw new Exception(s"step $i is not defined")
24-
else if i < 0 then premises(-i - 1)
25-
else s"${varPrefix}_$i"
29+
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)
32+
else s"${varPrefix}_$i"
2633

27-
val varDecl = " " * indent + s"val ${varPrefix}_$stepNum = "
28-
ps match
29-
case Sorry(_) => "sorry"
30-
case sp @ SCSubproof(_, _) =>
31-
varDecl + s"have(${sequent2code(sp.bot)}) subproof {\n" + scproof2code(sp.sp, sp.premises.map(index2stepvar), indent + 1, s"${varPrefix}_$stepNum") + "\n" + " " * indent + "}"
32-
case _ =>
33-
var tacticName = ps.getClass.getSimpleName
34-
var opening = "("
35-
var closing = ")"
36-
val (bot_, step_ref_seq) = (ps match
37-
case Restate(bot, t1) =>
38-
opening = ".from("
39-
(bot, Seq(t1))
40-
case RestateTrue(bot) =>
41-
tacticName = "Restate"
42-
(bot, null)
43-
case Hypothesis(bot, phi) => (bot, null)
44-
case Cut(bot, t1, t2, phi) => (bot, Seq(t1, t2))
45-
case LeftAnd(bot, t1, phi, psi) => (bot, Seq(t1))
46-
case LeftOr(bot, t, disjuncts) => (bot, t)
47-
case LeftImplies(bot, t1, t2, phi, psi) => (bot, Seq(t1, t2))
48-
case LeftIff(bot, t1, phi, psi) => (bot, Seq(t1))
49-
case LeftNot(bot, t1, phi) => (bot, Seq(t1))
50-
case LeftForall(bot, t1, phi, x, t) => (bot, Seq(t1))
51-
case LeftExists(bot, t1, phi, x) => (bot, Seq(t1))
52-
case LeftExistsOne(bot, t1, phi, x) => (bot, Seq(t1))
53-
case RightAnd(bot, t, conjuncts) => (bot, t)
54-
case RightOr(bot, t1, phi, psi) => (bot, Seq(t1))
55-
case RightImplies(bot, t1, phi, psi) => (bot, Seq(t1))
56-
case RightIff(bot, t1, t2, phi, psi) => (bot, Seq(t1, t2))
57-
case RightNot(bot, t1, phi) => (bot, Seq(t1))
58-
case RightForall(bot, t1, phi, x) => (bot, Seq(t1))
59-
case RightExists(bot, t1, phi, x, t) => (bot, Seq(t1))
60-
case RightExistsOne(bot, t1, phi, x) => (bot, Seq(t1))
61-
case Weakening(bot, t1) => (bot, Seq(t1))
62-
case LeftRefl(bot, t1, phi) => (bot, Seq(t1))
63-
case RightRefl(bot, phi) => (bot, null)
64-
case LeftSubstEq(bot, t1, equals, lambdaPhi) => (bot, Seq(t1))
65-
case RightSubstEq(bot, t1, equals, lambdaPhi) => (bot, Seq(t1))
66-
case LeftSubstIff(bot, t1, equals, lambdaPhi) =>
67-
tacticName = s"LeftSubstIff.withParametersSimple(List(${equals
68-
.map((a, b) => s"((${formula2code(a.body)}), (${formula2code(b.body)}))")
69-
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi._2)}))"
70-
(bot, Seq(t1))
71-
case RightSubstIff(bot, t1, equals, lambdaPhi) =>
72-
tacticName = s"RightSubstIff.withParametersSimple(List(${equals
73-
.map((a, b) => s"((${formula2code(a.body)}), (${formula2code(b.body)}))")
74-
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi._2)}))"
75-
(bot, Seq(t1))
76-
case InstSchema(bot, t1, mCon, mPred, mTerm) =>
77-
if mCon.isEmpty && mPred.isEmpty then
78-
tacticName = s"InstFunSchema(Map(${mTerm.toList
79-
.map((k, v) => s"${asFrontLabel(k)} -> ${term2code(v.body)}")
80-
.mkString(", ")}))"
34+
ps match
35+
case Sorry(_) => "sorry"
36+
case sp @ SCSubproof(_, _) =>
37+
indent(
38+
s"val ${varPrefix}_$stepNum = have(${any2code(sp.bot)}) subproof {\n" +
39+
scproof2codeAux(sp.sp, s"${varPrefix}_$stepNum", sp.premises.map(index2stepvar)) +
40+
"\n}"
41+
)
42+
case _ =>
43+
var tacticName = ps.getClass.getSimpleName
44+
var opening = "("
45+
var closing = ")"
46+
val (bot_, step_ref_seq) = (ps match
47+
case Restate(bot, t1) =>
48+
opening = ".from("
8149
(bot, Seq(t1))
82-
else if mCon.isEmpty && mTerm.isEmpty then
83-
tacticName = s"InstPredSchema(Map(${mPred.toList
84-
.map((k, v) => s"${asFrontLabel(k)} -> ${formula2code(v.body)}")
85-
.mkString(", ")}))"
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) =>
75+
tacticName = s"LeftSubstEq.withParametersSimple(List(${equals
76+
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
77+
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
8678
(bot, Seq(t1))
87-
else throw new Exception("InstSchema not implemented")
88-
case _ => throw new Exception(s"Tactic ${ps.getClass.getName} not implemented")
89-
)
79+
case RightSubstEq(bot, t1, equals, lambdaPhi) =>
80+
tacticName = s"RightSubstEq.withParametersSimple(List(${equals
81+
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
82+
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
83+
(bot, Seq(t1))
84+
case LeftSubstIff(bot, t1, equals, lambdaPhi) =>
85+
tacticName = s"LeftSubstIff.withParametersSimple(List(${equals
86+
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
87+
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
88+
(bot, Seq(t1))
89+
case RightSubstIff(bot, t1, equals, lambdaPhi) =>
90+
tacticName = s"RightSubstIff.withParametersSimple(List(${equals
91+
.map((a, b) => s"((${any2code(a.body)}), (${any2code(b.body)}))")
92+
.mkString(", ")}), lambda(Seq(${lambdaPhi._1.map(asFrontLabel).mkString(", ")}), ${any2code(lambdaPhi._2)}))"
93+
(bot, Seq(t1))
94+
case InstSchema(bot, t1, mCon, mPred, mTerm) =>
95+
if mCon.isEmpty && mPred.isEmpty then
96+
tacticName = s"InstFunSchema(Map(${mTerm.toList
97+
.map((k, v) => s"${asFrontLabel(k)} -> ${any2code(v.body)}")
98+
.mkString(", ")}))"
99+
(bot, Seq(t1))
100+
else if mCon.isEmpty && mTerm.isEmpty then
101+
tacticName = s"InstPredSchema(Map(${mPred.toList
102+
.map((k, v) => s"${asFrontLabel(k)} -> ${any2code(v.body)}")
103+
.mkString(", ")}))"
104+
(bot, Seq(t1))
105+
else throw new Exception("InstSchema not implemented")
106+
case _ => throw new Exception(s"Tactic ${ps.getClass.getName} not implemented")
107+
)
90108

91-
varDecl + (
92-
if (step_ref_seq != null && step_ref_seq.size == 1 && stepNum > 0 && step_ref_seq.head + 1 == stepNum)
93-
then s"thenHave(${sequent2code(bot_)}) by $tacticName"
94-
else
95-
s"have(${sequent2code(bot_)}) by $tacticName" + (
96-
if step_ref_seq == null then ""
97-
else s"$opening${step_ref_seq.map(index2stepvar).mkString(", ")}$closing"
109+
indent(
110+
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"
113+
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"
117+
)
98118
)
99-
)
119+
)
120+
}
121+
122+
p.steps.zipWithIndex.map((ps, i) => scproofstep2code(ps, i, premises, varPrefix)).mkString("\n")
100123
}
124+
unindent(scproof2codeAux(p))
125+
}
101126

102-
p.steps.zipWithIndex.map((ps, i) => scproofstep2line(ps, i, premises, indent, varPrefix)).mkString("\n")
127+
def generateTheoremCode(name: String, statement: K.Sequent, proof: K.SCProof): String = {
128+
s"val $name = Theorem(\n" +
129+
indent(any2code(statement)) +
130+
s"\n) {\n" +
131+
indent(scproof2code(proof)) +
132+
s"\n}"
103133
}
104134

105135
}

0 commit comments

Comments
 (0)