real.exp_log

Stream: new members

[Jalex Stark]

I feel like this error message is telling me that the elaborator can't unify \R with \R:

import analysis.calculus.specific_functions

example (x : ℝ) (hx : 0 < x) : real.log x < x := begin
suffices key : real.log x < real.exp (real.log x),
rw real.exp_log hx,
end

(edited to make the error a bit more explicit)

[Kevin Buzzard]

I think it's OK, the LHS of real.exp_log hx is real.exp (real.log x) and it can't find it in your goal (because the goal is real.log x < x)

[Kevin Buzzard]

The suffices puts the new goal key at the end, not the start, so the rewrite is still trying to work on real.log x < x (and I think rw only works on the first goal)

[Jalex Stark]

oof, thanks. maybe i need more coffee

[Kevin Buzzard]

  suffices key : real.log x < real.exp (real.log x),
  { rwa real.exp_log hx at key},

[Kevin Buzzard]

I always think it's a bit dirty using rwa like that.

[Jalex Stark]

because the rw and the a get applied in different places?

[Kevin Buzzard]

right :-)

[Kevin Buzzard]

but it's perfectly fine Lean code

[Kevin Buzzard]

Maybe sneaky is a better word :-)

[Jalex Stark]

yeah i agree that its better than rw ... at key, exact key which appears too many times in my codewars solutions

[Jalex Stark]

i think i forgot about rwa when I went through a phase of leaning on nonterminal simps

[Mario Carneiro]

I think that a "dirty" use of rwa thm at h would be if the assumption being referred to is not the rewritten h

[Patrick Massot]

I thought this is what they meant.

[Patrick Massot]

How can you have a dirty rwa otherwise?

[Mario Carneiro]

example (red herring : ℕ) (h : red = 0) (h2 : red = herring) : red = 0 :=
by rwa h at h2

[Reid Barton]

Then the rw part would be useless, right?

[Mario Carneiro]

I expect that an edge case exists, but yes, in almost all cases

[Mario Carneiro]

There are two ways you can use rwa normally: to rewrite a hypothesis to match the goal, or to rewrite the goal to match a hypothesis. I would call neither of these uses sneaky. I usually use the former, which is clearly marked since it uses an at h clause

[Mario Carneiro]

Here is another sneaky use, where the hypothesis being used is h before the rewrite:

example (red herring : ℕ) (h : red = 0) (h2 : red = herring) (dep : h = h) : red = 0 :=
by rwa h2 at h

deleting dep breaks the proof

[Reid Barton]

This is like a doubly red herring.