pow_mono

Stream: new members

[Jalex Stark]

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]

Hah, do you need this for codewars?

[Jalex Stark]

I'm working on what might become a kata

[Jalex Stark]

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

[Kevin Buzzard]

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]

I think it's pow_le_pow_of_le_left or similar

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

lift

[Kevin Buzzard]

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]

I replaced d>=1 by 0<=d

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Kevin Buzzard]

I am also surprised. @Reid Barton ?

[Kevin Buzzard]

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

[Kevin Buzzard]

I think there is something funny going on.

[Jalex Stark]

oh huh

[Kevin Buzzard]

no, a Lean restart fixed it

[Reid Barton]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Reid Barton]

for me it's quite consistent

[Kevin Buzzard]

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

[Reid Barton]

Yes

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

@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.