Add a tips page to the book #881
Conversation
This is a collection of tips I picked up during the workshop.
for more information, see https://pre-commit.ci
|
Thanks, Michael! (Wen, I asked Michael to make this pull request. He has a useful tips file, and it makes sense to add it to the book as backmatter. I hope others will submit new tips.) |
|
Hmm, something is unhappy but I'm not sure what. |
|
Fixed the issue. You were missing an |
| ``` | ||
| ?2 = suc (suc (x + y)) = y_5244 | ||
| ``` | ||
| i.e. your LHS and an unknown RHS (because it's a hole), but it will show the LHS fully computed, which you can copy into your file directly. |
There was a problem hiding this comment.
You may need to disambiguate LHS and RHS for the reader.
There was a problem hiding this comment.
You can also just remove ?2 and surrounding spaces (or replace it with refl) and then auto on the next ? below.
| The first example computes to `foo b + (foo b + zero)`, but the second one does not compute at all: Agda can't pattern match on `foo b`, it could be anything! | ||
|
|
||
| Doing this lets Agda do more definitional simplification, which means you have to do less work. | ||
| Unfortunately it does require you to know _which_ arguments are the one that Agda can evaluate, which requires looking at the definitions of the functions. |
There was a problem hiding this comment.
There's some general advice we can probably give here to help people guess which arguments are evaluated, e.g., left associative operators tend to evaluate their left argument.
There was a problem hiding this comment.
Perhaps tell people about jump-to-definition?
|
|
||
| However, notably they all use the same supporting proofs! | ||
| That means you can often write the overall proof however you find easiest and then rewrite it into another form if you want. | ||
| For example, do the proof slowly with equational reasoning, and then turn it into a compact proof with `rewrite`. |
There was a problem hiding this comment.
I'd hesitate to advise folks to rewrite their readable equational reasoning proofs into less readable rewrite ones.
I'd ask that you remove that particular tip.
(It's also not obvious that such a rewrite always works.)
| ∀ {s : ℕ} {s‵ : ℕ} | ||
| → Tree A s | ||
| → Tree A s | ||
| → s‵ ≡ s + s |
There was a problem hiding this comment.
This should be a regular quote or a prime, but this seems to be a backtick?
| This sets up a series of reasoning steps with holes for both the expressions at each step, and the step itself. | ||
| Since the reasoning steps are holes, Agda will always accept this, so you can make incremental progress while keeping your file compiling. | ||
|
|
||
| Now call "solve" (`C-c C-s` in Emacs). |
There was a problem hiding this comment.
I run C-c C-a (auto) instead, which has the added benefit of getting rid of the hole in a single step. (At least in vscode I need to C-c C-space to give after solving.)
| That means you can often write the overall proof however you find easiest and then rewrite it into another form if you want. | ||
| For example, do the proof slowly with equational reasoning, and then turn it into a compact proof with `rewrite`. | ||
|
|
||
| ## Avoid mutual recursion in proofs by recursing outside the lemma |
There was a problem hiding this comment.
I think I understand what this advice is trying to say, but it's a bit unclear. The title just adds to the confusion.
I think what you are trying to say here is that we should try to break up a proof into small lemmas, that do one reasoning step, which we then compose to get the overall goal?
|
|
||
| ## Avoiding "green slime" | ||
|
|
||
| "Green slime" is when you use a function in the index of a returned data type value. |
There was a problem hiding this comment.
Maybe some explanation why "green slime"?
There was a problem hiding this comment.
Further reading here: https://proofassistants.stackexchange.com/a/1615 (There is also a link to Connor's paper that coined this term.)
This is a collection of tips I picked up during the workshop.