Zulip Chat Archive

Stream: new members

Topic: fin coe struggle


view this post on Zulip Anatole Dedecker (Aug 24 2020 at 07:31):

Okay so I must be missing something but I can't find how to prove this :sad:

import tactic

lemma foo (n : ) : ((n : fin n.succ) : ) = n :=
begin
  sorry,
end

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 07:35):

What's the definition of the coercion? If this proof is not refl then I think it says that you shouldn't be using the coercion

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 07:36):

I mean the coercion from fin to fin. There are perfectly well defined maps between fins which will behave very well, but recently people have been using some far less well behaved maps eg +1 and then complaining that everything is horrible because there are secret %(n+1) operators involved

view this post on Zulip Shing Tak Lam (Aug 24 2020 at 07:38):

import tactic

lemma foo (n : ) : ((n : fin n.succ) : ) = n :=
fin.coe_coe_of_lt (nat.lt_succ_self _)

view this post on Zulip Anatole Dedecker (Aug 24 2020 at 07:38):

Thanks ! I should have searched better I guess...

view this post on Zulip Anatole Dedecker (Aug 24 2020 at 07:40):

Kevin Buzzard said:

I mean the coercion from fin to fin. There are perfectly well defined maps between fins which will behave very well, but recently people have been using some far less well behaved maps eg +1 and then complaining that everything is horrible because there are secret %(n+1) operators involved

I know these coercions are trickier than most other (e.g norm_cast can't deal with them), but this example should be true anyway (and it is indeed)

view this post on Zulip Kyle Miller (Aug 24 2020 at 07:41):

Kevin Buzzard said:

What's the definition of the coercion?

It looks like it's fin.val (nat.cast n), with some type hinting in there somewhere.

view this post on Zulip Kyle Miller (Aug 24 2020 at 07:43):

That means foo is n % (n + 1) = n. (Not definitionally, though.)

view this post on Zulip Kevin Buzzard (Aug 24 2020 at 07:49):

Any map that uses % somehow is going to be hard to work with. None of the natural maps from fin n to fin (n+1) use %

view this post on Zulip Reid Barton (Aug 24 2020 at 12:31):

It's probably better to use fin.last n instead of whatever introduced (n : fin n.succ).


Last updated: May 11 2021 at 00:31 UTC