Paperproof v2.4.0 - lean

Added

• Use Paperproof's parser from the terminal

  @celainica contributed terminal.lean (link), a script that lets you use Paperproof from within a terminal. This is useful for data processing in AI applications.

  For example, if you have the following theorem in myFile.lean file:

  theorem simple_proof (p q : Prop) (hp : p) (hq : q) : p ∧ q := by
    apply And.intro
    exact hp
    exact hq
  

  you can run lake exe terminal myFile.lean simple_proof myOutput.json, and get the following output:

  [{
    "theorems": [],
    "tacticString": "apply And.intro",
    "tacticDependsOn": ["_uniq.11", "_uniq.12"],
    "spawnedGoals": [],
    "position": {"stop": {"line": 0, "character": 0}, "start": {"line": 0, "character": 0}},
    "goalsAfter": [
      {
        "username": "left", "type": "p", "id": "_uniq.22",
        "hyps": [
          {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
          {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
          {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
          {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
        ]
      },
      {
        "username": "right", "type": "q", "id": "_uniq.23",
        "hyps": [
          {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
          {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
          {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
          {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
        ]
      }
    ],
    "goalBefore": {
      "username": "[anonymous]", "type": "p ∧ q", "id": "_uniq.15",
      "hyps": [
        {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
        {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
        {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
        {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
      ]
    }
  }, {
    "theorems": [],
    "tacticString": "exact hp",
    "tacticDependsOn": ["_uniq.13"],
    "spawnedGoals": [],
    "position": {"stop": {"line": 0, "character": 0}, "start": {"line": 0, "character": 0}},
    "goalsAfter": [],
    "goalBefore": {
      "username": "left", "type": "p", "id": "_uniq.22",
      "hyps": [
        {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
        {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
        {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
        {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
      ]
    }
  }, {
    "theorems": [],
    "tacticString": "exact hq",
    "tacticDependsOn": ["_uniq.14"],
    "spawnedGoals": [],
    "position": {"stop": {"line": 0, "character": 0}, "start": {"line": 0, "character": 0}},
    "goalsAfter": [],
    "goalBefore": {
      "username": "right", "type": "q", "id": "_uniq.23",
      "hyps": [
        {"value": null, "username": "p", "type": "Prop", "isProof": "universe", "id": "_uniq.11"},
        {"value": null, "username": "q", "type": "Prop", "isProof": "universe", "id": "_uniq.12"},
        {"value": null, "username": "hp", "type": "p", "isProof": "proof", "id": "_uniq.13"},
        {"value": null, "username": "hq", "type": "q", "isProof": "proof", "id": "_uniq.14"}
      ]
    }
  }]
  

Updated

• Made Paperproof support Lean v4.24.0.