pow_lt_pow_of_lt golf

Stream: maths

[Kevin Buzzard]

variable (x : ℝ) -- or [linear_ordered_field]
theorem pow_lt_pow_of_lt {i j : ℕ} : x > 1 → i < j → x^i < x^j := sorry

Is this in mathlib?

[Mario Carneiro]

all the other versions of this are in group_power.lean, but it looks like this one was missed

[Kevin Buzzard]

nat.pow_lt_pow_of_lt_right : ∀ {x : ℕ}, x > 1 → ∀ {i j : ℕ}, i < j → x ^ i < x ^ j

This should be a theorem about partially ordered semirings or something, right?

[Mario Carneiro]

linear_ordered_semiring

[Mario Carneiro]

because we don't have partially ordered semirings

[Kevin Buzzard]

I spotted this hole this time last year, when I didn't understand the purpose of the mathlib library. At the time, I just figured this was the sort of thing you had to prove yourself, because I had no concept of what "should be there already" (so I proved it in the case I needed it). I understand this concept much better now.

[Mario Carneiro]

here's my proof:

theorem pow_lt_pow {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
lt_of_lt_of_le
  ((lt_mul_iff_one_lt_left (pow_pos (lt_trans zero_lt_one ha) _)).2 ha)
  (pow_le_pow (le_of_lt ha) h)

[Kevin Buzzard]

I'm doing all my own example sheet questions again after last year's attempts. Some of the code I wrote a year ago was absolutely terrible.

Here's the library I wrote this year, to do a question on my problem sheet about n'th roots (n a positive integer)

https://github.com/ImperialCollegeLondon/M1F_example_sheets/blob/master/src/xenalib/real_nth_root.lean

Any stylistic comments or anything would be welcome. I only care about the reals but really that's for stylistic reasons -- I am trying to write a library with a lot of tactic mode proofs so maths students can follow them more easily, and I wanted to make it as simple as possible. Maybe some of this stuff is in mathlib but I understand my own proofs better -- I find them much more readable.

[Mario Carneiro]

My proof differs from yours in the proof strategy, which is most of why it is shorter

[Mario Carneiro]

lt_of_pow_lt also has a very short proof using pow_le_pow

[Mario Carneiro]

The lesson is "use lemmas"

[Mario Carneiro]

And I don't just mean use theorems that have already been proven, I mean arrange the proofs of similar facts to make the best use of commonality

[Mario Carneiro]

your assumptions to lt_of_pow_lt are also stronger than they need to be - it's nice when you can learn this by attempting the proof itself

[Mario Carneiro]

nth_root_unique is reducible in the sense that it has an equality hypothesis - I would prove a lemma which doesn't have that hypothesis first

[Mario Carneiro]

it also factors into x ^ n = y ^ n -> x = y, which should also be in group_power in some generality

[Kevin Buzzard]

here's my proof:

theorem pow_lt_pow {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
lt_of_lt_of_le
  ((lt_mul_iff_one_lt_left (pow_pos (lt_trans zero_lt_one ha) _)).2 ha)
  (pow_le_pow (le_of_lt ha) h)

pow_le_pow (le_of_lt ha) h is a dirty trick, isn't it?

[Kevin Buzzard]

So the reason I have noticed that pow_le_pow trick is because I manually completely unfolded your proof:

theorem pow_lt_pow' {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
begin
  apply lt_of_lt_of_le,
  { exact ((lt_mul_iff_one_lt_left (pow_pos (lt_trans zero_lt_one ha) _)).2 ha)},
  exact (pow_le_pow (le_of_lt ha) h)
end

theorem pow_lt_pow'' {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
begin
  apply lt_of_lt_of_le,
  { refine (lt_mul_iff_one_lt_left _).2 ha,
    refine pow_pos _ _,
    -- got it
    exact lt_trans zero_lt_one ha
  },
  { refine pow_le_pow _ h, -- dirty trick?
    exact le_of_lt ha
  }
end

into a form which I can actually read. Could there be some code which helps me do this unravelling? It is so much easier for me to inspect nodes of the tree when in tactic mode. @Simon Hudon can code do this? Break down some simple class of term mode functions into a tactic proof?

[Mario Carneiro]

explode does this

[Kevin Buzzard]

Even after this breaking-down I still lose information. For example after that first lt_of_lt_of_le -- when I do it in tactic mode I get an extra metavariable goal which Lean has solved in the term mode proof but has not solved in the tactic mode proof. I just want to inspect the metavariable-free goal which is actually proved at each function application I think. How does one do this?

[Kevin Buzzard]

How do I run explode?

[Kevin Buzzard]

found it

[Mario Carneiro]

ooh, explode actually works pretty well on that proof

[Kevin Buzzard]

Quick, we need an emoji

[Kevin Buzzard]

hey #explode is exactly the answer to my question!

[Kevin Buzzard]

:grinning:

[Kevin Buzzard]

import tactic.explode
import algebra.group_power

variables {α : Type*} [linear_ordered_semiring α]
theorem pow_lt_pow {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
lt_of_lt_of_le
  ((lt_mul_iff_one_lt_left (pow_pos (lt_trans zero_lt_one ha) _)).2 ha)
  (pow_le_pow (le_of_lt ha) h)

#explode pow_lt_pow

MWE. Say kids! Understand Mario's proofs in seconds with #explode! Cool name, cool tactic.

[Kevin Buzzard]

variables {α : Type*} [linear_ordered_semiring α]
theorem pow_lt_pow {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) : a ^ n < a ^ m :=
lt_of_lt_of_le
  ( iff.mpr
      ( lt_mul_iff_one_lt_left $
        pow_pos
          ( lt_trans
              zero_lt_one
              ha
          )
          _
      )
      ha
  )
  ( pow_le_pow
      ( le_of_lt $
        ha
      )
      h
  )

Here is another way of taking your proof apart Mario. I have tried to have some sort of a system when unravelling. Is there some sort of name for a form like this? Again I feel like I applied an algorithm. I used $ for functions of one variable and indented for two or more.

How do I tell which term fills the underscore in that proof, by the way? What's the easiest way?

[Reid Barton]

I discovered recently if you replace a _ by a hole {! !} then Lean will give you an error saying there's only one way to fill the hole and tell you what it should be

[Bryan Gin-ge Chen]

I was just about to say that ^

[Bryan Gin-ge Chen]

In this case it's n

[Kevin Buzzard]

theorem pow_lt_pow' {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) :
a ^ n < a ^ m :=
lt_of_lt_of_le -- 14
  ( iff.mpr -- 11
      ( lt_mul_iff_one_lt_left $ -- 10
        pow_pos -- 9 -- takes two inputs
          ( lt_trans -- 8
              zero_lt_one -- 7
              ha -- 5
          )
          _ -- gaargh explode doesn't tell me
      )
      ha -- 5
  )
  ( pow_le_pow -- 13
      ( le_of_lt $ -- 12
        ha -- 5
      )
      h -- 6
  )

I can't immediately see how to fill in that hole using the output of #explode though

[Kevin Buzzard]

Funky numbering by the way.

[Bryan Gin-ge Chen]

This is post-hoc and probably not immediate enough, but first note that the underscore is the second argument to pow_pos (easy to see right away with the bracket colorizer extension), and then compare with the corresponding line of #explode, which says 0 < a ^ n.

[Kevin Buzzard]

Maybe this indentation is better:

import tactic.explode
import algebra.group_power

variables {α : Type*} [linear_ordered_semiring α]
theorem pow_lt_pow' {a : α} {n m : ℕ} (ha : 1 < a) (h : n < m) :
a ^ n < a ^ m :=
lt_of_lt_of_le -- 14
  ( iff.mpr -- 11
      ( lt_mul_iff_one_lt_left  -- 10
        ( pow_pos -- 9 -- takes two inputs
          ( lt_trans -- 8
              zero_lt_one -- 7
            ha -- 5
          )
        _ -- gaargh explode doesn't tell me
        )
      )
    ha -- 5
  )
  ( pow_le_pow -- 13
      ( le_of_lt -- 12
        ha -- 5
      )
    h -- 6
  )

#explode pow_lt_pow'

[Kevin Buzzard]

import tactic.explode
import algebra.group_power

theorem pow_lt_pow'
{α : Type*} -- 0
[linear_ordered_semiring α] -- 1
{a : α} -- 2
{n m : ℕ} -- 3,4
(ha : 1 < a) -- 5
(h : n < m) : -- 6
a ^ n < a ^ m := -- proof starts
lt_of_lt_of_le -- 14
  ( iff.mpr -- 11
      ( lt_mul_iff_one_lt_left  -- 10
        ( pow_pos -- 9
          ( lt_trans -- 8
              zero_lt_one -- 7
            ha) -- 5
        _)) -- gaargh explode doesn't tell me
    ha) -- 5
  ( pow_le_pow -- 13
      ( le_of_lt -- 12
        ha) -- 5
    h) -- 6

#explode pow_lt_pow'

explode covers basically every other line of code

[Kevin Buzzard]

#explode zmodp.quadratic_reciprocity
-- (deterministic) timeout

boo

[Bryan Gin-ge Chen]

Hmm, so the line in the output of #explode corresponding to pow_pos is this:

9 │8    │ pow_pos                │ 0 < a ^ n

Why doesn't the second column read 8,3 (3 is the line corresponding to n : nat)? It's the same whether I put in n or _.

[Mario Carneiro]

Non-propositional arguments are automatically suppressed, because they would otherwise dominate the output and they are inferrable from the (fully elaborated) types in the right column

[Jeremy Avigad]

Wow, explode is really nice. It is great for teaching. I just tried

theorem foo (A B C : Prop) : (A → B → C) → (A ∧ B → C) :=
λ h hab, and.elim hab (λ ha hb, h ha hb)

#explode foo

It made me realize that the proof can be shortened:

theorem foo' (A B C : Prop) : (A → B → C) → (A ∧ B → C) :=
λ h hab, and.elim hab h

The tactic doesn't behave well with have, though.

theorem bar  (A B C : Prop) : A ∧ (B ∨ C) → (A ∧ B) ∨ (A ∧ C) :=
assume h : A ∧ (B ∨ C),
have h₁ : A, from and.left h,
have h₂ : B ∨ C, from and.right h,
or.elim h₂
  (assume h₃ : B,
    or.inl (and.intro h₁ h₃))
  (assume h₃ : C,
    or.inr (and.intro h₁ h₃))

#explore bar

@Mario Carneiro Would it be hard to handle have nicely in the tactic?

[Mario Carneiro]

hm, it's explode not explore but that is also an interesting name

[Jeremy Avigad]

Oops, sorry, I forgot to cut-and-paste that part and added it manually. You are right, it is also a good name.

[Mario Carneiro]

have should be handled well since it will translate to a proof line that is referred to twice

[Mario Carneiro]

what does it look like now? (on my phone)

[Mario Carneiro]

indeed it is best suited to the basic dtt proofs used in intro logic

[Kevin Buzzard]

In general, I think I'd rather read the output from the bottom up when trying to figure out what you're doing.

[Mario Carneiro]

yes absolutely

[Kevin Buzzard]

so...it's upside-down?

[Mario Carneiro]

well no, it is meant to be read bottom up

[Mario Carneiro]

but it follows the usual proof order

[Mario Carneiro]

it is a fitch style proof display

[Kevin Buzzard]

Thanks a lot for alerting me to it.

[Bryan Gin-ge Chen]

#explode bar looks like this now:

bar : ∀ (A B C : Prop), A ∧ (B ∨ C) → A ∧ B ∨ A ∧ C
0│   │ A                                                                                                                     ├ Prop
1│   │ B                                                                                                                     ├ Prop
2│   │ C                                                                                                                     ├ Prop
3│   │ h                                                                                                                     ├ A ∧ (B ∨ C)
4│   │ λ (h₁ : A),
  have h₂ : B ∨ C, from h.right,
  or.elim h₂ (λ (h₃ : B), or.inl ⟨h₁, h₃⟩) (λ (h₃ : C), or.inr ⟨h₁, h₃⟩) │ A → A ∧ B ∨ A ∧ C
5│3  │ and.left                                                                                                              │ A
6│4,5│ ∀E                                                                                                                    │ A ∧ B ∨ A ∧ C

[Mario Carneiro]

also pp.beta helps sometimes