Various proof explorer notes

[elidupree]

"This goal is immediately solved by the following tactics: tauto <- quickest auto <- shortest proof congruence <- also solves the other goals, so you can use it with ; intuition"

That message would be displayed prominently (when nothing is displayed in the same prominent way if there is no immediate solution)

in a list of tactics for H: injection H as H1 H2 [highlighted, green, etc] maybe injection H as <- <- rew <- H [lower in the list, not so highlighted, yellow; when you click/mouse over it to get more information, "be careful when rewriting by terms that can be injected"]

dependent destruction not listed (or listed lower) if it does the same thing as destruct same treatment for destruct if it seems to be losing information (if it's distinct from dependent destruction?)

Gentle suggestion to Require Import Coq.Program.Equality.; maybe later some of my own tactics libraries

Attempt a second step (primarily trivial steps) from a lot of tactics; having the goal immediately solvable after the tactic gives it additional priority in being displayed more prominently. For tactics that split the goal, attempt trivial tactics on all subgoals (better the more subgoals that can be solved immediately)

[elidupree]

List of new hypotheses that can be produced by any tactic, and you mouse over them to show the tactic(s) that produce them? Hard to tell whether it would make a good flow (reading a lot of irrelevant hypotheses might be a bunch of cognitive overhead), but it's worth considering

[elidupree]

Mouseover/click an individual function to unfold/cbv/etc it? How to decide what size of term you're trying to select? (E.g. the function would usually be in a hypothesis, and clicking a hypothesis means something different). What if you could select compound terms to try tactics with them? Double-clicking a word selects it if there isn't a special event handler.

Maybe it shows a drop-down menu. (Select "foo" and you see a list of options "unfold foo in [this hypothesis], unfold foo in , cbv [foo] in [this hypothesis], cbv [foo] in "). Single click to select word (and only selecting the hypothesis name counts as focusing on the hypothesis; that would also mean I don't have to split up hypotheses with the same type). Selecting partial words behaves the same way as selecting the whole word. (Could even generalize to some smarts about expanding your selection to a valid term? Either through some logic or trial and error?)

This "drop-down menu" COULD be a "right-click on selection" thing but could be already onscreen after just selecting. Should it be right next to the selection (overlapping other elements), or should there be a dedicated area of the screen for it? Or is it not so much of a "menu" as just influencing what tactics will be tried and dumped in a big "candidate tactics" area?

[elidupree]

Along with the warning for rewriting by a term that can be injection'd, also warn for rewriting by ANY term where applying it to ANY part of the goal would lead to an ill typed term; recommend the revert dependent H; rewrite approach instead (and remember that we have to try rewriting in every hypothesis explicitly, since rewrite H in * silently ignores hypotheses where there's an error)

[elidupree]

Browser back and forward buttons act on the proof state (I suggest this because I keep accidentally clicking "back" when I mean to go back by one tactic)

[elidupree]

interrupt tactics that take too long (probably at like 10ms to start with, maybe retrying them with longer timers when other explorations are exhausted)