Mathlib causes failure in mutual recursive definition

Stream: mathlib4

[Alex Keizer]

I've run into an issue were a mutually recursive definition, without termination_by hint, suddenly fails to compile after importing mathlib.
Here is a MWE

import Mathlib.Algebra.Order.Ring.Canonical
import Mathlib.Data.Nat.Basic

instance : OrderedCancelAddCommMonoid ℕ :=
  { Nat.commSemiring, Nat.linearOrder with
    lt := Nat.lt, add_le_add_left := @Nat.add_le_add_left,
    le_of_add_le_add_left := @Nat.le_of_add_le_add_left,
  }

-- The failure seems specific to that instance, if we have a different instance with `sorry`,
-- then the mutual def below will compile without failure
-- instance : OrderedCancelAddCommMonoid ℕ := sorry

mutual
  inductive Expr : Type
    | add : Nat → Com → Expr
    | zero : Expr

  inductive Com : Type
    | ret : Expr → Com
end


mutual
  -- `fail to show termination`, but only if the `OrderedCancelAddCommMonoid` instance is defined
  def Expr.eval : Expr → Nat
    | .add m c => m + c.eval
    | .zero => 0

  def Com.eval : Com → Nat
    | .ret e => e.eval
end

Oddly enough, the failure is tied to an instance of OrderedCancelAddCommMonoid ℕ. Without this instance, the mutual def compiles, but with the instance, Lean fails to show termination.

For reference, the misbehaving instance is implied by the LinearOrderedCommSemiring ℕ instance in Mathlib.Data.Nat.Order.Basic (so importing that file also causes the error by itself).

The workaround is easy, just adding an explicit termination hint, but I am very curious what is happening here. How does the existence of this typeclass instance cause a failure in the termination checker?

[Scott Morrison]

Briefly: the termination checker is running tactics, and my guess is that the import is changing the simp set, and thus the behaviour of a simp call. Not at a computer now, but have a look at WFTactics.lean in the Lean 4 repository to see the default behaviour.

[Tobias Grosser]

Thank you, @Scott Morrison. That's super helpful.

[Tobias Grosser]

I am currently trying to debug this. I will see if I can install a custom lean build and see if I can dbg_trace this. What I find interesting is that the error message is different from what I expect. I would have expected:

/-- Constructs a proof of decreasing along a well founded relation, by applying
lexicographic order lemmas and using `ts` to solve the base case. If it fails,
it prints a message to help the user diagnose an ill-founded recursive definition. -/
macro "decreasing_with " ts:tacticSeq : tactic =>
 `(tactic|
   (simp_wf
    repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
    repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
    first
    | done
    | $ts
    | fail "failed to prove termination, possible solutions:
  - Use `have`-expressions to prove the remaining goals
  - Use `termination_by` to specify a different well-founded relation
  - Use `decreasing_by` to specify your own tactic for discharging this kind of goal"))

Yet, we get the slightly different one about mutual inductives being the problem.

[Tobias Grosser]

I wonder if there is an easier way to debug this than installing my custom lean4 build and updating the prelude.

[Tobias Grosser]

Could I maybe copy some of the lean4 code in my own file, run some #eval line, and check there if the decreasing_with thing works?

[Sebastian Ullrich]

The elaborator will only show the error message from trying structural recursion (which does not exist for mutuals), you can force it to show the wf error using

termination_by _ x => sizeOf x

[Sebastian Ullrich]

No need to rebuild Lean, you can locally override decreasing_tactic: docs#tacticDecreasing_tactic

[Tobias Grosser]

These are the magic hints. Thank you.

[Sebastian Ullrich]

Combining the termination_by with trace.Meta.Tactic.simp.rewrite suggests that the instance enables an additional rewrite, which might screw up the goal for the remaining tactics

[Tobias Grosser]

OK. I made some mini-progress debugging this. This very example goes through if I add the following theorem:

@[simp]
theorem Nat.zero_lt_one_plus_n {n : Nat}:  0 < 1 + n := by sorry

I am not yet sure where things diverge, but I find it interesting that this trivial identity is not in the mathlib simp set.

[Tobias Grosser]

When trying to proof this identity, simp using:

theorem Nat.zero_lt_succ (n : Nat) : LT.lt 0 (succ n) := succ_le_succ (zero_le n)

does not work.

This is 0 < succ n, which seems to be pretty much 0 < 1 + n. I feel there is only some notation in the way.

[Kevin Buzzard]

succ n is n + 1

[Tobias Grosser]

I see: by rw [Nat.add_comm]; simp works.

[Tobias Grosser]

I am curious what's the mathlib solution to these trivial identities. Should we just rely on linarith or would it make sense to add a simpl lemma that turns 1 + n into n + 1?

[Mario Carneiro]

I think it is not clear when to use non-equalities in the simp set, because almost any theorem could be a simp set candidate in that case

[Mario Carneiro]

it does seem a bit like overfitting to have precisely 0 < 1 + n as a simp lemma

[Tobias Grosser]

In LLVM we an informal canonical form, where we always move constants to the right.

[Mario Carneiro]

what happens if you simp [add_comm]?

[Mario Carneiro]

simp also has a canonical form for AC rewriting, which it uses in permutation rules like this

[Tobias Grosser]

This means, we need to not have rewrites for '0 + m' and 'm + 0', but always first move the 0 to the right.

[Tobias Grosser]

Mario Carneiro said:

what happens if you simp [add_comm]?

This works.

[Mario Carneiro]

but it is not enabled by default, you have to pass add_comm, add_left_comm, add_assoc explicitly

[Tobias Grosser]

Interesting.

[Tobias Grosser]

I guess I was mostly curious why the termination proof broke for such a simple example.

[Tobias Grosser]

I am not sure if there is anything actionable to do in this case.

[Mario Carneiro]

The simp-ish thing used in termination proofs is a bit more powerful and should handle proofs of 0 < 1 + n

[Tobias Grosser]

It seemingly does not, no?

[Mario Carneiro]

because that's exactly the kind of goal that comes up in proofs about sizeOf

[Mario Carneiro]

I think something in the mathlib simp set messed it up

[Tobias Grosser]

OK.

[Tobias Grosser]

If I add @[simp] theorem x {m : Nat}: 0 < 1 + m := by sorry then it works again.

[Mario Carneiro]

without a simp marker?

[Tobias Grosser]

With.

[Tobias Grosser]

I am not sure how to debug this further. I can see that wrong simp lemmas may make simp run into a direction that avoids pattern to be found. But can adding simp lemmas in mathlib make simp less powerful for such a trivial identity?

[Tobias Grosser]

That is interesting.

[Sebastian Ullrich]

My best guess without digging further is that the additional simp lemma uses a representation of 0 that the final simp_arith doesn't recognize

[Mario Carneiro]

The subgoal generated by

set_option trace.Meta.Tactic.simp.rewrite true
mutual
  -- `fail to show termination`, but only if the `OrderedCancelAddCommMonoid` instance is defined
  def Expr.eval : Expr → Nat
    | .add m c => m + c.eval
    | .zero => 0

  def Com.eval : Com → Nat
    | .ret e => e.eval
end
decreasing_by
  simp_wf
  repeat (first | apply Prod.Lex.right | apply Prod.Lex.left)
  repeat (first | apply PSigma.Lex.right | apply PSigma.Lex.left)
  simp (config := { arith := true })
  done

is Zero.zero ≤ m, indicating that the Zero typeclass is causing problems

[Tobias Grosser]

Wow, that really shows me how to debug this.

[Tobias Grosser]

Interestingly, example {m : Nat }: Zero.zero ≤ m := by simp_arith fails with and without the OrderedCalcelAddCommMonoid. Given that this is as canonical as it gets, I guess this should be simplified.

[Tobias Grosser]

Maybe this is relevant: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/0.F0.9F.94.B6.20.28.22zero.20diamond.22.29/near/257669888

[Tobias Grosser]

A diamond between ofNat and Zero

[Tobias Grosser]

OK. I have made some progress. It seems the following can be proven with:

example {m : Nat }: Zero.zero < 1 + m := by
  simp (config := {decide:= false, arith := true}) only [Zero.zero, Nat.zero_eq]

similarly I need

example {m : Nat }: Zero.zero < m + One.one := by
   simp only [Nat.zero_eq, Nat.succ_pos', Zero.zero, One.one]

to prove the following one.

It seems to me I need to include Zero.zero and One.one in my simp set explicitly to make theorems that contain these work. Is this typical. I find that somehow surprising.

[Tobias Grosser]

And indeed, adding attribute [simp] Zero.zero One.one makes the proof reliably go through.

[Scott Morrison]

I think instead you should be writing Zero.zero : ℕ back into 0 : ℕ, etc?

[Tobias Grosser]

What do you mean by

writing Zero.zero : ℕ back into 0 : ℕ,

I interpret that as you asking for a theorem that maps Zero.zero: ℕ back to 0: ℕ. I tested it and the following works as well:

@[simp]
theorem Nat_Zero_eq_zero : (Zero.zero : ℕ) = (0 : ℕ) :=
  by simp [Zero.zero]

@[simp]
theorem Nat_One_eq_one : (One.one: ℕ) = (1 : ℕ) :=
  by simp [One.one]

I am not surprised by it and assumed that @[simp] Zero.zero pretty much would do the same thing. So I suspect I misunderstood and wonder if you maybe meant sth different? In general, I am a little surprised that apparently typeclasses allow us to write statements generic over types that rely on Zero.zero and that smoothly generalize to Nat, and at the same time the typeclass gets in the way of such a trivial identity. I read over https://leanprover.github.io/theorem_proving_in_lean/type_classes.html, but did not find such cases mentioned. Is there maybe a better source to learn about type classes.

[Chris Hughes]

I've done some more investigation. It seems that it is simp { arith := true } that introduces the Zero.zero. This simp { arith := true } also has different behaviour depending on which 0 is used. If the instance OfNat Nat 0 comes via Zero.toOfNat0, then simp { arith := true } fails to prove 0 < 1 + m but it succeeds when the instance is instOfNatNat.

import Mathlib.Algebra.Order.Ring.Canonical
import Mathlib.Data.Nat.Basic

instance : OrderedCancelAddCommMonoid ℕ :=
  { Nat.commSemiring, Nat.linearOrder with
    lt := Nat.lt, add_le_add_left := @Nat.add_le_add_left,
    le_of_add_le_add_left := @Nat.le_of_add_le_add_left,
  }

example (m c : ℕ) : sizeOf c < 1 + m + sizeOf c := by
  simp only [lt_add_iff_pos_left]
  simp (config := { arith := true }) only -- goal is `Zero.zero ≤ m`

example (m : ℕ) : 0 < 1 + m := by
  simp (config := { arith := true }) only --No goals

example (m : ℕ) : (@OfNat.ofNat ℕ 0 (Zero.toOfNat0)) < 1 + m := by
  simp (config := { arith := true }) only -- goal is `Zero.zero ≤ m`

example (m : ℕ) : (@OfNat.ofNat ℕ 0 (instOfNatNat 0)) < 1 + m := by
  simp (config := { arith := true }) only -- No goals

[Chris Hughes]

Where can I see the code for what simp (config := { arith := true }) only does?

[Chris Hughes]

My guess is that the problem is in toLinearExpr in Lean.Meta.Tactic.LinearArith.Nat.Basic

[Tobias Grosser]

It seems @Gabriel Ebner looked into this recently (a year ago)?

[Chris Hughes]

Maybe it's just a case of adding Zero.zero (and One.one) to isNatProjInstin Lean.Meta.Offset

[Chris Hughes]

I think what's going on is the following. Lean sees @OfNat.ofNat ℕ 0 (Zero.toOfNat0). It runs Lean.Meta.Linear.Nat.ToLinear.toLinearExpr. This function then calls isNatProjInst on the head symbol, and it is true because the head symbol is OfNat.ofNat which is in the list given by isNatProjInst. It then runs unfoldProjInst? on this, which I guess is where Zero.zero comes from. It doesn't unfold any further however, because Zero.zero is not in the list given in isNatProjInst.

Adding Zero.zero to the list in unfoldProjInst might fix this, but it seems a little hacky and unstable, because I still don't think it would work if the Zero instance itself came from AddMonoid or something.

[Chris Hughes]

Or maybe unfoldProjInst? is smart enough to keep unfolding in these cases. This seems likely, but I don't fully understand this function.

[Mario Carneiro]

one issue with this is that unfoldProjInst? is defined in lean core and Zero is defined in mathlib

[Chris Hughes]

But it doesn't matter because it's just checking the name. But yes it's ugly

[Chris Hughes]

Maybe Zero has to go back to core

[Chris Hughes]

Or we need an attribute or something that we can mark Zero with this attribute.

[Mario Carneiro]

I don't see why we want to unfold numbers in the first place, that sounds bad?

[Chris Hughes]

It struck me as a little strange to unfold addition to Nat.add and so on.

[Alex Keizer]

Maybe this is a different discussion, but do we even need Zero to be a separate typeclass from OfNat? Could we somehow make it a surface-level alias?

[Mario Carneiro]

yes, we get into diamond issues otherwise

[Tobias Grosser]

Mario Carneiro said:

I don't see why we want to unfold numbers in the first place, that sounds bad?

AFAIU this is all about the following two files. where we aim to turn an Expr into a Nat.Linear.Expr. It seems the algorithm is rather simple. It matches for known constructors, calls unfoldProjInst? if possible and otherwise assumes anything that cannot be unfolded is a parameter. This roughly makes sense to me. @Mario Carneiro I don't fully understand what you said above. Are you saying if let some e ← unfoldProjInst? e then should be completely dropped? I am not yet seeing why this is particularly bad and would avoid introducing Zero.zero.

In particular, I am not yet sure where the Zero.zero actually gets introduced. @Chris Hughes, did you find the line where this happens? unfolding sizeOf certainly does not yield a zero. Does some of the lean code itself introduce the zero?

partial def toLinearExpr (e : Expr) : M LinearExpr := do
  match e with
  | Expr.lit (Literal.natVal n) => return num n
  | Expr.mdata _ e              => toLinearExpr e
  | Expr.const ``Nat.zero ..    => return num 0
  | Expr.app ..                 => visit e
  | Expr.mvar ..                => visit e
  | _                           => addAsVar e
where
  visit (e : Expr) : M LinearExpr := do
    let f := e.getAppFn
    match f with
    | Expr.mvar .. =>
      let eNew ← instantiateMVars e
      if eNew != e then
        toLinearExpr eNew
      else
        addAsVar e
    | Expr.const declName .. =>
      let numArgs := e.getAppNumArgs
      if declName == ``Nat.succ && numArgs == 1 then
        return inc (← toLinearExpr e.appArg!)
      else if declName == ``Nat.add && numArgs == 2 then
        return add (← toLinearExpr (e.getArg! 0)) (← toLinearExpr (e.getArg! 1))
      else if declName == ``Nat.mul && numArgs == 2 then
        match (← evalNat (e.getArg! 0) |>.run) with
        | some k => return mulL k (← toLinearExpr (e.getArg! 1))
        | none => match (← evalNat (e.getArg! 1) |>.run) with
          | some k => return mulR (← toLinearExpr (e.getArg! 0)) k
          | none => addAsVar e
      else if isNatProjInst declName numArgs then
        if let some e ← unfoldProjInst? e then
          toLinearExpr e
        else
          addAsVar e
      else
        addAsVar e
    | _ => addAsVar e

which aims to fill this data-structure:

namespace Nat.Linear
inductive Expr where
  | num  (v : Nat)
  | var  (i : Var)
  | add  (a b : Expr)
  | mulL (k : Nat) (a : Expr)
  | mulR (a : Expr) (k : Nat)
  deriving Inhabited

[Mario Carneiro]

unfolding the OfNat application yields a Zero.zero

[Tobias Grosser]

I was looking at the example (m c : ℕ) : sizeOf c < 1 + m + sizeOf c := by example. unfolding sizeOf does not reach OfNat.

[Mario Carneiro]

there is a mathlib simp lemma taking that goal to 0 < 1 + m

[Tobias Grosser]

Ahhhh

[Mario Carneiro]

where 0 is spelled using an instance chain involving Zero

[Mario Carneiro]

because it's a theorem about additive monoids

[Tobias Grosser]

Ah, now I see. If we use more generic simp lemmas, than Zero.zero will eventually pop up.

[Tobias Grosser]

And then simp (config := { arith := true }) only cannot interpret it.

[Tobias Grosser]

Mario Carneiro said:

I don't see why we want to unfold numbers in the first place, that sounds bad?

How would this help?

[Mario Carneiro]

if we see a OfNat n application, we commit to interpreting the expression as .nat n and assert defeq of the instance to the nat instance, instead of unfolding things

[Tobias Grosser]

That seems to make sense.

[Tobias Grosser]

Thank you.