Transparent definition for tactics

Stream: mathlib4

[Klaus Gy]

I mentioned this already in another discussion, but I want to reformulate it here as a proper proposal.

let definitions don’t automatically unfold for simp (and probably other tactics). Would it be possible to have a tactic similar to let, but creating more transparent terms that don’t need unfolding in subsequent proofs?

def test : Nat :=
  let x := 3
  let y := 3
  -- unfolding is necessary for simp
  have : x = y := by unfold x y; simp
  -- this works fine
  have : 3 = 3 := by simp
  1

Of course, in this simple example I could just write rfl instead of by unfold x y; simp. But in more complex proofs, I often run into situations where I want to abbreviate a term T that appears repeatedly. After introducing let x := T and replacing T with x subsequently, some tactics stop working and I need to insert unfold t (or similar fixes). This feels unintuitive to me, both as a programmer and as a mathematician, since introducing local helper terms to clean up code or proofs is such a common practice and should work with minimal friction.

So I wonder: would it be technically possible to introduce a tactic alongside let, e.g. abbrev, that can be used inside proof contexts to create fully transparent abbreviations, working as drop-in replacements without breaking tactics or other proof details?

[Kevin Buzzard]

Try using letI in your actual example. This example above is a bit contrived because simp doesn't actually do anything; the reason the goal is closed is that after simp runs its simplification algorithm it tries rfl but only at some kind of reducible transparency, and letI doesn't help here. But it might help in your actual example.

[Aaron Liu]

Kevin Buzzard said:

This example above is a bit contrived because simp doesn't actually do anything; the reason the goal is closed is that after simp runs its simplification algorithm it tries rfl but only at some kind of reducible transparency, and letI doesn't help here. But it might help in your actual example.

what do you mean by this?

[Kevin Buzzard]

I'm saying that the issue isn't that let isn't unfolding for simp, it's let not unfolding for with_reducible rfl; letI unfolds more than let(doesn't it?) so maybe the OP will have more luck with letI when using the "other tactics".

[Aaron Liu]

Kevin Buzzard said:

letI unfolds more than let(doesn't it?)

it's the same within in the body, letI only differs from let once you finish elaborating the body of the let

[Aaron Liu]

Kevin Buzzard said:

I'm saying that the issue isn't that let isn't unfolding for simp, it's let not unfolding for with_reducible rfl

with_reducible rfl seems to be doing fine

def test : Nat :=
  let x := 3
  let y := 3
  -- unfolding is not necessary for rfl
  have : x = y := by with_reducible rfl
  -- this works fine
  have : 3 = 3 := by simp
  1

[Robin Arnez]

You might want simp +zetaDelta:

def test : Nat :=
  let x := 3
  let y := 3
  have : x = y := by simp +zetaDelta
  have : 3 = 3 := by simp
  1

[Kyle Miller]

You can also tell simp to unfold specific let variables using simp [x, y].

[Artie Khovanov]

nevertheless I think it would be convenient to have notation for long terms in tactic mode

[Kyle Miller]

It would be a relatively large and delicate change to add transparency to let declarations, and it would affect all basic Lean systems.

The alternative is making metavariables instead. These are completely transparent. It's possible to conveniently create them using a secret internal notation:

def test : Nat :=
  let_mvar% ?x := 3;
  let_mvar% ?y := 3;
  have : ?x = ?y := by
    -- ⊢ 3 = 3
    rfl
  1

It's not a tactic though, just a term. The semicolon is necessary.

[Klaus Gy]

@Kyle Miller thank you, that's what i was looking for! And Thanks @Robin Arnez , +zetaDelta is also a very nice trick I didn't know!