## Stream: general

### Topic: What tactic forces beta reduction in goal or hypothesis

#### 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?

#### 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.

#### 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


#### 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.

#### 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.

#### Patrick Massot (Oct 10 2018 at 13:45):

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

#### 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.

Hold on

#### 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


#### Patrick Massot (Oct 10 2018 at 13:56):

and probably set other config flag to false

#### Patrick Massot (Oct 10 2018 at 13:56):

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

#### 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