# Zulip Chat Archive

## 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