## Stream: maths

### Topic: pow_lt_pow_of_lt golf

#### Kevin Buzzard (Nov 14 2018 at 14:36):

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 (Nov 14 2018 at 14:44):

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

#### Kevin Buzzard (Nov 14 2018 at 14:44):

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 (Nov 14 2018 at 14:45):

linear_ordered_semiring

#### Mario Carneiro (Nov 14 2018 at 14:45):

because we don't have partially ordered semirings

#### Kevin Buzzard (Nov 14 2018 at 14:47):

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 (Nov 14 2018 at 14:51):

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 (Nov 14 2018 at 14:53):

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 (Nov 14 2018 at 14:54):

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

#### Mario Carneiro (Nov 14 2018 at 14:54):

lt_of_pow_lt also has a very short proof using pow_le_pow

#### Mario Carneiro (Nov 14 2018 at 14:55):

The lesson is "use lemmas"

#### Mario Carneiro (Nov 14 2018 at 14:56):

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 (Nov 14 2018 at 14:59):

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 (Nov 14 2018 at 15:00):

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 (Nov 14 2018 at 15:02):

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

#### Kevin Buzzard (Nov 14 2018 at 15:23):

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 (Nov 14 2018 at 15:26):

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 (Nov 14 2018 at 15:29):

explode does this

#### Kevin Buzzard (Nov 14 2018 at 15:29):

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 (Nov 14 2018 at 15:30):

How do I run explode?

found it

#### Mario Carneiro (Nov 14 2018 at 15:34):

ooh, explode actually works pretty well on that proof

#### Kevin Buzzard (Nov 14 2018 at 15:34):

Quick, we need an emoji

#### Kevin Buzzard (Nov 14 2018 at 15:35):

hey #explode is exactly the answer to my question!

:grinning:

#### Kevin Buzzard (Nov 14 2018 at 15:38):

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 (Nov 14 2018 at 15:52):

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 (Nov 14 2018 at 15:54): 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 (Nov 14 2018 at 15:54): I was just about to say that ^ #### Bryan Gin-ge Chen (Nov 14 2018 at 15:55): In this case it's n #### Kevin Buzzard (Nov 14 2018 at 15:59): 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 (Nov 14 2018 at 15:59):

Funky numbering by the way.

#### Bryan Gin-ge Chen (Nov 14 2018 at 16:07):

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 (Nov 14 2018 at 16:07):

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 (Nov 14 2018 at 16:08):

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 (Nov 14 2018 at 16:11):

#explode zmodp.quadratic_reciprocity
-- (deterministic) timeout


boo

#### Bryan Gin-ge Chen (Nov 14 2018 at 16:12):

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 (Nov 14 2018 at 16:13):

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 (Nov 14 2018 at 16:14):

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 (Nov 14 2018 at 16:18):

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

#### Jeremy Avigad (Nov 14 2018 at 16:19):

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 (Nov 14 2018 at 16:20):

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

#### Mario Carneiro (Nov 14 2018 at 16:20):

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

#### Mario Carneiro (Nov 14 2018 at 16:22):

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

#### Kevin Buzzard (Nov 14 2018 at 16:22):

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

yes absolutely

#### Kevin Buzzard (Nov 14 2018 at 16:22):

so...it's upside-down?

#### Mario Carneiro (Nov 14 2018 at 16:23):

well no, it is meant to be read bottom up

#### Mario Carneiro (Nov 14 2018 at 16:23):

but it follows the usual proof order

#### Mario Carneiro (Nov 14 2018 at 16:24):

it is a fitch style proof display

#### Kevin Buzzard (Nov 14 2018 at 16:25):

Thanks a lot for alerting me to it.

#### Bryan Gin-ge Chen (Nov 14 2018 at 16:25):

#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 (Nov 14 2018 at 16:26):

also pp.beta helps sometimes

Last updated: May 14 2021 at 20:13 UTC