Zulip Chat Archive

Stream: general

Topic: apply bug?


view this post on Zulip 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".

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:26):

oh wow

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:26):

exact one_lt_pow (one_lt_two) (by norm_num), works

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:27):

This won't work in my use case I suspect

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:28):

I suspect it might be the let

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:28):

yeah

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:28):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:30):

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

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:31):

I think that produces a let-binding

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:31):

I specifically want a have binding here

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:31):

Oh sorry I misunderstood. You mean your obtain?

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:31):

so that lean can't accidentally unfold x

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:31):

yes

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:32):

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

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:33):

oh, you are right, false alarm

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:34):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:34):

What's the difference between your code and mine?

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:35):

the first line

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:35):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:36):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:37):

Many thanks.

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:37):

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

view this post on Zulip Kevin Buzzard (Apr 16 2020 at 10:37):

killer codewars question is back on

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:37):

This is still deeply unsettling

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:38):

as far as I can tell, the exact hx line should work with no problems

view this post on Zulip Mario Carneiro (Apr 16 2020 at 10:38):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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