smarter subst?

Stream: lean4

[Michael Jam]

I often find myself in situations where rw/subst/generalize tactics don't work because some variable occurs in the other, or because what I'm trying to substitute isn't an atomic variable.
So I have to manually write an auxiliary lemma that generalizes variables, which looks ugly.
I'm wondering what the right way to deal with those proofs is. Here is an mwe:

theorem th {n : Nat} (x : Fin (n + 1)) (h : x.val = n) : x = ⟨n, Nat.lt_succ_self n⟩ :=
sorry

How do you prove this efficiently?

[Henrik Böving]

My proof would be:

theorem th {n : Nat} (x : Fin (n + 1)) (h : x.val = n) : x = ⟨n, Nat.lt_succ_self n⟩ := by
  cases x
  simp [h]

[Michael Jam]

Ok that's nice my mwe is too simple. Do you think you could have a proof that doesn't use cases x? I'm in a context where x has an abstract type so I can't use cases on it.

[Michael Jam]

I'll try to come up with a better example later

[Jannis Limperg]

For generalize, check out docs#tactic.interactive.generalizes. In general, many tactics work better with less dependent goals; this is the eternal paradox of dependent type theory. ;)

[Jannis Limperg]

Oh no Lean 4, sorry. In that case there's no equivalent to generalizes yet.

[Leonardo de Moura]

@Jannis Limperg generalize may take multiple entries in Lean 4

def Fin.succ (f : Fin n) : Fin (Nat.succ n) :=
  ⟨f.val + 1, Nat.succ_lt_succ f.isLt ⟩

theorem ex (P : ∀ n, Fin n → Prop) (n : Nat) (f : Fin n) : P (Nat.succ n) (Fin.succ f) := by
  generalize n'_eq : Nat.succ n = n', f'_eq : Fin.succ f = f'
  sorry

[Jannis Limperg]

Oh nice! I didn't realise you already had this covered.