Zulip Chat Archive

Stream: new members

Topic: real.exp_log


view this post on Zulip Jalex Stark (Apr 30 2020 at 14:47):

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)

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:52):

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)

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:52):

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)

view this post on Zulip Jalex Stark (Apr 30 2020 at 14:53):

oof, thanks. maybe i need more coffee

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:53):

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

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:54):

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

view this post on Zulip Jalex Stark (Apr 30 2020 at 14:55):

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

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:55):

right :-)

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:55):

but it's perfectly fine Lean code

view this post on Zulip Kevin Buzzard (Apr 30 2020 at 14:55):

Maybe sneaky is a better word :-)

view this post on Zulip Jalex Stark (Apr 30 2020 at 14:56):

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

view this post on Zulip Jalex Stark (Apr 30 2020 at 14:56):

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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:07):

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

view this post on Zulip Patrick Massot (Apr 30 2020 at 15:08):

I thought this is what they meant.

view this post on Zulip Patrick Massot (Apr 30 2020 at 15:08):

How can you have a dirty rwa otherwise?

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:09):

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

view this post on Zulip Reid Barton (Apr 30 2020 at 15:10):

Then the rw part would be useless, right?

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:11):

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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:12):

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

view this post on Zulip Mario Carneiro (Apr 30 2020 at 15:15):

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

view this post on Zulip Reid Barton (Apr 30 2020 at 15:18):

This is like a doubly red herring.


Last updated: May 13 2021 at 23:16 UTC