Possible issue in Mathlib.Data.List.Basic

[pthomas505]

If import Mathlib.Data.List.Basic is uncommented here:

import Mathlib.Util.CompileInductive
--import Mathlib.Data.List.Basic


inductive Formula : Type
  | pred_const_ : String → List String → Formula
  | pred_var_ : String → List String → Formula
  | eq_ : String → String → Formula
  | true_ : Formula
  | false_ : Formula
  | not_ : Formula → Formula
  | imp_ : Formula → Formula → Formula
  | and_ : Formula → Formula → Formula
  | or_ : Formula → Formula → Formula
  | iff_ : Formula → Formula → Formula
  | forall_ : String → Formula → Formula
  | exists_ : String → Formula → Formula
  | def_ : String → List String → Formula
  deriving Inhabited, DecidableEq

compile_inductive% Formula

open Formula

structure Definition : Type :=
(name : String)
(args : List String)
(q : Formula)
deriving DecidableEq

abbrev Env : Type := List Definition

def Function.updateIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β)
  (a' : α)
  (b : β)
  (a : α) :
  β :=
  if a = a' then b else f a

def Function.updateListIte
  {α β : Type}
  [DecidableEq α]
  (f : α → β) :
  List α → List β → α → β
  | x::xs, y::ys => Function.updateIte (Function.updateListIte f xs ys) x y
  | _, _ => f


structure Interpretation (D : Type) : Type :=
  (nonempty : Nonempty D)
  (pred_const_ : String → (List D → Prop))
  (pred_var_ : String → (List D → Prop))

def VarAssignment (D : Type) : Type := String → D

def Holds
  (D : Type)
  (I : Interpretation D)
  (V : VarAssignment D) : Env → Formula → Prop
  | _, pred_const_ X xs => I.pred_const_ X (xs.map V)
  | _, pred_var_ X xs => I.pred_var_ X (xs.map V)
  | _, eq_ x y => V x = V y
  | _, true_ => True
  | _, false_ => False
  | E, not_ phi => ¬ Holds D I V E phi
  | E, imp_ phi psi =>
    Holds D I V E phi → Holds D I V E psi
  | E, and_ phi psi =>
    Holds D I V E phi ∧ Holds D I V E psi
  | E, or_ phi psi =>
    Holds D I V E phi ∨ Holds D I V E psi
  | E, iff_ phi psi =>
    Holds D I V E phi ↔ Holds D I V E psi
  | E, forall_ x phi =>
    ∀ d : D, Holds D I (Function.updateIte V x d) E phi
  | E, exists_ x phi =>
    ∃ d : D, Holds D I (Function.updateIte V x d) E phi
  | ([] : Env), def_ _ _ => False
  | d :: E, def_ name args =>
    if name = d.name ∧ args.length = d.args.length
    then Holds D I (Function.updateListIte V d.args (List.map V args)) E d.q
    else Holds D I V E (def_ name args)
termination_by _ E phi => (E, phi)

then this is reported at the E, imp_ phi psi case in the definition of Holds:

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

case h
D: Type
V: VarAssignment D
E: Env
phipsi: Formula
x✝: (y : (_ : VarAssignment D) ×' (_ : Env) ×' Formula) →
  (invImage (fun a => PSigma.casesOn a fun V snd => PSigma.casesOn snd fun E snd => (E, snd))
          Prod.instWellFoundedRelationProd).1
      y { fst := V, snd := { fst := E, snd := imp_ phi psi } } →
    Prop
a✝: x✝ { fst := V, snd := { fst := E, snd := phi } }
  (_ :
    (invImage (fun a => PSigma.casesOn a fun V snd => PSigma.casesOn snd fun E snd => (E, snd))
          Prod.instWellFoundedRelationProd).1
      { fst := V, snd := { fst := E, snd := phi } } { fst := V, snd := { fst := E, snd := imp_ phi psi } })
⊢ sizeOf psi < sizeOf (imp_ phi psi)

$ cat lean-toolchain 
leanprover/lean4:nightly-2023-06-20
$ cat lake-manifest.json 
{"version": 4,
 "packagesDir": "lake-packages",
 "packages":
 [{"git":
   {"url": "https://github.com/EdAyers/ProofWidgets4",
    "subDir?": null,
    "rev": "c43db94a8f495dad37829e9d7ad65483d68c86b8",
    "name": "proofwidgets",
    "inputRev?": "v0.0.11"}},
  {"git":
   {"url": "https://github.com/leanprover-community/mathlib4.git",
    "subDir?": null,
    "rev": "d2aa4e1a62d9655041df1a006bc5701cb2dc125a",
    "name": "mathlib",
    "inputRev?": null}},
  {"git":
   {"url": "https://github.com/gebner/quote4",
    "subDir?": null,
    "rev": "c71f94e34c1cda52eef5c93dc9da409ab2727420",
    "name": "Qq",
    "inputRev?": "master"}},
  {"git":
   {"url": "https://github.com/JLimperg/aesop",
    "subDir?": null,
    "rev": "ca73109cc40837bc61df8024c9016da4b4f99d4c",
    "name": "aesop",
    "inputRev?": "master"}},
  {"git":
   {"url": "https://github.com/leanprover/std4",
    "subDir?": null,
    "rev": "e68aa8f5fe47aad78987df45f99094afbcb5e936",
    "name": "std",
    "inputRev?": "main"}}]}

Zulip discussion that led to finding this: https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/feature.20request.3A.20proving.20termination

[pthomas505]

import Mathlib.Data.Finset.Basic appears to cause the same issue.

[fpvandoorn]

The issue seems to be Nat.linearOrderedCommSemiring in Data.Nat.Order.Basic which doesn't interact well with the default decreasing_tactic implementation (in Lean.Init.WFTactics). I haven't figured out the proper fix yet.