coercionlean

Lean4 Coercion between Nat/ Fin3/Fin9 with simp tactic pass the proof of 0=2

example (i:Fin 9)(h:(i.1/3 :Fin 3).1 = i/3): 0 = i.1/3:= by
  simp at h
  exact h

This finishes the proof, but

  1. if i = 6, then h certainly is true. But the claim is 0 = i.1/3 <=> 0 = 2
  2. either something wrong with the simp or h is wrong.

Could anyone explain what's wrong about this? if H is true(I believe its true) can anyone prove it

Solution

  • This happens because the coercion is in an unexpected place: The h here is interpreted as h : ((i.val : Fin 3) / 3).val = i.val / 3, so you get ((6 : Fin 3) / 3).val = (0 / 3).val = 0. On newer versions of Mathlib, the coercion from Nat to Fin is disabled by default to avoid such unintuitive behavior (but you can enable it using open scoped Fin.NatCast).