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

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

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

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?

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

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