Strange stack overflow / timeout

Stream: lean4

[Ramon Fernandez Mir]

I've been playing with Lean 4, trying to prove some basic facts about matrices and writing a few tactics. I encountered an issue that I can't quite explain and I'm not sure how to debug. Essentially, what I want is to get cases for every index and then prove inequalities between ground terms whose values come from matrices. I've seen different errors depending on the example I was working with anywhere from stack overflows, cores dumped, or simply timing out. Here's a #mwe that I believe illustrates my issue:

def m : (Fin 2) → (Fin 2) → Int :=
fun i j => #[#[52532234335, -234231224], #[-122223, 29338123232]][i][j]

lemma works : ∀ (x : Fin 2), Int.natAbs (m x x) ≤ 10 ^ 80 := by {
  intros x;
  have h : x = 0 ∨ x = 1 := sorry;
  cases h;
  allGoals (subst x; dec_trivial)
}

lemma doesnot : ∀ (x : Fin 2), Int.natAbs (m x x) ≤ 10 ^ 80 := by {
  intros x;
  obtain ⟨a, b⟩ from x;
  have h : a = 0 ∨ a = 1 := sorry;
  cases h;
  allGoals (subst a; sorry)
  -- allGoals (subst x; dec_trivial) -- stack overflow / timeout
}

I translated dec_trivial from what we had in Lean 3 and obtain I copied from an example somewhere in the docs:

def as_true (c : Prop) [Decidable c] : Prop :=
if c then True else False

lemma of_as_true {c : Prop} [h₁ : Decidable c] (h₂ : as_true c) : c :=
match h₁, h₂ with
| (isTrue h_c),  h₂ => h_c
| (isFalse h_c), h₂ => False.elim h₂

syntax (name := Parser.Tactic.triv) "triv" : tactic

@[tactic triv] def triv : Tactic := fun _ => closeMainGoal (mkConst `trivial)

macro "dec_trivial" : tactic => `(exact (of_as_true (by triv)))

macro "obtain " p:term " from " d:term : tactic =>
`(tactic| match $d:term with | $p:term => ?_)

So somehow, obtain seems to be breaking everything. But then if I make the numbers in the matrix small, everything is fine. Even just removing Int.natAbs in the doesnot lemma, the proof goes through... What am I missing??

[Yakov Pechersky]

dec_trivial is a kernel computation, so it evaluates using unary arithmetic, which will blow up with huge numbers. You want a norm_num there instead

[Gabriel Ebner]

kernel computation, so it evaluates using unary arithmetic

This was in Lean 3. In Lean 4, the kernel evaluation should use GMP as well.

[Yakov Pechersky]

Wonderful! Sorry for the FUD

[Mac]

Ramon Fernandez Mir Sorry, but I am having trouble reproducing this error. Here is the full code I am using:

import Lean
open Lean Elab Tactic

def as_true (c : Prop) [Decidable c] : Prop :=
  if c then True else False

theorem of_as_true {c : Prop} [h₁ : Decidable c] (h₂ : as_true c) : c :=
  match h₁, h₂ with
  | (isTrue h_c),  h₂ => h_c
  | (isFalse h_c), h₂ => False.elim h₂

syntax (name := Parser.Tactic.triv) "triv" : tactic

@[tactic Parser.Tactic.triv] def triv : Tactic :=
  fun _ => closeMainGoal (mkConst `trivial)

macro "dec_trivial" : tactic => `(exact (of_as_true (by triv)))

macro "obtain " p:term " from " d:term : tactic =>
`(tactic| match $d:term with | $p:term => ?_)

def m : (Fin 2) → (Fin 2) → Int :=
fun i j => #[#[52532234335, -234231224], #[-122223, 29338123232]][i][j]

theorem works : ∀ (x : Fin 2), Int.natAbs (m x x) ≤ 10 ^ 80 := by {
  intros x;
  have h : x = 0 ∨ x = 1 := sorry;
  cases h;
  allGoals (subst x; dec_trivial)
}

theorem doesnot : ∀ (x : Fin 2), Int.natAbs (m x x) ≤ 10 ^ 80 := by {
  intros x;
  obtain ⟨a, b⟩ from x;
  have h : a = 0 ∨ a = 1 := sorry;
  cases h;
  allGoals (subst a; admit)
  allGoals (subst x; dec_trivial) -- stack overflow / timeout
}

It works for me (the last line completes successfully and nothing breaks).

[Mac]

One a somewhat unrelated note, I do not understand why the definition of of_as_true was written to match on both h₁ and h₂ when it only really matches against is h₁. Also, the parentheses in the match seem unnecessary (but that could easily be an artifact from translating this from Lean 3).

[Mac]

Ah, now that I think about it. What version of Lean 4 are you using?

[Mac]

Have you tried testing this on the latest nightly?

[Jannis Limperg]

Mac said:

One a somewhat unrelated note, I do not understand why the definition of of_as_true was written to match on both h₁ and h₂ when it only really matches against is h₁. Also, the parentheses in the match seem unnecessary (but that could easily be an artifact from translating this from Lean 3).

I think this is to ensure that the case split on h1 gets propagated into the type of h2. Lean 4 has match (generalizing := true) for this afair.

[Mac]

Jannis Limperg said:

I think this is to ensure that the case split on h1 gets propagated into the type of h2. Lean 4 has match (generalizing := true) for this afair.

Ah. And, of I am not mistaken, generalizing := true is the default for Prop.

[Mac]

Regardless, in Lean 4, this definition does work:

theorem of_as_true {c : Prop} [h₁ : Decidable c] (h₂ : as_true c) : c :=
  match h₁ with
  | isTrue h_c  => h_c
  | isFalse h_c => False.elim h₂

[Ramon Fernandez Mir]

Mac said:

Have you tried testing this on the latest nightly?

Yes and still can't solve it...

[Ramon Fernandez Mir]

In general though, how can I debug an issue like this one? How can I get some sort of execution trace?

[Mario Carneiro]

One thing that helps is to minimize the example. Remove everything that doesn't contribute to the bug. If it has to do with kernel computation then you can probably get it down to example : ... := by dec_trivial

[Mac]

Ramon Fernandez Mir said:

Yes and still can't solve it...

Ah. Sorry that I can't help more since I can't reproduce it. One thing I would try is all positive or all negative numbers (especially since it might have something to do with Int.natAbs).

[Ramon Fernandez Mir]

Mario Carneiro said:

One thing that helps is to minimize the example. Remove everything that doesn't contribute to the bug. If it has to do with kernel computation then you can probably get it down to example : ... := by dec_trivial

So I managed to find an even simpler example that hangs:

def m : (Fin 2) → (Fin 2) → Int :=
fun i j => #[#[0, 0], #[0, 100000000]][i][j]

theorem simpler (h : 1 < 2) : Int.natAbs (m ⟨1, h⟩ ⟨1, h⟩) ≤ 100000000 :=
by dec_trivial

This is on a fresh project running on lean 4.0.0-nightly-2021-07-14. Also, if you make the numbers small, it works. If you replace the ⟨1, h⟩ by simply 1, it works. And removing Int.natAbs also makes it work. So quite mysterious altogether.

[Mac]

Yay, that worked. I can finally reproduce this! :)

[Mac]

I was able to get the stack overflow with this cut-down example as well:

def as_true (c : Prop) [Decidable c] : Prop :=
  if c then True else False

theorem of_as_true {c : Prop} [h₁ : Decidable c] (h₂ : as_true c) : c :=
  match h₁ with
  | isTrue h_c  => h_c
  | isFalse h_c => False.elim h₂

def n := 100000000

def m : (Fin 2) → (Fin 2) → Int :=
fun i j => #[#[0, 0], #[0, n]][i][j]

theorem simpler (h : 1 < 2) : Int.natAbs (m ⟨1,h⟩ ⟨1,h⟩) ≤ n :=
of_as_true trivial -- stack overflow

[Mac]

The processing time increases as the order of magnitude of n increases. Thus, @Yakov Pechersky appears to be right, the kernel is for some reason doing unary arithmetic, causing the stack blow-up.

[Mac]

Given that this doesn't occur when Int.natAbs is absent or the ⟨1,h⟩ is replaced with 1, I would assume this has to do with the kernel not realizing that Int.natAbs (m ⟨1,h⟩ ⟨1,h⟩) is a computable Nat (and, more generally, that the less than is decidable through computation) and is thus relying on its logical representation (rather than its computable one).

[Mac]

Note that decide fails in with ⟨1,h⟩ but not with 1:

theorem decide1 (h : 1 < 2) : Int.natAbs (m ⟨1,h⟩ ⟨1,h⟩) ≤ n :=
by decide
/--
expected type must not contain free or meta variables
  Int.natAbs (m { val := 1, isLt := h } { val := 1, isLt := h }) ≤ n
-/

-- the `h` parameter is irrelevant
theorem decide2 (h : 1 < 2) : Int.natAbs (m 1 1) ≤ n :=
by decide -- works

[Mac]

However, decide still fails without Int.natAbs while the of_as_true trivial does not:

theorem decide3 (h : 1 < 2) : m ⟨1,h⟩ ⟨1,h⟩ ≤ n :=
by decide
/--
expected type must not contain free or meta variables
  m { val := 1, isLt := h } { val := 1, isLt := h } ≤ Int.ofNat n
-/

theorem simpler3 (h : 1 < 2) : m ⟨1,h⟩ ⟨1,h⟩ ≤ n :=
of_as_true trivial -- works

So it is clear that decide is getting caught up on the h.

[Mac]

My biggest confusion is thus why m ⟨1,h⟩ ⟨1,h⟩ ≤ n works (with of_as_true trivial). Based on the behavior with decide, I would expect it to break as well.

[Mario Carneiro]

The kernel representation can compute this though, so I would expect it to work

[Mario Carneiro]

That is, lean 3 #reduce would work on this even without any fancy kernel nats

[Mario Carneiro]

Here it is minimized some more:

def n := 30000
theorem simpler (h : True) : Nat.ble ((fun _ => n) h) n = true := rfl

(The number has been reduced so that it is long enough to be noticeable without bricking your machine)

[Mario Carneiro]

My guess is that at this point, lean's defeq heuristics say to unfold Nat.ble instead of the beta redex, after which point it loses the ability to take advantage of the kernel computation

[Daniel Selsam]

(deleted)

[Mario Carneiro]

The check to not reduce open terms is correct here by the way; even if it's a prop, it can be a false assumption, in which case the compiled code could go off the rails

[Mario Carneiro]

well, even closed terms can have that issue in the presence of axioms

[Daniel Selsam]

@Mario Carneiro This commit fixes the performance issue: https://github.com/dselsam/lean4/commit/6ced516e6acb8cf038b2e9a1d2c87a1a6497bef8 I may be missing something obvious but I don't see why it would be unsound -- reduce_nat only does built-in operations on terms that actually reduce to nat literals.

[Mario Carneiro]

I think you are right

[Mario Carneiro]

although that check in reduce_nat is probably a perfomance optimization since it's a lot easier to check the has_fvar bit on an expression than see whether it is nat.succ, nat.add etc

[Mac]

Daniel Selsam said:

reduce_nat only does built-in operations on terms that actually reduce to nat literals.

But couldn't that still be a problem? For example:

axiom h : 300 < 256
def n : UInt8 := ⟨300,h⟩
#eval n -- 44

n is still a nat literal -- it just happens to be the wrong nat literal. I imagine this could cause unsoundness in a more sophisticated example.

[Mario Carneiro]

n doesn't reduce to 44 though

[Mario Carneiro]

It's also not a nat literal

[Mario Carneiro]

n.1 has type Nat, and it whnf-reduces to a nat literal, namely 300, and it is provably equal to 44 but I don't think you can make it reduce to 44

[Mac]

Well, this crashes with max recursion:

axiom h : 300 < 256
def n : UInt8 := ⟨300,h⟩
def n' := n + 1
#reduce n'
/-
maximum recursion depth has been reached
(use `set_option maxRecDepth <num>` to increase limit)
-/

Is that expected?

[Mac]

Oh, apparently that just always happens:

def n : UInt8 := 0
def n' := n + 0
#reduce n' -- same error

Is this expected?

[Daniel Selsam]

It does not seem surprising -- calling reduce on a proof isn't usually a good idea. Note that there is a TODO in the code to allow #reduce to take additional arguments e.g. to avoid reducing proofs https://github.com/leanprover/lean4/blob/master/src/Lean/Elab/BuiltinCommand.lean#L222-L224

[Mac]

Ah so it is trying to reduce the isLt proof of UInt8 and that is causing the crash. Makes sense.