TOOL: Given one or more Lean files, extract the implication status of all equations appearing in the file

[teorth]

Given one or more Lean files as input, extract all the implications and proof_wanted statements from that file. Then, for any two equations i, j that appear anywhere in these implications, report the status of the implication i => j as one of the following:

• Explicitly proven. This implication is an explicit theorem in the files.
• Implicitly proven. This implication is not explicitly a theorem, but can be derived from the explicit theorems in the files.
• Explicitly conjectured. This implication is not proven, but is an explicit proof_wanted in the files.
• Implicitly conjectured. This implication is not proven or explicitly conjectured, but follows from the explicit theorems and conjectures in the files.
• Open. The implication is not even conjectured to be true or false.
• Implicitly conjectured false. The implication is not disproven or explicitly conjectured false, but its falsity follows from the explicit theorems and conjectures in the files.
• Explicitly conjectured false. The negation of this implication is an explicit proof_wanted in the files, but this negation does not follow from proven theorems.
• Implicitly disproven. The negation of this implication is not an explicit theorem in the files, but follows from these theorems.
• Explicitly disproven. The negation of this implication is an explicit theorem in the files.

[Command-Master]

claim

[Command-Master]

Should this tool be a metaprogram, or is it fine for it to shallowly parse the files (i.e. search for (G: Type*) [Magma G] (G: Equation(\d+) G) : Equation(\d+) G and ∃ (G: Type) (_: Magma G), Equation(\d+) G ∧ ¬ Equation(\d+) G, and add special suuport for Equation1_true)?

[dwrensha]

22 demonstrates a starting point for one way to do this kind of analysis directly in Lean.

[teorth]

Should this tool be a metaprogram, or is it fine for it to shallowly parse the files (i.e. search for (G: Type*) [Magma G] (G: Equation(\d+) G) : Equation(\d+) G and ∃ (G: Type) (_: Magma G), Equation(\d+) G ∧ ¬ Equation(\d+) G, and add special suuport for Equation1_true)?

In the longer term I think a metaprogram would be the most robust solution (that would also be adaptable for other projects), but a "quick and dirty" shallow approach may be faster in the short term. So it could go either way. One compromise is to try to write a quick and dirty program, but in a way that many of the components of the code could be refactored into a more robust long-term solution later.

[Command-Master]

If #22 could be modified so Implication contains whether it's conjectured I could directly process the Output structure it produces

[Command-Master]

Isn't this already implemented in scripts/process_implications.py?