Minor refactor of the Section03functions/Sheet1 #5
Conversation
|
|
||
| -- Lean is a dependently-typed language | ||
| -- Every expression has a type, and `#check` can tell you the type | ||
|
|
There was a problem hiding this comment.
These newline removals aren't important but this file is already pretty long imo and sticking comments clearly to the blocks they're describing feels a tiny bit better to me. This also matches how the rest of the file is laid out. Totally not critical though
|
|
||
| def MyDifficultProposition : Prop := ∀ n : ℕ, ∃ p, n ≤ p ∧ Prime p ∧ Prime (p + 2) | ||
| def MyEasyProposition : Prop := ∀ n : ℕ, ∃ p, n ≤ p ∧ Prime p ∧ Prime (p + 2) ∧ Prime (p + 4) | ||
| def MyVeryEasyProposition : Prop := ∀ n : ℕ, ∃ p, n ≤ p |
There was a problem hiding this comment.
I moved MyVeryEasyProposition below, see why below.
|
|
||
| example (n : ℕ) (hn : 2 ≤ n) : | ||
| ∃ x y z : ℕ, 4 * x * y * z = n * (x * y + x * z + y * z) := sorry | ||
| -- Erdős-Strauss conjecture. We're not going to prove it now (unless you know how?) |
There was a problem hiding this comment.
More clearly motivate the reader isn't supposed to fill in the sorry (it was supposed to be filled out in the previous chapters)
| -- Erdős-Strauss conjecture | ||
|
|
||
| example (n : ℕ) (hn : 2 ≤ n) : | ||
| ∃ x y z : ℕ, 4 * x * y * z = n * (x * y + x * z + y * z) := sorry |
There was a problem hiding this comment.
I don't understand what this example tries to convey that isn't already conveyed earlier. (Also unsure why it's also unproven.) Maybe it demonstrates accepting parameters? But that isn't a specific feature of proofs per se. Maybe could be explained earlier separately? Anyway I felt this is distracting from the most important point below so I dropped it
| theorem my_proof : MyVeryEasyProposition := fun n => ⟨n, le_rfl⟩ | ||
|
|
||
| def MyVeryEasyProposition : Prop := 2 = 2 | ||
| def my_proof : MyVeryEasyProposition := rfl |
There was a problem hiding this comment.
I moved MyVeryEasyProposition here so that I don't have to scroll or mentally jump up to look it up.
I also simplified the proposition itself to be a much simpler one that we've just seen. We're introducing the most important idea here (proofs are of types of their propositions), and I think having any amount of extra complexity here is detracting from the point. In the original example, the first switch to theorem syntax (we've not seen it in this file before), the fun syntax (we've never seen it before), the ⟨ ⟩ syntax (we've never seen it before), and le_rfl (we don't know what this is) all feel to me like they're detracting from the key point we want to convey.
I think it doesn't hurt to readd this example later below again if we want to but it didn't seem essential to me. The examples already below seem to already tie the story more nicely imo.
| -- my proof "has type my proposition", or "has type 2 = 2", or "is a proof of 2 = 2" | ||
|
|
||
| -- But just proof terms get ugly... | ||
| example (a b : ℕ) : a + a * b = (b + 1) * a := |
There was a problem hiding this comment.
Now by this point I think we have the story flowing nicely:
- First, we've shown expressions have types
- Then we taught to give them names via
def - Then we taught propositions are of type
Prop - Then we taught that proofs are of type of their propositions
- Then we taught that it's easier to write proof via
byand tactics
Each concept builds on the other, each step is introduced on its own with no sudden jumps introducing two things at once.
|
If something like this is merged in, the mirrored file in the Solutions folder will need to be updated respectively. It seems to have drifted a bit already so I didn't touch it. |
1 participant
This may be rather opinionated so I figured I'd throw this in to see if our tastes align.
I'll motivate the changes as inline comments on the PR.