From 2bcaaf604b0942789418bfb21e61843ea2a27ed2 Mon Sep 17 00:00:00 2001
From: Michael Peyton Jones <me@michaelpj.com>
Date: Fri, 2 Jun 2023 09:02:07 +0100
Subject: [PATCH 1/4] Add a tips page to the book

This is a collection of tips I picked up during the workshop.
---
 src/plfa/backmatter/Tips.md | 197 ++++++++++++++++++++++++++++++++++++
 1 file changed, 197 insertions(+)
 create mode 100644 src/plfa/backmatter/Tips.md

diff --git a/src/plfa/backmatter/Tips.md b/src/plfa/backmatter/Tips.md
new file mode 100644
index 000000000..60985b967
--- /dev/null
+++ b/src/plfa/backmatter/Tips.md
@@ -0,0 +1,197 @@
+---
+title     : "Tips"
+permalink : /Tips/
+---
+
+# Interactive development 
+
+## Equational reasoning skeleton
+
+When starting to work on an equational reasoning problem, you can begin like this:
+```agda
+begin
+    ?
+  ≡⟨ ? ⟩
+    ?
+  ≡⟨ ? ⟩
+    ?
+  ≡⟨ ? ⟩
+    ?
+∎
+```
+
+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).
+This will solve the expression holes at the beginning and the end so you don't have to fill them in.
+You can do this again if you fix a step, so if you fill in the reasoning you want to do for a step, you can use "solve" and Agda will fill in the next term.
+
+## Goal information will show computed terms
+
+Suppose you have a partial equational reasoning proof:
+```agda
+begin
+    2 + (x + y)
+  ≡⟨ ?2 ⟩
+    ?
+  ≡⟨ ? ⟩
+    ?
+  ≡⟨ ? ⟩
+    ?
+∎
+```
+
+The first term can be computed more.
+To see this, you can ask for the goal context for `?2` and it will show something like this:
+```
+?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.
+
+## Quickly setting up `with` clauses
+
+If you have a function like this:
+```agda
+foo a = ?
+```
+and you want to introduce a `with`-clause, there is no direct hotkey for this. 
+The fastest thing to do is to write
+```agda
+foo a with my-thing
+... | x = ?
+```
+and then ask to case-split on `x`.
+
+## Quickly setting up record skeletons
+
+"Refine" (`C-c C-r` in Emacs) will set up a skeleton for a record constructor if Agda knows a hole must be a record type.
+This is useful for e.g. isomorphisms, products, sigmas, or existentials.
+
+# General tips
+
+## Try and make your definitions compute as much as possible
+
+For example, compare:
+```agda
+2 * foo b
+```
+vs
+```agda
+foo b * 2 
+```
+
+The definition of `*` does case analysis on its first argument.
+This means that if the first argument to `*` is a constructor application, Agda can do some computation for you. 
+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.
+
+## `x + x` is better than `2 * x`
+
+An expression like `2 * x` will compute to `x + (x + zero)`.
+You now need to get rid of the `x + zero` with a rewrite or similar.
+You don't have this problem if you just write `x + x`.
+
+This is probably less true for larger constants: writing out `8 * x` would be tedious.
+
+## The three styles of proof all tend to use the same assumptions
+
+Consider these three proofs of the same theorem:
+```agda
+*-distrib-+ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+ zero n p = refl
+*-distrib-+ (suc m) n p =
+  begin
+    (suc m + n) * p
+  ≡⟨⟩
+    suc (m + n) * p
+  ≡⟨⟩
+    p + (m + n) * p
+  ≡⟨ cong (p +_) (*-distrib-+ m n p) ⟩
+    p + (m * p + n * p)
+  ≡⟨ sym (+-assoc p (m * p) (n * p)) ⟩
+    (p + m * p) + n * p
+  ≡⟨⟩
+    (suc m * p) + n * p
+  ∎
+
+*-distrib-+‵ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+‵ zero n p = refl
+*-distrib-+‵ (suc m) n p = trans ( cong (p +_) (*-distrib-+‵ m n p)) ( sym ( +-assoc p (m * p) (n * p)))
+
+*-distrib-+‶ : ∀ (m n p : ℕ) → (m + n) * p ≡ m * p + n * p
+*-distrib-+‶ zero n p = refl
+*-distrib-+‶ (suc m) n p rewrite +-assoc p (m * p) (n * p) | *-distrib-+‶ m n p = refl
+```
+
+They use three approaches for doing "multiple steps":
+1. Equational reasoning
+2. `trans`
+3. `rewrite`
+
+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`.
+
+## Avoid mutual recursion in proofs by recursing outside the lemma
+
+Look at the second part of the proof of commutativity of `+`:
+```agda
++-comm m (suc n) =
+  begin
+    m + suc n
+  ≡⟨ +-suc m n ⟩
+    suc (m + n)
+  ≡⟨ cong suc (+-comm m n) ⟩
+    suc (n + m)
+  ≡⟨⟩
+    suc n + m
+  ∎
+```
+We use two equalities: the `+-suc` lemma, and a recursive use of `+-comm`.
+
+If you were doing this for the first time, you might be tempted to make _one_ lemma for both those steps.
+It wouldn't look that different, it would just have `n` and `m` swapped.
+But then you would find that you needed to call `+-comm` from the lemma, which needs mutual recursion.
+
+Instead, you can do what's done here and use the recursive call before/after your lemma.
+
+## When to use implicit parameters
+
+Roughly: if it can be inferred easily from the result, e.g.
+```
+≤-refl : ∀ { n : ℕ } → n ≤ n
+```
+Agda will be able to infer the `n` from the `n ≤ n` in the result.
+
+Note that the situation is different for constructors and functions.
+Generally, Agda can infer `x` from `f x` if `f` is a constructor (like `≤`) but _not_ if it is a function (like `_+_`).
+
+## Avoiding "green slime"
+
+"Green slime" is when you use a function in the index of a returned data type value.
+For example:
+```agda
+data Tree (A : Set) : ℕ → Set where
+  leaf : A → Tree A 1
+  node : ∀ {s : ℕ} → Tree A s → Tree A s → Tree A (s + s)
+```
+Here we end up with a `Tree (s + s)` as the result of `node`.
+This means that if we pattern match on a value of type `Tree A n`, Agda may get confused about making `n` and `s + s` the same.
+
+There are a few ways to avoid green slime, but one way that often works is to use a variable and also include a proof that it has the value that you want. So:
+
+```agda
+data Tree (A : Set) : ℕ → Set where
+  leaf : A → Tree A 1
+  node : 
+    ∀ {s : ℕ} {s‵ : ℕ}
+    → Tree A s 
+    → Tree A s 
+    → s‵ ≡ s + s
+    → Tree A s‵
+```
+
+Now you can still get the information about the sum by matching on the proof, but Agda has an easier time.

From bb65b2f966b611a54adbce008fbaff7e0c6bf419 Mon Sep 17 00:00:00 2001
From: "pre-commit-ci[bot]"
 <66853113+pre-commit-ci[bot]@users.noreply.github.com>
Date: Fri, 2 Jun 2023 08:13:28 +0000
Subject: [PATCH 2/4] [pre-commit.ci] auto fixes from pre-commit.com hooks

for more information, see https://pre-commit.ci
---
 src/plfa/backmatter/Tips.md | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

diff --git a/src/plfa/backmatter/Tips.md b/src/plfa/backmatter/Tips.md
index 60985b967..342fa5825 100644
--- a/src/plfa/backmatter/Tips.md
+++ b/src/plfa/backmatter/Tips.md
@@ -3,7 +3,7 @@ title     : "Tips"
 permalink : /Tips/
 ---
 
-# Interactive development 
+# Interactive development
 
 ## Equational reasoning skeleton
 
@@ -20,7 +20,7 @@ begin
 ∎
 ```
 
-This sets up a series of reasoning steps with holes for both the expressions at each step, and the step itself. 
+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).
@@ -55,7 +55,7 @@ If you have a function like this:
 ```agda
 foo a = ?
 ```
-and you want to introduce a `with`-clause, there is no direct hotkey for this. 
+and you want to introduce a `with`-clause, there is no direct hotkey for this.
 The fastest thing to do is to write
 ```agda
 foo a with my-thing
@@ -78,11 +78,11 @@ For example, compare:
 ```
 vs
 ```agda
-foo b * 2 
+foo b * 2
 ```
 
 The definition of `*` does case analysis on its first argument.
-This means that if the first argument to `*` is a constructor application, Agda can do some computation for you. 
+This means that if the first argument to `*` is a constructor application, Agda can do some computation for you.
 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.
@@ -186,10 +186,10 @@ There are a few ways to avoid green slime, but one way that often works is to us
 ```agda
 data Tree (A : Set) : ℕ → Set where
   leaf : A → Tree A 1
-  node : 
+  node :
     ∀ {s : ℕ} {s‵ : ℕ}
-    → Tree A s 
-    → Tree A s 
+    → Tree A s
+    → Tree A s
     → s‵ ≡ s + s
     → Tree A s‵
 ```

From b9fc504f767a1b92d445a921eb564af3b999dfce Mon Sep 17 00:00:00 2001
From: Michael Peyton Jones <me@michaelpj.com>
Date: Fri, 2 Jun 2023 09:14:26 +0100
Subject: [PATCH 3/4] Add to TOC

---
 data/tableOfContents.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/data/tableOfContents.yml b/data/tableOfContents.yml
index 178922483..a171fd30f 100644
--- a/data/tableOfContents.yml
+++ b/data/tableOfContents.yml
@@ -48,5 +48,6 @@ part:
   chapter:
   - include: src/plfa/backmatter/Acknowledgements.md
     epub-type: acknowledgements
+  - include: src/plfa/backmatter/Tips.md
   - include: src/plfa/backmatter/Fonts.lagda.md
     epub-type: appendix

From 7b76e4449beeae473109e3b741b07db47a0240c2 Mon Sep 17 00:00:00 2001
From: Wen Kokke <wenkokke@users.noreply.github.com>
Date: Sun, 4 Jun 2023 13:42:33 +0100
Subject: [PATCH 4/4] Add epub-type

---
 data/tableOfContents.yml | 1 +
 1 file changed, 1 insertion(+)

diff --git a/data/tableOfContents.yml b/data/tableOfContents.yml
index a171fd30f..113dc2bdf 100644
--- a/data/tableOfContents.yml
+++ b/data/tableOfContents.yml
@@ -49,5 +49,6 @@ part:
   - include: src/plfa/backmatter/Acknowledgements.md
     epub-type: acknowledgements
   - include: src/plfa/backmatter/Tips.md
+    epub-type: appendix
   - include: src/plfa/backmatter/Fonts.lagda.md
     epub-type: appendix