# Zulip Chat Archive

## Stream: general

### Topic: apply bug?

#### Kevin Buzzard (Apr 16 2020 at 09:56):

@Scott Morrison was asking what the apply bug was here. I just ran into what I think might be a pretty hideous manifestation of it (but might be something else):

import algebra.group_power -- proof is irrelevant lemma one_lt_pow {x : ℤ} (hx : 1 < x) {n : ℕ} (hn : 0 < n) : 1 < x^n := begin cases n with n, cases hn, clear hn, induction n with d hd, rw pow_one, exact hx, rw pow_succ, apply one_lt_mul, exact le_of_lt hx, exact hd, end #check one_lt_pow -- one_lt_pow : 1 < ?M_1 → ∀ {n : ℕ}, 0 < n → 1 < ?M_1 ^ n example : 1 < (2 : ℤ)^222 := begin -- refine one_lt_pow _ _, -- <- works fine apply one_lt_pow, -- <- disaster /- deep recursion was detected at 'replace' (potential solution: increase stack space in your system) -/ end

I think `apply`

might be trying to unify 2^222 with "forall n,..." or something? In practice this is a horrible error because the failure is immediate and (in my case) the red line was a long way further down; it just looked to me like Lean had "switched off".

#### Mario Carneiro (Apr 16 2020 at 10:01):

I think `lt`

on `int`

is defined by cases such that it reduces to `true`

or `false`

. So if you attempt to use whnf on it it will fully reduce the arguments

#### Kevin Buzzard (Apr 16 2020 at 10:21):

My problems are much worse than I thought. @Mario Carneiro can you fill in the sorry below?

import algebra.group_power tactic.norm_num lemma one_lt_pow {x : ℤ} (hx : 1 < x) {n : ℕ} (hn : 0 < n) : 1 < x^n := begin cases n with n, cases hn, clear hn, induction n with d hd, rw pow_one, exact hx, rw pow_succ, apply one_lt_mul, exact le_of_lt hx, exact hd, end theorem simple : true := begin let x : ℤ := 2^222, have hx : 1 < x := one_lt_pow (one_lt_two) (by norm_num), have hx2 : 1 < x^222, { refine one_lt_pow _ (by norm_num), /- x : ℤ := 2 ^ 222, hx : 1 < x ⊢ 1 < x -/ sorry }, trivial end

#### Kevin Buzzard (Apr 16 2020 at 10:22):

With `pp.all`

on it's

hx : @has_lt.lt.{0} int int.has_lt (@has_one.one.{0} int int.has_one) x ⊢ @has_lt.lt.{0} int int.has_lt (@has_one.one.{0} int int.has_one) x

but `exact hx`

gives me `deep recursion was detected at 'replace' (potential solution: increase stack space in your system)`

#### Kevin Buzzard (Apr 16 2020 at 10:24):

I'm on 3.7.2 if this makes any difference, with the mathlib commit from codewars

#### Mario Carneiro (Apr 16 2020 at 10:26):

oh wow

#### Mario Carneiro (Apr 16 2020 at 10:26):

`exact one_lt_pow (one_lt_two) (by norm_num),`

works

#### Kevin Buzzard (Apr 16 2020 at 10:27):

This won't work in my use case I suspect

#### Mario Carneiro (Apr 16 2020 at 10:28):

I suspect it might be the `let`

#### Kevin Buzzard (Apr 16 2020 at 10:28):

yeah

#### Kevin Buzzard (Apr 16 2020 at 10:28):

There's no weird tactic which is better than `exact`

?

#### Kevin Buzzard (Apr 16 2020 at 10:29):

In your solution you're making a second proof of 1<x, I want to use `hx`

#### Mario Carneiro (Apr 16 2020 at 10:30):

ah, this is interesting:

theorem simple : true := begin obtain ⟨x, x_def⟩ : ∃ x, x = 2^222 := ⟨_, rfl⟩, have hx : 1 < x, { rw [x_def], exact one_lt_pow (one_lt_two) (by norm_num), -- invalid type ascription, term has type -- 1 < 2 ^ ?m_1 -- but is expected to have type -- 1 < 2 ^ 222 } end

#### Mario Carneiro (Apr 16 2020 at 10:30):

side note: Is there a way to use `set`

to get the result of the first line?

#### Kevin Buzzard (Apr 16 2020 at 10:30):

`set x : Z := 2^222 with hx`

?

#### Mario Carneiro (Apr 16 2020 at 10:31):

I think that produces a let-binding

#### Mario Carneiro (Apr 16 2020 at 10:31):

I specifically want a have binding here

#### Kevin Buzzard (Apr 16 2020 at 10:31):

Oh sorry I misunderstood. You mean your `obtain`

?

#### Mario Carneiro (Apr 16 2020 at 10:31):

so that lean can't accidentally unfold `x`

#### Mario Carneiro (Apr 16 2020 at 10:31):

yes

#### Kevin Buzzard (Apr 16 2020 at 10:32):

Note that you switched to nat. I don't know if this is relevant.

#### Mario Carneiro (Apr 16 2020 at 10:33):

oh, you are right, false alarm

#### Kevin Buzzard (Apr 16 2020 at 10:34):

have h : ∃ x : ℤ, x = 2^222 := ⟨_, rfl⟩, cases h with x x_def,

#### Mario Carneiro (Apr 16 2020 at 10:34):

this works fine:

theorem simple : true := begin obtain ⟨x, x_def⟩ : ∃ x : ℤ, x = 2^222 := ⟨_, rfl⟩, have hx : 1 < x, { rw [x_def], exact one_lt_pow (one_lt_two) (by norm_num) }, have hx2 : 1 < x^222, { refine one_lt_pow _ (by norm_num), exact hx, }, trivial end

#### Kevin Buzzard (Apr 16 2020 at 10:34):

What's the difference between your code and mine?

#### Mario Carneiro (Apr 16 2020 at 10:35):

the first line

#### Kevin Buzzard (Apr 16 2020 at 10:35):

(other than the fact that yours works ;-) )

#### Mario Carneiro (Apr 16 2020 at 10:35):

In your code, `x`

is a let binding, which means that lean can choose to unfold it whenever it wants

#### Mario Carneiro (Apr 16 2020 at 10:36):

in mine it is a variable, which cannot be unfolded and where you only get an equality to the real value via `x_def`

#### Mario Carneiro (Apr 16 2020 at 10:36):

this makes it more controllable, since lean will fail instead of go on a wild goose chase on a bad application

#### Kevin Buzzard (Apr 16 2020 at 10:36):

Oh this is great, it works in my use case too :D

#### Kevin Buzzard (Apr 16 2020 at 10:37):

Many thanks.

#### Kevin Buzzard (Apr 16 2020 at 10:37):

Many thanks indeed, in fact; I would never have undone this myself.

#### Kevin Buzzard (Apr 16 2020 at 10:37):

killer codewars question is back on

#### Mario Carneiro (Apr 16 2020 at 10:37):

This is still deeply unsettling

#### Mario Carneiro (Apr 16 2020 at 10:38):

as far as I can tell, the `exact hx`

line should work with no problems

#### Mario Carneiro (Apr 16 2020 at 10:38):

there is no need to unfold anything as it's a syntactic match

#### Mario Carneiro (Apr 16 2020 at 10:43):

Here is a simplified version:

set_option trace.type_context.is_def_eq true theorem simple : true := begin let x : ℤ := 2^222, have hx : 1 < x := sorry, have hx2 : 1 < x := hx, end

#### Mario Carneiro (Apr 16 2020 at 10:45):

I think I remember something trying a whnf on the top level when giving the types of terms, maybe to get the universe level? The problem is that `1 < x`

is defeq to `true`

, but the proof of this is too long

#### Mario Carneiro (Apr 16 2020 at 10:53):

This version works with no imports

theorem simple : true := begin let x : ℤ := (((*) 2)^[222]) (1:ℤ), have hx : 1 < x := sorry, have hx2 := hx, trivial end

#### Mario Carneiro (Apr 16 2020 at 10:53):

I can't find anything suspicious in the traces, I think this requires C++ debugging

Last updated: May 16 2021 at 21:11 UTC