Bug in show_term

Stream: new members

[Pim Spelier]

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]

set_option pp.proofs true

[Kenny Lau]

(above the example)

[Pim Spelier]

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]

set_option pp.all true

[Reid Barton]

There's a reason the rw tactic exists

[Scott Morrison]

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]

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]

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

[Kenny Lau]

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

[Pim Spelier]

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]

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

[Reid Barton]

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]

basically avoid eq.rec at all cost

[Pim Spelier]

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]

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

[Johan Commelin]

And rewriting along type equalities seems pretty "evil"

[Johan Commelin]

list.map (equiv.refl h)?

[Johan Commelin]

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

[Reid Barton]

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

[Pim Spelier]

Why not?

[Pim Spelier]

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]

Pim Spelier said:

Why not?

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

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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