## Stream: general

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

#### Chase Meadors (Jan 13 2021 at 20:40):

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 (Jan 13 2021 at 20:47):

Does simp [f] not do anything at all?

#### Chase Meadors (Jan 13 2021 at 20:48):

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 (Jan 13 2021 at 20:51):

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

#### Yakov Pechersky (Jan 13 2021 at 20:52):

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 (Jan 13 2021 at 20:53):

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 (Jan 13 2021 at 20:55):

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 (Jan 13 2021 at 20:55):

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 (Jan 13 2021 at 20:57):

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 (Jan 13 2021 at 20:57):

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 (Jan 13 2021 at 20:58):

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

Last updated: May 12 2021 at 05:19 UTC