aesop and maxSynthPendingDepth

Stream: general

[Kevin Buzzard]

@Jannis Limperg just to flag the aesop-related issue which came out of a discussion in this thread.

import Mathlib

-- the higher the number, the longer aesop takes
set_option maxSynthPendingDepth 6

set_option trace.profiler true in
theorem Module.FaithfullyFlat.extracted (R : Type) (M : Type) [CommRing R] [AddCommGroup M]
    [Module R M]
    (iff_exact :
    ∀ {N1 : Type} [AddCommGroup N1] [Module R N1] {N2 : Type}
    [AddCommGroup N2] [Module R N2] {N3 : Type} [AddCommGroup N3]
    [Module R N3] (l12 : N1 →ₗ[R] N2) (l23 : N2 →ₗ[R] N3),
    Function.Exact ⇑l12 ⇑l23 ↔ Function.Exact ⇑(LinearMap.rTensor M l12) ⇑(LinearMap.rTensor M l23))
    ⦃N N' N'' : Type⦄ [AddCommGroup N] [AddCommGroup N'] [AddCommGroup N''] [Module R N]
    [Module R N'] [Module R N''] ⦃f : N →ₗ[R] N'⦄ ⦃g : N' →ₗ[R] N''⦄ :
    Function.Exact ⇑f ⇑g → Function.Exact ⇑(LinearMap.rTensor M f) ⇑(LinearMap.rTensor M g) := by
  aesop

In a branch, someone set this pending depth number to 50 to see what would happen, and it caused two time-outs in mathlib and this was one. The aesop proof in mathlib is complete overkill and the tactic should not be being used at all (in fact it should be being used to find the simple proof!) but I thought I would flag the issue explicitly to you in case you had any interest in it. By the time the pendingdepth is set to 7 the error is

aesop: error in norm simp: failed to synthesize
  AddCommGroup
    (TensorProduct R
      (TensorProduct R
        (TensorProduct R
          (TensorProduct R
            (TensorProduct R (TensorProduct R (TensorProduct R (TensorProduct R (TensorProduct R N M) M) M) M) M) M)
          M)
        M)
      M)
(deterministic) timeout at `typeclass`, maximum number of heartbeats (20000) has been reached

and it seems that aesop is stuck in a loop forever trying to apply iff_exact in the "bad" direction and adding "tensor M" to the end of a term. The typeclass trace is in the message I linked to above. This is not a problem (the depth should never be as big as 7 and aesop finds a super-simple proof which should be dropped in as a replacement anyway) but I thought maybe it was worth recording.

[Jannis Limperg]

Thanks for the ping and the detailed write-up! As far as I can tell, Aesop only calls simp here (after some trivial pre-processing steps). So the issue, if it is one, would be with simp.