Let, have, show and assume

Stream: lean4

[Artur Chakhvadze]

Hi! I just started learning Lean 4 and I cannot understand the precise semantics and differences between let, have, show and assume. I haven't found any reference that explains in detail. Can someone clarify this for me?

[Robert Maxton]

@Artur Chakhvadze
First, of those, only let can be used as a term; the rest are all only applicable in tactic mode.

let defines a variable (which can be a function or a type, since those are all 'first class' in Lean -- that is, you can compute on them.)

[Robert Maxton]

have is like let, but assumes you only care about the type, so it throws away the actual definition. This is mostly useful for Props where the definition is a proof, and all you really care about is that the Prop is inhabited and not which specific proof you used to inhabit it (proof-irrelevance).

[Julian Berman]

have can be used in term mode too:

example : 2 = 2 := have : true := rfl; rfl

[Robert Maxton]

... huh. I literally just tried that to double check and got errors
oh, whoops, I typo'd. Nevermind! Then yes, let and have can both be used in term-mode

[Julian Berman]

It looks like show works in term mode as well:

example : 2 = 2 := show 2 = 2 from Eq.refl 2

[Robert Maxton]

Ah, that's show ... from..., which is not the same as show. But I suppose that's a quibble.

[Julian Berman]

I think the important bit is less what mode they work in. I'd add obtain and rcases as others which are "kind of similar".

[Robert Maxton]

I'm actually typing up an explanation, but keep getting interrupted :v

[Julian Berman]

Oh I'll keep quiet then :) go for it.

[Robert Maxton]

show t looks for a goal that unifies with t, which means it looks for a goal whose type is compatible with t. If t is a complete term, that means it needs to have the same type as t; if t has holes (_s) or metavariables (like ?foo), it looks for a goal for which some substitution of the holes and metavariables could be the same type as t. It makes that the current active goal and replaces the statement of the goal with t, with as many holes and metavariables filled in as it can infer.

(There is a detail here I don't actually know, which is the precise transparency level show works on when unifying. I suspect it works up to reducibility, but it may only work up to definitional equality. For a good overview of the difference, see this post)

[Julian Berman]

(I said I'd be quiet :), but since I suspect there's a chance someone new doesn't know what a few of those words mean, I think a "simplified" version of what show does is is it expresses "I have some goal, but I think that goal is really equivalent to a different one, so I'm telling Lean I'm going to prove the other equivalent goal and that it should be happy with that".

The details of what "equivalent" and "should be happy with" are what Robert explained with more precise words.)

[Robert Maxton]

show p from t involves let_fun, which is a bit confusing (at least to me!) so I'm going to skim over the details; it essentially constructs a term of type p from the argument t. from means it's working in term mode, so t should be a 'function' (or theorem, which is just a function on Props) that returns something of type p.

Alternatively, you can use show p by t, which is equivalent to show p from by t but looks less silly; it moves into tactic mode and constructs a p by the tactic(s) t.

[Robert Maxton]

aaaand I don't think assume is actually a thing! At least, Lean doesn't recognize it and I don't see any hits for assume outside of comments in the github.

[Robert Maxton]

aight, done, you can correct me at well now :p

[Artur Chakhvadze]

Thanks a lot for explaining everything in such detail! It is a shame that the official documentation doesn't have a page with those explanations.

I think I saw assume in some Lean 3 snippets and it probably isn't a thing in Lean 4 anymore.

One last question I have -- why do two first examples typecheck and the last one with have shows an error?
image.png

[Robert Maxton]

One thing I do recommend is to get your own copy of Mathlib in VSCode and abuse the hell out of the hover feature; it lets gives you quick access to all the docstring comments, which are honestly the principal source of documentation in Lean and Mathlib

[Robert Maxton]

it also lets you go-to-definition in a pinch, tho that can be very dense

[Robert Maxton]

w.r.t. example: so, as a side note, there's the theorem rfl, which is a term of type ∀ {α : Sort u} {a : α}, a = a; and then there's the tactic rfl, which is a much stronger low-level tactic that will do quite a bit more. so most of the time you will probably want := by rfl instead of := rfl

Anyway that's kind of orthogonal to your actual question lol. I'm not entirely sure why that happens, but I can at least give you the first step:

[Robert Maxton]

So, details on show ... from ... after all: show p from t is sugar for ((fun this => t) this) : p; that is, it makes a constant function fun _ => t, calls it on a dummy value, and then asserts the output has type p. This expansion passes through a let_fun definition that I believe is also how top-level definitions and theorems are implemented under the hood; they're both defined in such a way that the unification/type inference system, which is pretty powerful in Lean, has a chance to compare the intended and actual results before the type checker has to do its final verification.

[Robert Maxton]

I had thought that have also went through let_fun like that, but maybe not? Or maybe I'm just barking up the wrong tree entirely

[Mario Carneiro]

Artur Chakhvadze said:

I think I saw assume in some Lean 3 snippets and it probably isn't a thing in Lean 4 anymore.

It's spelled intro now