max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2
lean4-htt/tests/elab/inductive_pred.lean.out.expected
Joachim Breitner 1362cc6041
refactor: simplify structural recursion elaboration (#13008) 
This PR removes the custom `M`/`State` monad from structural recursion
elaboration, replacing it with plain `MetaM`. This simplifies the code
and makes the control flow more explicit, in preparation for #12987
which
introduces named `_f` auxiliary definitions for structural recursion.

Key changes:
- Remove `State`/`M` types from `Structural.Basic`, use `MetaM`
throughout
- Extract `withRecFunsAsAxioms` helper for adding recursive functions as
temporary axioms
- Split `tryAllArgs` into `findRecArgCandidates` (analysis) and
`tryCandidates` (backtracking execution)
- Move `withoutModifyingEnv` into each phase that needs it
- For inductive predicates, return matchers from `mkIndPredBRecOnF`
instead of accumulating in state
- Pass `fnTypes` explicitly to `mkBRecOnMotive` instead of re-inferring

This is a pure refactoring with no behavior changes (except matcher
numbering in `inductive_pred` test due to changed
`saveState`/`restoreState` boundaries).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

---------

Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
2026-03-20 16:10:27 +00:00

310 lines
17 KiB
Text
Raw Blame History

[Elab.definition.structural] getRecArgInfos report: Not considering parameter n of Ex.Power2.mul':
it is unchanged in the recursive calls
[Elab.definition.structural] recArgInfos:
{ fnName := `Ex.Power2.mul',
fixedParamPerm := #[some 0, none, none, none],
recArgPos := 2,
indicesPos := #[0],
indGroupInst := { toIndGroupInfo := { all := #[`Ex.Power2], numNested := 0 }, levels := [], params := #[] },
indIdx := 0 }
{ fnName := `Ex.Power2.mul',
fixedParamPerm := #[some 0, none, none, none],
recArgPos := 3,
indicesPos := #[1],
indGroupInst := { toIndGroupInfo := { all := #[`Ex.Power2], numNested := 0 }, levels := [], params := #[] },
indIdx := 0 }
{ fnName := `Ex.Power2.mul',
fixedParamPerm := #[some 0, none, none, none],
recArgPos := 1,
indicesPos := #[],
indGroupInst := { toIndGroupInfo := { all := #[`Nat], numNested := 0 }, levels := [], params := #[] },
indIdx := 0 }
[Elab.definition.structural] inductive groups: [Power2, Nat]
[Elab.definition.structural] Trying argument set [2]
[Elab.definition.structural] Reduced fixed params from [n] to [], erasing [n]
[Elab.definition.structural] New recArgInfos #[{ fnName := `Ex.Power2.mul',
fixedParamPerm := #[none, none, none, none],
recArgPos := 2,
indicesPos := #[0],
indGroupInst := { toIndGroupInfo := { all := #[`Ex.Power2], numNested := 0 }, levels := [], params := #[] },
indIdx := 0 }]
[Elab.definition.structural] assignments of type formers of Ex.Power2 to functions: [[0]]
[Elab.definition.structural] funTypes: [funType_1], motives: [fun {n} x =>
∀ {m : Nat} (x_1 : Power2 m), @funType_1 n m x x_1]
[Elab.definition.structural] FTypes: [∀ (a : Nat) (t : Power2 a),
@below (fun {n} x => ∀ {m : Nat} (x_1 : Power2 m), @funType_1 n m x x_1) a t →
∀ {m : Nat} (x : Power2 m), @funType_1 a m t x]
[Elab.definition.structural] matcherApp before adding below transformation:
@mul'.match_1_1 n (fun m x x_1 => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x✝² x✝¹
(fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1)))
fun h1 n_1 h2 =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (@mul' n n_1 h1 h2))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)
[Meta.IndPredBelow.match] 💥️ @mul'.match_1_1 n
(fun m x x_1 => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x✝² x✝¹
(fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1)))
fun h1 n_1 h2 =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (@mul' n n_1 h1 h2))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n
n_1) and [fun {n} x => ∀ {m : Nat} (x_1 : Power2 m), @funType_1 n m x x_1]
[Meta.IndPredBelow.match] new decls:
[Below: h✝, Ex.Power2.below, [h1]]
[Meta.IndPredBelow.match] oldCount = 1; fvars = [h1, h✝]
[Meta.IndPredBelow.match] alt 0:
fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n)
h1)) ↦ fun h1 h =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1))
[Meta.IndPredBelow.match] new decls:
[Below: h✝, Ex.Power2.below, [h1]]
[Meta.IndPredBelow.match] oldCount = 3; fvars = [h1, n✝, h2, h✝]
[Elab.definition.structural] Trying argument set [3]
[Elab.definition.structural] assignments of type formers of Ex.Power2 to functions: [[0]]
[Elab.definition.structural] funTypes: [funType_1], motives: [fun {m} x => ∀ (x_1 : Power2 n), @funType_1 m x_1 x]
[Elab.definition.structural] FTypes: [∀ (a : Nat) (t : Power2 a),
@below (fun {m} x => ∀ (x_1 : Power2 n), @funType_1 m x_1 x) a t → ∀ (x : Power2 n), @funType_1 a x t]
[Elab.definition.structural] matcherApp before adding below transformation:
@mul'.match_1_1 n (fun m x x_1 => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x✝² x✝¹
(fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1)))
fun h1 n_1 h2 =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (@mul' n n_1 h1 h2))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)
[Meta.IndPredBelow.match] ✅️ @mul'.match_1_1 n
(fun m x x_1 => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x✝² x✝¹
(fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1)))
fun h1 n_1 h2 =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (@mul' n n_1 h1 h2))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n
n_1) and [fun {m} x => ∀ (x_1 : Power2 n), @funType_1 m x_1 x]
[Meta.IndPredBelow.match] ✅️ pattern base to Ex.Power2.below
[Meta.IndPredBelow.match] instantiate ∀ {motive : (a : Nat) → Power2 a → Prop},
@below motive (@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))
base with [fun {m} x => ∀ (x_1 : Power2 n), @funType_1 m x_1 x] []}
[Meta.IndPredBelow.match] rec indices below.base []
[Meta.IndPredBelow.match] ✅️ pattern @ind n✝ h2 to Ex.Power2.below
[Meta.IndPredBelow.match] instantiate ∀ {motive : (a : Nat) → Power2 a → Prop} {n : Nat} (a : Power2 n),
@below motive n a →
motive n a →
@below motive
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat)
(@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n)
⋯ with [fun {m} x => ∀ (x_1 : Power2 n), @funType_1 m x_1 x] [n✝, h2]}
[Meta.IndPredBelow.match] rec indices below.ind [(0, 1)]
[Meta.IndPredBelow.match] transform ih✝ to 1, h2
[Meta.IndPredBelow.match] new decls:
[]
[Meta.IndPredBelow.match] oldCount = 1; fvars = [h1]
[Meta.IndPredBelow.match] alt 0:
fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n)
h1)) ↦ fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1))
[Meta.IndPredBelow.match] new decls:
[Below: ih✝, Ex.Power2.below, [h2], Motive: a_ih✝, 0, [h2]]
[Meta.IndPredBelow.match] oldCount = 3; fvars = [h1, n✝, h2, ih✝, a_ih✝]
[Meta.IndPredBelow.match] alt 1:
fun h1 n_1 h2 =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (@mul' n n_1 h1 h2))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n
n_1) ↦ fun h1 n_1 h2 ih a_ih =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (a_ih h1))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)
[Elab.definition.structural] FArgs: [fun {m} x x_1 x_2 =>
@mul'.match_1_10 n funType_1
(fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x_2 x x_1
(fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1)))
fun h1 n_1 h2 ih a_ih =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (a_ih h1))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat)
(@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)]
[Elab.definition.structural] packedFArgs: [fun {m} x x_1 x_2 =>
@mul'.match_1_10 n funType_1
(fun m x x_3 below => Power2 (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n m)) m x_2 x x_1
(fun h1 =>
@of_eq_true
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@Eq.trans Prop
(Power2
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Power2 n) True
(@congrArg Nat Prop
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@OfNat.ofNat Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n Power2 (Nat.mul_one n))
(@eq_true (Power2 n) h1)))
fun h1 n_1 h2 ih a_ih =>
@Eq.rec Nat
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2)))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1))
(fun x h => Power2 x) (@ind (@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n n_1) (a_ih h1))
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) n
(@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat)
(@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n_1))
(mul_left_comm (@OfNat.ofNat Nat (nat_lit 2) (instOfNatNat (nat_lit 2))) n n_1)]
Reference in a new issue View git blame Copy permalink