Tactic(s) to automate unfolding

Stream: new members

[Mark Fischer]

I'm finding that whenever I want to prove anything using constants that I've defined earlier, I end up needing to manually unfold them. It's not a big deal though it makes me wonder if there are tactics that just do the rote work for me.

Here's an example I'm trying to clean up a bit.

import Mathlib

def declSize : (x : ℕ) × { y : ℕ // x = y ^ 2 } := ⟨9, 3, rfl⟩
def size : ℕ := declSize.fst

def box_idxs (n : ℕ) : Finset ℕ :=
  let root := declSize.snd.val
  let offset := n / root * root * size + (n % root) * root
  let mbed : ℕ ↪ ℕ := {
    toFun := λi ↦
      let r := i / root
      let c := i % root
      offset + size * r + c
    inj' := by
      intro a b eq
      -- Unfold all relevant constants in eq
      simp only [root] at eq
      unfold size at eq
      unfold declSize at eq
      ----------------------
      simp only at eq
      omega
  }
  .map mbed <| .range size

[Paul Rowe]

If you use abbrev instead of def for your constants, does that give you what you want?

[Patrick Massot]

Can’t you do it in one step as simp only [root, size, declSize] at eq?

[Patrick Massot]

You can also use the simp configuration to unfold lets, but of course there is no configuration option to unfold all global definitions since this would be a disaster (in your case it would unfold the definition of subtypes and of powers for instance).

[Kevin Cheung]

abbrev is such a useful thing that is hardly mentioned in the few books that I have read so far. Thanks for mentioning it.

[Mark Fischer]

In my case, most of the time I don't need Lean to unfold the definitions, so abbrev feels aggressive. Though notably, none of my definitions are likely to bloat term/slow compilation much, so it's probably more just my learning journey.