forked from Lean-zh/HTPIwL
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Appendix.qmd
221 lines (170 loc) · 12.4 KB
/
Appendix.qmd
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
# Appendix {.unnumbered}
\markdouble{Appendix}
## Tactics Used
Tactics marked with an asterisk (*) are defined in the file `HTPIDefs.lean` in the HTPI Lean Package that accompanies this book. They will not work without that file. The others are standard Lean tactics or are defined in Lean's mathematics library, `mathlib`.
::: {style="margin: 0% 10%"}
| Tactic | Where Introduced |
|:--|:----|
| `apply` | [Sections 3.1 & 3.2](Chap3.html#proofs-involving-negations-and-conditionals) |
| `apply?` | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `assume`* | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `bicond_neg`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `by_cases` | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `by_cases on`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `by_contra` | [Sections 3.1 & 3.2](Chap3.html#proofs-involving-negations-and-conditionals) |
| `by_induc`* | [Section 6.1](Chap6.html#proof-by-mathematical-induction) |
| `by_strong_induc`* | [Section 6.4](Chap6.html#strong-induction) |
| `conditional`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `contradict`* | [Sections 3.1 & 3.2](Chap3.html#proofs-involving-negations-and-conditionals) |
| `contrapos`* | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `decide` | [Section 6.1](Chap6.html#proof-by-mathematical-induction) |
| `define`* | [Introduction to Lean: Types](IntroLean.html#types) |
| `demorgan`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `disj_syll`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `double_neg`* | [Introduction to Lean: Tactic Mode](IntroLean.html#tactic-mode) |
| `exact` | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `exists_unique`* | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `fix`* | [Section 3.3](Chap3.html#proofs-involving-quantifiers) |
| `have` | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `linarith` | [Section 6.1](Chap6.html#proof-by-mathematical-induction) |
| `obtain`* | [Section 3.3](Chap3.html#proofs-involving-quantifiers) |
| `or_left`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `or_right`* | [Section 3.5](Chap3.html#proofs-involving-disjunctions) |
| `push_neg` | [Section 8.1](Chap8.html#equinumerous-sets) |
| `quant_neg`* | [Section 3.3](Chap3.html#proofs-involving-quantifiers) |
| `rel` | [Section 6.3](Chap6.html#recursion) |
| `rewrite` | [Section 3.6](Chap3.html#existence-and-uniqueness-proofs) |
| `rfl` | [Section 3.7](Chap3.html#more-examples-of-proofs) |
| `ring` | [Section 3.7](Chap3.html#more-examples-of-proofs) |
| `rw` | [Section 3.7](Chap3.html#more-examples-of-proofs) |
| `set` | [Section 4.5](Chap4.html#equivalence-relations) |
| `show`* | [Introduction to Lean: A First Example](IntroLean.html#a-first-example) |
| `trivial` | [Section 7.2](Chap7.html#prime-factorization) |
:::
## Transitioning to Standard Lean
If you want to continue to use Lean to write mathematical proofs, you may want to learn more about Lean. A good place to start is the [Lean Community website](https://leanprover-community.github.io/index.html). The resources there use "standard" Lean, which is somewhat different from the Lean in this book.
In a few cases we have used notation in this book that differs from standard Lean notation. For example, if `h` is a proof of `P ↔ Q`, then we have used `h.ltr` and `h.rtl` to denote proofs of the left-to-right and right-to-left directions of the biconditional. The standard Lean notation for these is `h.mp` and `h.mpr`, respectively ("mp" and "mpr" stand for "modus ponens" and "modus ponens reverse"). As explained at the end of [Section 5.4](Chap5.html#closures), the notations `Pred U` and `Rel A B` denote the types `U → Prop` and `A → B → Prop`, respectively. Although `Rel` is standard notation (defined in Lean's math library `mathlib`), `Pred` is not; the notation `BinRel A` is also not standard Lean. In place of `Pred U` you should use `U → Prop`, and in place of `BinRel A` you should use `Rel A A`.
However, the biggest difference between the Lean in this book and standard Lean is that the tactics marked with an asterisk in the table above are not a part of standard Lean. If you want to learn to write proofs in standard Lean, you'll need to learn replacements for those tactics. We discuss some such replacements below. Some of these replacements are built into Lean, and some are defined in `mathlib`.
* #### `assume`, `fix`
If you are proving `P → Q` and you want to begin by assuming `h : P`, in standard Lean you would begin your proof by writing `intro h`. You don't need to specify that `h` is an identifier for the assumption `P`; Lean will figure that out on its own.
If you are proving `∀ (x : U), P x` and you want to begin by introducing the variable `x` to stand for an arbitrary object of type `U`, in standard Lean you would begin your proof by writing `intro x`. Again, you don't need to specify the type of `x`, because Lean will figure it out.
Thus, the tactic `intro` does the job of both `assume` and `fix`. Furthermore, you can introduce multiple assumptions or objects with a single use of the `intro` tactic: `intro a b c` is equivalent to `intro a; intro b; intro c`.
* #### `bicond_neg`, `demorgan`, `double_neg`, `quant_neg`
We have mostly used these tactics to reexpress negative statements as more useful positive statements. The tactic `push_neg` can be used for this purpose.
* #### `by_cases on`
If you have `h : P ∨ Q`, then you can break your proof into cases by using the tactic `cases' h with hP hQ`. In case 1, `h : P ∨ Q` will be replaced by `hP : P`, and in case 2 it will be replaced by `hQ : Q`. In both cases, you have to prove the original goal. You may also want to learn about the tactics `cases` and `rcases`.
* #### `by_induc`, `by_strong_induc`
We saw in Section 7.2 that if you are proving a statement of the form `∀ (l : List U), ...`, then you can begin a proof by induction on the length of `l` by using the tactic `apply List.rec`. Similarly, if you are proving `∀ (n : Nat), ...`, you can begin a proof by induction by using the tactic `apply Nat.recAux`. For strong induction, you can use `apply Nat.strongRec`.
There are also tactics `induction` and `induction'` that you may want to learn about.
* #### `conditional`
The commands `#check @imp_iff_not_or` and `#check @not_imp` produce the results
::: {.ind}
```
@imp_iff_not_or : ∀ {a b : Prop}, a → b ↔ ¬a ∨ b
@not_imp : ∀ {a b : Prop}, ¬(a → b) ↔ a ∧ ¬b
```
:::
Thus, `rewrite [imp_iff_not_or]` will convert a statement of the form `P → Q` into `¬P ∨ Q`, and `rewrite [←imp_iff_not_or]` will go in the other direction. Similarly, `rewrite [not_imp]` will convert a statement of the form `¬(P → Q)` into `P ∧ ¬Q`, and `rewrite [←not_imp]` will go in the other direction.
* #### `contradict`
Suppose your goal is `False` (as it would be if you are doing a proof by contradiction), and you have `h : ¬P`. Recall that Lean treats `¬P` as meaning the same thing as `P → False`, and therefore `h _` will prove the goal, if the blank is filled in which a proof of `P`. It follows that `apply h` will set `P` as the goal. In other words, in this situation `apply h` has the same effect as `contradict h`.
You could also get the same effect with the tactic `suffices hP : P from h hP`. Think of this as meaning "it would suffice now to prove `P`, because if `hP` were a proof of `P`, then `h hP` would prove the goal." Lean therefore sets `P` to be the goal.
Similarly, in a proof by contradiction, if you have `h : P`, then `suffices hnP : ¬P from hnP h` will set `¬P` as the goal.
Yet another possibility is `contrapose! h`. (This is a variant on the `contrapose!` tactic, discussed in the next section.)
* #### `contrapos`
If your goal is a conditional statement, then the tactics `contrapose` and `contrapose!` will replace the goal with its contrapositive (`contrapose!` also uses `push_neg` to try to simplify the negated statements that arise when forming a contrapositive). You may also find the theorem `not_imp_not` useful:
::: {.ind}
```
@not_imp_not : ∀ {a b : Prop}, ¬a → ¬b ↔ b → a
```
:::
* #### `define`
The tactic `whnf` (which stands for "weak head normal form") is similar to `define`, although it sometimes produces results that
are a little confusing.
Another way to write out definitions is to prove a lemma stating the definition and then use that lemma as a rewriting rule in the `rewrite` tactic. See, for example, the use of the theorem `inv_def` in [Section 4.2](Chap4.html#relations).
* #### `disj_syll`
The following theorems can be useful:
::: {.ind}
```
@Or.resolve_left : ∀ {a b : Prop}, a ∨ b → ¬a → b
@Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a
@Or.neg_resolve_left : ∀ {a b : Prop}, ¬a ∨ b → a → b
@Or.neg_resolve_right : ∀ {a b : Prop}, a ∨ ¬b → b → a
```
:::
For example, if you have `h1 : P ∨ Q` and `h2 : ¬P`, then `Or.resolve_left h1 h2` is a proof of `Q`.
* #### `exists_unique`
If your goal is `∃! (x : U), P x` and you think that `a` is the unique value of `x` that makes `P x` true, then you can use the tactic `apply ExistsUnique.intro a`. This will leave you with two goals to prove, `P a` and `∀ (y : U), P y → y = a`.
* #### `obtain`
There is an `obtain` tactic in standard Lean, but it is slightly different from the one used in this book. If you have `h : ∃ (x : U), P x`, then the tactic `obtain ⟨u, h1⟩ := h` will introduce both `u : U` and `h1 : P u` into the tactic state. Note that `u` and `h1` must be enclosed in angle brackets, `⟨ ⟩`. To enter those brackets, type `\<` and `\>`.
If you have `h : ∃! (x : U), P x`, then `obtain ⟨u, h1, h2⟩ := h` will also introduce `u : U` and `h1 : P u` into the tactic state. In addition, it will introduce `h2` as an identifier for a statement that is equivalent to `∀ (y : U), P y → y = u`. (Unfortunately, the statement introduced is more complicated.)
You may also find the theorems `ExistsUnique.exists` and `ExistsUnique.unique` useful:
::: {.ind}
```
@ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop},
(∃! (x : α), p x) → ∃ (x : α), p x
@ExistsUnique.unique : ∀ {α : Sort u_1} {p : α → Prop},
(∃! (x : α), p x) → ∀ {y₁ y₂ : α}, p y₁ → p y₂ → y₁ = y₂
```
:::
* #### `or_left`, `or_right`
If your goal is `P ∨ Q`, then the tactics `or_left` and `or_right` let you assume that one of `P` and `Q` is false and prove the other. Perhaps the easiest way to do that in standard Lean is to use proof by cases. For example, to assume `P` is false and prove `Q` you might proceed as follows:
```lean
-- Goal is P ∨ Q
by_cases hP : P
· -- Case 1. hP : P
exact Or.inl hP
done
· -- Case 2. hP : ¬P
apply Or.inr
--We now have hP : ¬P, and goal is Q
**done::
```
* #### `show`
There is a `show` tactic in standard Lean, but it works a little differently from the `show` tactic we have used in this book. When our goal was a statement `P` and we had an expression `t` that was a proof of `P`, we usually completed the proof by writing `show P from t`. In standard Lean you can complete the proof by writing `exact t`, as explained near the end of [Section 3.6](Chap3.html#existence-and-uniqueness-proofs).
## Typing Symbols
::: {style="margin: 0% 10%"}
| Symbol | How To Type It |
|:--:|:----:|
| `¬` | `\not` or `\n` |
| `∧` | `\and` |
| `∨` | `\or` or `\v` |
| `→` | `\to` or `\r` or `\imp` |
| `↔` | `\iff` or `\lr` |
| `∀` | `\forall` or `\all` |
| `∃` | `\exists` or `\ex` |
| `⦃` | `\{{` |
| `⦄` | `\}}` |
| `=` | `=` |
| `≠` | `\ne` |
| `∈` | `\in` |
| `∉` | `\notin` or `\inn` |
| `⊆` | `\sub` |
| `⊈` | `\subn` |
| `∪` | `\union` or `\cup` |
| `∩` | `\inter` or `\cap` |
| `⋃₀` | `\U0` |
| `⋂₀` | `\I0` |
| `\` | `\\` |
| `∆` | `\symmdiff` |
| `∅` | `\emptyset` |
| `𝒫` | `\powerset` |
| `·` | `\.` |
| `←` | `\leftarrow` or `\l` |
| `↑` | `\uparrow` or `\u` |
| `ℕ` | `\N` |
| `ℤ` | `\Z` |
| `ℚ` | `\Q` |
| `ℝ` | `\R` |
| `ℂ` | `\C` |
| `≤` | `\le` |
| `≥` | `\ge` |
| `∣` | `\|` |
| `×` | `\times` or `\x` |
| `∘` | `\comp` or `\circ` |
| `≡` | `\==` |
| `∼` | `\sim` or `\~` |
| `ₛ` | `\_s` |
| `ᵣ` | `\_r` |
| `⟨` | `\<` |
| `⟩` | `\>` |
:::