|
| 1 | +import lisa.automation.Tableau |
| 2 | +import lisa.utils.ProofsConverter.* |
1 | 3 | import lisa.utils.parsing.ProofPrinter._ |
2 | 4 | import lisa.utils.FOLPrinter.* |
3 | | -import lisa.kernel.proof.SequentCalculus.* |
4 | | -import lisa.utils.K |
5 | | -import lisa.prooflib.ProofTacticLib.* |
6 | | -import lisa.fol.FOLHelpers.* |
7 | | -import lisa.fol.FOL as F |
8 | | -import lisa.utils.KernelHelpers.lambda |
9 | 5 | import lisa.utils.ProofsShrink.* |
10 | | -import lisa.automation.Tableau |
11 | | - |
12 | | -// TODO: fix printing of ∧ and ∨ with > 2 arguments, currently handled as recursive binary operators |
13 | | -// TODO: remove unnecessary variables "val s_..." in generated proofs |
14 | | -// TODO: generate more realistic variable names |
15 | | -// TODO: handle automatic global variable declaration before theorems/proofs |
16 | | - |
17 | | -def scproof2code(p: K.SCProof, premises: Seq[String] = Seq.empty, indent: Int = 0, varPrefix: String = "s"): String = { |
18 | | - def scproofstep2line(ps: SCProofStep, stepNum: Int, premises: Seq[String], indent: Int, varPrefix: String): String = { |
19 | | - def sequent2code(sq: Sequent): String = asFront(sq).toString.replace("⇒", "==>").replace("⇔", "<=>") |
20 | | - def formula2code(form: K.Formula): String = asFront(form).toString.replace("⇒", "==>").replace("⇔", "<=>") |
21 | | - def term2code(term: K.Term): String = asFront(term).toString.replace("⇒", "==>").replace("⇔", "<=>") |
22 | | - |
23 | | - def index2stepvar(i: Int): String = |
24 | | - if i < -premises.size then throw new Exception(s"step $i is not defined") |
25 | | - else if i < 0 then premises(-i - 1) |
26 | | - else s"${varPrefix}_$i" |
27 | | - |
28 | | - val varDecl = " " * indent + s"val ${varPrefix}_$stepNum = " |
29 | | - ps match |
30 | | - case Sorry(_) => "sorry" |
31 | | - case sp @ SCSubproof(_, _) => |
32 | | - varDecl + s"have(${sequent2code(sp.bot)}) subproof {\n" + scproof2code(sp.sp, sp.premises.map(index2stepvar), indent + 1, s"${varPrefix}_$stepNum") + "\n" + " " * indent + "}" |
33 | | - case _ => |
34 | | - var tacticName = ps.getClass.getSimpleName |
35 | | - var opening = "(" |
36 | | - var closing = ")" |
37 | | - val (bot_, step_ref_seq) = (ps match |
38 | | - case Restate(bot, t1) => |
39 | | - opening = ".from(" |
40 | | - (bot, Seq(t1)) |
41 | | - case RestateTrue(bot) => |
42 | | - tacticName = "Restate" |
43 | | - (bot, null) |
44 | | - case Hypothesis(bot, phi) => (bot, null) |
45 | | - case Cut(bot, t1, t2, phi) => (bot, Seq(t1, t2)) |
46 | | - case LeftAnd(bot, t1, phi, psi) => (bot, Seq(t1)) |
47 | | - case LeftOr(bot, t, disjuncts) => (bot, t) |
48 | | - case LeftImplies(bot, t1, t2, phi, psi) => (bot, Seq(t1, t2)) |
49 | | - case LeftIff(bot, t1, phi, psi) => (bot, Seq(t1)) |
50 | | - case LeftNot(bot, t1, phi) => (bot, Seq(t1)) |
51 | | - case LeftForall(bot, t1, phi, x, t) => (bot, Seq(t1)) |
52 | | - case LeftExists(bot, t1, phi, x) => (bot, Seq(t1)) |
53 | | - case LeftExistsOne(bot, t1, phi, x) => (bot, Seq(t1)) |
54 | | - case RightAnd(bot, t, conjuncts) => (bot, t) |
55 | | - case RightOr(bot, t1, phi, psi) => (bot, Seq(t1)) |
56 | | - case RightImplies(bot, t1, phi, psi) => (bot, Seq(t1)) |
57 | | - case RightIff(bot, t1, t2, phi, psi) => (bot, Seq(t1, t2)) |
58 | | - case RightNot(bot, t1, phi) => (bot, Seq(t1)) |
59 | | - case RightForall(bot, t1, phi, x) => (bot, Seq(t1)) |
60 | | - case RightExists(bot, t1, phi, x, t) => (bot, Seq(t1)) |
61 | | - case RightExistsOne(bot, t1, phi, x) => (bot, Seq(t1)) |
62 | | - case Weakening(bot, t1) => (bot, Seq(t1)) |
63 | | - case LeftRefl(bot, t1, phi) => (bot, Seq(t1)) |
64 | | - case RightRefl(bot, phi) => (bot, null) |
65 | | - case LeftSubstEq(bot, t1, equals, lambdaPhi) => (bot, Seq(t1)) |
66 | | - case RightSubstEq(bot, t1, equals, lambdaPhi) => (bot, Seq(t1)) |
67 | | - case LeftSubstIff(bot, t1, equals, lambdaPhi) => |
68 | | - tacticName = s"LeftSubstIff(List(${equals |
69 | | - .map((a, b) => s"((${formula2code(a)}), (${formula2code(b)}))") |
70 | | - .mkString(", ")}), lambda(Seq(${lambdaPhi.vars.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi.body)}))" |
71 | | - (bot, Seq(t1)) |
72 | | - case RightSubstIff(bot, t1, equals, lambdaPhi) => |
73 | | - tacticName = s"RightSubstIff(List(${equals |
74 | | - .map((a, b) => s"((${formula2code(a)}), (${formula2code(b)}))") |
75 | | - .mkString(", ")}), lambda(Seq(${lambdaPhi.vars.map(asFrontLabel).mkString(", ")}), ${formula2code(lambdaPhi.body)}))" |
76 | | - (bot, Seq(t1)) |
77 | | - case InstSchema(bot, t1, mCon, mPred, mTerm) => |
78 | | - if mCon.isEmpty && mPred.isEmpty then |
79 | | - tacticName = s"InstFunSchema(Map(${mTerm.toList |
80 | | - .map((k, v) => s"${asFrontLabel(k)} -> ${term2code(v.body)}") |
81 | | - .mkString(", ")}))" |
82 | | - (bot, Seq(t1)) |
83 | | - else if mCon.isEmpty && mTerm.isEmpty then |
84 | | - tacticName = s"InstPredSchema(Map(${mPred.toList |
85 | | - .map((k, v) => s"${asFrontLabel(k)} -> ${formula2code(v.body)}") |
86 | | - .mkString(", ")}))" |
87 | | - (bot, Seq(t1)) |
88 | | - else throw new Exception("InstSchema not implemented") |
89 | | - case _ => throw new Exception(s"Tactic ${ps.getClass.getName} not implemented") |
90 | | - ) |
91 | | - |
92 | | - varDecl + ( |
93 | | - if (step_ref_seq != null && step_ref_seq.size == 1 && stepNum > 0 && step_ref_seq.head + 1 == stepNum) |
94 | | - then s"thenHave(${sequent2code(bot_)}) by $tacticName" |
95 | | - else |
96 | | - s"have(${sequent2code(bot_)}) by $tacticName" + ( |
97 | | - if step_ref_seq == null then "" |
98 | | - else s"$opening${step_ref_seq.map(index2stepvar).mkString(", ")}$closing" |
99 | | - ) |
100 | | - ) |
101 | | - } |
102 | | - |
103 | | - p.steps.zipWithIndex.map((ps, i) => scproofstep2line(ps, i, premises, indent, varPrefix)).mkString("\n") |
104 | | -} |
105 | | - |
106 | | -object MLExtract extends lisa.Main { |
107 | | - |
108 | | - /* |
109 | | - You may use the following tactics: |
110 | | - - Restate | "Trivially" true Sequent. Deals with alpha equivalence and most propositional rules but not distributivity |
111 | | - - Weakening | "Trivially" weaker sequent (than the previous one). |
112 | | - - Tautology.from | Anything that can be solved by propositional reasoning alone |
113 | | -
|
114 | | - - LeftForall | To introduce a ∀ quantifier in an assumption |
115 | | - - LeftExists | To introduce a ∃ quantifier in an assumption (the variable must not be free somewhere else) |
116 | | - - RightForall | To introduce a ∀ quantifier in the conclusion (the variable must not be free somewhere else) |
117 | | - - RightExists | To introduce a ∃ quantifier in the conclusion |
118 | | - - InstantiateForall | To obtain a formula of the form P(t) from a quantified assumption ∀(x, P(x)) |
119 | | -
|
120 | | -
|
121 | 6 |
|
122 | | - thm1 and thm2 illustrate how those tactics can be used, as well as the usage of "assume", "have", "thenHave", "by", "thesis", "of" and "subproof". |
123 | | - */ |
| 7 | +object Kernel2Code extends lisa.Main { |
124 | 8 |
|
125 | 9 | val x = variable |
126 | 10 | val y = variable |
|
0 commit comments