search

LS-Lab / KeYmaeraX-release

KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
http://keymaeraX.org/
GNU General Public License v2.0
76 stars 38 forks source link

[UI] [bug] Error using "minmax" tactic through top menu bar #85

Closed rbohrer closed 3 years ago

rbohrer commented 3 years ago

Expected behavior: Using the "minmax" tactic through the top menu will expand "minmax" in the formula I specify Got: An error message Version: 4.9.4 Release

Reproduce/details: 1) Open the attached model 2) implyR(1) 3) Go to top menu -> Defs -> minmax. 4) A window will appear asking you to click on where to apply the tactic 5) Click formula -1 6) Error message is displayed on UI: "minmax only applicable to min/max, but got max(x,y)=0"

Potential cause: I assume the position argument of "minmax" needs to point to a term, but the UI feeds it a position which points to a formula

Extra context: in this case, we did not need the extra precision offered by "minmax," instead "expandAll" worked fine. Rather, a user was quite surprised by the error message.

MinMaxBug.txt

smitsch commented 3 years ago

The position selection dialog supports sub-positions when pressing Alt. Hovering then highlights terms, and Alt-Click applies the tactic to the term directly.

Our plan is to change the behavior when an entire formula is selected to expanding all min/max in that formula.

rbohrer commented 3 years ago

Thanks! It's quite non-urgent, I just like to make sure these things are on everyone's radar.

(P.S., it seemed not to email me when you made a comment. So... if I do not respond to GitHub comments, I am not ignoring you, it's just being weird)