Fin cast and succ

Stream: new members

[Malvin Gattinger]

I thought this one should be (true and) easy, but I am stuck.

import Mathlib.Data.Fin.Basic

theorem fin_succ_succ (i : Fin n) : (i + 1 + 1 = i.succ.succ) :=
  by
  apply Fin.eq_of_veq
  simp
  -- why do I now have three cast arrows in the left side?
  sorry

Probably I should not use Fin.eq_of_veq at all? Am I misunderstanding Fin? I am assuming that the = I want to show is within Fin (n+2) right?

[Ruben Van de Velde]

It would be easier to investigate if you added the imports needed to make this a #mwe

[Malvin Gattinger]

Oh, sorry. I wrongly thought Fin would be available by default.

[Eric Wieser]

What's the goal state after the by? I suspect there are coercions in weird places

[Joël Riou]

The statement is true, but it seems quite confusing to me. Lean knows that this has to be an equality in Fin (n+2) only by considering the RHS: if you do let j := i + 1 + 1, Lean will not accept this term! The correct way to take the successor of something in Fin is to use the syntax i.succ.
Otherwise, if you really want to prove this, the definition of + in Fin.add is by taking the sum in the natural numbers and then taking the reminder of a division: proving the equality can be quite painful, but simp and linarith can handle it:

theorem fin_succ_succ {n : ℕ} (i : Fin n) : i + 1 + 1 = i.succ.succ := by
  ext
  dsimp only [HAdd.hAdd, Add.add, Fin.add]
  simp
  have := i.is_lt
  linarith

[Malvin Gattinger]

Right, my mistake was to use i + 1 instead of i.succ in the larger theorem for which I then reached this as a subgoal. Using i.succ instead makes the whole problem go away :tada: Thanks everyone!

[Notification Bot]

Malvin Gattinger has marked this topic as resolved.

[Notification Bot]

Malvin Gattinger has marked this topic as unresolved.

[Malvin Gattinger]

I have another +1 vs succ problem when using vectors. Would you also find this statement confusing, and can I do something else to avoid the coercions? (When does one say coercion and when cast, btw?)

import Mathlib.Data.Vector.Basic

theorem vec_succ (i : Fin n) (ys : Vector α n.succ) : (a ::ᵥ ys).get (i.succ) = ys.get i :=
  by
  -- Vector.get (a ::ᵥ ys) ↑↑(Fin.succ i) = Vector.get ys ↑↑i
  simp
  -- Vector.get (a ::ᵥ ys) (↑↑i + 1) = Vector.get ys (Fin.castSucc i)
  sorry

[Eric Wieser]

That looks very weird; shouldn't the n.succ just be n?

[Malvin Gattinger]

Indeed with n instead of n.succ it goes through just with simp, but with a one-item-longer vector it should still be true?

[Eric Wieser]

With the one-time longer vector it's a very weird statement

[Eric Wieser]

The +1 in your second goal comment is in Fin n which has modular arithmetic

[Eric Wieser]

The ↑↑ in your first goal statement is effectively i.succ.val % (n + 2)