From 44320bda5c0851f6605bf217618c827001cf3b2b Mon Sep 17 00:00:00 2001 From: Patrick Massot Date: Mon, 24 Feb 2025 23:33:44 +0100 Subject: [PATCH] Use a short track --- GlimpseOfLean.lean | 1 + GlimpseOfLean/Exercises/Shorter.lean | 646 +++++++++++++++ .../Exercises/Topics/SequenceLimits.lean | 17 +- GlimpseOfLean/Introduction.lean | 11 +- GlimpseOfLean/Library/Basic.lean | 18 - GlimpseOfLean/Library/Short.lean | 27 + GlimpseOfLean/Solutions/Shorter.lean | 763 ++++++++++++++++++ .../Solutions/Topics/SequenceLimits.lean | 17 +- README.md | 20 +- 9 files changed, 1482 insertions(+), 38 deletions(-) create mode 100644 GlimpseOfLean/Exercises/Shorter.lean create mode 100644 GlimpseOfLean/Library/Short.lean create mode 100644 GlimpseOfLean/Solutions/Shorter.lean diff --git a/GlimpseOfLean.lean b/GlimpseOfLean.lean index 7f4b5aa..b430c39 100644 --- a/GlimpseOfLean.lean +++ b/GlimpseOfLean.lean @@ -1,4 +1,5 @@ import GlimpseOfLean.Introduction +import GlimpseOfLean.Solutions.Shorter import GlimpseOfLean.Solutions.«01Rewriting» import GlimpseOfLean.Solutions.«02Iff» import GlimpseOfLean.Solutions.«03Forall» diff --git a/GlimpseOfLean/Exercises/Shorter.lean b/GlimpseOfLean/Exercises/Shorter.lean new file mode 100644 index 0000000..95b802d --- /dev/null +++ b/GlimpseOfLean/Exercises/Shorter.lean @@ -0,0 +1,646 @@ +import GlimpseOfLean.Library.Short + +/- # A shorter Glimpse of Lean + +This file is the short track of the Glimpse of Lean project. It is meant for people +who want to spend two hours discovering Lean. The hope is that two hours are +enough to reach at least the first exercises about limits of sequences of real numbers. +If you go faster or have a bit more time, you can try to do all those exercises. + +Of course the proofs are not always the most idiomatic ones since we aim to keep +the amount of things to explain very low, while still giving a glimpse of how Lean +sees mathematical proofs. + +Every command that is typed to make progress in the proof is called a “tactic”. We will +learn about ten of them. For each tactic, we will see a couple of examples and then you +will have exercise. The goal of each exercise is to replace the word `sorry` by +a sequence of tactics that bring Lean to report there are no remaining goal +without reporting any error along the way. + +The opening and closing curly braces for each proof are not mandatory, but they help +making sure errors don’t escape your attention. In particular you should be careful +to check that are not underlined in red since this would mean there is an error. +-/ + +/- ## Computing -/ + +/- +We start with basic computations using real numbers. We could play the micro-management +game invoking properties like commutatitivity and associativity of addition. +But we can also ask Lean to take care of any proof that only uses those properties +using the `ring` tactic. +By “only those properties” we mean in particular it won’t use any assumption +specific to the proof at hand. + +The word `ring` refers to the abstract mathematical definition that encapsulates the +basic properties of addition, subtraction and multiplication. Knowing about this +abstract algebra is not required here. +-/ + +example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by { + ring +} + +/- +Now it’s your turn: replace the word sorry with the relevant tactic to +finish the exercise. +-/ + +example (a b : ℝ) : (a+b)*(a-b) = a^2 - b^2 := by { + sorry +} + +/- +Our next tactic in the `congr` tactic (`congr` stands for “congruence”). +It tries to prove equalities by comparing both sides and creating new goals each time it +sees some mismatch. +-/ + +example (a b : ℝ) (f : ℝ → ℝ) : f ((a+b)^2) = f (a^2 + 2*a*b + b^2) := by { + congr + -- `congr` recognized the pattern `f _ = f _` and created a new goal + -- about the mismatching part, namely the arguments supplied to `f`. + ring +} + +/- +Try it on the next example. +-/ + +example (a b : ℝ) (f : ℝ → ℝ) : f ((a+b)^2 - 2*a*b) = f (a^2 + b^2) := by { + sorry +} + +/- +When there are several mismatches, `congr` creates several goals. +Sometimes it gets over-enthusastic and matches “too much”. For instance, if the goal +is `f (a+b) = f (b+a)` then `congr` will recognize the common pattern +`f (_ + _) = f (_ + _)` and create two goals: `a = b` and `b = a`. +This can be controlled in various ways. The most basic one is enough for us: we can limit +the number of function application layers by putting a number after `congr`. +In the example the two functions that are applied are `f` and addition, and we want to +go only through the application of `f`. +-/ + +example (a b : ℝ) (f : ℝ → ℝ) : f (a + b) = f (b + a) := by { + congr 1 -- try removing that 1 or increasing it to see the issue. + ring +} + +/- +Actually `congr` does more than finding mismatches, it also try to resolve them +using assumptions. In the next example, `congr` creates the goal `a + b = c` by +matching, and then immediately proves it by noticing and using assumption `h`. +-/ + +example (a b c : ℝ) (h : a + b = c) (f : ℝ → ℝ) : f (a + b) = f c := by { + congr +} + +/- +The tactics `ring` and `congr` are the basic tools we will use to compute. +But sometimes we need to chain several computation steps. +This is the job of the `calc` tactic. + +In the following example, it helps to carefully consider the tactic state +displayed after each `by` after the `calc` line. +-/ + +example (a b c d : ℝ) (h : c = b*a - d) (h' : d = a*b) : c = 0 := by { + calc + c = b*a - d := by congr + _ = b*a - a*b := by congr + _ = 0 := by ring +} + +/- +Note that each `_` stands for the righ-hand side of the previous line. +So we are really proving a sequence of equalities, and then the `calc` tactic +takes care of applying transitivity of equality (or equalities and inequalities +when proving inequalities). Each proof in this sequence is introduced by `:= by`. + +The indentation rules for `calc` are a bit subtle, especially when there +are other tactics after `calc`. Be careful to always align the `_`. +Aligning the equality signs and the `:=` signs looks nice but is not mandatory. + +Laying out those calculation steps and copy-pasting the common pieces can be a +bit tedious on larger examples, but we get help from the calc widget, as can be +seen on the video at + +https://www.imo.universite-paris-saclay.fr/~patrick.massot/calc_widget.webm + +Note that subterm selection is done using Shift-click. This is different from +regular selection of text in your editor or browser. +-/ + +example (a b c : ℝ) (h : a = -b) (h' : b + c = 0) : b*(a - c) = 0 := by { + sorry + +/- +We can also handle inequalities using `gcongr` (which stands for “generalized congruence”) +instead of `congr`. +-/ + +example (a b : ℝ) (h : a ≤ 2*b) : a + b ≤ 3*b := by { + calc + a + b ≤ 2*b + b := by gcongr + _ = 3*b := by ring +} + +example (a b : ℝ) (h : b ≤ a) : a + b ≤ 2*a := by { + sorry +} + +/- +The last tactic you will use in computation is the simplifier `simp`. It will +repeatedly apply a number of lemmas that are marked as simplification lemmas. +For instance the proof below simplifies `x - x` to `0` and then `|0|` to `0`. +-/ + +example (x : ℝ) : |x - x| = 0 := by { + simp +} + + +/- ## Universal quantifiers and implications + +Now let’s learn about the `∀` quantifier. + +Let `P` be a predicate on a type `X`. This means for every mathematical +object `x` with type `X`, we get a mathematical statement `P x`. + +Lean sees a proof `h` of `∀ x, P x` as a function sending any `x : X` to +a proof `h x` of `P x`. +This already explains the main way to use an assumption or lemma which +starts with a `∀`: we can simply feed it an element of `X`. + +Note we don't need to spell out the type of `x` in the expression `∀ x, P x` +as long as the type of `P` is clear to Lean, which can then infer the type of `x`. + +Let's define a predicate to play with `∀`. In that example we have a function +`f : ℝ → ℝ` at hand, and `X = ℝ`. +-/ + +def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x + +/- +In the above definition, note how there is no parentheses in `f x`. +This is how Lean denotes function application. In `f (-x)` there are parentheses +to prevent Lean from seeing a subtraction of `f` and `x` (which would make no sense). +Also be careful the space between `f` and `(-x)` is mandatory. + +The `apply` tactic can be used to specialize universally quantified statements. +-/ + +example (f : ℝ → ℝ) (hf : even_fun f) : f (-3) = f 3 := by { + apply hf 3 +} + +/- +Fortunately, Lean is willing to work for us, so we can leave out the `3` and +let the `apply` tactic compare the goal with the assumption +and decide to specialize it to `x = 3`. +-/ + +example (f : ℝ → ℝ) (hf : even_fun f) : f (-3) = f 3 := by { + apply hf +} + +/- +In the following exercise, you get to choose whether you want help from Lean +or do all the work. +-/ +example (f : ℝ → ℝ) (hf : even_fun f) : f (-5) = f 5 := by { + sorry +} + +/- +This was about using a `∀`. Let us now see how to prove a `∀`. + +In order to prove `∀ x, P x`, we use `intro x₀` to fix an arbitrary object +with type `X`, and call it `x₀` (`intro` stands for “introduce”). +Note we don’t have to use the letter `x₀`, any name will work. + +We will prove that the real cosine function is even. After introducing some `x₀`, +the simplifier tactic can finish the proof. +-/ + +open Real in -- this line insists that we mean real cos, not the complex numbers one. +example : even_fun cos := by { + intros x₀ + simp +} + +/- +In order to get slightly more interesting examples, we will both use and prove +some universally quantified statements. + +In the next proof, we also take the opportunity to introduce the +`unfold` tactic, which simply unfolds definitions. Here this is purely +for didactic reason, Lean doesn't need those `unfold` invocations. +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by { + -- Our assumption on that f is even means ∀ x, f (-x) = f x + unfold even_fun at hf -- note how `hf` changes after this line + -- and the same for g + unfold even_fun at hg + -- We need to prove ∀ x, (f+g)(-x) = (f+g)(x) + unfold even_fun + -- Let x₀ be any real number + intro x₀ + -- and let's compute + calc + (f + g) (-x₀) = f (-x₀) + g (-x₀) := by simp + _ = f x₀ + g (-x₀) := by congr 1; apply hf + -- put you cursor between `;` and `apply` in the previous line to see the intermediate goal + _ = f x₀ + g x₀ := by congr 1; apply hg + _ = (f + g) x₀ := by simp +} + + +/- +Tactics like `congr` and `ring` will not unfold definitions that appear in the goal. +This is why the first computation line is necessary, although it only unfolds a definition. +The last line is not necessary however, since it only proves +something that is true by definition, and is not followed by any other tactic. + +Also that `congr` can generate several goals so we don’t have to call it twice. + +Hence we can compress the above proof to: +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by { + intro x₀ + calc + (f + g) (-x₀) = f (-x₀) + g (-x₀) := by simp + _ = f x₀ + g x₀ := by congr 1; apply hf; apply hg +} + +/- +If you would rather uncompress the proof, you can use the `specialize` tactic to +specialize a universally quantified assumption before using it. +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by { + -- Let x₀ be any real number + intro x₀ + specialize hf x₀ -- hf is now only about the x₀ we just introduced + specialize hg x₀ -- hg is now only about the x₀ we just introduced + -- and let's compute + -- (note how `congr` now finds assumptions finishing those steps) + calc + (f + g) (-x₀) = f (-x₀) + g (-x₀) := by simp + _ = f x₀ + g (-x₀) := by congr + _ = f x₀ + g x₀ := by congr + _ = (f + g) x₀ := by simp +} +/- +Now let's practice. If you need to learn how to type a unicode symbol you can +put your mouse cursor above the symbol and wait for one second. +Recall you can set a depth limit in `congr` by giving it a number as in `congr 1`. + +Note also that you can call your arbitrary real number `x` instead of `x₀` if +you want to save some typing. We called it `x₀` only to emphasize it doesn’t +need to be the same notation as in the statement. +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) : even_fun (g ∘ f) := by { + sorry +} + +/- +Let's now combine the universal quantifier with implication. + +In the next definitions, note how `∀ x₁, ∀ x₂, ...` is abbreviated to `∀ x₁ x₂, ...`. +-/ + +def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂ + +def non_increasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≥ f x₂ + +/- +Note how Lean uses a single arrow `→` to denote implication. This is the same arrow +as in `f : ℝ → ℝ`. Indeed Lean sees a proof of the implication `P → Q` as a +function from proofs of `P` to proofs of `Q`. + +So an assumption `hf : non_decreasing f` is a function that takes as input two numbers +and a inequality between them and outputs an inequality between their images under `f`. +-/ + +example (f : ℝ → ℝ) (hf : non_decreasing f) (x₁ x₂ : ℝ) (hx : x₁ ≤ x₂) : f x₁ ≤ f x₂ := by { + apply hf x₁ x₂ hx +} + +/- +We can ask Lean to work more for us, as in the following example: +-/ + +example (f : ℝ → ℝ) (hf : non_decreasing f) (x₁ x₂ : ℝ) (hx : x₁ ≤ x₂) : f x₁ ≤ f x₂ := by { + apply hf -- Lean compares the goal with the assumption `hf`. It recognizes that `hf` + -- needs to be specialized to the numbers `x₁` and `x₂` that are given, to get + -- the implication `x₁ ≤ x₂ → f x₁ ≤ f x₂` and then asks for a proof of the + -- premise `x₁ ≤ x₂` + apply hx -- Our assumption hx is such a proof +} + +/- +Note that the tactic `apply` does not mean anything vague like “make something +of that expression somehow”. It asks for an input that is either a full proof +as in the first example, or a proof of statement involving universal +quantifiers and implications in front of some statement that can be specialized +to the current goal (as in the previous example). + +In this very simple example, we did not gain much. Now compare the following +two proofs of the same statement. +-/ + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : + non_decreasing (g ∘ f) := by { + intro x₁ x₂ hx + apply hg (f x₁) (f x₂) (hf x₁ x₂ hx) +} + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : + non_decreasing (g ∘ f) := by { + intro x₁ x₂ h + apply hg + apply hf + apply h +} + +/- +Take some time to understand how, in the second proof, Lean saves us the +trouble of finding the relevant pairs of numbers and also nicely cuts the proof +into pieces. You can choose your way in the following variation. +-/ + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) : + non_increasing (g ∘ f) := by { + sorry +} + +/- +At this stage you should feel that such proof actually don’t require any thinking at all. +And indeed Lean can easily handle the full proof in one tactic (but we won’t need this +here). + +We can also use the `specialize` tactic to feed arguments to an assumption +before using it, as we saw with the example of even functions. +-/ + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : + non_decreasing (g + f) := by { + intro x₁ x₂ h + specialize hf x₁ x₂ h + specialize hg x₁ x₂ h + calc + (g + f) x₁ = g x₁ + f x₁ := by simp + _ ≤ g x₂ + f x₂ := by gcongr + _ = (g + f) x₂ := by simp +} + + +/- # Finding lemmas + +Lean’s mathematical library contains many useful facts, and remembering all of +them by name is infeasible. We already saw the simplifier tactic `simp` which +applies many lemmas without using their names. +-/ + +/- Use `simp` to prove the following. Note that `X : Set ℝ` +means that `X` is a set containing (only) real numbers. -/ +example (x : ℝ) (X Y : Set ℝ) (hx : x ∈ X) : x ∈ (X ∩ Y) ∪ (X \ Y) := by { + sorry +} + +/- +The `apply?` will find lemmas from the library and tell you their names. +It creates a suggestion below the goal display. You can click on this suggestion +to edit your code. +Use `apply?` to find the lemma that every continuous function with compact support +has a global minimum. -/ + +example (f : ℝ → ℝ) (hf : Continuous f) (h2f : HasCompactSupport f) : ∃ x, ∀ y, f x ≤ f y := by { + sorry +} + +/- ## Extential quantifiers + +In order to prove `∃ x, P x`, we give some `x₀` using tactic `use x₀` and +then prove `P x₀`. This `x₀` can be an object from the local context +or a more complicated expression. In the example below, the property +to check after `use` is true by definition so the proof is over. +-/ +example : ∃ n : ℕ, 8 = 2*n := by { + use 4 +} + +/- +In order to use `h : ∃ x, P x`, we use the `rcases` tactic to fix +one `x₀` that works. + +Again `h` can come straight from the local context or can be a more +complicated expression. + +The examples will use divisibility in ℤ (beware the ∣ symbol which is +not ASCII but a unicode symbol). The angle brackets appearing after the +word `with` are also unicode symbols. +If your keyboard is not configured to directly type those symbols, you can +put your mouse cursor above the symbol and wait for one second to see how +to type them in this editor. + +-/ + +example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := by { + rcases h₁ with ⟨k, hk⟩ -- we fix some `k` such that `b = a * k` + rcases h₂ with ⟨l, hl⟩ -- we fix some `l` such that `c = b * l` + -- Since `a ∣ c` means `∃ k, b = a*k`, we need the `use` tactic. + use k*l + calc + c = b*l := by congr + _ = (a*k)*l := by congr + _ = a*(k*l) := by ring +} + +example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c := by { + sorry +} + +/- +## Limits + +We learned enough tactics to manipulate a definition involving both kinds of quantifiers: +limits of sequences of real numbers. + +-/ + +/-- A sequence `u` converges to a limit `l` if the following holds. -/ +def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε + +/- If u is constant with value l then u tends to l. +Hint: `simp` can rewrite `|l - l|` to `0`. +Also remember `apply?` can find lemmas whose name you don’t want to remember, such as +the lemma saying that positive implies non-negative. -/ +example (h : ∀ n, u n = l) : seq_limit u l := by { + sorry +} + +/- When dealing with absolute values, we'll use the lemma: + +`abs_le {x y : ℝ} : |x| ≤ y ↔ -y ≤ x ∧ x ≤ y` + +When dealing with max, we’ll use + +`ge_max_iff (p q r) : r ≥ max p q ↔ r ≥ p ∧ r ≥ q` + +The way we will use those lemmas is with the rewriting command +`rw`. Let's see an example. +In that example, we kept `apply?` instead of accepting its suggestions in order to emphasize +there is no need to remember those lemma names. +-/ + +-- If `u` tends to `l` and `v` tends `l'` then `u+v` tends to `l+l'` +example (hu : seq_limit u l) (hv : seq_limit v l') : + seq_limit (u + v) (l + l') := by { + intros ε ε_pos + rcases hu (ε/2) (by apply?) with ⟨N₁, hN₁⟩ + rcases hv (ε/2) (by apply?) with ⟨N₂, hN₂⟩ + use max N₁ N₂ + intros n hn + rw [ge_max_iff] at hn -- Note how hn changes from `n ≥ max N₁ N₂` to `n ≥ N₁ ∧ n ≥ N₂` + specialize hN₁ n hn.1 + specialize hN₂ n hn.2 + calc + |(u + v) n - (l + l')| = |u n + v n - (l + l')| := by simp + _ = |(u n - l) + (v n - l')| := by congr; ring + _ ≤ |u n - l| + |v n - l'| := by apply? + _ ≤ ε/2 + ε/2 := by gcongr + _ = ε := by simp +} + + +/- Let's do something similar: the squeezing theorem using both `ge_max_iff` and `abs_le`. +You will probably want to rewrite using `abs_le` in several assumptions as well as in the +goal. You can use `rw [abs_le] at *` for this. -/ +example (hu : seq_limit u l) (hw : seq_limit w l) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : + seq_limit v l := by { + sorry +} + + +/- In the next exercise, we'll use + +`eq_of_abs_sub_le_all (x y : ℝ) : (∀ ε > 0, |x - y| ≤ ε) → x = y` + +as the first step. +-/ + +-- A sequence admits at most one limit. You will be able to use that lemma in the following +-- exercises. +lemma uniq_limit (hl : seq_limit u l) (hl' : seq_limit u l') : l = l' := by { + apply eq_of_abs_sub_le_all + sorry +} + +/- +## Conjunctions + +In order to prove more things about sequences of real number, we now explain how to +handle one more logical gadget: conjunction. + +Given two statements `P` and `Q`, the conjunction `P ∧ Q` is the statement that +`P` and `Q` are both true (`∧` is sometimes called the “logical and”). + +In order to prove `P ∧ Q` we use the `constructor` tactic that splits the goal +into proving `P` and then proving `Q`. + +In order to use a proof `h` of `P ∧ Q`, we use `h.1` to get a proof of `P` +and `h.2` to get a proof of `Q`. We can also use `rcases h with ⟨hP, hQ⟩` to +get `hP : P` and `hQ : Q`. + +Let us see both in action in a very basic logic proof: let us deduce `Q ∧ P` +from `P ∧ Q`. +-/ + +example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by { + constructor + apply h.2 + apply h.1 +} + +/- + +## Subsequences + +We will now play with subsequences. + +The new definition we will use is that `φ : ℕ → ℕ` is an extraction +if it is (strictly) increasing. +-/ + +def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m + +/- +In the following, `φ` will always denote a function from `ℕ` to `ℕ`. + +The next lemma is proved by an easy induction, but we haven't seen induction +in this tutorial. If you did the natural number game then you can delete +the proof below and try to reconstruct it. Otherwise you can simply take a quick look +at how proofs by induction look like (but we won’t need any other one here). +-/ +/-- An extraction is greater than id -/ +lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n := by { + intros hyp n + induction n with + | zero => apply? + | succ n ih => exact Nat.succ_le_of_lt (by + calc n ≤ φ n := ih + _ < φ (n + 1) := by apply hyp; apply?) +} + +/- +In the exercise, we use `∃ n ≥ N, ...` which is the abbreviation of +`∃ n, n ≥ N ∧ ...`. + +Don’t forget to move the cursor around to see what each `apply?` is proving. +-/ + +/-- Extractions take arbitrarily large values for arbitrarily large +inputs. -/ +lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by { + sorry +} + +/-- A real number `a` is a cluster point of a sequence `u` +if `u` has a subsequence converging to `a`. -/ +def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a + +/-- If `a` is a cluster point of `u` then there are values of +`u` arbitrarily close to `a` for arbitrarily large input. -/ +lemma near_cluster : + cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε := by { + sorry +} + + +/-- If `u` tends to `l` then its subsequences tend to `l`. -/ +lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) : +seq_limit (u ∘ φ) l := by { + sorry +} + +/-- If `u` tends to `l` all its cluster points are equal to `l`. -/ +lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l := by { + sorry +} + +/-- `u` is a Cauchy sequence -/ +def CauchySequence (u : ℕ → ℝ) := + ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε + +example : (∃ l, seq_limit u l) → CauchySequence u := by { + sorry +} + + diff --git a/GlimpseOfLean/Exercises/Topics/SequenceLimits.lean b/GlimpseOfLean/Exercises/Topics/SequenceLimits.lean index b870642..a4cea7a 100644 --- a/GlimpseOfLean/Exercises/Topics/SequenceLimits.lean +++ b/GlimpseOfLean/Exercises/Topics/SequenceLimits.lean @@ -1,5 +1,7 @@ import GlimpseOfLean.Library.Basic +namespace Topics + /- In this file we manipulate the elementary definition of limits of sequences of real numbers. @@ -33,10 +35,12 @@ example (a b c d : ℝ) (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d := by A sequence `u` is a function from `ℕ` to `ℝ`, hence Lean says `u : ℕ → ℝ` The definition we'll be using is: +-/ --- Definition of « u tends to l » -`def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε` +/-- Definition of « u tends to l » -/ +def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε +/- Note the use of `∀ ε > 0, _` which is an abbreviation of `∀ ε, ε > 0 → _ ` @@ -138,7 +142,7 @@ Recall we listed three variations on the triangle inequality at the beginning of -- A sequence admits at most one limit. You will be able to use that lemma in the following -- exercises. -lemma uniq_limit : seq_limit u l → seq_limit u l' → l = l' := by { +lemma unique_limit : seq_limit u l → seq_limit u l' → l = l' := by { sorry } @@ -162,9 +166,11 @@ We will now play with subsequences. The new definition we will use is that `φ : ℕ → ℕ` is an extraction if it is (strictly) increasing. +-/ -`def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m` +def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m +/- In the following, `φ` will always denote a function from `ℕ` to `ℕ`. The next lemma is proved by an easy induction, but we haven't seen induction @@ -193,10 +199,9 @@ lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by /- A real number `a` is a cluster point of a sequence `u` if `u` has a subsequence converging to `a`. - -`def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a` -/ +def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a /-- If `a` is a cluster point of `u` then there are values of `u` arbitrarily close to `a` for arbitrarily large input. -/ diff --git a/GlimpseOfLean/Introduction.lean b/GlimpseOfLean/Introduction.lean index 31e687f..e36d1f0 100644 --- a/GlimpseOfLean/Introduction.lean +++ b/GlimpseOfLean/Introduction.lean @@ -69,6 +69,11 @@ example (f : ℝ → ℝ) (u : ℕ → ℝ) (x₀ : ℝ) (hu : seq_limit u x₀) } /- -Now that this proof is over, you can use the file explorer to the -left of this panel to open the file `Exercises > 01Rewriting.lean`. --/ \ No newline at end of file +Now that this proof is over, you can choose between the short track or the longer one. +If you want to do the short track then you should follow the link from the README page +to the file `Shorter.lean` on the lean4web server. + +If you follow the longer track using a local installation or GitPod or Codespaces, +you should use the file explorer to the left of this panel to open the file +`Exercises > 01Rewriting.lean`. +-/ diff --git a/GlimpseOfLean/Library/Basic.lean b/GlimpseOfLean/Library/Basic.lean index d4e4dfb..41ffdb7 100644 --- a/GlimpseOfLean/Library/Basic.lean +++ b/GlimpseOfLean/Library/Basic.lean @@ -25,24 +25,6 @@ lemma abs_sub_le' {α : Type _} [LinearOrderedAddCommGroup α] (a b c : α) : |a - c| ≤ |a - b| + |c - b| := abs_sub_comm c b ▸ abs_sub_le _ _ _ -def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε - -lemma unique_limit {u l l'} : seq_limit u l → seq_limit u l' → l = l' := by - refine fun hl hl' ↦ eq_of_abs_sub_le_all fun ε ε_pos ↦ ?_ - rcases hl (ε/2) (by linarith) with ⟨N, hN⟩ - rcases hl' (ε/2) (by linarith) with ⟨N', hN'⟩ - specialize hN (max N N') (le_max_left _ _) - specialize hN' (max N N') (le_max_right _ _) - calc |l - l'| = |(l-u (max N N')) + (u (max N N') -l')| := by ring_nf - _ ≤ |l - u (max N N')| + |u (max N N') - l'| := abs_add_le _ _ - _ = |u (max N N') - l| + |u (max N N') - l'| := by rw [abs_sub_comm] - _ ≤ ε/2 + ε/2 := add_le_add hN hN' - _ = ε := add_halves _ - -def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m - -def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a - open BigOperators lemma Finset.sum_univ_eq_single {β : Type u} {α : Type v} [Fintype α] [AddCommMonoid β] diff --git a/GlimpseOfLean/Library/Short.lean b/GlimpseOfLean/Library/Short.lean new file mode 100644 index 0000000..2baa8a5 --- /dev/null +++ b/GlimpseOfLean/Library/Short.lean @@ -0,0 +1,27 @@ +import Mathlib.Tactic +import Mathlib.Data.Real.Basic +import Mathlib.Data.Complex.Trigonometric + +lemma ge_max_iff {α : Type*} [LinearOrder α] {p q r : α} : r ≥ max p q ↔ r ≥ p ∧ r ≥ q := + max_le_iff + +open Lean PrettyPrinter Delaborator SubExpr in +@[app_delab Max.max] +def delabMax : Delab := do + let e ← getExpr + guard <| e.isAppOfArity ``Max.max 4 + let m := mkIdent `max + let x ← withNaryArg 2 delab + let y ← withNaryArg 3 delab + `($(m) $(x) $(y)) + +open Lean PrettyPrinter Delaborator SubExpr in +@[app_delab Min.min] +def delabMin : Delab := do + let e ← getExpr + guard <| e.isAppOfArity ``Min.min 4 + let m := mkIdent `min + let x ← withNaryArg 2 delab + let y ← withNaryArg 3 delab + `($(m) $(x) $(y)) + diff --git a/GlimpseOfLean/Solutions/Shorter.lean b/GlimpseOfLean/Solutions/Shorter.lean new file mode 100644 index 0000000..0427772 --- /dev/null +++ b/GlimpseOfLean/Solutions/Shorter.lean @@ -0,0 +1,763 @@ +import GlimpseOfLean.Library.Short + +/- # A shorter Glimpse of Lean + +This file is the short track of the Glimpse of Lean project. It is meant for people +who want to spend two hours discovering Lean. The hope is that two hours are +enough to reach at least the first exercises about limits of sequences of real numbers. +If you go faster or have a bit more time, you can try to do all those exercises. + +Of course the proofs are not always the most idiomatic ones since we aim to keep +the amount of things to explain very low, while still giving a glimpse of how Lean +sees mathematical proofs. + +Every command that is typed to make progress in the proof is called a “tactic”. We will +learn about ten of them. For each tactic, we will see a couple of examples and then you +will have exercise. The goal of each exercise is to replace the word `sorry` by +a sequence of tactics that bring Lean to report there are no remaining goal +without reporting any error along the way. + +The opening and closing curly braces for each proof are not mandatory, but they help +making sure errors don’t escape your attention. In particular you should be careful +to check that are not underlined in red since this would mean there is an error. +-/ + +/- ## Computing -/ + +/- +We start with basic computations using real numbers. We could play the micro-management +game invoking properties like commutatitivity and associativity of addition. +But we can also ask Lean to take care of any proof that only uses those properties +using the `ring` tactic. +By “only those properties” we mean in particular it won’t use any assumption +specific to the proof at hand. + +The word `ring` refers to the abstract mathematical definition that encapsulates the +basic properties of addition, subtraction and multiplication. Knowing about this +abstract algebra is not required here. +-/ + +example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by { + ring +} + +/- +Now it’s your turn: replace the word sorry with the relevant tactic to +finish the exercise. +-/ + +example (a b : ℝ) : (a+b)*(a-b) = a^2 - b^2 := by { + -- sorry + ring + -- sorry +} + +/- +Our next tactic in the `congr` tactic (`congr` stands for “congruence”). +It tries to prove equalities by comparing both sides and creating new goals each time it +sees some mismatch. +-/ + +example (a b : ℝ) (f : ℝ → ℝ) : f ((a+b)^2) = f (a^2 + 2*a*b + b^2) := by { + congr + -- `congr` recognized the pattern `f _ = f _` and created a new goal + -- about the mismatching part, namely the arguments supplied to `f`. + ring +} + +/- +Try it on the next example. +-/ + +example (a b : ℝ) (f : ℝ → ℝ) : f ((a+b)^2 - 2*a*b) = f (a^2 + b^2) := by { + -- sorry + congr + ring + -- sorry +} + +/- +When there are several mismatches, `congr` creates several goals. +Sometimes it gets over-enthusastic and matches “too much”. For instance, if the goal +is `f (a+b) = f (b+a)` then `congr` will recognize the common pattern +`f (_ + _) = f (_ + _)` and create two goals: `a = b` and `b = a`. +This can be controlled in various ways. The most basic one is enough for us: we can limit +the number of function application layers by putting a number after `congr`. +In the example the two functions that are applied are `f` and addition, and we want to +go only through the application of `f`. +-/ + +example (a b : ℝ) (f : ℝ → ℝ) : f (a + b) = f (b + a) := by { + congr 1 -- try removing that 1 or increasing it to see the issue. + ring +} + +/- +Actually `congr` does more than finding mismatches, it also try to resolve them +using assumptions. In the next example, `congr` creates the goal `a + b = c` by +matching, and then immediately proves it by noticing and using assumption `h`. +-/ + +example (a b c : ℝ) (h : a + b = c) (f : ℝ → ℝ) : f (a + b) = f c := by { + congr +} + +/- +The tactics `ring` and `congr` are the basic tools we will use to compute. +But sometimes we need to chain several computation steps. +This is the job of the `calc` tactic. + +In the following example, it helps to carefully consider the tactic state +displayed after each `by` after the `calc` line. +-/ + +example (a b c d : ℝ) (h : c = b*a - d) (h' : d = a*b) : c = 0 := by { + calc + c = b*a - d := by congr + _ = b*a - a*b := by congr + _ = 0 := by ring +} + +/- +Note that each `_` stands for the righ-hand side of the previous line. +So we are really proving a sequence of equalities, and then the `calc` tactic +takes care of applying transitivity of equality (or equalities and inequalities +when proving inequalities). Each proof in this sequence is introduced by `:= by`. + +The indentation rules for `calc` are a bit subtle, especially when there +are other tactics after `calc`. Be careful to always align the `_`. +Aligning the equality signs and the `:=` signs looks nice but is not mandatory. + +Laying out those calculation steps and copy-pasting the common pieces can be a +bit tedious on larger examples, but we get help from the calc widget, as can be +seen on the video at + +https://www.imo.universite-paris-saclay.fr/~patrick.massot/calc_widget.webm + +Note that subterm selection is done using Shift-click. This is different from +regular selection of text in your editor or browser. +-/ + +example (a b c : ℝ) (h : a = -b) (h' : b + c = 0) : b*(a - c) = 0 := by { + -- sorry + calc + b*(a - c) = b*(-b - c) := by congr + _ = -b*(b + c) := by ring + _ = -b*0 := by congr + _ = 0 := by ring +} + -- sorry + +/- +We can also handle inequalities using `gcongr` (which stands for “generalized congruence”) +instead of `congr`. +-/ + +example (a b : ℝ) (h : a ≤ 2*b) : a + b ≤ 3*b := by { + calc + a + b ≤ 2*b + b := by gcongr + _ = 3*b := by ring +} + +example (a b : ℝ) (h : b ≤ a) : a + b ≤ 2*a := by { + -- sorry + calc + a + b ≤ a + a := by gcongr + _ = 2*a := by ring + -- sorry +} + +/- +The last tactic you will use in computation is the simplifier `simp`. It will +repeatedly apply a number of lemmas that are marked as simplification lemmas. +For instance the proof below simplifies `x - x` to `0` and then `|0|` to `0`. +-/ + +example (x : ℝ) : |x - x| = 0 := by { + simp +} + + +/- ## Universal quantifiers and implications + +Now let’s learn about the `∀` quantifier. + +Let `P` be a predicate on a type `X`. This means for every mathematical +object `x` with type `X`, we get a mathematical statement `P x`. + +Lean sees a proof `h` of `∀ x, P x` as a function sending any `x : X` to +a proof `h x` of `P x`. +This already explains the main way to use an assumption or lemma which +starts with a `∀`: we can simply feed it an element of `X`. + +Note we don't need to spell out the type of `x` in the expression `∀ x, P x` +as long as the type of `P` is clear to Lean, which can then infer the type of `x`. + +Let's define a predicate to play with `∀`. In that example we have a function +`f : ℝ → ℝ` at hand, and `X = ℝ`. +-/ + +def even_fun (f : ℝ → ℝ) := ∀ x, f (-x) = f x + +/- +In the above definition, note how there is no parentheses in `f x`. +This is how Lean denotes function application. In `f (-x)` there are parentheses +to prevent Lean from seeing a subtraction of `f` and `x` (which would make no sense). +Also be careful the space between `f` and `(-x)` is mandatory. + +The `apply` tactic can be used to specialize universally quantified statements. +-/ + +example (f : ℝ → ℝ) (hf : even_fun f) : f (-3) = f 3 := by { + apply hf 3 +} + +/- +Fortunately, Lean is willing to work for us, so we can leave out the `3` and +let the `apply` tactic compare the goal with the assumption +and decide to specialize it to `x = 3`. +-/ + +example (f : ℝ → ℝ) (hf : even_fun f) : f (-3) = f 3 := by { + apply hf +} + +/- +In the following exercise, you get to choose whether you want help from Lean +or do all the work. +-/ +example (f : ℝ → ℝ) (hf : even_fun f) : f (-5) = f 5 := by { + -- sorry + apply hf + -- sorry +} + +/- +This was about using a `∀`. Let us now see how to prove a `∀`. + +In order to prove `∀ x, P x`, we use `intro x₀` to fix an arbitrary object +with type `X`, and call it `x₀` (`intro` stands for “introduce”). +Note we don’t have to use the letter `x₀`, any name will work. + +We will prove that the real cosine function is even. After introducing some `x₀`, +the simplifier tactic can finish the proof. +-/ + +open Real in -- this line insists that we mean real cos, not the complex numbers one. +example : even_fun cos := by { + intros x₀ + simp +} + +/- +In order to get slightly more interesting examples, we will both use and prove +some universally quantified statements. + +In the next proof, we also take the opportunity to introduce the +`unfold` tactic, which simply unfolds definitions. Here this is purely +for didactic reason, Lean doesn't need those `unfold` invocations. +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by { + -- Our assumption on that f is even means ∀ x, f (-x) = f x + unfold even_fun at hf -- note how `hf` changes after this line + -- and the same for g + unfold even_fun at hg + -- We need to prove ∀ x, (f+g)(-x) = (f+g)(x) + unfold even_fun + -- Let x₀ be any real number + intro x₀ + -- and let's compute + calc + (f + g) (-x₀) = f (-x₀) + g (-x₀) := by simp + _ = f x₀ + g (-x₀) := by congr 1; apply hf + -- put you cursor between `;` and `apply` in the previous line to see the intermediate goal + _ = f x₀ + g x₀ := by congr 1; apply hg + _ = (f + g) x₀ := by simp +} + + +/- +Tactics like `congr` and `ring` will not unfold definitions that appear in the goal. +This is why the first computation line is necessary, although it only unfolds a definition. +The last line is not necessary however, since it only proves +something that is true by definition, and is not followed by any other tactic. + +Also that `congr` can generate several goals so we don’t have to call it twice. + +Hence we can compress the above proof to: +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by { + intro x₀ + calc + (f + g) (-x₀) = f (-x₀) + g (-x₀) := by simp + _ = f x₀ + g x₀ := by congr 1; apply hf; apply hg +} + +/- +If you would rather uncompress the proof, you can use the `specialize` tactic to +specialize a universally quantified assumption before using it. +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f + g) := by { + -- Let x₀ be any real number + intro x₀ + specialize hf x₀ -- hf is now only about the x₀ we just introduced + specialize hg x₀ -- hg is now only about the x₀ we just introduced + -- and let's compute + -- (note how `congr` now finds assumptions finishing those steps) + calc + (f + g) (-x₀) = f (-x₀) + g (-x₀) := by simp + _ = f x₀ + g (-x₀) := by congr + _ = f x₀ + g x₀ := by congr + _ = (f + g) x₀ := by simp +} +/- +Now let's practice. If you need to learn how to type a unicode symbol you can +put your mouse cursor above the symbol and wait for one second. +Recall you can set a depth limit in `congr` by giving it a number as in `congr 1`. + +Note also that you can call your arbitrary real number `x` instead of `x₀` if +you want to save some typing. We called it `x₀` only to emphasize it doesn’t +need to be the same notation as in the statement. +-/ + +example (f g : ℝ → ℝ) (hf : even_fun f) : even_fun (g ∘ f) := by { + -- sorry + intro x + calc + (g ∘ f) (-x) = g (f (-x)) := by simp + _ = g (f x) := by congr 1; apply hf + -- sorry +} + +/- +Let's now combine the universal quantifier with implication. + +In the next definitions, note how `∀ x₁, ∀ x₂, ...` is abbreviated to `∀ x₁ x₂, ...`. +-/ + +def non_decreasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≤ f x₂ + +def non_increasing (f : ℝ → ℝ) := ∀ x₁ x₂, x₁ ≤ x₂ → f x₁ ≥ f x₂ + +/- +Note how Lean uses a single arrow `→` to denote implication. This is the same arrow +as in `f : ℝ → ℝ`. Indeed Lean sees a proof of the implication `P → Q` as a +function from proofs of `P` to proofs of `Q`. + +So an assumption `hf : non_decreasing f` is a function that takes as input two numbers +and a inequality between them and outputs an inequality between their images under `f`. +-/ + +example (f : ℝ → ℝ) (hf : non_decreasing f) (x₁ x₂ : ℝ) (hx : x₁ ≤ x₂) : f x₁ ≤ f x₂ := by { + apply hf x₁ x₂ hx +} + +/- +We can ask Lean to work more for us, as in the following example: +-/ + +example (f : ℝ → ℝ) (hf : non_decreasing f) (x₁ x₂ : ℝ) (hx : x₁ ≤ x₂) : f x₁ ≤ f x₂ := by { + apply hf -- Lean compares the goal with the assumption `hf`. It recognizes that `hf` + -- needs to be specialized to the numbers `x₁` and `x₂` that are given, to get + -- the implication `x₁ ≤ x₂ → f x₁ ≤ f x₂` and then asks for a proof of the + -- premise `x₁ ≤ x₂` + apply hx -- Our assumption hx is such a proof +} + +/- +Note that the tactic `apply` does not mean anything vague like “make something +of that expression somehow”. It asks for an input that is either a full proof +as in the first example, or a proof of statement involving universal +quantifiers and implications in front of some statement that can be specialized +to the current goal (as in the previous example). + +In this very simple example, we did not gain much. Now compare the following +two proofs of the same statement. +-/ + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : + non_decreasing (g ∘ f) := by { + intro x₁ x₂ hx + apply hg (f x₁) (f x₂) (hf x₁ x₂ hx) +} + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : + non_decreasing (g ∘ f) := by { + intro x₁ x₂ h + apply hg + apply hf + apply h +} + +/- +Take some time to understand how, in the second proof, Lean saves us the +trouble of finding the relevant pairs of numbers and also nicely cuts the proof +into pieces. You can choose your way in the following variation. +-/ + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) : + non_increasing (g ∘ f) := by { + -- sorry + intro x₁ x₂ hx + apply hg (f x₁) (f x₂) (hf x₁ x₂ hx) + -- sorry +} + +/- +At this stage you should feel that such proof actually don’t require any thinking at all. +And indeed Lean can easily handle the full proof in one tactic (but we won’t need this +here). + +We can also use the `specialize` tactic to feed arguments to an assumption +before using it, as we saw with the example of even functions. +-/ + +example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_decreasing g) : + non_decreasing (g + f) := by { + intro x₁ x₂ h + specialize hf x₁ x₂ h + specialize hg x₁ x₂ h + calc + (g + f) x₁ = g x₁ + f x₁ := by simp + _ ≤ g x₂ + f x₂ := by gcongr + _ = (g + f) x₂ := by simp +} + + +/- # Finding lemmas + +Lean’s mathematical library contains many useful facts, and remembering all of +them by name is infeasible. We already saw the simplifier tactic `simp` which +applies many lemmas without using their names. +-/ + +/- Use `simp` to prove the following. Note that `X : Set ℝ` +means that `X` is a set containing (only) real numbers. -/ +example (x : ℝ) (X Y : Set ℝ) (hx : x ∈ X) : x ∈ (X ∩ Y) ∪ (X \ Y) := by { + -- sorry + simp + apply hx + -- sorry +} + +/- +The `apply?` will find lemmas from the library and tell you their names. +It creates a suggestion below the goal display. You can click on this suggestion +to edit your code. +Use `apply?` to find the lemma that every continuous function with compact support +has a global minimum. -/ + +example (f : ℝ → ℝ) (hf : Continuous f) (h2f : HasCompactSupport f) : ∃ x, ∀ y, f x ≤ f y := by { + -- sorry + -- use `apply?` to find: + exact Continuous.exists_forall_le_of_hasCompactSupport hf h2f + -- sorry +} + +/- ## Extential quantifiers + +In order to prove `∃ x, P x`, we give some `x₀` using tactic `use x₀` and +then prove `P x₀`. This `x₀` can be an object from the local context +or a more complicated expression. In the example below, the property +to check after `use` is true by definition so the proof is over. +-/ +example : ∃ n : ℕ, 8 = 2*n := by { + use 4 +} + +/- +In order to use `h : ∃ x, P x`, we use the `rcases` tactic to fix +one `x₀` that works. + +Again `h` can come straight from the local context or can be a more +complicated expression. + +The examples will use divisibility in ℤ (beware the ∣ symbol which is +not ASCII but a unicode symbol). The angle brackets appearing after the +word `with` are also unicode symbols. +If your keyboard is not configured to directly type those symbols, you can +put your mouse cursor above the symbol and wait for one second to see how +to type them in this editor. + +-/ + +example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : b ∣ c) : a ∣ c := by { + rcases h₁ with ⟨k, hk⟩ -- we fix some `k` such that `b = a * k` + rcases h₂ with ⟨l, hl⟩ -- we fix some `l` such that `c = b * l` + -- Since `a ∣ c` means `∃ k, b = a*k`, we need the `use` tactic. + use k*l + calc + c = b*l := by congr + _ = (a*k)*l := by congr + _ = a*(k*l) := by ring +} + +example (a b c : ℤ) (h₁ : a ∣ b) (h₂ : a ∣ c) : a ∣ b + c := by { + -- sorry + rcases h₁ with ⟨k, hk⟩ + rcases h₂ with ⟨l, hl⟩ + use k+l + calc + b + c = a*k + a*l := by congr + _ = a*(k + l) := by ring + -- sorry +} + +/- +## Limits + +We learned enough tactics to manipulate a definition involving both kinds of quantifiers: +limits of sequences of real numbers. + +-/ + +/-- A sequence `u` converges to a limit `l` if the following holds. -/ +def seq_limit (u : ℕ → ℝ) (l : ℝ) : Prop := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε + +/- If u is constant with value l then u tends to l. +Hint: `simp` can rewrite `|l - l|` to `0`. +Also remember `apply?` can find lemmas whose name you don’t want to remember, such as +the lemma saying that positive implies non-negative. -/ +example (h : ∀ n, u n = l) : seq_limit u l := by { + -- sorry + intros ε ε_pos + use 0 + intros n hn + calc |u n - l| = |l - l| := by congr; apply h + _ = 0 := by simp + _ ≤ ε := by apply? + -- sorry +} + +/- When dealing with absolute values, we'll use the lemma: + +`abs_le {x y : ℝ} : |x| ≤ y ↔ -y ≤ x ∧ x ≤ y` + +When dealing with max, we’ll use + +`ge_max_iff (p q r) : r ≥ max p q ↔ r ≥ p ∧ r ≥ q` + +The way we will use those lemmas is with the rewriting command +`rw`. Let's see an example. +In that example, we kept `apply?` instead of accepting its suggestions in order to emphasize +there is no need to remember those lemma names. +-/ + +-- If `u` tends to `l` and `v` tends `l'` then `u+v` tends to `l+l'` +example (hu : seq_limit u l) (hv : seq_limit v l') : + seq_limit (u + v) (l + l') := by { + intros ε ε_pos + rcases hu (ε/2) (by apply?) with ⟨N₁, hN₁⟩ + rcases hv (ε/2) (by apply?) with ⟨N₂, hN₂⟩ + use max N₁ N₂ + intros n hn + rw [ge_max_iff] at hn -- Note how hn changes from `n ≥ max N₁ N₂` to `n ≥ N₁ ∧ n ≥ N₂` + specialize hN₁ n hn.1 + specialize hN₂ n hn.2 + calc + |(u + v) n - (l + l')| = |u n + v n - (l + l')| := by simp + _ = |(u n - l) + (v n - l')| := by congr; ring + _ ≤ |u n - l| + |v n - l'| := by apply? + _ ≤ ε/2 + ε/2 := by gcongr + _ = ε := by simp +} + + +/- Let's do something similar: the squeezing theorem using both `ge_max_iff` and `abs_le`. +You will probably want to rewrite using `abs_le` in several assumptions as well as in the +goal. You can use `rw [abs_le] at *` for this. -/ +example (hu : seq_limit u l) (hw : seq_limit w l) (h : ∀ n, u n ≤ v n) (h' : ∀ n, v n ≤ w n) : + seq_limit v l := by { + -- sorry + intros ε ε_pos + rcases hu ε ε_pos with ⟨N, hN⟩ + rcases hw ε ε_pos with ⟨N', hN'⟩ + use max N N' + intros n hn + rw [ge_max_iff] at hn + specialize hN n hn.1 + specialize hN' n hn.2 + specialize h n + specialize h' n + rw [abs_le] at * + constructor + calc + -ε ≤ u n - l := by apply hN.1 + _ ≤ v n - l := by gcongr + calc + v n - l ≤ w n - l := by gcongr + _ ≤ ε := by apply hN'.2 + -- sorry +} + + +/- In the next exercise, we'll use + +`eq_of_abs_sub_le_all (x y : ℝ) : (∀ ε > 0, |x - y| ≤ ε) → x = y` + +as the first step. +-/ + +-- A sequence admits at most one limit. You will be able to use that lemma in the following +-- exercises. +lemma uniq_limit (hl : seq_limit u l) (hl' : seq_limit u l') : l = l' := by { + apply eq_of_abs_sub_le_all + -- sorry + intros ε ε_pos + rcases hl (ε/2) (by apply?) with ⟨N, hN⟩ + rcases hl' (ε/2) (by apply?) with ⟨N', hN'⟩ + calc + |l - l'| ≤ |l - u (max N N')| + |u (max N N') - l'| := by apply? + _ = |u (max N N') - l| + |u (max N N') - l'| := by congr 1; apply? + _ ≤ ε/2 + ε/2 := by gcongr; apply hN; apply?; apply hN'; apply? + _ = ε := by simp + -- sorry +} + +/- +## Conjunctions + +In order to prove more things about sequences of real number, we now explain how to +handle one more logical gadget: conjunction. + +Given two statements `P` and `Q`, the conjunction `P ∧ Q` is the statement that +`P` and `Q` are both true (`∧` is sometimes called the “logical and”). + +In order to prove `P ∧ Q` we use the `constructor` tactic that splits the goal +into proving `P` and then proving `Q`. + +In order to use a proof `h` of `P ∧ Q`, we use `h.1` to get a proof of `P` +and `h.2` to get a proof of `Q`. We can also use `rcases h with ⟨hP, hQ⟩` to +get `hP : P` and `hQ : Q`. + +Let us see both in action in a very basic logic proof: let us deduce `Q ∧ P` +from `P ∧ Q`. +-/ + +example (P Q : Prop) (h : P ∧ Q) : Q ∧ P := by { + constructor + apply h.2 + apply h.1 +} + +/- + +## Subsequences + +We will now play with subsequences. + +The new definition we will use is that `φ : ℕ → ℕ` is an extraction +if it is (strictly) increasing. +-/ + +def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m + +/- +In the following, `φ` will always denote a function from `ℕ` to `ℕ`. + +The next lemma is proved by an easy induction, but we haven't seen induction +in this tutorial. If you did the natural number game then you can delete +the proof below and try to reconstruct it. Otherwise you can simply take a quick look +at how proofs by induction look like (but we won’t need any other one here). +-/ +/-- An extraction is greater than id -/ +lemma id_le_extraction' : extraction φ → ∀ n, n ≤ φ n := by { + intros hyp n + induction n with + | zero => apply? + | succ n ih => exact Nat.succ_le_of_lt (by + calc n ≤ φ n := ih + _ < φ (n + 1) := by apply hyp; apply?) +} + +/- +In the exercise, we use `∃ n ≥ N, ...` which is the abbreviation of +`∃ n, n ≥ N ∧ ...`. + +Don’t forget to move the cursor around to see what each `apply?` is proving. +-/ + +/-- Extractions take arbitrarily large values for arbitrarily large +inputs. -/ +lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by { + -- sorry + intro h N N' + use max N N' + constructor + apply? + calc + N ≤ max N N' := by apply? + _ ≤ φ (max N N') := by apply? + -- sorry +} + +/-- A real number `a` is a cluster point of a sequence `u` +if `u` has a subsequence converging to `a`. -/ +def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a + +/-- If `a` is a cluster point of `u` then there are values of +`u` arbitrarily close to `a` for arbitrarily large input. -/ +lemma near_cluster : + cluster_point u a → ∀ ε > 0, ∀ N, ∃ n ≥ N, |u n - a| ≤ ε := by { + -- sorry + intro hyp ε ε_pos N + rcases hyp with ⟨φ, φ_extr, hφ⟩ + rcases hφ ε ε_pos with ⟨N', hN'⟩ + rcases extraction_ge φ_extr N N' with ⟨q, hq, hq'⟩ + use φ q + constructor + apply hq' + apply hN' _ hq + -- sorry +} + + +/-- If `u` tends to `l` then its subsequences tend to `l`. -/ +lemma subseq_tendsto_of_tendsto' (h : seq_limit u l) (hφ : extraction φ) : +seq_limit (u ∘ φ) l := by { + -- sorry + intro ε ε_pos + rcases h ε ε_pos with ⟨N, hN⟩ + use N + intro n hn + apply hN + calc + N ≤ n := by apply? + _ ≤ φ n := id_le_extraction' hφ n + -- sorry +} + +/-- If `u` tends to `l` all its cluster points are equal to `l`. -/ +lemma cluster_limit (hl : seq_limit u l) (ha : cluster_point u a) : a = l := by { + -- sorry + rcases ha with ⟨φ, φ_extr, lim_u_φ⟩ + apply uniq_limit + apply lim_u_φ + apply? + -- sorry +} + +/-- `u` is a Cauchy sequence -/ +def CauchySequence (u : ℕ → ℝ) := + ∀ ε > 0, ∃ N, ∀ p q, p ≥ N → q ≥ N → |u p - u q| ≤ ε + +example : (∃ l, seq_limit u l) → CauchySequence u := by { + -- sorry + intro hyp + rcases hyp with ⟨l, hl⟩ + intro ε ε_pos + rcases hl (ε / 2) (by apply?) with ⟨N, hN⟩ + use N + intro p q hp hq + calc + |u p - u q| = |u p - l + (l - u q)| := by congr; ring + _ ≤ |u p - l| + |l - u q| := by apply? + _ = |u p - l| + |u q - l| := by congr 1; apply? + _ ≤ ε/2 + ε/2 := by gcongr; apply?; apply? + _ = ε := by simp + -- sorry +} + diff --git a/GlimpseOfLean/Solutions/Topics/SequenceLimits.lean b/GlimpseOfLean/Solutions/Topics/SequenceLimits.lean index a263cb5..6a13239 100644 --- a/GlimpseOfLean/Solutions/Topics/SequenceLimits.lean +++ b/GlimpseOfLean/Solutions/Topics/SequenceLimits.lean @@ -1,5 +1,7 @@ import GlimpseOfLean.Library.Basic +namespace Topics + /- In this file we manipulate the elementary definition of limits of sequences of real numbers. @@ -37,10 +39,12 @@ example (a b c d : ℝ) (hab : a ≤ b) (hcd : c ≤ d) : a + c ≤ b + d := by A sequence `u` is a function from `ℕ` to `ℝ`, hence Lean says `u : ℕ → ℝ` The definition we'll be using is: +-/ --- Definition of « u tends to l » -`def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε` +/-- Definition of « u tends to l » -/ +def seq_limit (u : ℕ → ℝ) (l : ℝ) := ∀ ε > 0, ∃ N, ∀ n ≥ N, |u n - l| ≤ ε +/- Note the use of `∀ ε > 0, _` which is an abbreviation of `∀ ε, ε > 0 → _ ` @@ -187,7 +191,7 @@ Recall we listed three variations on the triangle inequality at the beginning of -- A sequence admits at most one limit. You will be able to use that lemma in the following -- exercises. -lemma uniq_limit : seq_limit u l → seq_limit u l' → l = l' := by { +lemma unique_limit : seq_limit u l → seq_limit u l' → l = l' := by { -- sorry intros hl hl' apply eq_of_abs_sub_le_all @@ -229,9 +233,11 @@ We will now play with subsequences. The new definition we will use is that `φ : ℕ → ℕ` is an extraction if it is (strictly) increasing. +-/ -`def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m` +def extraction (φ : ℕ → ℕ) := ∀ n m, n < m → φ n < φ m +/- In the following, `φ` will always denote a function from `ℕ` to `ℕ`. The next lemma is proved by an easy induction, but we haven't seen induction @@ -268,10 +274,9 @@ lemma extraction_ge : extraction φ → ∀ N N', ∃ n ≥ N', φ n ≥ N := by /- A real number `a` is a cluster point of a sequence `u` if `u` has a subsequence converging to `a`. - -`def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a` -/ +def cluster_point (u : ℕ → ℝ) (a : ℝ) := ∃ φ, extraction φ ∧ seq_limit (u ∘ φ) a /-- If `a` is a cluster point of `u` then there are values of `u` arbitrarily close to `a` for arbitrarily large input. -/ diff --git a/README.md b/README.md index b1dda16..15009a4 100644 --- a/README.md +++ b/README.md @@ -1,12 +1,22 @@ # A glimpse of Lean This repository is an introduction to theorem proving in Lean for the impatient. -The goal is to get a feel for what proving in Lean looks like in 2 or 3 hours. -After reading the `Introduction.lean` file, you should read explanations and do exercises in the -`Basics` folder, and then choose to work on one file from the `Topics` folder. -Of course you can play with all files from that folder if you have more time. +The goal is to get a feel for what proving in Lean looks like in 2 or 3 hours, +or maybe devote half a day or a full day. -To work using Lean, you either have to install Lean locally, use Codespaces or use Gitpod. +There are two tracks. Both start with reading the `Introduction.lean` file. + +Then the short track continues in the `Shorter.lean` file which is meant to give +you access to not completely empty mathematical proofs in two hours if you are +ready to move really fast. + +If you have a bit more time, you should instead read explanations and do +exercises in the `Basics` folder, and then choose to work on one file from the +`Topics` folder. Of course you can play with all files from that folder if you +have even more time. + +To work using Lean, you either have to install Lean locally, or use a lean4web +server, or use Codespaces or use Gitpod. * To use codespaces, make sure you're logged in to Github, click the button below, select `4-core`, and then press `Create codespace`. After a few minutes an editor with Lean working will open in your browser.