Exercises for Ch.Tactics

[lakesare]

[Based on #84]

In this PR

• Created exercises & solutions for Ch.Tactics
• Fixed some markdown across the book

Links to the latest versions of updated files

• Ch.Tactics Exercises, Solutions

These are the only files that changed significantly, all other changes is markdown stuff, doesn't need to be reviewed.

[lakesare]

@JLimperg, @hargoniX, could you take a look at this please?

[hargoniX]

I'm not sure about the exercises here, they use (IMHO, I am not a tactic developer) very bad style. You explicitly rely on names of meta variables and you tell users to create hypothesis with fixed names instead of user provided names. This is exactly the type of stuff we do not want to have for macro hygiene and proof stability.

Other than that I don't know if we want to have the formatting changes, I am neutral to them if someone has an opinion they should speak up.

[lakesare]

@hargoniX, ofc that shouldn't be done like that in real tactic development, that's explicitly for the sake of an exercise! I assume that's clear, but can add a comment.

We also shouldn't create tactics that affect 2 unrelated goals at a time, but it's good to know we can do that, because that clarifies the mental model of how tactic internals work.

[hargoniX]

I have used this argument for "Explicitly for the shake of exercise" before myself :D the people do much prefer proper examples (although I don't have nice suggestions for those right now) instead of artificial ones (like I originally had myself too).

[lakesare]

I think the 1st exercise is essential because it's super useful for the mental model (literally connects proof terms & tactics) and stretches your usual assumptions about what tactics can do (they can wreak havoc, change all mvar usernames, randomize goal positions, affect the hypotheses of multiple goals at a time, etc., it's just a social convention that they don't), 2&3&4 just make people memorize the function names, 5th + additional exercises could be more real-world.

[hargoniX]

I see that there are now a ton of formatting changes here as well, did you make sure that the book still compiles without looking weirder than before?

I am still not sure about the tactic writing style here, in particular you mentioned you wanted to make step 5 more real-worldy but it does still do the wrong thing of claiming its own names. It wouldn't even be too hard to do it with a user provided name would it? Just andify ab ac as a_and_b or something like that.

But since this review has been dragging out for a while I'd like a second opinion (maybe @JLimperg ?) maybe I'm just being too anal about stuff.

[lakesare]

I see that there are now a ton of formatting changes here as well, did you make sure that the book still compiles without looking weirder than before?

Yep, formatting changes are here so that the book looks less weird than previously.

I am still not sure about the tactic writing style here, in particular you mentioned you wanted to make step 5 more real-worldy but it does still do the wrong thing of claiming its own names. It wouldn't even be too hard to do it with a user provided name would it? Just andify ab ac as a_and_b or something like that.

I agreed it would be nice to have more real-worldly exercises as additional exercises (and instead of 5th), but I can't contribute more time to this right now.

Really I think the 1st&2nd exercises are essential for aforementioned reasons, and other exercises can go for the time being, we can indeed substitute them for something more real-worldly later. Removed the 4th and 5th.

[hargoniX]

I guess it's better to have at least some exercises, let's merge this for now and incrementally improve later on.