have vs let

Stream: lean4

[Tom]

Chapter 3 of TPIL, in the section "Introducing Auxiliary Subgoals" mentions that

"internally, the expression have h : p := s; t produces the term (fun (h : p) => t) s."

However, earlier in the book, it's mentioned that let is strictly more powerful from a type inference point of view. What's the reasoning for this rewrite to a lambda application rather than a let binding?

Thanks!

[Sebastian Ullrich]

let is more powerful because it makes the value s available while checking t. have is meant to be used for proofs, which are irrelevant, so the specific s does not matter.

[Tom]

Hi Sebastian,

I am sure I understand your explanation yet.

Is your point that the h in have h: s always has to be a term (value) of type Prop (and not some higher Sort), and hence dependent types don't come into play (hence the distinction/type checking advantages will not ultimately matter?)

During my reading of TPiL, I have always been able to use let wherever I've seen have and as such, I've only viewed the distinction as purely a proof readability/convention tool. Is there something more to it? Is there something about let which makes the implementation of e.g. proof irrelevance more difficult?

Thanks.

[Kevin Buzzard]

Props can be dependent types, e.g. forall a, a+a=2*a.

[Kevin Buzzard]

The difference between let and have is that let remembers the definition of the term, and have just remembers the type. So for example after have a : Nat := 3, you'll find that a = 3 is unprovable. But with let it'll be rfl.

[Tom]

Thank you, Kevin; I think you are referring to the proof irrelevance that Sebastian mentioned, correct?
I'll think about this some more and come back once I've had the chance to explore the internals a bit more; I'll either be able to articulate my question better or will have answered my own question.