Zulip Chat Archive

Stream: new members

Topic: Bug in show_term


view this post on Zulip 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'.

view this post on Zulip Kenny Lau (Aug 30 2020 at 10:30):

set_option pp.proofs true

view this post on Zulip Kenny Lau (Aug 30 2020 at 10:30):

(above the example)

view this post on Zulip 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

view this post on Zulip Reid Barton (Aug 30 2020 at 10:41):

set_option pp.all true

view this post on Zulip Reid Barton (Aug 30 2020 at 10:41):

There's a reason the rw tactic exists

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip Mario Carneiro (Aug 30 2020 at 14:52):

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

view this post on Zulip Kenny Lau (Aug 30 2020 at 14:59):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Aug 30 2020 at 17:24):

basically avoid eq.rec at all cost

view this post on Zulip 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)?

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Aug 30 2020 at 17:30):

And rewriting along type equalities seems pretty "evil"

view this post on Zulip Johan Commelin (Aug 30 2020 at 17:31):

list.map (equiv.refl h)?

view this post on Zulip Johan Commelin (Aug 30 2020 at 17:31):

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

view this post on Zulip Reid Barton (Aug 30 2020 at 17:35):

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

view this post on Zulip Pim Spelier (Aug 30 2020 at 17:36):

Why not?

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Aug 30 2020 at 17:37):

Pim Spelier said:

Why not?

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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