Help proving lemma; rw produces new name

Stream: new members

[Mayank Manjrekar]

Hi, I'm trying to prove the following simple result about Fin types

import Mathlib.Tactic

theorem only_one (r : Fin 1) : r = 0 := by
  apply (Fin.mk_eq_mk).mpr
  simp

example (r : Fin (2 - 1)) : r = 0 := by
  simp at r  -- fails

The last "simp" there produces the following goal

r✝: Fin (2 - 1)
r: Fin 1
⊢ r✝ = 0

How do I unify r and r✝?

For the example above, I know that the following works:

example (r : Fin (2 - 1)) : r = 0 := by
  apply Fin.mk_eq_mk.mpr
  simp

[Damiano Testa]

In this case, you can prove it as follows:

example (r : Fin (2 - 1)) : r = 0 := by
  ext
  simp

[Damiano Testa]

In your initial proof, simp does indeed what you want, as you can see from the new r : Fin 1 hypothesis.

I think that the reason for the new hygienic goal is due to the fact that rewrite first creates the new, rewritten declaration and then tries to replace the old one with the new one. In your situation, the new one is formed, however, since the Type of r is not "equal" to the Type after the rewrite, the replace step does not work. Lean therefore leaves the old declaration r as unreachable, which is what you observe from the r✝.

[Damiano Testa]

Honestly, I do not really know what kind of "equality" is needed for the replacement step to be successful. In your case, Fin (2 - 1) and Fin 1 are defeq and even syntactically equal:

example : Fin (2 - 1) = Fin 1 := rfl  -- succeeds, so defeq
example (h : Fin 1 = Fin 2) : Fin (2 - 1) = Fin 2 := by rw [h]  -- succeeds, so actually also syntactically equal

I really am not sure...

[Mayank Manjrekar]

I'd like to understand this better -- specifically, the difference between Defeq and propositional inequality, and when I should expect rewrite tactic to work. Is there a good reference for this? From what you mention, it looks like it is generally not possible to reuse theorems like Fin.coe_fin_one (a: Fin 1) : a = 0.

Here are some experiments I have been doing:

variable {P : ℕ → Prop} {R : Prop} {Q : ℕ → Type}
example (n m: ℕ) (h0 : n = m) (a b : Q n) (c : Q m) (h1 : ∀ (d : Q m), d = c)  : a = b := by
  rw [h0] at a -- preserves old declaration
  rw [h0] at b -- preserves old declaration
  sorry

example (n m: ℕ) (h0 : n = m) (a : P n) (h1 : P m → R) : R := by
  rw [h0] at a  -- does not preserve old declaration. Are all values of type Prop "equal"?
  exact h1 a

example (n m: ℕ) (h0 : n = m) (a b : Q n) (c : Q m) (h1 : ∀ (d : Q m), d = c)  : a = b := by
  cases h0  -- rewrites m to n everywhere.
  rw [h1 a, h1 b]

Could you explain what is going on here?

[Eric Wieser]

I think the relevant difference here is "appears in the type of something else in your context" vs not. If you rewrite something in the local context but something else was already referring to it, you need to make the substitution in multiple places simultaneously

[Eric Wieser]

That's a hard (maybe impossible?) problem in general; rw certainly can't do it, and cases only works if one side of the equality is a free variable.

[Mayank Manjrekar]

Okay, I get it. Thank you!