Zulip Chat Archive

Stream: new members

Topic: pow_mono


Jalex Stark (Apr 28 2020 at 17:37):

Is this example true? (and if so, how to prove it? I listed my imports, and I can't get anything useful out of library_search or suggest, even after reverting stuff)

import data.real.basic
import data.complex.exponential
import analysis.asymptotics
import tactic
example {x y : } {d : } (hxy : x  y) (hx : 0  x) (hd : d 1) : (x ^ d  y^d) :=  sorry

Kevin Buzzard (Apr 28 2020 at 17:37):

Hah, do you need this for codewars?

Jalex Stark (Apr 28 2020 at 17:38):

I'm working on what might become a kata

Jalex Stark (Apr 28 2020 at 17:39):

the statement is if f g : \R \to \R big O of a polynomial then so is f\circ g

Kevin Buzzard (Apr 28 2020 at 17:39):

You don't need d>=1 I guess, and you can prove it by induction on d but when I was looking for some related thing recently (when doing codewars last Sat night) I couldn't find it in the library

Reid Barton (Apr 28 2020 at 17:39):

I think it's pow_le_pow_of_le_left or similar

Kevin Buzzard (Apr 28 2020 at 17:40):

that works if d: nat, but we have d:int and d>=0

Kevin Buzzard (Apr 28 2020 at 17:40):

There's a trick for this isn't there, some recent tactic which magics up a nat

Reid Barton (Apr 28 2020 at 17:40):

lift

Kevin Buzzard (Apr 28 2020 at 17:41):

example {x y : } {d : } (hxy : x  y) (hx : 0  x) (hd : 0  d) : (x ^ d  y ^ d) :=
begin
  lift d to  using hd,
  apply pow_le_pow_of_le_left hx hxy,
end

Kevin Buzzard (Apr 28 2020 at 17:41):

I replaced d>=1 by 0<=d

Jalex Stark (Apr 28 2020 at 17:42):

I was about to post the same code
(well not literally)

example {x y : } {d : } (hxy : x  y) (hx : 0  x) (hd : 0  d) : (x ^ d  y^d) :=  begin
lift d to nat,
apply pow_le_pow_of_le_left; assumption, assumption,
end

Jalex Stark (Apr 28 2020 at 17:42):

I was surprised to type assumption twice, does ";" mean something other than "try the next thing on all goals?"

Jalex Stark (Apr 28 2020 at 17:43):

:light_bulb: does it mean "try the next thing on all goals that are created as a result of this tactic"?

Kevin Buzzard (Apr 28 2020 at 17:43):

I am also surprised. @Reid Barton ?

Kevin Buzzard (Apr 28 2020 at 17:43):

Right, but lift d to nat doesn't, for some reason, create the goal d>=0.

Kevin Buzzard (Apr 28 2020 at 17:44):

I think there is something funny going on.

Jalex Stark (Apr 28 2020 at 17:44):

oh huh

Kevin Buzzard (Apr 28 2020 at 17:44):

no, a Lean restart fixed it

Reid Barton (Apr 28 2020 at 17:45):

I think it actually does and this is something where the tactic state gets confused

Reid Barton (Apr 28 2020 at 17:45):

if you add skip, after you can see that the new goal was already created before skip

Kevin Buzzard (Apr 28 2020 at 17:46):

I am observing random behaviour regarding whether the goal d>=0 appears immediately or a bit later. Actually I can't reproduce :-(

Reid Barton (Apr 28 2020 at 17:47):

for me it's quite consistent

Kevin Buzzard (Apr 28 2020 at 17:48):

consistently you're getting the second goal not immediately appearing?

Reid Barton (Apr 28 2020 at 17:48):

Yes

Reid Barton (Apr 28 2020 at 17:49):

Unfortunately I don't know whether this is testable from the command line

Kevin Buzzard (Apr 28 2020 at 17:49):

so at least I'm not the only one going mad

Kevin Buzzard (Apr 28 2020 at 17:50):

@Jalex Stark I prefer the using hd variant because in general if I can keep to one goal I try to do so. For example if I am trying to prove a<c and I have a hypothesis h : b < cand want to reduce to a < b I will typically do refine lt_trans _ h rather than just applying lt_trans and picking up the pieces later.


Last updated: Dec 20 2023 at 11:08 UTC