refactor: construct .eq_def before .eq_n

[nomeata]

I have a theory that we’d get less “failed to generate equational theorem” like in #5667 if we first generate the .unfold theorem (a bit easier, no hypotheses to consider), and then use that to define the .eq_n that don't hold by rfl anyways.

This (stashed, partial) work explores that direction, and shows that indeed it fixes #5667.

But of course plenty of other programs break. This brecOn business is not so easy!

[leanprover-community-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-5669 build failed against this PR. (2024-10-10 17:18:37) View Log
• 💥 Mathlib branch lean-pr-testing-5669 build failed against this PR. (2024-10-10 20:58:55) View Log
• 💥 Mathlib branch lean-pr-testing-5669 build failed against this PR. (2025-02-06 16:00:24) View Log

[nomeata]

I gave this another shot, storing some of my observations here.

I figured it might be more robust to prove the equational theorems if we had an unfolding lemma for T.brecOn, like we do for WellFounded.fix. Here is a possible construction of such a lemma for Nat:

def Nat.below.mk (motive : Nat → Sort u) (f : (n : Nat) → motive n) (n : Nat) :
    Nat.below (motive := motive) n :=
  Nat.rec (motive := fun n => Nat.below (motive := motive) n)
    PUnit.unit (fun n ih => PProd.mk (f n) ih) n

@[simp] theorem Nat.below.mk_eq1 :
  Nat.below.mk motive f 0 = PUnit.unit := rfl
@[simp] theorem Nat.below.mk_eq2 :
  Nat.below.mk motive f (n+1) = PProd.mk (f n) (Nat.below.mk motive f n) := rfl

protected def Nat.brecOn'.{u} {motive : Nat → Sort u}
  (t : Nat) (F_1 : (t : Nat) → Nat.below (motive := motive) t → motive t) :
  motive t ×' Nat.below (motive := motive) t :=
  Nat.rec ⟨F_1 Nat.zero PUnit.unit, PUnit.unit⟩ (fun n n_ih => ⟨F_1 n.succ n_ih, n_ih⟩) t

-- @[simp] theorem Nat.brecOn'_eq1 :
--    Nat.brecOn' (motive := motive) 0 f = ⟨f 0 PUnit.unit, PUnit.unit⟩ := rfl
-- @[simp] theorem Nat.brecOn'_eq2 :
--    Nat.brecOn' (motive := motive) (n+1) f =
--     ⟨ f (n+1) (Nat.brecOn' (motive := motive) n f),
--      (Nat.brecOn' (motive := motive) n f) ⟩ := rfl

theorem Nat.brecOn'_eq (motive : Nat → Sort u) (f) (n : Nat) :
    Nat.brecOn' (motive := motive) n f =
      let f' := Nat.below.mk motive (fun n => (Nat.brecOn' (motive := motive) n f).1) n
      ⟨f n f', f'⟩ :=
  Nat.rec rfl (fun n n_ih =>
    congrArg (fun x => PProd.mk (f n.succ x) x)
     (n_ih.trans (congrArg (fun x => PProd.mk x.1 _) n_ih.symm)
  )) n

theorem Nat.brecOn_eq (motive : Nat → Sort u) (f) (n : Nat) :
    Nat.brecOn (motive := motive) n f =
      f n (Nat.below.mk motive (fun n => Nat.brecOn (motive := motive) n f) n) :=
  congrArg (fun x => x.1) (Nat.brecOn'_eq motive f n)

The @[simp] lemmas are just to understand the proofs better when dsimp’ing.

First big question: Can we write metaprogram that generate all these definitions and proofs, even for much more complex data types. (Especially Nat.brecOn'_eq looks hard, maybe there is an easier formulation).

With that, it seems we can prove unfolding lemmas a bit more easily:

example {f : Nat → Option Nat} {t} :
  -- only needed to instantiate, because unification does not do that
  let F := fun t f_1 =>
    match f t with
    | some u => u
    | none =>
      (match (motive := (t : Nat) → Nat.below (motive := (fun t => Nat)) t → Nat) t with
        | Nat.zero => fun x => Nat.zero
        | Nat.succ t' => fun x => x.1)
        f_1

  replace f t =
    match f t with
    | some u => u
    | none =>
      match t with
      | Nat.zero => Nat.zero
      | Nat.succ t' => replace f t' := by
  intro F
  delta replace
  apply (Nat.brecOn_eq (motive := (fun t => Nat)) F t).trans
  · unfold F
    split
    · rfl
    · split
      · rfl
      · rfl

Anyways, it's clearly not a simple option to go that route, so shelving that idea here.