## Stream: new members

### Topic: Bug in show_term

#### Pim Spelier (Aug 30 2020 at 10:29):

There seems to be a bug in show_term: in the example

example (a b : ℕ) (h : b = a) (x : fin a) : fin b  :=
begin
show_term{rw h,
exact x,}
end


show_term suggests exact _.mpr x, but lean doesn't seem to know what to do with the underscore, and gives the error unknown identifier '_.mpr'.

#### Kenny Lau (Aug 30 2020 at 10:30):

set_option pp.proofs true

#### Kenny Lau (Aug 30 2020 at 10:30):

(above the example)

#### Pim Spelier (Aug 30 2020 at 10:37):

Now show_term suggest exact (id (eq.rec (eq.refl (fin b)) h)).mpr x, but lean still doesn't like it:

invalid 'eq.rec' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables ?m_1

#### Reid Barton (Aug 30 2020 at 10:41):

set_option pp.all true

#### Reid Barton (Aug 30 2020 at 10:41):

There's a reason the rw tactic exists

#### Scott Morrison (Aug 30 2020 at 12:56):

Adding a bit more context, pretty printing is hard, and Lean doesn't promise that it round trips, even with pp.all (although that comes pretty close). Some tactics generate large proof terms, and so show_term is not always useful, and you may need to dance around a bit with pp options to even get parseable expressions.

#### Alex J. Best (Aug 30 2020 at 14:44):

In this case you can do  example (a b : ℕ) (h : b = a) (x : fin a) : fin b := h.symm.rec x for a slick term :smile:

#### Mario Carneiro (Aug 30 2020 at 14:52):

example : ∀ (a b : ℕ), b = a → fin a → fin b | a _ rfl := id


#### Kenny Lau (Aug 30 2020 at 14:59):

in any case, don't use tactics to define data

#### Pim Spelier (Aug 30 2020 at 16:27):

So in this example, would it be better (more in line with the lean style) to write h.symm.rec x as Alex suggests, or to use tactic mode?

#### Reid Barton (Aug 30 2020 at 16:49):

In this example, you probably shouldn't define the function this way at all, but instead use docs#fin.cast

#### Reid Barton (Aug 30 2020 at 16:50):

this has the advantage that (fin.cast h x).val reduces to x.val, while with the definitions discussed here, it would get stuck on the eq.rec

#### Kenny Lau (Aug 30 2020 at 17:24):

basically avoid eq.rec at all cost

#### Pim Spelier (Aug 30 2020 at 17:28):

Thanks Reid, that makes sense. However, the example is a MWE, we actually want to use it in a slightly different case:

example (α β : Type*) (h : α = β) (x : list β) : list α :=
begin
rw h,
exact x,
end


I couldn't find a list.cast or anything similar, so should I just use tactic mode here (even though I'm defining data)?

#### Johan Commelin (Aug 30 2020 at 17:30):

"don't define data in tactic mode" is a slogan exactly because it wants you to avoid eq.rec.

#### Johan Commelin (Aug 30 2020 at 17:30):

And rewriting along type equalities seems pretty "evil"

#### Johan Commelin (Aug 30 2020 at 17:31):

list.map (equiv.refl h)?

#### Johan Commelin (Aug 30 2020 at 17:31):

But probably h should itself be a function, or an equiv.

#### Reid Barton (Aug 30 2020 at 17:35):

Right, you probably shouldn't have an equality of types in the first place

Why not?

#### Pim Spelier (Aug 30 2020 at 17:36):

I just changed the type equality in the hypothesis to an equivalence, and now everything seems to work fine with list.map, thanks!

#### Johan Commelin (Aug 30 2020 at 17:37):

Pim Spelier said:

Why not?

Because unit \times nat ≠ nat but they certainly are equiv.

#### Kevin Buzzard (Aug 30 2020 at 17:42):

because nat = int is unprovable in Lean, and one could imagine a refactoring of int where it is redefined to be a type alias for nat with an exotic addition and multiplication, and then it would be true.

#### Pim Spelier (Aug 30 2020 at 17:46):

Ok, that makes sense! It's an isomorphism in the category of types, which makes way more sense than an equality.

#### Kevin Buzzard (Aug 30 2020 at 17:48):

One shouldn't talk about equality of objects in a category, because mathematicians only really care about categories up to equivalence a lot of the time so they like to randomly replace a category with an equivalent category, and this will not change isomorphism but it might change equality. Equality is hence some kind of unstable notion if you're thinking about categories in this way. If you think about the definition of an isomorphism of objects in Type u then you see it's exactly equiv.

#### Scott Morrison (Aug 31 2020 at 01:15):

(With the added excitement that equiv can change universe levels, while isomorphisms can't.)

Last updated: May 17 2021 at 21:12 UTC