Remove all ProofScript sequent features

[brianhuffman]

This PR completely removes all SAWScript primitives and code that implements "sequents" in the SAW ProofScript monad. The following SAW primitives are removed:

• split_goal
• print_focus
• unfocus
• focus_concl
• focus_hyp
• delete_hyps
• retain_hyps
• delete_concl
• goal_cut
• normalize_sequent
• goal_intro_hyp
• goal_intro_hyps
• goal_revert_hyp
• goal_insert
• goal_insert_and_specialize
• goal_apply_hyp
• simplify_local
• enable_sequent_goals
• disable_sequent_goals

The reason for doing this is to remove unnecessary complexity (see #3281), both from the SAW user interface and from the implementation. Over 1000 lines of trusted code are removed from SAWCentral/Proof.hs.

We should be able to emulate all the removed functionality with use of goal_apply, a few new SAWCore theorems, and just a couple of new SAW primitives. I'll keep this PR in draft state until those new primitives are implemented.

This PR builds on #3279.

[sauclovian-g]

I really don't think this is the right way to go. For example, how do you plan to reimplement goal_cut?

[brianhuffman]

We can implement goal_cut very simply in a few lines of Haskell code; no special support is required in Proof.hs. We only need to apply a suitably-instantiated cut_rule theorem with goal_apply:

cut_rule : (P Q : Prop) -> (P -> Q) -> P -> Q;

[brianhuffman]

Here is my plan for what operations we should implement to make a suitable replacement for the sequent-based tactics:

• thm_specialize : Theorem -> [Term] -> Theorem A pure variant of specialize_theorem, as suggested in specialize_theorem should have pure function type #3278.
• thm_apply : Theorem -> [Theorem] -> Theorem A modus-ponens rule, as suggested in Operations on Theorems for forward-reasoning #91.
• goal_intro_thm : ProofScript Theorem Replaces a goal of the form P -> Q with a goal Q, and returns a local theorem P (actually {P} |- P). This is much like the already-existing goal_intro, but returns a Theorem instead of a Term.

For convenience, we should reimplement a couple of commands for which I've removed the sequent versions:

• goal_insert : Theorem -> ProofScript () Given a theorem P, replaces goal Q with a new goal P -> Q. Implemented by applying the rule (P : Prop) -> P -> (Q : Prop) -> (P -> Q) -> Q.
• goal_cut : Term -> ProofScript () Given a term P, replaces goal Q with two new goals P -> Q and P. Implemented (as described above) by applying the rule (P Q : Prop) -> (P -> Q) -> P -> Q.

Note that giving users a goal_intro_thm command will enable them to write proof scripts that apply local theorems to other subgoals outside their intended scope. With #3279, this doesn't lead to unsoundness, but still it would be preferable to make that harder to do. My favorite idea at the moment is to introduce another SAW proof command:

• subproof : ProofScript () -> ProofScript () In a proof state with multiple proof goals P1 .. Pn, create a nested subproof that starts in a proof state with just a single goal P1. The given inner proof script must then discharge that goal. The outer proof continues with the remaining goals P2..Pn.

Then we could make goal_intro and goal_intro_thm fail if they are called in any proof state with more than one proof goal. The error message would direct users to use subproof and call goal_intro and goal_intro_thm within the inner do block. The inner do block would delimit the scope of the local terms and theorems from goal_intro and goal_intro_thm.

[glguy]

This seems like it would do a lot to make our manual proof system a lot more useable.

[sauclovian-g]

I don't really think that keeping multiple goals and local hypotheses, but deleting all the infrastructure for managing them, is the best way forward. I think the usability of the proof system is better served by having a functioning sequent calculus implementation.

Admittedly, that's going to take some work...

[glguy]

It seems like the proposed alternative replaces the functionality of the removed code with more general tooling. The previous sequent stuff was pretty challenging to use for anything. The times I tried using it I would find a bug that needed to be fixed before I could do what I needed. I don't think anyone's actually using it in anger.