What does the `show` tactic actually do?

Stream: new members

[Dan Abramov]

I've been using Lean for a while and I still have no idea what show actually does.

Partially it's because its documentation seems to be written for somebody who already understands some fundamental ideas like "unification", and doesn't consider it necessary to elaborate with even a single tiny example of what that means in practice. Unfortunately I'm a learning procrastinator, so I have not read about those (yet?)

Screenshot 2025-07-20 at 01.45.47.png

You can try to search for it:

Screenshot 2025-07-20 at 01.50.04.png

Ironically, one of the results is someone asking where to find the documentation. (Maybe even more ironically, the answer that got inlined in the Google search page is someone saying they don't know if a list of keywords even exists.)

The first result does look related but it is not a reference (so you have to scan the text). Luckily the text does seem to dive into some detail about it, but less fortunately it is written almost entirely in the abstract style and not so much in the "here's how we usually use it in practice" mode. Which is great for a certain frame of mind but maybe not always.

I understand so far that it changes the goal to some equivalent, and maybe a bit more, but the "a bit more" part is a bit fuzzy and I just haven't found a good resource that explains how people use it in practice. Like, at which point in a proof you would think, "show would be nice here". What is the rule of thumb for using it?

Are there any cases where it particularly helps? Or does it serve more as a midpoint documentation about "where we are" in the proof?

[Dan Abramov]

The reason I'm curious about it is that I'm starting to realize that the way things are framed in the InfoView is actually kind of important. With more complex expressions, especially choice, I really need to "outline" some stuff to "see the pattern" sometimes. So I'm starting to use change a bit more to explore the definitionally equivalent things, and curious if I'm missing a bunch of patterns that people normally do. Using set to "notice" repeating patterns is another habit I picked up (not sure if good or bad habit).

[Kyle Miller]

"Unification" is the definitional equality procedure. The terminology comes from logic languages like Prolog. You can think of show as being a term-mode change.

[Kyle Miller]

Oh, wait, you mean the show tactic. There's not much use for the show tactic, since we have change.

In a recent Lean, the value-add for show is that you can use it to select one of the goals. The change tactic only applies to the first goal.

[Kyle Miller]

The show term though is somewhat useful. Writing show T from e is like (e : T), but it annotates the expression to ensure that its type is actually T. All (e : T) does is makes sure that the type of the result is definitionally equal to ("unifies with") T.

[Kyle Miller]

You can see it in things like rw [show a = b from rfl] to change all as to bs. The type of rfl will be something like a = a, so it's important to have this annotation that actually makes it be a = b.

[Dan Abramov]

ahhh okay

[Kyle Miller]

change T is pretty much the same as refine show T from ?_

[Kyle Miller]

and until recently, the show tactic was a synonym for this — hence why the tactic is called show