Style guide: _tac instantiations and attributes #834
Conversation
docs/Style.thy
Outdated
| Isabelle code is much easier to maintain when indented consistently. In apply style proofs we | ||
| indent by 2 spaces, and add an additional space for every additional subgoal. | ||
| Isabelle code is much easier to maintain when indented consistently. | ||
| When in doubt, and not constrained by vertically aligning items or subgoal-count offsets, use |
There was a problem hiding this comment.
Extremely minor grammar nitpick
| When in doubt, and not constrained by vertically aligning items or subgoal-count offsets, use | |
| When in doubt and not constrained by vertically aligning items or subgoal-count offsets, use |
There was a problem hiding this comment.
shrug ... if it helps, I'll add the comma
There was a problem hiding this comment.
I'm suggesting to remove the comma, I don't think it's right.
docs/Style.thy
Outdated
| section \<open>Wrapping/indenting complex rule instantiations, usually as part of @{text "_tac"} methods\<close> | ||
|
|
||
| text \<open> | ||
| For simple instantiations, they can fit it on one line, like so. |
There was a problem hiding this comment.
This sentence is a bit unclear to me. Are you saying that simple instantiations that can fit on one line should look like the following?
There was a problem hiding this comment.
Yes. I should make that more explicit.
docs/Style.thy
Outdated
|
|
||
| lemma | ||
| "\<lbrakk>a; b\<rbrakk> \<Longrightarrow> a \<and> b" | ||
| apply (frule_tac P=a and Q="id b" in conjI) \<comment> \<open>when @{text a} and @{text b} contain bound vars\<close> |
There was a problem hiding this comment.
It's not clear to me what the intention of the comment is here. Is it about using the _tac form instead of where?
There was a problem hiding this comment.
Yes, that is correct. I want to avoid guiding people towards writing out the rule_tac version when a fact[where ...] will suffice. The rule_tac version is less generic, as it applies only to the _tacs, but the attribute version has many more uses.
There was a problem hiding this comment.
I agree with that goal but then I think that the comment needs to be more explicit. As it is, the mention of bound variables seems to come out of nowhere and the alternative attribute version isn't mentioned.
However, I'm then struggling to think of a way to keep it short. Would it make sense to add it as a note instead, with something vaguely like
@{text "_tac"} methods as shown here are generally used when the instantiations contain bound vars, otherwise instantiations with the @{text "[where ...]" attribute are preferred as they are more general.
There was a problem hiding this comment.
Ok, tuned, how does the latest commit look to you?
There was a problem hiding this comment.
One potential typo, otherwise looks good to me!
| text \<open> | ||
| There is an important principle here: telling apart transformed/attributed facts from unaltered | ||
| facts at a glance. In other words avoid:\<close> |
There was a problem hiding this comment.
This is a very useful comment, good thinking to include it. People are generally much better at following rules if they know the intention behind it, as opposed to it just being some arbitrary thing that they need to remember.
docs/Style.thy
Outdated
| (@{text "fact[where ...]"}) as they are more general.\<close> | ||
|
|
||
| text \<open> | ||
| For simple instantiations which can fit it on one line, style them as follows. |
There was a problem hiding this comment.
| For simple instantiations which can fit it on one line, style them as follows. | |
| For simple instantiations which can fit on one line, style them as follows. |
There was a problem hiding this comment.
Mondays. Thanks. Ok, then I can squash it all together now.
We generally tend to do two newlines before a section, and the style guide was inconsistent about it. Add extra subcoal-count indent example (in words). Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Signed-off-by: Rafal Kolanski <rafal.kolanski@proofcraft.systems>
Adds two sections:
_tacmethods[def]rule_tac ... [and ...] in ...#746I also added consistent double-newline before sections, and added some more emphasis on 2 being the standard indent at the start of the indentation section.
Commits are independent so can be reviewed separately. Let the bikeshedding begin.