wwitzel
commented
2 years ago We can take this a step further. Instead of requiring explicit proof steps to eliminate definitions, we could simply categorize extraneous definitions as extraneous and report them that way when dependencies are reported. This has the advantage of clarity and simplicity. Explicit steps to eliminate definitions are somewhat confusing and not really necessary. It's less confusing to indicate a list of "definitions" that are really conservative extensions and easily verifiable as long as they are presented in an appropriate order. Simply order them so that a definition may depend upon a previous definition but not the other way around. As long as that is the case, each introduced symbol only appears on the left side of an equation, and these symbols do not appear in the theorem being proven or any of its other dependencies, then it is legitimate to regard these as extraneous definitions (conservative extensions). What should we call them when we report dependencies to be most clear? Perhaps "Superfluous utilized definitions"? I don't know.
There is now a Judgment.eliminate_definition method which may be used to eliminate an axiom/theorem dependency by performing literal generalization and then specializing it to its definition in the axiom/theorem. We should simplify things for the user by automatically doing this for any applicable dependency, repeating until all possibilities have been handled. This would happen at the %qed stage after proving the theorem but then extending the proof to eliminate definitions. These may take multiple passes of looking through dependencies as new possibilities may emerge after eliminating other definitions (a literal may only appear once in the dependencies, on the left of an equation, to be eliminated). It should be possible to make this algorithm fairly efficient through proper bookkeeping so that O(N^2) examinations of dependencies is not necessary -- hopefully closer to O(N).