apply bug?

Stream: general

[Kevin Buzzard]

@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]

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]

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]

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]

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

[Mario Carneiro]

oh wow

[Mario Carneiro]

exact one_lt_pow (one_lt_two) (by norm_num), works

[Kevin Buzzard]

This won't work in my use case I suspect

[Mario Carneiro]

I suspect it might be the let

[Kevin Buzzard]

yeah

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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]

side note: Is there a way to use set to get the result of the first line?

[Kevin Buzzard]

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

[Mario Carneiro]

I think that produces a let-binding

[Mario Carneiro]

I specifically want a have binding here

[Kevin Buzzard]

Oh sorry I misunderstood. You mean your obtain?

[Mario Carneiro]

so that lean can't accidentally unfold x

[Mario Carneiro]

yes

[Kevin Buzzard]

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

[Mario Carneiro]

oh, you are right, false alarm

[Kevin Buzzard]

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

[Mario Carneiro]

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]

What's the difference between your code and mine?

[Mario Carneiro]

the first line

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

Many thanks.

[Kevin Buzzard]

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

[Kevin Buzzard]

killer codewars question is back on

[Mario Carneiro]

This is still deeply unsettling

[Mario Carneiro]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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