simplifying local terms introduced by `let`

Stream: general

[Ayhon]

If I have a local definition in a proposition, introduced by let like the following.

example(x : Int)
: let aux := if x >= 0 then x else -x
  aux = x.natAbs
:= by
  intro aux
  if h:x >= 0 then
    simp [h] at *
    sorry
  else
    sorry

How can I simplify aux in each branch of the if? Understandably, simp only works at the type level, but I would like to invoke it at the "value" level of the let definition.

[Sebastian Ullrich]

simp [h, aux] at *, assuming your Lean is sufficiently new

[Ayhon]

Sebastian Ullrich said:

simp [h, aux] at *, assuming your Lean is sufficiently new

That might be the problem then. I'm using 4.16.0-rc2

[Sebastian Ullrich]

It works with 4.17.0 in the playground

[Sebastian Ullrich]

unfold may be an alternative

[Ayhon]

But that would just substitute the definition of aux in my current goal or proposition I chose, no?

[Sebastian Ullrich]

Oh, you want to simplify the RHS of aux without substituting it?

[Ayhon]

Yes, indeed

[Ayhon]

I'm actually using these let definitions as a way of managing the readability of my proof state. So far I've found that using generalize x_def: rhs = x works for my use case, but it introduces two elements to my local context, x and x_def, which I would prefer to prevent. I was wondering if there was a way of doing so

[Sebastian Ullrich]

But that is likely the right way to do it as then you can rewrite in x_def without affecting anyone else. With let, you can only do defeq transformations in general because dependent terms may otherwise become type-incorrect.

[Ayhon]

I see. In that case I will use generalize instead, or something based upon it. Another perceived advantage of introducing these terms with let is that I could define them in the proposion I'm trying to prove and simply introduce them with intro, without having to explicitly set the term I'm substituting. But I can imagine having some kind of intro' which introduces let bindings in this way.

As an illustrating example, here I don't have to do generalize tree'_def: tree.delete_rebalance target = tree', but just intro tree'.

theorem Spec.BSTree.delete_rebalance.spec[LinearOrder α][Inhabited α]
{tree tree': BSTree α}{target: α}
: tree.is_avl
→ let tree' := tree.delete_rebalance target
  tree'.toSet = tree.toSet \ {target} ∧
  tree'.is_avl

[Ayhon]

Arguably, if you want to set the equality from the proof, you'd do so as a proposition directly, so perhaps it's not even that useful to have such an intro' if you write the proposition correctly.