Skip to content

Commit

Permalink
Fix some typos and a delaborator
Browse files Browse the repository at this point in the history
  • Loading branch information
PatrickMassot committed Nov 13, 2024
1 parent 685bca1 commit 0c1449c
Show file tree
Hide file tree
Showing 5 changed files with 28 additions and 18 deletions.
8 changes: 4 additions & 4 deletions GlimpseOfLean/Exercises/01Rewriting.lean
Original file line number Diff line number Diff line change
Expand Up @@ -31,8 +31,8 @@ example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by {
/- In the first example above, take a closer look at where Lean displays parentheses.
The `ring` tactic certainly knows about associativity of multiplication, but sometimes
it is useful to understand that binary operation really are binary and an expression like
`a*b*c` is read as `(a*b)*c` by Lean and the fact that is equal `a*(b*c)` is a lemma
that is used by the `ring` tactic when needed.
`a*b*c` is read as `(a*b)*c` by Lean and the fact that this is equal to `a*(b*c)` is a
lemma that is used by the `ring` tactic when needed.
-/


Expand Down Expand Up @@ -84,8 +84,8 @@ In the previous examples, we rewrote the goal using a local assumption. But we c
also use lemmas. For instance let us prove a lemma about exponentiation.
Since `ring` only knows how to prove things from the axioms of rings,
it doesn't know how to work with exponentiation.
For the following lemma, we will rewrite with the lemma
`exp_add x y` twice, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
For the following lemma, we will rewrite twice with the lemma
`exp_add x y`, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
-/
example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
rw [exp_add (a + b) c]
Expand Down
10 changes: 5 additions & 5 deletions GlimpseOfLean/Exercises/03Forall.lean
Original file line number Diff line number Diff line change
Expand Up @@ -59,10 +59,9 @@ example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f +
Tactics like `unfold`, `apply`, `exact`, `rfl` and `calc` will automatically unfold definitions.
You can test this by deleting the `unfold` lines in the above example.
Tactics like `rw`, `ring` and `linarith` will generally
not unfold definitions that appear in the goal.
Tactics like `rw` and `ring` will generally not unfold definitions that appear in the goal.
This is why the first computation line is necessary, although its proof is simply `rfl`.
Before that line, `rw hf x` won't find anything like `f (-x)` hence will give up.
Before that line, `rw [hf x]` won't find anything like `f (-x)` hence will give up.
The last line is not necessary however, since it only proves
something that is true by definition, and is not followed by a `rw`.
Expand Down Expand Up @@ -170,7 +169,7 @@ example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
/- # Finding lemmas
Lean's mathematical library contains many useful facts,
and remembering all of them my name is infeasible.
and remembering all of them by name is infeasible.
The following exercises teach you two such techniques.
* `simp` will simplify complicated expressions.
* `apply?` will find lemmas from the library.
Expand Down Expand Up @@ -200,7 +199,8 @@ You learned about tactics:
You now have a choice what to do next. There is one more basic file `04Exists`
about the existential quantifier and conjunctions. You can do that now,
or dive directly in one of the specialized files.
In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`.
In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`
(where `∧` is the symbol for conjunctions, aka the logical “and” operator).
You can start with specialized files in the `Topics` folder. You have choice between
* `ClassicalPropositionalLogic` (easier, logic) if you want to learn
Expand Down
10 changes: 10 additions & 0 deletions GlimpseOfLean/Library/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -96,3 +96,13 @@ lemma lowerBounds_range {α ι : Type _} [Preorder α] {s : ι → α} {x : α}
lemma upperBounds_range {α ι : Type _} [Preorder α] {s : ι → α} {x : α} :
x ∈ upperBounds (Set.range s) ↔ ∀ i, s i ≤ x :=
lowerBounds_range (α := OrderDual α)

open Lean PrettyPrinter Delaborator

@[delab app.Real.exp]
def my : Delab := do
let args := (← SubExpr.getExpr).getAppArgs
let stx ← delab args[0]!
let e := mkIdent `exp
`(term|$e $stx)

8 changes: 4 additions & 4 deletions GlimpseOfLean/Solutions/01Rewriting.lean
Original file line number Diff line number Diff line change
Expand Up @@ -33,8 +33,8 @@ example (a b : ℝ) : (a+b)^2 = a^2 + 2*a*b + b^2 := by {
/- In the first example above, take a closer look at where Lean displays parentheses.
The `ring` tactic certainly knows about associativity of multiplication, but sometimes
it is useful to understand that binary operation really are binary and an expression like
`a*b*c` is read as `(a*b)*c` by Lean and the fact that is equal `a*(b*c)` is a lemma
that is used by the `ring` tactic when needed.
`a*b*c` is read as `(a*b)*c` by Lean and the fact that this is equal to `a*(b*c)` is a
lemma that is used by the `ring` tactic when needed.
-/


Expand Down Expand Up @@ -89,8 +89,8 @@ In the previous examples, we rewrote the goal using a local assumption. But we c
also use lemmas. For instance let us prove a lemma about exponentiation.
Since `ring` only knows how to prove things from the axioms of rings,
it doesn't know how to work with exponentiation.
For the following lemma, we will rewrite with the lemma
`exp_add x y` twice, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
For the following lemma, we will rewrite twice with the lemma
`exp_add x y`, which is a proof that `exp(x+y) = exp(x) * exp(y)`.
-/
example (a b c : ℝ) : exp (a + b + c) = exp a * exp b * exp c := by {
rw [exp_add (a + b) c]
Expand Down
10 changes: 5 additions & 5 deletions GlimpseOfLean/Solutions/03Forall.lean
Original file line number Diff line number Diff line change
Expand Up @@ -59,10 +59,9 @@ example (f g : ℝ → ℝ) (hf : even_fun f) (hg : even_fun g) : even_fun (f +
Tactics like `unfold`, `apply`, `exact`, `rfl` and `calc` will automatically unfold definitions.
You can test this by deleting the `unfold` lines in the above example.
Tactics like `rw`, `ring` and `linarith` will generally
not unfold definitions that appear in the goal.
Tactics like `rw` and `ring` will generally not unfold definitions that appear in the goal.
This is why the first computation line is necessary, although its proof is simply `rfl`.
Before that line, `rw hf x` won't find anything like `f (-x)` hence will give up.
Before that line, `rw [hf x]` won't find anything like `f (-x)` hence will give up.
The last line is not necessary however, since it only proves
something that is true by definition, and is not followed by a `rw`.
Expand Down Expand Up @@ -179,7 +178,7 @@ example (f g : ℝ → ℝ) (hf : non_decreasing f) (hg : non_increasing g) :
/- # Finding lemmas
Lean's mathematical library contains many useful facts,
and remembering all of them my name is infeasible.
and remembering all of them by name is infeasible.
The following exercises teach you two such techniques.
* `simp` will simplify complicated expressions.
* `apply?` will find lemmas from the library.
Expand Down Expand Up @@ -215,7 +214,8 @@ You learned about tactics:
You now have a choice what to do next. There is one more basic file `04Exists`
about the existential quantifier and conjunctions. You can do that now,
or dive directly in one of the specialized files.
In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`.
In the latter case, you should come back to `04Exists` if you get stuck on anything with `∃`/`∧`
(where `∧` is the symbol for conjunctions, aka the logical “and” operator).
You can start with specialized files in the `Topics` folder. You have choice between
* `ClassicalPropositionalLogic` (easier, logic) if you want to learn
Expand Down

0 comments on commit 0c1449c

Please sign in to comment.