beta reduction

Stream: Lean for teaching

[Alexandre Rademaker]

I am teaching algorithms design with Lean. We can prove simple theorems and basically reduce step by step definitions with unfold and rewrite. But when I reach terms that can be beta reduced, simp and rw finish the proof. Is there any tactic to apply one beta reduction?

[Matthew Ballard]

For head beta, beta% is a term elaborator

[Shreyas Srinivas]

Do you have a course webpage?

[Matthew Ballard]

You can also turn off beta (and other reductions) in docs#Lean.Meta.Simp.Config if you want to intentional about the steps but still use simp.

[Alexandre Rademaker]

Hi @Shreyas Srinivas , I am working on it. For now, https://github.com/emap-ed-20242/syllabus. I am basically trying to follow https://www.amazon.com/Algorithm-Design-Haskell-Richard-Bird/dp/1108491618. But I also found this nice book implemented in Isabelle (https://functional-algorithms-verified.org/).

[Alexandre Rademaker]

Hi @Matthew Ballard , I want to show one beta reduction at a time, that is my point. simp is not needed, rfl is enough or rw. I didn't find the beta%

[Matthew Ballard]

docs#elabBeta

[Chris Bailey]

There's also a beta reduction gadget for conv mode in mathlib:

import Mathlib.Tactic

example : ((fun (x y z : Nat) => id y) 0 1 2) = 1 := by
  conv =>
    beta_reduce
    trace_state -- id 1 = 1
  sorry

But if there are multiple arguments they'll all get applied.

[Kyle Miller]

@Chris Bailey There's also a beta_reduce tactic

[Chris Bailey]

Even better.

[Kyle Miller]

@Alexandre Rademaker You can use the rewrite tactic rather than rw. The rw tactic is basically rewrite [...]; try rfl

[Kyle Miller]

@Matthew Ballard I'm not sure how beta% would help here? The point is to try to do beta reduction in a target, not beta reduce during elaboration.

[Kyle Miller]

If you want tight control over your reductions, I think the clearest thing would be to do change with explicitly what you want to transform it to, since there's not really a tactic that does single beta reductions. However, I suppose you could use conv to navigate to a term and then use a custom version of beta_reduce that does just a single beta reduction at the head.

[Matthew Ballard]

Oh, I read that as working forward from a term to a goal and not backwards on the goal.

[Alexandre Rademaker]

I turns out that with more control in the rewrite solves my problem! Using the example below I could perfectly illustrate how foldr works:

example : foldr Nat.add 0 [1,2,3] = 6 := by
  unfold foldr
  unfold foldr
  unfold foldr
  unfold foldr
  rewrite (config := {occs := .pos [3]}) [Nat.add]
  rewrite (config := {occs := .pos [2]}) [Nat.add]
  rewrite (config := {occs := .pos [1]}) [Nat.add]
  rfl

[Alexandre Rademaker]

If I use (· + ·) instead of Nat.add than I would need the beta reduction control.. right?