Replace "presumptions" with allow/deny lists

[wwitzel]

This may finally solve the "presumptions.txt" headaches! It simplifies the issue on the user side and the implementation side. The idea is to have separate allow/deny lists of theorems and packages that may or may not be used for a particular theorem proof. Unlike the current implementation with presumptions, when attempting to use a theorem that is neither list, an error will occur (rather than silently rejecting anything that isn't presumed). Ideally, we'd use pop-up dialogs with buttons that allow the user to choose whether to allow, deny, allow the parent package, or deny the parent package (if they allow/deny the parent package, they will then have the option to go up another level or not). When the theorem is proved, these allow/deny lists will be updated with these explicit choices. The current system records only presumptions that were needed in the proof and tends to break when automation features are added or modified. The ability to allow/deny packages will help so these don't break so often. And when they do break, it will be easier to fix (as long as wise choices were made previously) because you'll be alerted when coming across anything that was neither allowed nor denied and it will be easy, in interactive mode with pop-ups, to resolve. When not in interactive mode, they'll simply be an exception raised, but something more informative than the current system.

Pop-ups can be implemented using IPython.display and javascript (https://www.stefaanlippens.net/jupyter-notebook-dialog.html).

One other note. To keep it simple for the users, we only need to worry about whether things are allowed or denied when something is being displayed (presumably as part of the proof) and not worry about it when things are incidentally derived (side-effects in the current nomenclature). We can still deny the incidentals/side-effects, but we can just let them go through if it is neither explicitly allowed or denied. If it gets used to prove something to be displayed, that's when we will check to see whether it is fully allowed or not.

[wwitzel]

Instead of

Under these presumptions, we begin our proof of

We can say

With these allowed/disallowed theorem/package dependencies, we begin our proof of

That's one option.

[wwitzel]

I'm thinking that disallowances should take priority over allowances (a theory could be allowed but with an exception for one or more sub-theories or theorems). While proving a particular theorem, when attempting to use a theorem:

1. Check if it is disallowed. If it is, raise UnusableProof and go no further.
2. Check if it is allowed. If it is not allowed, query the user as to whether the theorem (or containing theory package) should be allowed or disallowed. If disallowed, raise UnusableProof and go no further. If allowed, continue.
3. For the theorem we are trying to use, prevent circular logic (proactively) by checking the following. Recurse through its allowed or used (if proven) theorems to see if anything leads back to the theorem we are trying to prove. a) If circularity is detected, ask the user if they want to disallow the theorem to avoid circular logic. If so, disallow the theorem and raise UnusableProof. If not, raise CircularLogicError. b) If circularity is not detected, carry on and use the theorem.

It would be possible to be more proactive by considering all theorems/sub-packages within an allowed theory package in step 3, but that would probably have an undesirable performance penalty. If we just check specific theorems that are allowed, or were used in a proof, that shouldn't be too burdensome.

[wwitzel]

For pop-ups in Jupyter, here are other possibilities: https://stackoverflow.com/questions/60166968/how-to-create-a-popup-in-a-widget-call-back-function-in-ipywidgets

Maybe just use widget buttons instead of popups.

[wwitzel]

I'm having trouble finding a way to wait for a user input from buttons: https://github.com/jupyter-widgets/ipywidgets/issues/3039 The simplest but most archaic-looking solution would be to use "input" and wait for a text response ("(A)llow/(D)isallow/(U)p/(C)ancel"). A javascript "alert" blocks, but doesn't return any input. I'm not finding a simple solution other than the archaic "input".

Planning to use the simpler "input" approach for now.

[wwitzel]

Implemented with merger of 300-presumptions_allow_and_deny.