Zulip Chat Archive

Stream: new members

Topic: deep recursion was detected at 'replace'


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

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 17:36):

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

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

view this post on Zulip Yakov Pechersky (Oct 05 2020 at 17:50):

The zify tactic.

view this post on Zulip Kevin Lacker (Oct 05 2020 at 17:57):

aha that's exactly what i wanted! thanks

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

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

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

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

view this post on Zulip Kevin Lacker (Oct 05 2020 at 19:09):

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

view this post on Zulip Kevin Lacker (Oct 05 2020 at 19:11):

well, looks like that works. success

view this post on Zulip Mario Carneiro (Oct 05 2020 at 19:45):

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 19:48):

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

view this post on Zulip Mario Carneiro (Oct 05 2020 at 19:58):

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

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 20:00):

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

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

view this post on Zulip Kevin Lacker (Oct 05 2020 at 20:06):

norm_num does solve that

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

view this post on Zulip Mario Carneiro (Oct 05 2020 at 20:35):

Who is doing that?

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

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 20:43):

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

view this post on Zulip Rob Lewis (Oct 05 2020 at 20:45):

attribute [irreducible] int.le fixes it

view this post on Zulip Mario Carneiro (Oct 05 2020 at 21:33):

Curiouser:

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

view this post on Zulip Mario Carneiro (Oct 05 2020 at 21:33):

we haven't even applied h yet

view this post on Zulip Mario Carneiro (Oct 05 2020 at 21:33):

This is fine:

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

view this post on Zulip Mario Carneiro (Oct 05 2020 at 21:37):

wait, what?

#check h -- deep recursion

view this post on Zulip Mario Carneiro (Oct 05 2020 at 21:43):

ah, crap, I know what this is

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

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

view this post on Zulip Mario Carneiro (Oct 05 2020 at 21:48):

Basically this is a term for which infer_type blows up

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

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

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

view this post on Zulip Rob Lewis (Oct 06 2020 at 10:26):

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

view this post on Zulip Rob Lewis (Oct 06 2020 at 11:58):

#4474

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

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

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

view this post on Zulip Rob Lewis (Oct 07 2020 at 11:17):

That does look suspicious!

view this post on Zulip Mario Carneiro (Oct 07 2020 at 11:22):

#4503


Last updated: May 15 2021 at 22:14 UTC