Zulip Chat Archive

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?

Mario Carneiro (Feb 14 2020 at 01:27):

  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: Dec 20 2023 at 11:08 UTC