Using rewrite to simplify a bound variable expression

Stream: new members

[Ken Roe]

theorem fsimp3 { x : ℕ } : x=0 → f x = 1 :=
begin
    intro, unfold f, rw a
end

theorem fsimp4 {e : ℕ } : e=0 → (λ x : ℕ, x+(f x)=1+x)=(λ x : ℕ, 1=1) :=
begin
    intro,
    rewrite fsimp3, simp
end

How do I get the "rewrite fsimp3" tactic to work in the "fsimp4" proof?

[Scott Morrison]

Probably use conv. Do you want to post an MWE?

[Ken Roe]

Go ahead and post

[Scott Morrison]

No, I was suggesting that _you_ post a minimal example that shows the problem --- in particular you haven't included the definition of f!

[Scott Morrison]

I think def f (x : ℕ) := x + 1 probably serves your purpose.

[Mario Carneiro]

rw does not work under a binder. You can either use simp instead, or use conv or funext to enter the binder

[Reid Barton]

For conv, see https://github.com/leanprover/mathlib/blob/master/docs/extras/conv.md

[Ken Roe]

Oops--Missed that def

def f (x : ℕ) := x+1

theorem fsimp3 { x : ℕ } : x=0 → f x = 1 :=
begin
    intro, unfold f, rw a
end

theorem fsimp4 {e : ℕ } : e=0 → (λ x : ℕ, x+(f x)=1+x)=(λ x : ℕ, 1=1) :=
begin
    intro,
    rewrite fsimp3, simp
end

[Scott Morrison]

I'm pretty confused how you intend to do anything using rw fsimp3, even under the binder.

[Scott Morrison]

You've only got e=0, but now want to say something about all x?

[Ken Roe]

It looks like conv fails:

theorem fsimp4 {e : ℕ } : e=0 → (λ x : ℕ, x+(f x)=1+x)=(λ x : ℕ, 1=1) :=
begin
    intro, simp, conv
    begin
        to_lhs,
        funext,
        rw fsimp3, reflexivity,
    end
end

I get the error:

convert tactic failed, there are unsolved goals
state:
e : ℕ,
a : e = 0,
x : ℕ
⊢ x = 0

[Reid Barton]

That's because, as Scott pointed out, what you're trying to prove is not true

[Ken Roe]

Actually, I found the error:

theorem fsimp4 {e : ℕ } : e=0 → (λ x : ℕ, x+(f x)=1+x) e=(λ x : ℕ, 1=1) e :=
begin
    intro, conv
    begin
        to_lhs,
        simp, rw a,
        funext,
        rw fsimp3, skip, reflexivity
    end
end

However, the error I got is confusing. The "x=0" got changed to "x" on the screen in the message.

[Mario Carneiro]

this proof attempt is not valid for the same reason as before. You can't try to prove the functions are equal because they aren't. You can only prove that the functions evaluated at e are equal, so you need to do beta reduction first (using dsimp) and then try to prove it