Let assumptions in theorems

Stream: general

[Jason Rute]

Consider the following partial proof:

example : let x := 0 in x = 0 := begin intro, end

If I put the curser right before end the goal is

x : ℕ := 0
⊢ x = 0

I tried to enter that into Lean as follows:

example (x : ℕ := 0) : x = 0 := begin end

However, I get a different goal (which is neither equivalent nor even true).

x : opt_param ℕ 0
⊢ x = 0

My questions:

1. Is there a way to enter the goal x : ℕ := 0 ⊢ x = 0 into Lean with the x : ℕ := 0 on the left hand side?
2. Is there a way to tactic-programmatically know that x in the first example (in the context of the goal, after applying intro) is a let binder (or whatever the appropriate terminology is) and that 0 is the value assigned to x?

[Mario Carneiro]

1. no

[Mario Carneiro]

2. Mechanisms for this are limited, I don't recall any function to tell you the value directly. Perhaps 3.5 can improve this. A workaround is to revert the target hypothesis (and dependents), and check if the resulting goal is a pi (so it was a regular argument) or a let (so it was a let binder and you can access the value).

[Rob Lewis]

There was some functionality for dealing with things like 2. added in 3.5c (https://leanprover-community.github.io/mathlib_docs/core/init/meta/type_context.html). See also #1953.

[Floris van Doorn]

There is already a function local_def_value which follows Mario's suggestion. I will update #1953 soon to add some more tactics.

[Floris van Doorn]

@Edward Ayers Is there a difference between get_context and get_local_context in the type_context file?

[Edward Ayers]

Yes I should have put a docstring on get_context.

• get_context gets the local context that an mvar was defined in. For example, the list of entries above ⊢ in a goal state is the context for the goal metavariable.
• get_local_context gets the current local context of the type context. As well as each mvar having a local context, the type context itself carries a local context that can be modified. IIRC, when a type_context monad is run this will be the local context of the main goal (ie, the first mvar returned by get_goals.