feat: generate (co)induction proof principles for mutually (co)inductive predicates

[wkrozowski]

This PR adds support for generating lattice-theoretic (co)induction proof principles for predicates defined via mutual blocks using inductive_fixpoint/coinductive_fixpoint constructs.

Key Changes

• The order on product lattices (used to define fixpoints of mutual blocks) is unfolded.
• Hypotheses in generated principles are curried.
• Conclusions are projected to focus only on the predicate of interest (rather than being a conjunction of conclusions for all functions defined in the mutual block.

Example

Given:

mutual
    def f : Prop :=
      g
    coinductive_fixpoint

    def g : Prop :=
      f
    coinductive_fixpoint
  end

The system now generates these coinduction principles:

f.coinduct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2) (hyp_2 : pred_2 → pred_1) : pred_1 → f

and

g.coinduct (pred_1 pred_2 : Prop) (hyp_1 : pred_1 → pred_2) (hyp_2 : pred_2 → pred_1) : pred_2 → g

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 8424ddbb3edf4c3b440d0c4e1216e3ebf19bdaf4 --onto 18a82c04fc59d3dba392308e09d65ee431240d89. You can force Mathlib CI using the force-mathlib-ci label. (2025-07-14 16:59:08)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 8424ddbb3edf4c3b440d0c4e1216e3ebf19bdaf4 --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-07-14 16:59:09)

[nomeata]

Conclusions are projected to focus only on the predicate of interest (rather than being a conjunction of conclusions for all functions defined in the mutual block.

I’d expect that in many application, one does want the conclusions for all involved functions. If you only provide the projections, then the user has to do the proof multiple times.

I see that for partial_fixpoint, I’m only generating the conjunction variant so far:

mutual
def a (n : Nat) : Nat := b (n + 1)
partial_fixpoint
def b (n : Nat) : Nat := a (n + 2)
partial_fixpoint
end

/--
info: a.fixpoint_induct (motive_1 motive_2 : (Nat → Nat) → Prop) (adm_1 : Lean.Order.admissible motive_1)
  (adm_2 : Lean.Order.admissible motive_2) (h_1 : ∀ (b : Nat → Nat), motive_2 b → motive_1 fun n => b (n + 1))
  (h_2 : ∀ (a : Nat → Nat), motive_1 a → motive_2 fun n => a (n + 2)) : motive_1 a ∧ motive_2 b
-/
#guard_msgs in
#check a.fixpoint_induct

For functional induction, I generate both:

mutual
def a (n : Nat) : Nat := b (n + 1)
decreasing_by sorry
def b (n : Nat) : Nat := a (n + 2)
decreasing_by sorry
end

/--
info: a.mutual_induct (motive1 motive2 : Nat → Prop) (case1 : ∀ (n : Nat), motive2 (n + 1) → motive1 n)
  (case2 : ∀ (n : Nat), motive1 (n + 2) → motive2 n) : (∀ (n : Nat), motive1 n) ∧ ∀ (n : Nat), motive2 n
-/
#guard_msgs in
#check a.mutual_induct


/--
info: a.induct (motive1 motive2 : Nat → Prop) (case1 : ∀ (n : Nat), motive2 (n + 1) → motive1 n)
  (case2 : ∀ (n : Nat), motive1 (n + 2) → motive2 n) (n : Nat) : motive1 n
-/
#guard_msgs in
#check a.induct

I wonder if we should do the latter in all cases. But it’s hard to decide without a real sizeable use-case yet.

In any case, adding the .mutual_induct variant for (co)inductive predicates can be done later; no need to do it here.i

[nomeata]

If it’s possible, i.e. known at the call site, I’d prefer to pass in the expected number of components, so that the function doesn't run over if the last type itself happens to be a PProd.

[nomeata]

Suggested change

	let newMotives ← motives.mapM ( instantiateForall · #[predVar])
	let newMotives ← motives.mapM (instantiateForall · #[predVar])