fin coe struggle

Stream: new members

[Anatole Dedecker]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Shing Tak Lam]

import tactic

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

[Anatole Dedecker]

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

[Anatole Dedecker]

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)

[Kyle Miller]

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.

[Kyle Miller]

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

[Kevin Buzzard]

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 %

[Reid Barton]

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