Can I avoid the use of "change", and should I?

Stream: general

[Chase Meadors]

Sometimes I encounter a situation where I know the goal or a hypothesis is definitionally the same as a simpler expression, usually when evaluating an explicitly defined function. In these situations, I find that simp or unfold don't do what I expect and "reduce" the expression. Here's a MWE related to something I was working on:

example {α : Type} {P : α → Prop} (next : α → α) (s : α) (h : ∀ a : α, P a → P (next a)) :
  ∃ f : ℕ → α, ∀ n : ℕ, P (f n) :=
begin
  let f : ℕ → α := λ n, nat.rec_on n s (λ n, next),
  use f,
  intro n,
  induction n with n hn,
  change P s,
end

Here's a toy scenario where I want to take a function next : next : α → α and a hypothesis that next preserves P, and inductively build a function f : ℕ → α.
Right before the change step, the context is:

case nat.zero
α: Type
P: α → Prop
next: α → α
s: α
h: ∀ (a : α), P a → P (next a)
f: ℕ → α := λ (n : ℕ), n.rec_on s (λ (n : ℕ), next)
⊢ P (f 0)

And of course, trivially, definitionally, we have f 0 = s, by the definition. Lean knows this, because I can do change P s. But, is this normal? I suppose I would expect something like simp (I also tried simp[f]) to do this.

Perhaps this is precisely what change is meant for?

[Eric Wieser]

Does simp [f] not do anything at all?

[Chase Meadors]

simp[f], results in

⊢ P (nat.rec s (λ (n : ℕ), next) 0)

and then further simplification fails. So it unfolds f, I suppose, but...

[Yakov Pechersky]

You don't need to change. But you are missing (hs : P s)

[Yakov Pechersky]

example {α : Type} {P : α → Prop} (next : α → α) (s : α) (h : ∀ a : α, P a → P (next a)) (hs : P s) :
  ∃ f : ℕ → α, ∀ n : ℕ, P (f n) :=
begin
  let f : ℕ → α := λ n, nat.rec_on n s (λ n, next),
  use f,
  intro n,
  induction n with n hn,
  { exact hs },
  { apply h,
    exact hn }
end

[Eric Wieser]

If your next tactic is exact or apply, you can usually remove the change. If the next tactic is rw, you usually can't

[Chase Meadors]

Ah, I see. I just tried remove "change" in a few places where I was doing exact next, and it worked. I suppose this is another situation where I was trying to "change" for my own psychological comfort. But if I'm going to rewrite something next, it needs to actually find the pattern, so it could be useful.

[Damiano Testa]

While I realize that this is besides the point, and I am learning from this thread, but wouldn't the constant function equal to s also prove the statement?

[Chase Meadors]

Ha, yes, I suppose so. I had extracted this as a minimal example from a different context where I was building a sequence that I wanted to have a certain supremum, but failed to make my example "fully minimal", I suppose.

[Ruben Van de Velde]

Something like this avoids relying on exact using definitional equality

import tactic

example {α : Type} {P : α → Prop} (next : α → α) (s : α) (h : ∀ a : α, P a → P (next a)) (hs: P s) :
  ∃ f : ℕ → α, ∀ n : ℕ, P (f n) :=
begin
  set f : ℕ → α := λ n, nat.rec_on n s (λ n, next) with hf,
  use f,
  intro n,
  induction n with n hn,
  { rw hf,
    dsimp only,
    exact hs },
  apply h,
  rw hf at hn,
  dsimp only at hn,
  exact hn,
end

[Damiano Testa]

Anyway, thank you for bringing this up: I had encountered similar doubts myself and this thread is clarifying the behaviour and use of change!