## Stream: new members

### Topic: deep recursion was detected at 'replace'

#### Kevin Lacker (Oct 05 2020 at 17:30):

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 (Oct 05 2020 at 17:36):

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 (Oct 05 2020 at 17:36):

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

#### Kevin Lacker (Oct 05 2020 at 17:40):

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 (Oct 05 2020 at 17:50):

The zify tactic.

#### Kevin Lacker (Oct 05 2020 at 17:57):

aha that's exactly what i wanted! thanks

#### Kevin Lacker (Oct 05 2020 at 19:01):

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 (Oct 05 2020 at 19:04):

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

#### Kevin Lacker (Oct 05 2020 at 19:05):

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 (Oct 05 2020 at 19:07):

First rw h1 and then

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


#### Kevin Lacker (Oct 05 2020 at 19:09):

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

#### Kevin Lacker (Oct 05 2020 at 19:11):

well, looks like that works. success

#### Mario Carneiro (Oct 05 2020 at 19:45):

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

#### Rob Lewis (Oct 05 2020 at 19:48):

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

#### Mario Carneiro (Oct 05 2020 at 19:58):

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

#### Rob Lewis (Oct 05 2020 at 20:00):

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 (Oct 05 2020 at 20:00):

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

#### Kevin Lacker (Oct 05 2020 at 20:06):

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

#### Kevin Lacker (Oct 05 2020 at 20:06):

norm_num does solve that

#### Rob Lewis (Oct 05 2020 at 20:17):

Huh.

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

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


#### Mario Carneiro (Oct 05 2020 at 20:35):

Who is doing that?

#### Mario Carneiro (Oct 05 2020 at 20:41):

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 (Oct 05 2020 at 20:43):

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 (Oct 05 2020 at 20:43):

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

#### Rob Lewis (Oct 05 2020 at 20:45):

attribute [irreducible] int.le fixes it

#### Mario Carneiro (Oct 05 2020 at 21:33):

Curiouser:

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


#### Mario Carneiro (Oct 05 2020 at 21:33):

we haven't even applied h yet

#### Mario Carneiro (Oct 05 2020 at 21:33):

This is fine:

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


#### Mario Carneiro (Oct 05 2020 at 21:37):

wait, what?

#check h -- deep recursion


#### Mario Carneiro (Oct 05 2020 at 21:43):

ah, crap, I know what this is

#### Mario Carneiro (Oct 05 2020 at 21:43):

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

#### Mario Carneiro (Oct 05 2020 at 21:45):

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 (Oct 05 2020 at 21:48):

Basically this is a term for which infer_type blows up

#### Mario Carneiro (Oct 05 2020 at 21:55):

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


#### Mario Carneiro (Oct 05 2020 at 21:57):

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 (Oct 06 2020 at 10:25):

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 (Oct 06 2020 at 10:26):

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

#4474

#### Rob Lewis (Oct 07 2020 at 10:57):

@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 (Oct 07 2020 at 11:12):

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 (Oct 07 2020 at 11:14):

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 (Oct 07 2020 at 11:17):

That does look suspicious!

#### Mario Carneiro (Oct 07 2020 at 11:22):

#4503

Last updated: May 15 2021 at 22:14 UTC