How does `let` work?

Stream: general

[Dan Velleman]

I'm trying to figure out how let works. Consider the following silly example:

example : nat.prime 5 :=
begin
let P := {n : nat | nat.prime n},
have h : 5 ∈ P,
end

At this point, the immediate goal is 5 ∈ P. If I use dsimp, then this goal is translated into nat.prime 5, so the information about what P stands for must be stored somewhere that is available to dsimp, but I can't figure out where it is. It seems like it is a definition, but changing dsimp to unfold P doesn't work. I thought the definition must be stored as a declaration in the environment, but I've searched for it there and I can't find it. Where is dsimp getting the information from?

[Adam Topaz]

If you look at your goal state, you should see P : set nat := ...

[Dan Velleman]

Yes, I see that. My problem is that I'm trying to write a tactic that accesses that information. If I use tactic.local_context, the only thing I can find there is that P has type set nat. How do I find out what it is defined to be equal to?

[Adam Topaz]

Ah, I see... You might want to look at how let and/or set is implemented.
It may also be worthwhile to ask this question in the #metaprogramming / tactics stream.

[Dan Velleman]

Oh, I may have found it. I think I have to call tactic.local_defs, not tactic.local_context.

[Adam Topaz]

Here's the code for the tactic set (which is similar to let):
https://github.com/leanprover-community/mathlib/blob/199e8ca8f03a76351168456183a9a25cd851b272/src/tactic/interactive.lean#L801

[Dan Velleman]

No, tactic.local_defs doesn't do it. It just returns a list of the expressions that have definitions--in my case, that's just P--but not what the definitions actually are.

[Jannis Limperg]

docs#tactic.local_def_value should be it. This stuff is indeed well hidden in the stdlib (for no particular reason afaik).

[Dan Velleman]

Thanks. Yes, I think that's what I was looking for.

[Dan Velleman]

OK, tactic.local_def_value does what I wanted. But now I'm still wondering why unfold P doesn't work. It looks to me like unfold looks for definitions in the environment, but not in the local context. Wouldn't it make sense for it to look in the local context as well?

[Kevin Buzzard]

Does delta P work?

[Dan Velleman]

delta P gives the error message unknown declaration 'P'.

[Kevin Buzzard]

You can just use changein tactic mode to make the substitution; I don't know of any other way. I always use set not let because then I have the hypothesis to rewrite with. I'm aware this is not answering your question though

[Mario Carneiro]

simp and dsimp support unfolding lets, so you can use dsimp only [P] in lieu of unfold P

[Mario Carneiro]

they are the only definition unfolding tactics that know about let decls