How to coerce Fin m to Fin n everywhere given m = n?

Stream: new members

[Mathias Sven]

I don't have much experience with coercion, I have so far been able to understand simple numeric conversions or data structure conversions (i.e.: something.toSomething), but it is not clear to me how to cleanly do this.

For example, here is a minimal MWE which is just:

import Mathlib

example {xs : Array ℕ} {n m : ℕ} (h1 : m = 2 * n) (h2 : xs.size = m) [NeZero m] :
  ∃ i : Fin m, xs[i - 1] = xs[i] ∨ xs[i - 2] = xs[i] := by
  sorry

The objective is to change the goal to something that uses i : Fin (2 * n) instead.

And by cleanly, I mean that I have tried conv among other tactics like using some lemmas I found, eg: Fin.cast, finCongr h1, Equiv.exists_congr_left and lift i to Fin (2 * n) using h1 but all of them left me with leftovers in the goal or didn't work (like lift), as in it didn't reduce to a nice expression such: ∃ i : Fin (2 *n), xs[i - 1] = xs[i] ∨ xs[i - 2] = xs[i].

It would also be nice if there was a tactic that simply changed all occurrences of a type with another among so that whatever I do the goal I don't have to repeat for each other hypothesis.

[Aaron Liu]

docs#Fin.cast

[Aaron Liu]

you can rewrite it too

[Aaron Liu]

import Mathlib

set_option pp.funBinderTypes true in
example {xs : Array ℕ} {n m : ℕ} (h1 : m = 2 * n) (h2 : xs.size = m) [NeZero m] :
    ∃ i : Fin m, xs[i - 1] = xs[i] ∨ xs[i - 2] = xs[i] := by
  rw! [h1]
  -- ⊢ ∃ (i : Fin (2 * n)), xs[i - 1] = xs[i] ∨ xs[i - 2] = xs[i]
  sorry

[Mathias Sven]

I see, thanks! I honestly spent way longer than I would like to admit on this given how simple the solution is... What got me was that Fin.cast was a function, so I didn't know how to apply to every term nicely (as it wasn't an equality). rw! was also not in my toolbox, this was much simpler than I expected

[Ruben Van de Velde]

Also maybe subst h1 would work

[Mathias Sven]

Seems to work on the MWE, but it was also one of the things I tried and it didn't work on my original example. Seems it is because I had it more like this:

example {xs : Array ℕ} {n : ℕ} (h1 : xs.size = 2 * n) [NeZero n] [NeZero xs.size] :
  ∃ i : Fin xs.size, xs[i - 1] = xs[i] ∨ xs[i - 2] = xs[i] := by
  subst h1

But it gave me this, so I looked at other alternatives

Tactic `subst` failed: invalid equality proof, it is not of the form (x = t) or (t = x)
  xs.size = 2 * n

[Ruben Van de Velde]

Ah yeah, that won't work

[Violeta Hernández]

As a general rule you should avoid doing any rewriting of types if you can ever avoid it.

[Aaron Liu]

fortunately this isn't rewriting types it's rewriting nats