What tactic forces beta reduction in goal or hypothesis

Stream: general

[Kevin Sullivan]

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]

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]

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]

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]

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]

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

[Kevin Sullivan]

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.

[Patrick Massot]

Hold on

[Patrick Massot]

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]

and probably set other config flag to false

[Patrick Massot]

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

[Kevin Buzzard]

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