deep recursion was detected at 'replace'

Stream: new members

[Kevin Lacker]

example (c : ℕ) (h : 6 * 10 ^ 5 + c = 4 * (10 * c + 6)) : 599976 = 39 * c :=
by linarith

when i try to compile this i get an error saying "deep recursion was detected at 'replace'. potential solution: increase stack space". for other expressions of this form but with smaller numbers, it works fine. is this just, the numbers are too large to handle? any suggestion for what to do about it?

[Rob Lewis]

No, this should be fine. Somehow ring must be triggering kernel reduction on natural number arithmetic (cc @Mario Carneiro ):

example (c : ℕ) : 6 * 10 ^ 5 + c - 4 * (10 * c + 6) + (39 * c - 599976) = 0 := by ring -- deep recursion detected

[Rob Lewis]

It works if you make c an integer (or anything other than a nat pobably).

[Kevin Lacker]

is there a way to jump from, statement x is true about the natural number c, to statement x is true in the integers about c

[Yakov Pechersky]

The zify tactic.

[Kevin Lacker]

aha that's exactly what i wanted! thanks

[Kevin Lacker]

hmm, I'm still getting these deep recursion errors sometimes with integers. for example, this line gets a deep recursion error:

lemma helper (c n : ℤ) (h1 : n = 10 * c + 6) (h2 : 10 ^ 6 ≤ 10 * c) : n ≥ 153846 := by linarith

[Johan Commelin]

But maybe you can help it with a little bit of rewriting, le_trans and norm_num?

[Kevin Lacker]

i'm trying, it's just a lot of rewriting. even this fails: lemma helper (n : ℕ) (h : 1000000 ≤ n) : n ≥ 153846 := by linarith

[Johan Commelin]

First rw h1 and then

calc _ \ge 10 * c : by norm_num
... \ge 10 ^ 6 : h2
... \ge 153846 : by norm_num

[Kevin Lacker]

you can prove 153846 \le 10 ^ 6 by norm_num?

[Kevin Lacker]

well, looks like that works. success

[Mario Carneiro]

Wait, how is ring supposed to prove Rob's goal? It uses nat subtraction

[Rob Lewis]

Oh, good point -- that makes this more curious.

[Mario Carneiro]

Kevin's original goal doesn't use subtraction, so presumably linarith wouldn't have introduced it

[Rob Lewis]

It would have, after zifying. I copied that goal from somewhere in the trace output but it should have had casts in it.

[Rob Lewis]

In the middle of something else, I'll look again in a bit

[Kevin Lacker]

the simplest example of something that I expected to work but did not is: example : 123456 < 1000000 := by linarith

[Kevin Lacker]

norm_num does solve that

[Rob Lewis]

Huh.

constant c : ℕ
axiom h : 39*(c : ℤ) < 599976

#check id_rhs (39*(c : ℤ) + 1 ≤ 599976) h -- deep recursion

[Mario Carneiro]

Who is doing that?

[Mario Carneiro]

I've learned the hard way that you can't rely on definitional unfolding like that going the way you want. If you need to do that unfolding you should apply a lemma that says so

[Rob Lewis]

It's done in linarith, but even applying the lemma seems to cause the same error:

constant c : ℕ
axiom h : 39*(c : ℤ) < 599976

#check int.add_one_le_iff.mpr h -- deep recursion

[Rob Lewis]

There should be no unfolding at all there, or am I missing something?

[Rob Lewis]

attribute [irreducible] int.le fixes it

[Mario Carneiro]

Curiouser:

#check iff.mpr (@int.add_one_le_iff (39*(c : ℤ) : ℤ) 599976) -- deep recursion

[Mario Carneiro]

we haven't even applied h yet

[Mario Carneiro]

This is fine:

#check @iff.mpr _ _ (@int.add_one_le_iff (39*(c : ℤ) : ℤ) 599976)

[Mario Carneiro]

wait, what?

#check h -- deep recursion

[Mario Carneiro]

ah, crap, I know what this is

[Mario Carneiro]

I just remembered that int.lt is defined to be either true or false depending on the result of recursion

[Mario Carneiro]

which means that when you have something of type int.lt something something, it's not immediately obvious that this is even well typed, because it might evaluate to something other than a proposition

[Mario Carneiro]

Basically this is a term for which infer_type blows up

[Mario Carneiro]

No, that's not right. infer_type is fine but to_expr blows up

def c : ℕ := sorry
example (h : @coe ℕ ℤ _ c < 5999) : true :=
by do
  [h] ← tactic.local_context,
  tactic.infer_type h >>= tactic.trace,
  e ← tactic.mk_app `id [h],
  tactic.infer_type e >>= tactic.trace,
  tactic.to_expr ```(h), -- boom
  tactic.admit

[Mario Carneiro]

IIRC linarith uses a lot of pexpr quotations to construct its terms. Maybe it should switch to using instance_cache.mk_app like ring does?

[Rob Lewis]

Arguably it should, but that seems like a heavy change for this weird issue. With Gabriel's type class caching improvements linarith doesn't spend a huge amount of time in type class search, and instance_cache is kind of an inconvenient workaround for things that should be faster natively.

[Rob Lewis]

I'm trying to make int.le irreducible, it's going alright so far.

[Rob Lewis]

#4474

[Rob Lewis]

@Mario Carneiro returning to this:

import tactic.ring
example : (876544 : ℤ) * -1 + (1000000 - 123456) = 0 := by ring -- deep recursion detected

The problem is at type checking time. ring succeeds and produces a proof that infer_type thinks is right, but the kernel doesn't like it. Neither does tactic.type_check. The proof comes mostly from norm_num as you would expect, and using norm_num directly works fine, so I'm a little confused.

[Mario Carneiro]

Aha: If I use this to get the proof that was sent:

example : (9477 : ℤ) * -1 + (10000 - 523) = 0 :=
by do
  [g] ← tactic.get_goals,
  `[ring],
  tactic.trace g

and remove parts to get a MWE, I get this:

example : (9477 : ℤ) * -1 + (10000 - 523) = 0 :=
norm_num.subst_into_add (9477 * -1) (10000 - 523) (-9477) 9477 0
  sorry
  (tactic.ring.unfold_sub 10000 523 9477
     sorry)
  sorry

Here

tactic.ring.unfold_sub : ∀ {α : Type} [_inst_1 : add_group α] (a b c : α), a + -b = c → a - b = c

is used to prove

(10000 - 523 : int) = 9477

[Mario Carneiro]

And sure enough, if I look at the norm_num proof there is a suspicious application of a theorem called

(norm_num.int_sub_hack 10000 523 9477
              (norm_num.sub_pos 10000 523 (-523) 9477 (eq.refl (-523))
...

/-- This is needed because when `a` and `b` are numerals lean is more likely to unfold them
than unfold the instances in order to prove that `add_group_has_sub = int.has_sub`. -/
theorem int_sub_hack (a b c : ℤ) (h : @has_sub.sub ℤ add_group_has_sub a b = c) : a - b = c := h

[Rob Lewis]

That does look suspicious!

[Mario Carneiro]

#4503