Is there a theorem about `k > 0 -> n < m -> n^k < m^k`?

Stream: new members

[R Dong]

I am not sure if this is not available or I am not searching for documents correctly. There's something very similar but with \le instead

[Alex Mobius]

I'm just wrong it seems

[Kevin Buzzard]

Can you formalise the statement in Lean with a #mwe? I can't even read the statement you're talking about because it's only present in the title of the thread and on mobile it's hard to see this.

[Alex Mobius]

Really depends on the variable types, I'm assuming n and m are also positive in your case. If it's just all nats, then https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/Order/Ring/Basic.html#pow_lt_pow_left

[R Dong]

Sorry, it's this:

(n m k : Nat) : n < m -> n ^ k < m ^ k

[Alex Mobius]

What's k?

[R Dong]

Also a Nat (updated)

[Alex Mobius]

Then see link above.

[R Dong]

Yeah, I am trying to apply the theorem. It says it can't synthesize StrictOrderedSemiring

[Damiano Testa]

If you change > to ≠, then exact? should find the lemma for you.

[Alex Mobius]

It's not exact, it's of a different shape. @R Dong please post your code, we would be able to help you better. I cannot reproduce your error.

[R Dong]

lemma nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  induction c with
  | zero =>
    simp
    rw [← Nat.pow_one 2]
    apply Nat.pow_lt_pow_of_lt
    simp
    rw [Nat.add_assoc, Nat.add_left_comm]
    apply Nat.lt_add_of_pos_right
    apply Nat.zero_lt_of_ne_zero
    rw [Nat.add_succ]
    apply Nat.succ_ne_zero
  | succ c' ihc =>
    apply lt_trans ihc
    apply pow_lt_pow_left (c' + 2 < c' + 3)

[Damiano Testa]

This is what I meant:

import Mathlib

example (n m k : Nat) : k ≠ 0 -> n < m -> n ^ k < m ^ k := by
  exact?

[R Dong]

exact? gives me nothing, but apply? have some suggestions using refine. I've not really learned about refine though

[R Dong]

Yeah, I solved it with refine. I need to figure out what it does

[R Dong]

I am checking understanding here: if I have a theorem of P -> Q -> R and R as a goal, should apply turn the goal into P and Q?

[Alex Mobius]

@R Dong refine is like exact, but you can leave "holes" in the expression. It's going to match the expression exactly, but where holes are, parts of expression will be pulled out as new goals.
Holes look like ?_ or '?goal_name' if you like to name your goals.

[R Dong]

Ok

[Alex Mobius]

What "apply" does to a goal is it tries to match the "tail end" of an expression (splitting by arrows) to your goals, and all the arguments are pulled out as new goals.

[Alex Mobius]

so yes, applied to a proposition, it pulls out premises, but you can apply arbitrary functions and foralls and whatnot

[R Dong]

So I got it with this:

lemma nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  induction c with
  | zero =>
    simp
    rw [← Nat.pow_one 2]
    apply Nat.pow_lt_pow_of_lt
    simp
    rw [Nat.add_assoc, Nat.add_left_comm]
    apply Nat.lt_add_of_pos_right
    apply Nat.zero_lt_of_ne_zero
    rw [Nat.add_succ]
    apply Nat.succ_ne_zero
  | succ c' ihc =>
    apply lt_trans ihc
    refine Nat.pow_lt_pow_left ?succ.h ?succ.a
    apply Nat.lt_succ_self
    apply Nat.add_one_ne_zero

[Alex Mobius]

If you're doing math, rather than learning tactics, here's a simpler proof:

import Mathlib

theorem nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  ring_nf

[R Dong]

I don't know it existed

[Damiano Testa]

Alex Mobius said:

If you're doing math, rather than learning tactics, here's a simpler proof:

import Mathlib

theorem nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  ring

This proof still requires some work.

[Alex Mobius]

My bad, fixed now!

[Damiano Testa]

Alex Mobius said:

My bad, fixed now!

Are you saying that this is a complete proof, or simply that it takes you to a position from which you can then conclude?

[Alex Mobius]

No, I'm just particularly inattentive/reckless today, it seems. Here's the actual proof:

import Mathlib

example (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  simp_arith
  calc
    3   ≤ 16 := by decide
    _   <= 2^4 := by rfl
    _   ≤ (c+2)^4 := by apply Nat.pow_le_pow_left; simp
    _   ≤ (c+2)^(n+4)  := by apply Nat.pow_le_pow_right <;> simp

[Damiano Testa]

You can also shorten it a little:

theorem nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) :=
  (Nat.le_add_left 2 c).trans_lt <| lt_self_pow c.one_lt_succ_succ (Nat.one_lt_succ_succ _)

[Alex Mobius]

Arguably less readable!

[R Dong]

How did you learn all these tactics

[Kevin Buzzard]

You only need one tactic :-)

import Mathlib

theorem nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) : 2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  calc 2 < 2 ^ 4 := by omega
  _      ≤ 2 ^ (n + 4) := pow_le_pow_right₀ (by omega) (by omega)
  _      ≤ (c + 2) ^ (n + 4) := Nat.pow_le_pow_left (by omega) _

[Alex Mobius]

XD

[R Dong]

When I came out of tutorials I basically just know rfl, rw, apply, repeat, induction, cases, assumption and exact

[Alex Mobius]

sledgehammer x4 combo

[Alex Mobius]

Well, I learn new tactics mostly from aesop? and new lemmas mostly from simp?, but also there's https://hrmacbeth.github.io/math2001/Index_of_Tactics.html and now also https://lean-lang.org/doc/reference/latest/Tactic-Proofs/Tactic-Reference/#tactic-ref-search

[Kevin Buzzard]

There are only a finite number of tactics and if you just keep practicing you pick them up. The ones I use in my course are here https://www.ma.imperial.ac.uk/~buzzard/xena/formalising-mathematics-2024/Part_C/Part_C.html

[R Dong]

I don't have a course in my university so basically I am on my own

[Alex Mobius]

Well, here are two excellent courses linked for you, and TPIL I assume you've read

[R Dong]

I've read FPIL

[Alex Mobius]

Well, TPIL is a much better source for proofs, mathematical or otherwise, but especially mathematical.

[R Dong]

Well, I can try it again

[Heather Macbeth]

Kevin Buzzard said:

You only need one tactic :-)

Or two tactics and no lemmas :-)

theorem nat_2_lt_c_plus_2_pow_n_plus_4 (n c : Nat) :
    2 < (c + 1 + 1) ^ (n + 1 + 3) := by
  calc 2 < 2 ^ 4 := by omega
  _      ≤ 2 ^ (n + 4) := by gcongr <;> omega
  _      ≤ (c + 2) ^ (n + 4) := by gcongr; omega

[Alex Mobius]

Right, gcongr, I was trying to remember that one.