Stream: Coq users

Topic: Named goals for inductive proofs


view this post on Zulip 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

view this post on Zulip 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".

view this post on Zulip 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).

view this post on Zulip 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 :-)

view this post on Zulip 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 *)

view this post on Zulip 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: Feb 04 2023 at 22:29 UTC