Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

simp_arith: unwanted reduction of atoms due to overloaded vs. nonoverloaded operations #6152

Open
nomeata opened this issue Nov 21, 2024 · 2 comments
Labels
bug Something isn't working P-medium We may work on this issue if we find the time

Comments

@nomeata
Copy link
Collaborator

nomeata commented Nov 21, 2024

In #5384 we found that this blows up with kernel deep recursion:

-- A function that reduced badly, as a canary for kernel reduction
def bad (n : Nat) : Nat :=
  if h : n = 0 then 0 else bad (n / 2)
termination_by n

theorem foo : 2 * bad 42000 = bad 42000 + bad 42000 := by simp_arith

This was fixed in #5708, but abstracting out atoms in the actual proof by reflection.

It turns out that the the fix isn’t complete, as

theorem foo2 : Nat.mul 2 (bad 42000) = Nat.add (bad 42000) (bad 42000) := by simp_arith

and

theorem foo3 : Nat.mul 2 (bad 42000) = Nat.add (bad 42000) (bad 42000) := by
  simp (arith := true) only

still blows up.

Versions

Lean 4.15.0-nightly-2024-11-20

@nomeata nomeata changed the title simp_arith: unwanted reduction of atoms simp_arith: unwanted reduction of atoms due to overloaded vs. nonoverloaded operations Nov 21, 2024
@nomeata
Copy link
Collaborator Author

nomeata commented Nov 21, 2024

I investigated this closer and noticed that it matters whether I use the overloaded or the non-overloaded operations in the type hint. This runs into the kernel recursion again:

theorem foo2 : 2 * bad 42000 = bad 42000 + bad 42000 :=
  of_eq_true
    ((fun (x : Nat) =>
        @id ((Nat.mul 2 x = Nat.add x x) = True) -- NB!
…

And indeed that’s the issue: We cannot leave it to the kernel to proveNat.mul and . * . equal if there are “dangerous“ arguments; both these cause the kernel to run go astray:

theorem foo6 : 2 * bad 42000 = 0         := sorryAx ((Nat.mul 2 (bad 42000) = 0))
theorem foo7 : Nat.mul 2 (bad 42000) = 0 := sorryAx ((2 * (bad 42000) = 0))

(Curious that these pass the elaborator’s defeq check; different heuristics, it seems!)

This raises two questions: What exactly is happening with simp_arith, and doesn’t that mean that simp_arith is broken when the goal contains Nat.mul?

And indeed the latter is true:

theorem foo' : Nat.mul 2 (bad 42000) = Nat.add (bad 42000) (bad 42000) := by simp_arith -- deep recursion

so the bug isn’t fixed properly.

This is what’s happening in simp_arith:

So my fix, by introducing the abstraction and the type hint, had two effects:

  • As long as the goal was using the overloaded functions, the kernel is happy on the “outside”
  • The discrepancy between .denote and .toArith still requires the kernel to do the unfolding, but this is under the abstraction, and the kernel won’t go bad here.

This worked in the cases where the goal uses the overloaded functions, matching the type hint. But we still have a bug if the non-overloaded functions appear in the goal.

A possible fix could be extend the Expr type used by simp_arith to remember if the overloaded or non-overloaded form was used, and use that in the denotation function and the type hint function.

Another possible fix could be to restrict simp_arith to simply only handle the overloaded functions. This is justified since they are the simp normal form, and also omega does that. This is the easier route.

Of course it would be nice if the kernel would simply do the right thing, and not reduce Nat.mul too soon, but I do not know if that is achievable.

@nomeata
Copy link
Collaborator Author

nomeata commented Nov 21, 2024

Ok, the fix doesn’t actually work (see branch joachim/more-5384).

Even if the goal, the denotation function and the type hint all use the plain Nat.add, the kernel will still go astray.

Maybe the problem isn’t fixable outside the kernel, and this reduce_nat reduction (which will whnf its arguments) is too eager, and needs to be delayed until there is no hope of of solving this otherwise.

lbool type_checker::lazy_delta_reduction(expr & t_n, expr & s_n) {
    while (true) {
        lbool r = is_def_eq_offset(t_n, s_n);
        if (r != l_undef) return r;

        if (!has_fvar(t_n) && !has_fvar(s_n)) {
            if (auto t_v = reduce_nat(t_n)) {
                return to_lbool(is_def_eq_core(*t_v, s_n));
            } else if (auto s_v = reduce_nat(s_n)) {
                return to_lbool(is_def_eq_core(t_n, *s_v));
            }
        }

Tricky.


Here is a test case that shows that the too eager evaluation here:

-- A function that reduced badly, as a canary for kernel reduction
def bad (n : Nat) : Nat :=
  if h : n = 0 then 0 else bad (n / 2)
termination_by n

def Nat_mul := @Nat.mul

/-- error: (kernel) deep recursion detected -/
#guard_msgs in
example : Nat_mul 2 (bad 42000) = Nat.mul 2 (bad 42000) := by rfl

/-- error: (kernel) deep recursion detected -/
#guard_msgs in
example : id (Nat.mul 2 (bad 42000)) = Nat.mul 2 (bad 42000) := by rfl

This makes it hard to write any kind of denotation function or even a type hint that would relate to an expression headed by Nat.mul.

@nomeata nomeata added the bug Something isn't working label Nov 21, 2024
@leanprover-bot leanprover-bot added the P-medium We may work on this issue if we find the time label Nov 22, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug Something isn't working P-medium We may work on this issue if we find the time
Projects
None yet
Development

No branches or pull requests

2 participants