induction and `set`

Stream: new members

[Vlad Tsyrklevich]

I'm sure this has been discussed before, but 'set' is a useless search keyword. I want to prove an equality of two function calls valued in Nat using induction, say foo α = bar α. Using set n := foo α with hn creates the variable/hypothesis

n : ℕ := foo α
hn : n = foo α

but when I try to induction n, the value of n is not replaced in hn. If I write the variable/hypothesis explicitly obviously everything works as expected. What am I missing to make this work?

opaque foo (α : Type*) : Nat
opaque bar (α : Type*) : Nat

theorem baz (α : Type*) : foo α = bar α := by
  set n := foo α with hn
  induction n
  · -- hn : n = foo α
    -- ⊢ 0 = bar α
    sorry
  · sorry

theorem baz2 (α : Type*) (n : Nat) (hn : n = foo α) : n = bar α := by
  induction n
  · -- hn : 0 = foo α
    -- ⊢ 0 = bar α
    sorry
  · sorry

[Aaron Liu]

that's so weird

[Aaron Liu]

oh never mind it makes sense now

[Robin Arnez]

have (eq := hn) n := foo α should work better since it doesn't create a let declaration

[Aaron Liu]

it's because n is not a cdecl or nondependent ldecl, so induction treats it differently

[Aaron Liu]

the same as doing induction foo α, it only generalizes the occurrences in the goal

[Vlad Tsyrklevich]

Robin Arnez said:

have (eq := hn) n := foo α should work better since it doesn't create a let declaration

Thanks! If I had infinite time it'd be nice to add a warning to induction to inform users of this when they hit this case.

[Robin Arnez]

Oh and maybe have +generalize (eq := hn) n := foo α if you want to replace the foo α in the goal