Minor TPiL4 doc suggestion

Stream: lean4

[Tom]

In Chapter 3, in the section "Working with Propositions as Types" there is the following:

"This looks exactly like the definition of the constant function in the last chapter, ..."

Based on the type, I think it's trying to draw a parallel with something like the const function e.g. in Haskell, however I don't see any mention of a similar const function in Ch 2 of TPiL. I looked at the version for Lean 3 and it seems that perhaps this sentence is a mistake/leftover from that?

Thanks.

[Alastair Horn]

I believe it's referring to this part of chapter 2: "the expression fun x : Nat => true denotes the constant function that always returns true"

[Tom]

I spotted that too but discarded it because the type of that function is Nat -> Bool, unlike the theorem in the section I'm referring to: theorem t1 : p → q → p := fun hp : p => fun hq : q => hp.
That's why I'm wondering if it's referring to a const function defined as def const (a: p) (b: q): p := a, ie with the type p -> q -> p (and note that if you remove the function definition sugar, you end up with the same "computable" version of the theorem)
Conceptually, that makes sense as an example/comparison. The const function is now making the "same" statement as the theorem, i.e. if you give me a p, I don't care/can ignore q.

[Dan Velleman]

Yes, this sentence is poorly worded. I think the problem is that in the phrase "This looks exactly like ...," it is unclear what "this" refers to. There are actually two function definitions here--one introduced by fun hp : p and one introduced by fun hq : q. The second function is the return value of the first function. It is the second function definition that "looks exactly like the definition of the constant function in the last chapter." The second definition is fun hq : q => hp, and I think the point they are trying to make is that the return value of this function, hp, doesn't depend on the input to the function, hq. That's what makes it look like a constant function: the function takes the input hq, ignores it, and returns hp no matter what hq is.

[Tom]

Good point. Btw, I am happy to submit a documentation PR if someone steps in and tells me what the original intent is/was.

[Jeremy Avigad]

I don't remember what the original intent was; I am guessing that it was just a mistake. I'll fix it.

[Jeremy Avigad]

Done. Thanks for pointing this out.

On running the tests, I noticed that the following conv proof is now broken:

example (a b c : Nat) : a * (b * c) = a * (c * b) := by
  conv =>
    -- |- a * (b * c) = a * (c * b)
    lhs
    -- |- a * (b * c)
    congr
    -- 2 goals : |- a and |- b * c
    rfl
    -- |- b * c
    rw [Nat.mul_comm]

I think this is a Lean 4 bug. I can open an issue if that would be helpful.