Summary
This week, we started working on Chapter 3 of mathematics in lean
Logic
The rules of thumb table in Maris’ cheat sheet gives a good overview of how to deal with different logic goals (somewhere around page 15). Also, this list of tactics can be very helpful. I have summarized some of the new tactics of this week below.
intro
The intro tactic helps you putting parts of your goals into hypotheses, by ✨intro✨ducing new hypotheses. For goals with universal quantifiers ($\forall$), you can use it as follows. Consider a goal
⊢ ∀ x : P x
Here, we assume that P is a property of x, where x is a term of type $T$. The intro tactic can be used as
intro x
To create a new hypothesis and change the goal as
x : T
⊢ P x
We can also use the intro tactic when we need to prove implication. Consider the following goal:
⊢ P x → Q x
Then, running
intro h
introduces a new hypothesis $h$ and changes the goal as
h : P x
⊢ Q x
dsimp and change
The definitional simplifier helps to unfold definitions. In the exercises, we use it for simplifying expressions involving functions. The change tactic works similarly, but let’s you specify how you want your goal to look after the simplification.
use
To deal with goals starting with existential quantifiers ($\exists$), we can use the ✨use✨ tactic. Consider the following goal:
⊢ ∃ x : P x
Then, the use tactic let’s your specify an example of such an $x$. For example, running
use 42
changes te goal to
⊢ P 42
For next week
For next week, try to do enough exercises from chapter 3, sections 1,2,3, so that you feel comfortable using the tactics introduced this week.