Zulip Chat Archive

Stream: general

Topic: How does `let` work?


Dan Velleman (Feb 14 2022 at 17:29):

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 (Feb 14 2022 at 17:32):

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

Dan Velleman (Feb 14 2022 at 17:35):

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 (Feb 14 2022 at 17:36):

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 (Feb 14 2022 at 17:36):

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

Adam Topaz (Feb 14 2022 at 17:39):

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 (Feb 14 2022 at 17:45):

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 (Feb 14 2022 at 17:49):

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

Dan Velleman (Feb 14 2022 at 17:50):

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

Dan Velleman (Feb 14 2022 at 19:11):

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 (Feb 14 2022 at 21:30):

Does delta P work?

Dan Velleman (Feb 14 2022 at 23:12):

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

Kevin Buzzard (Feb 14 2022 at 23:33):

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 (Feb 14 2022 at 23:42):

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

Mario Carneiro (Feb 14 2022 at 23:43):

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


Last updated: Dec 20 2023 at 11:08 UTC