Summary
This week, we continued working on the exercises of chapter 2. While we initially scheduled these as homework, many of us did not finish these exercises yet. In this post, we will provide hints for some of these exercises. These might be helpful if you are stuck but do not want to look at the solutions.
Also, please join our Zulip. Make an account for the Lean Zulip (https://leanprover.zulipchat.com/) and send Carli or Maris a message, so that we can add you to our chat. Feel free to post any questions you have here.
The last exercise of section 3
To prove that $\lvert a \cdot b \rvert \leq (a^2 + b^2)/2$, you can use the following theorem, with $\alpha$ an AddGroup (like $\mathbb{R}$ in this exercise)
abs_le' {a b : α} : |a| ≤ b ↔ a ≤ b ∧ -a ≤ b
To apply this theorem, remember that .mp (modus ponens) or .mpr (modus ponens reverse) can be used to turn equivalence into an implication. To handle the new goal with a logic and that will appear afterwards, use one of the tactics that we introduced last week (also on the webpage of seminar 2). This tactic creates two goals, of which you can already solve one directly by turning one of the examples in this section into a theorem.
Section 4
In section 4, one of the exercises is to prove that $\min ((\min a, b), c) = \min (a, (\min (b, c))$. I was very happy to prove it in 15 lines, and it took me way longer than I expected. The following theorems should be enough to solve this exercise. The only tactic I used was apply
le_antisymm : a ≤ b → b ≤ a → a = b
le_min (h₁ : c ≤ a) (h₂ : c ≤ b) : c ≤ min a b
le_trans : a ≤ b → b ≤ c → a ≤ c
min_le_left : min a b ≤ a
min_le_right : min a b ≤ b
For proving that $\lvert a \rvert - \lvert b \rvert \leq \lvert a - b \rvert$, try to have a version of abs_add with a clever choice of variables as hypothesis, and use the linarith tactic somewhere.
For the exercises with dividers, it is a good exercise to try to guess the names of the theorems. Remember that you can use
#check theorem_name
to see if a theorem exists, and what the theorem is.
Section 5 / the trans tactic
For this section, note that the order of operations when combining multiple infs ($\sqcap$, typed as \inf) and/or sups ($\sqcup$, typed as \sup) is as follows:
a ⊔ b ⊔ c = (a ⊔ b) ⊔ c
a ⊓ b ⊓ c = (a ⊓ b) ⊓ c
a ⊔ b ⊓ c = a ⊔ (b ⊓ c)
The first two lines are similar to binary operations that we have already seen, like addition and multiplication in $\mathbb{R}$. However, the last line shows that inf has higher precedence than sup.
The exercises in section 5 are very similar to previous exercises involving $\min$ and $\leq$. Instead of using transitivity as a theorem, there is also a dedicated tactic. Consider a binary relation $R$ that is transitive (like $\leq$), and suppose that your goal is as follows:
⊢ a R c
While there should be some theorem or axiom of the form $a R b \to (b R c \to a R c)$, applying such theorem on the goal will replace $b$ by some weird question mark. Instead, the trans tactic lets us introduce such $b$. Using it as
trans b
changes the goal to two new goals:
⊢ a R b
⊢ b R c
Recall that you can use $\cdot$ (type: \.) to adress the two goals individually, and that you can use <;> to adress them at the same time.
Similarly, for binary relations $R$ that are reflexive (like $\leq$ or $=$), we have the tactic called rfl. Consider the goal
⊢ a R a
We prove this goal with:
rfl
For next week
As most of us did not manage to finish chapter two yet, this will be the homework for next week. Try to finish Section 3, 4 and 5.