## Stream: general

### Topic: Let assumptions in theorems

#### Jason Rute (Feb 13 2020 at 23:58):

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?

1. no

#### Mario Carneiro (Feb 14 2020 at 01:30):

1. 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 (Feb 14 2020 at 09:53):

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 (Feb 14 2020 at 17:50):

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 (Feb 14 2020 at 17:50):

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

#### Edward Ayers (Feb 14 2020 at 20:12):

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.

Last updated: Aug 03 2023 at 10:10 UTC