Zulip Chat Archive

Stream: general

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


view this post on Zulip 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?

view this post on Zulip Eric Wieser (Jan 13 2021 at 20:47):

Does simp [f] not do anything at all?

view this post on Zulip 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...

view this post on Zulip Yakov Pechersky (Jan 13 2021 at 20:51):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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