Zulip Chat Archive

Stream: general

Topic: What tactic forces beta reduction in goal or hypothesis


view this post on Zulip Kevin Sullivan (Oct 10 2018 at 03:52):

Clearly a newbie question -- but I don't see the answer at hand. Sorry to have to ask. E.g., if my current goal is 3 * 3 -= 8, how, in a tactic script, do I force the * expression to be evaluated, yielding 9 = 8 as the new goal?

view this post on Zulip Simon Hudon (Oct 10 2018 at 03:54):

If you're dealing with number literals, use norm_num. It works whether you have large numbers or small ones. Reduction will get pretty slow.

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:13):

Because 3 * 3 = 9 is true by definition, if your goal is 3 * 3 = ... then in tactic mode you can change it to 9 = ... with the show tactic.

example (h : 9 = 8) : 3 * 3 = 8 :=
begin
  show 9 = 8,
  exact h,
end

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 06:14):

The funny thing is that this works too:

example (h : 9 = 8) : 3 * 3 = 8 :=
begin
  exact h,
end

because Lean is quite happy to treat 3 * 3 and 9 as equal objects when attempting to convince itself that the hypothesis really is equal to the goal.

view this post on Zulip Kevin Sullivan (Oct 10 2018 at 13:40):

The more general case is one where the current goal involves expressions in which functions are applied to arguments. I'm looking for the tactic that simplifies the goal by reducing all of the (or perhaps selected) function application expressions to values.

view this post on Zulip Patrick Massot (Oct 10 2018 at 13:45):

If you are ready to provide the new goal explicitly then change will do that

view this post on Zulip Kevin Sullivan (Oct 10 2018 at 13:51):

I was hoping to be able to just use a "simpl" (or whatever) tactic. Seems that Lean doesn't natively provide such a thing. I find that surprising.

view this post on Zulip Patrick Massot (Oct 10 2018 at 13:52):

Hold on

view this post on Zulip Patrick Massot (Oct 10 2018 at 13:56):

you could try something like:

meta def tactic.interactive.beta_red : tactic unit := `[dsimp only [] {beta := tt}]

example {α : Type*}  (a : α) : (λ x, x) a = a :=
begin
  beta_red,
  refl
end

view this post on Zulip Patrick Massot (Oct 10 2018 at 13:56):

and probably set other config flag to false

view this post on Zulip Patrick Massot (Oct 10 2018 at 13:56):

I think we already has the same discussion before (or a closely related one)

view this post on Zulip Kevin Buzzard (Oct 10 2018 at 20:22):

Maybe unfold is what you're looking for? Do you want to post an example of what you're trying to do?


Last updated: May 08 2021 at 05:14 UTC