Joachim Breitner (Dec 05 2020 at 21:59): Joachim Breitner (Dec 05 2020 at 21:59):Mostly a hack and a proof of concept, but it’s possible to use [name] { … } to focus subgoals of a proof by induction or inversion:
https://www.joachim-breitner.de/blog/777-Named_goals_in_Coq
Théo Zimmermann (Dec 06 2020 at 12:04):Very cool! Note that the "named goal selection feature" is relatively ancient (8.6 I think) and what I implemented relatively recently (8.9) is rather "named goal focusing".
Théo Zimmermann (Dec 06 2020 at 12:19):It seems to me that your "hack" could be a good prototype for a CEP that would argue how this feature should behave if it was supported out of the box by Coq. It's probably not too hard to implement, and what has been refraining such a feature was rather the lack of a clear view of what it should do exactly and how it should behave in corner cases (like nested induction).
Joachim Breitner (Dec 06 2020 at 15:19):I must admit I don't know the difference between named goal selection and focusing, but I'm eager to learn :-)
Théo Zimmermann (Dec 06 2020 at 16:02):Selection: [foo]: tactic_on_foo. (* foo not selected anymore *)
Focusing: [foo]: { tactic_on_foo. (* foo or its descendants still focused *)
Paolo Giarrusso (Dec 06 2020 at 17:37):ah... so they're internally different, even if they seem the same for users? (focusing seems just selection + brackets)
Last updated: Oct 13 2024 at 01:02 UTC