# Zulip Chat Archive

## 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)

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`

?

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

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!

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

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

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

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