Zulip Chat Archive

Stream: lean4

Topic: aliasing complex terms


Rosie Baish (Jun 14 2022 at 13:03):

Is there a way to alias a complex term with a shorthand
e.g. Rather than the pretty printer outputting "(func a b c d e f g)" it outputs "x", and whenever x appears in the proof it's replaced by the long version
It would be an exact replacement, not parameterised by anything.
The reason for this is that the proof I'm working on has loads of really long terms in that make reading and comprehending the output really hard

Xubai Wang (Jun 14 2022 at 13:19):

(deleted)

Wojciech Nawrocki (Jun 14 2022 at 14:00):

If you are in a tactic proof, you could do something like

example (f : α  α  α) (x y : α) : f (f x y) (f x y) = f x y := by
  let z := f x y
  have : f x y = z := rfl
  rw [this]
  ...

There might be a tactic for this, but I couldn't immediately find it.

Ruben Van de Velde (Jun 14 2022 at 14:15):

There's set in mathlib3

Alex Keizer (Jun 14 2022 at 14:54):

There's generalize, borrowing Wojciech example

example (f : α  α  α) (x y : α) : f (f x y) (f x y) = f x y := by
  generalize f x y = z;
  sorry

However, it "forgets" the concrete value of z and only replaces things in the goal.
We can use the generalize hz : f x y = z notation to add an hypothesis hz : f x y = z to the context, allowing us to unfold z again at a later point in the proof.

Eventually we should be able to write generalize hz : f x y = z at h |- to do the substitution at hypotheses as well, but until that is implemented we can work around it by reverting the hypotheses that mention f x y.

For example,

example (f : α  α  α) (x y w : α) (h : f x y = w)
  : f (f x y) (f x y) = f x y := by
  revert h;
  generalize hz : f x y = z;
  intro h;
  sorry

Result in the proof state

α : Sort ?u.7
f : α  α  α
x y w z : α
hz : f x y = z
h : z = w
 f z z = z

Before the sorry


Last updated: Dec 20 2023 at 11:08 UTC