Infix operators/notation not explained before being used at
-- notation, :: is infix for cons
4.3.5. Exercises
Phrasing it as "values greater than 0" may make this proof trickier since Lean's contradiction tactic does not automatically detect 0 > 0 as a contradiction whereas it does detect 0 ≠ 0
Need to use something like gt_irrefl for the function what I can tell which is not something we've talked about . Likewise creating proofs to give the function requires something like nat.le_succ_of_le
4.4.8. Exercises
The map-reduce is a substantial step up from the other exercises. I think it might be better to either remove this one or change it to something that's a little easier to do
4.5. Recursive Proofs
Typo in this paragraph
provide a concrete and pecific example of this reasoning and how we can automate it using tools we already have, concluding what is called the induction axiom for natural numbers (arguments to P);
4.5.1.3. Summary: Proof by Induction
I think the code about factorials was mistakenly placed here or missing an explanation around it
4.5
Proofs about (+) and (*) are often hard to follow in lean due to using not using the kinds of infix operators that we're used to seeing. It might be very helpful to provide comments on each line to show the goal in terms of infix operators
I think it would be good to give some guidance for the mul_distrib_add_nat_left exercise as this was fairly tricky to figure out especially since it's not clear at first what the simp tactic recognizes for nat.add and what it does not
For the foldr' definition here, I think it might make more sense to use id instead of e here for the pattern matching. Using e is explained later in chapter 5, but isn't yet explained here
def foldr' {α : Type} : @monoid α → list α → α
| (monoid.mk op e _ _) l := foldr op e l
Chapter 4
4.3.2
Infix operators/notation not explained before being used at
4.3.5. Exercises
Phrasing it as "values greater than 0" may make this proof trickier since Lean's contradiction tactic does not automatically detect
0 > 0as a contradiction whereas it does detect0 ≠ 0Need to use something like
gt_irreflfor the function what I can tell which is not something we've talked about . Likewise creating proofs to give the function requires something likenat.le_succ_of_le4.4.8. Exercises
The
map-reduceis a substantial step up from the other exercises. I think it might be better to either remove this one or change it to something that's a little easier to do4.5. Recursive Proofs
Typo in this paragraph
4.5.1.3. Summary: Proof by Induction
I think the code about factorials was mistakenly placed here or missing an explanation around it
4.5
Proofs about (+) and (*) are often hard to follow in lean due to using not using the kinds of infix operators that we're used to seeing. It might be very helpful to provide comments on each line to show the goal in terms of infix operators
I think it would be good to give some guidance for the mul_distrib_add_nat_left exercise as this was fairly tricky to figure out especially since it's not clear at first what the
simptactic recognizes for nat.add and what it does notFor the
foldr'definition here, I think it might make more sense to useidinstead ofehere for the pattern matching. Usingeis explained later in chapter 5, but isn't yet explained here4.5.3. Inductive Families
Still shows the coming soon text here