maxRecDepth on simp [reduceOfInt]

Stream: lean4

[Tobias Grosser]

The following simp call fails for me:

-- set_option maxRecDepth 1600
theorem test2 (e : (BitVec 1023)) :
    some 0#1023 =
    if (BitVec.ofInt 1023 (-70368744177664) &&& 70368040490200#1023 != 0)
      then none else none := by
  /-
  tactic 'simp' failed, nested error:
  maximum recursion depth has been reached
  use `set_option maxRecDepth <num>` to increase limit
  use `set_option diagnostics true` to get diagnostic information
  -/
  simp only [BitVec.reduceOfInt]

[Tobias Grosser]

and can be fixed with a sufficiently large maxRecDepth of 1600.

[Tobias Grosser]

AFAIU this should not happen.

[Tobias Grosser]

[reduction] unfolded declarations (max: 1536, num: 2): ▼
  [] Nat.rec ↦ 1536
  [] Nat.pow ↦ 1534
[reduction] unfolded reducible declarations (max: 1536, num: 1): ▼
  [] Nat.casesOn ↦ 1536

[Tobias Grosser]

The elaboration time with maxRecDepth increased is fast, but setting this globally triggers timeouts in other parts of my project.

[Tobias Grosser]

Any ideas how to debug this best?

[Henrik Böving]

With

theorem test2 (e : (BitVec 1023)) :
    some 0#1023 =
    if (BitVec.ofInt 1023 (-70368744177664) &&& 70368040490200#1023 != 0)
      then none else none := by
  set_option trace.Meta.Tactic.simp true in
  simp (config:={failIfUnchanged := false}) only [BitVec.reduceOfInt]

we get:

[Meta.Tactic.simp.unify] eq_self:1000, failed to unify
      ?a = ?a
    with
      (89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944#1023 &&&
            70368040490200#1023 !=
          0) =
        true

[Meta.Tactic.simp.unify] eq_self:1000, failed to unify
      ?a = ?a
    with
      (89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944#1023 &&&
            70368040490200#1023 !=
          0) =
        true

eq_self is one of the simp only builtins

looking at the trace of the unifier:

theorem test2 (e : (BitVec 1023)) :
    some 0#1023 =
    if (BitVec.ofInt 1023 (-70368744177664) &&& 70368040490200#1023 != 0)
      then none else none := by
  set_option trace.Meta.isDefEq true in
  simp (config:={failIfUnchanged := false}) only [BitVec.reduceOfInt]

there seems to be a query at the end that goes bad:

[Meta.isDefEq] ✅️ if ?b then ?x
    else ?y =?= if (BitVec.ofInt 1023 (-70368744177664) &&& 70368040490200#1023 != 0) = true then none else none ▶

[Meta.isDefEq] ❌️ ?a =
      ?a =?= (89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944#1023 &&&
          70368040490200#1023 !=
        0) =
      true ▶

[Meta.isDefEq] ❌️ ?a =
      ?a =?= (89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944#1023 &&&
          70368040490200#1023 !=
        0) =
      true ▶

[Meta.isDefEq] ✅️ ?c =?= (89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944#1023 &&&
          70368040490200#1023 !=
        0) =
      true ▶

[Meta.isDefEq] 💥️ ?h₁ =?= Eq.refl
      ((89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944#1023 &&&
            70368040490200#1023 !=
          0) =
        true) ▶

Unfodling this trace it unfolds everything to:

 match -70368744177664 % Int.ofNat (2 ^ 1023) with
    | Int.ofNat n => n
    | Int.negSucc a =>
      0 =?= 89884656743115795386465259539451236680898848947115328636715040578866337902750481566354238661203768010560056939935696678829394884407208311246423715319737062188883946712432742638151109800623047059726541476042502884419075341171231440736956555270413618581675255342293149119973622969239858152417678094443367890944 %
      2 ^ 1023

and at this point we are presumably computing 2 ^ 1023 in whnf and loose.

I'm not quite sure what is creating the ?h query but it looks similar to the ones that eq_self is asking for so it's potentially responsible here I guess?

[Tobias Grosser]

The same failure arises with:

--set_option maxRecDepth 1600
theorem test2 (e : (BitVec 1023)) :
    some 0#1023 =
    if (BitVec.ofInt 1023 (-70368744177664) &&& 70368040490200#1023 != 0)
      then none else none := by
  /-
  tactic 'simp' failed, nested error:
  maximum recursion depth has been reached
  use `set_option maxRecDepth <num>` to increase limit
  use `set_option diagnostics true` to get diagnostic information
  -/
  /- equal to `simp only [reduceOfInt]`-/
  simp?  [-Int.reduceNeg, reduceOfInt, -reduceAnd, -ofNat_eq_ofNat,
    -bne_self_eq_false, -Bool.false_eq_true, -reduceIte, -reduceCtorEq, -eq_self,
    -bne_iff_ne, -ite_self, -Option.some_eq_ite_none_right, -Option.some_eq_ite_none_left
    ]

Which should be equal to simp only [reduceOfInt], but should not add eq_self to the simp set AFAIU.

[Tobias Grosser]

(deleted)

[Henrik Böving]

Yeah the simp.rewrit trace doesn't show it anymore like that but the defeq query remains, not clear to me what part of the system creates the defeq query then

[Tobias Grosser]

Is it possible that ground terms in an if-condition are somehow evaluated? Even though before reduction, the argument of the condition contained some variables.

[Tobias Grosser]

If I am not mistaken, simprocArrayCore and simprocCore seem to create these equalities at https://github.com/leanprover/lean4/blob/fe45ddd6105078a0a3bd855e5d94673e794f6b88/src/Lean/Meta/Tactic/Simp/Simproc.lean#L312 to apply the result of the simpproc.

[Tobias Grosser]

This also seems relevant:

/-- Given `h₁ : a = b` and `h₂ : b = c` returns a proof of `a = c`. -/
def mkEqTrans (h₁ h₂ : Expr) : MetaM Expr := do
  if h₁.isAppOf ``Eq.refl then
    return h₂
  else if h₂.isAppOf ``Eq.refl then
    return h₁
  else
    let hType₁ ← infer h₁
    let hType₂ ← infer h₂
    match hType₁.eq?, hType₂.eq? with
    | some (α, a, b), some (_, _, c) =>
      let u ← getLevel α
      return mkApp6 (mkConst ``Eq.trans [u]) α a b c h₁ h₂
    | none, _ => throwAppBuilderException ``Eq.trans ("equality proof expected" ++ hasTypeMsg h₁ hType₁)
    | _, none => throwAppBuilderException ``Eq.trans ("equality proof expected" ++ hasTypeMsg h₂ hType₂)

[Tobias Grosser]

I guess mkEqTrans is creating Eq.refl in our case?