Iota Reduction by barabbs · Pull Request #43 · digama0/lean4lean

barabbs · 2026-08-08T09:44:01Z

I took a run at ι-reduction (this iota branch, merged with your current master). Everything builds, Experimental included; the one gap the branch adds is a single sorry, VEnv.WF.patsStrong, discussed at the end.

ι is modelled as a schematic pattern rule, reusing the Pattern engine, giving VEnv a third field pats next to constants/defeqs, and lifting NormalEq's pat_wf into the live IsDefEq as a new pat constructor. addInduct (which was a sorry) now installs one rule per recursor rule into that registry, and TrEnv carries the rules across to translated environments (TrEnv.pats_iota', TrEnv.iota_defeq, TrEnv.iota_rec), which is what the ι case of recursor reduction (inductiveReduceRecCore.WF) now runs on.

Below are some design decisions taken (a few of which touch your own code), please let me know if you think they are sensible and in line with your plans, or if there's anything that should be changed.

pat rule's check. The natural phrasing puts IsDefEq under an ∃, which the positivity checker rejects once it's a real inductive rather than the NormalEq structure. The sub-equality types are instead carried as data (chk), tied to the check by a non-recursive Realizes, and asserted with ∀ t ∈ chk, …. Proved this equivalent to Check.OK (IsDefEqU …) (Realizes.toOK / OK.exists_realizer), and the Params instance's pat_wf reconstructs exactly that form.
iotaCheck = .true. The kernel does no parameter check at reduction time; parameter agreement falls out of the redex being well-typed, which is already a premise. So the check is trivial and the caller never has to discharge it.
Carried recursor data. VInductDecl gets a recs field; VRecursor / VRecRule mirror RecursorVal / RecursorRule. iotaRHS applies the carried rule.rhs to the same argument slice inductiveReduceRec takes. It was checked by rfl against real Nat.rec (successor case, recursive call and all), and Tests/IotaShape.lean checks it against inductiveReduceRec on a set of library inductives (mutual, indexed, nested, K-like, reflexive).
VInductDecl.WF specifies a direct mutual block: strict positivity, the universe bound imax(ℓ', ℓ) ≤ ℓ on constructor fields, large elimination only under the kernel's elimOnlyAtUniverseZero conditions, the recursor telescope split, and every rule firing on a constructor of the type former its recursor eliminates. Nested inductives (Tree.node : List Tree → Tree, with Tree.rec_1 over List Tree) are outside it: the kernel compiles them to a direct block (ElimNestedInductive) before checking, and modelling that pass is future work.
AddInduct carries kernel data only, at every safety level: the InductiveVals/RecursorVals, the four stage successes of addInduct, the translation of each type former, constructor and recursor at the stage the kernel checks it, freshness and the insertion order. env_eq, wf, find?_mono, rec_find, ctor_find and the rest are derived, as AddQuot does. It is a structure in Type (its intermediate environments appear in statements) inside the Prop-valued TrEnv'.induct; happy to restate it in the AddQuot1 style if you'd rather keep everything in Prop.
Params.pat_env. Your Params class gains pat_env : env.pats p r → Pat p r, the one field the church_rosser pat case needs (it routes through your ParRed.extra).

And after merging the latest edits in master:

TrEnv'.induct at every safety level, and a real addQuot.WF. With AddInduct real, inductives appear in the translated environments, so no_inductInfo (and the vacuous addQuot.WF that rested on it) are gone: Verify/Environment/Quot.lean proves quotient initialization from checkEqType. That needs Eq to be safe, which the C++ check_eq_type does not check, so checkEqType now rejects an unsafe Eq (recorded in divergences.md, in the spirit of the prelude checks).
TrEnv.pats_iota' needs a hsafe hypothesis. Your ignore constructor can skip an unsafe recursor without registering its rule, which makes the plain statement false. The guard (safety ≤ recInfo.safety) rules that out and is trivially true for any safe recursor.
OrderedStrong in the strong system. IsDefEq.strong and the inversion lemmas now take OrderedStrong (Ordered, strong typing of the environment, and subject reduction of the registered rules), so your substitution theorems (substEq', substDF, …) and the primitives layer were retyped accordingly — every one of those call sites held VEnv.WF, so it is WF.orderedStrong everywhere. IsDefEqStrong.substEq' gained a pat case, backed by three pattern-stability lemmas under Subst. This is the one place where master's theorems become conditional on the deferred patsStrong.
insertDefs_wf moved from Extension.lean to Lemmas.lean. pats_iota' (which I put in Lemmas.lean) uses it, and since Extension.lean imports Lemmas.lean it had to move up. Pure relocation, still referenced from Extension.lean through the import.

What's where

1. Expressing ι, the pats registry and the IsDefEq.pat rule.

VEnv.lean — the pats field, addPat, and the LE.pats monotonicity field.
Typing/Pattern.lean — the check bridge (Check.Realizes, Realizes.toOK, OK.exists_realizer) and the transport helpers (RHS.apply_closedN, Matches.closedN, apply_levelWF, Matches.levelWF, RHS.instL_apply, matches_instL, the three Realizes.map_*, and their Subst versions RHS.subst_apply, matches_subst, Realizes.map_subst).
Typing/Basic.lean — the IsDefEq.pat constructor, and PatTyped/PatWF (what Ordered.pat asks of a rule).
Typing/Strong.lean — IsDefEqStrong.pat and its recursion cases, PatStrong/PatsStrongOn, and OrderedStrong.
Typing/Lemmas.lean — addPat_le, addPat_self, the pat cases across closedN', mono, levelWF, weakN, instN, instL, isType', and the two inversion lemmas; the pat clause of Ordered with Ordered.patWF.
Typing/ChurchRosser.lean — the pat case in church_rosser and Params.pat_env.
Typing/Env.lean, Typing/EnvLemmas.lean — WFPrefix, PatsStrong, WF.strong, WF.orderedStrong, and the deferred WF.patsStrong.

2. Installing rules: recursor data, iotaRHS, and addInduct.

VDecl.lean — VRecRule (with ctorParams), VRecursor (+ getMajorIdx, getFirstIndexIdx), and recs on VInductDecl.
VExpr.lean — a Decidable (ClosedN …) instance and the syntactic helpers (mkApps, piBinders, getAppFn, …).
Typing/Pattern.lean — the ι builders varN_pathOf and SimplePattern.iotaRHS.
Inductive.lean — the shape predicates (RecShape, CtorResult, CtorPositive, LargeElim, …), VInductDecl.WF, addRecRule, and the staged addInduct.

3. Extension lemmas and the Params instance.

Typing/InductiveLemmas.lean — addInduct_le, addInduct_pat and addInduct_WF (all proved), and the supporting foldlM lemmas.
Typing/InductiveParams.lean (new) — the Params instance toParams, the PatsIota population invariant, the five side-conditions (pat_simple, pat_uniq, pat_app_l, pat_app_l_uniq, pat_app_uniq, all proved), and inductParams/crDefEq_of_induct, which run church_rosser on an environment built by addInduct.
Typing/Pattern.lean — the constructor-spine combinatorics behind those side-conditions (subpattern_varN_const, not_app_subpattern_varN_const, varN_const_inter, varN_const_inj).

4. Verify bridge, AddInduct and the exposed lemmas.

Environment/Basic.lean — TrIndType, TrRecursor, the AddInduct structure and its derived bookkeeping.
Environment/Lemmas.lean — TrEnv.pats_iota', TrEnv.iota_defeq, TrEnv.iota_rec and the inverse pats_iota_inv'; the pat clause of Aligned and Aligned.addInduct.
Environment/Quot.lean (new) — the real addQuot.WF.
TypeChecker/WHNF.lean — inductiveReduceRecCore.WF, the ι case of reduceRecursor on the registered rules (Inductive/Reduce.lean factors that step out as inductiveReduceRecCore).

5. Integrating with master.

Environment/Lemmas.lean — the hsafe hypothesis on TrEnv.pats_iota'.
Environment/Extension.lean — pats supplied in the two _mono lemmas.
Typing/Strong.lean, Verify/Primitive.lean, Verify/Environment/Primitive/*, Verify/Typing/TrTerm.lean — the OrderedStrong retyping of the substitution theorems and the primitives layer.
Quot.lean, divergences.md — the unsafe-Eq check.
Tests/IotaShape.lean, Tests/ShapeDecide.lean — the kernel-agreement checks and the decision procedures for the syntactic clauses (kept out of the theory).
Experimental/ — the pat cases of ParallelReduction, Stratified, StratifiedUntyped closed (Typing.pat_env, IsDefEq1.pat).

iota_defeq is axiom-clean ([propext]). pats_iota' and iota_rec report a sorryAx, but it's entirely the existing TrProj placeholder riding in through the TrEnv' type (a bare TrEnv' → True shows the same axiom), so nothing new is added there.

The deferred obligation

The branch leaves exactly one sorry of its own, VEnv.WF.patsStrong (EnvLemmas.lean): subject reduction of every registered ι rule in every well-formed prefix of the environment and in the constant-only extensions of such a prefix — the environments in which constant types and definitional axioms are strengthened. It is the thesis's regularity of reductions for ι, and not a consequence of Ordered (under an arbitrary well-typed axiom such as List Nat ≡ List Bool, List.rec Nat m n c (List.cons Bool true tl) is well-typed and its reduct is not). Proving it needs inversion of the redex's typing and injectivity of the block's type formers, i.e. the same open metatheory as Injectivity.lean; the direct-block WF is what makes that argument applicable. Everything in the strong system routes through it (WF.orderedStrong), so after the retyping above your substitution theorems and the primitives development are conditional on it too — that is the main thing I'd like your read on.

Things I chose that you may want differently:

AddInduct in Type vs Prop (above).
Unsafe Eq: a stricter checkEqType rather than an EqSafe precondition on addDecl.WF.
δ rules as patterns: toParams takes extra_pat as the hypothesis DefEqsAsPats, which holds for environments built from axioms and inductives (inductParams) and fails once a def or quot is declared; registering δ rules as .defn pats needs the model to tell definitions from constructors, which a bare VEnv doesn't record. Left to your call, as the representation question it is.
Nested inductives: outside VInductDecl.WF until the kernel's nested elimination is modelled.
Not modelled: K-like reduction as a rule (the flag k is recorded, unused; the equalities are derivable from proofIrrel and ι, the toCtorWhenK refinement is open) and structure η (tryEtaStructCore.WF is open).

Happy to revise any of the decisions above, and to take a pass at patsStrong once the injectivity side is settled. Let me know what you think.

Alessandro :)

Pattern/RHS/Check depend only on Theory.VExpr; moving them out of Theory/Typing/ lets VEnv reference the pattern registry without inverting the Theory/Typing layer hierarchy. No semantic change.

Adds the `pats` field (pattern -> reduct/check -> Prop) to VEnv, the `addPat` extension helper, `VEnv.LE.pats` monotonicity, and the `addPat_le`/`addPat_self` lemmas. This is the registry through which iota-reduction rules will be installed by `addInduct`; no rule consumes it yet.

Adds the schematic pattern-reduction rule `IsDefEq.pat` (and its strengthened mirror `IsDefEqStrong.pat`), the vehicle for iota/recursor reduction. The check's sub-equalities are threaded through a pure `Check.Realizes` predicate plus a positive `∀ t ∈ chk, …` premise, so `IsDefEq` never nests under `Exists` (which strict positivity rejects). Adds reusable Pattern transport lemmas (RHS.apply_closedN/instL_apply, Matches.closedN/levelWF/instL, Realizes.map_liftN/instN/instL) and the OK/Realizes bridges. All structural recursions on IsDefEq gain their pat case; most fully proven, seven genuinely-hard reduct-metatheory obligations left as marked -- IOTA-TODO(soundness). No new axioms.

Replaces the stubbed VInductDecl.WF/addInduct. addInduct registers a declaration's type formers, constructors, and recursors as constants and installs one ι rule per recursor rule via addPat. The ι reduct is built by SimplePattern.iotaRHS: the carried recursor rule template applied to the recursor's params/motives/minors and the constructor's fields — exactly inductiveReduceRec's argument slicing (validated by rfl against Nat.rec). Adds VRecursor/VRecRule to VDecl, a Decidable ClosedN instance, and Pattern.varN_pathOf. VInductDecl.WF records the checkable typing + rhs-closedness conditions (deep positivity/universe constraints noted as future work).

Proves VEnv.addInduct_le (env ≤ env' after addInduct) and the consumer-facing VEnv.addInduct_pat: a registered iota rule is present in the resulting env's pats (fully proved, sorryAx-free). Adds the concrete VEnv.toParams Params instance with pat_wf proved directly from IsDefEq.pat via the Check.OK/Realizes bridge; its structural disjointness side-conditions and addInduct_WF (which needs an Ordered-level pats extension) are marked -- IOTA-TODO(soundness). Helpers: foldlM_le, addRecRule_le, addRecRule_pats, foldlM_mono_of_mem.

Replaces the constructorless AddInduct with a real structure baking env₁.addInduct decl = some env₂, making TrEnv'.induct non-vacuous; AddInduct.to_addInduct and AddInduct.le are real. Exposes the handback interface for the erasure-verification consumer: TrEnv.iota_defeq (fully proved via IsDefEq.pat) and TrEnv.pats_iota (statement matching addInduct_pat; proof is -- IOTA-TODO(soundness), the sole new trust surface). Adds VExpr.mkApps. Aligned.addInduct and TrEnv'.of_value induct cases are IOTA-TODO (need an Aligned-level pats stage).

Enriches AddInduct with the correspondence between a kernel RecursorVal resolved from the environment and the VRecursor that owns it (fields rec_find/wf/value_find — true obligations the consumer discharges from the real kernel), and proves TrEnv.pats_iota by induction on TrEnv' via VEnv.addInduct_pat and monotonicity. Also closes TrEnv'.of_value's induct case. The lemma statement is unchanged. TrEnv.pats_iota's #print axioms carries only the pre-existing TrProj placeholder sorryAx (forced by the TrEnv' hypothesis type, as a bare TrEnv'->True lemma also shows) — no new soundness gap. The downstream consumer now inherits no new trust from the iota interface. Only Aligned.addInduct remains IOTA-TODO (a structural gap in Aligned, which lacks an addPat clause; pats_iota does not depend on it).

…riant Introduces VEnv.PatsIota (every registered pattern is a SimplePattern.iota shape whose recursor head is a registered constant; equal heads force equal arity) and proves VEnv.WF.patsIota by induction on VEnv.WF'. Uses it to prove pat_simple, pat_app_l, pat_app_l_uniq of VEnv.toParams (all axiom-clean). Adds constructor-spine combinatorics to Pattern.lean (subpattern_varN_const, not_app_subpattern_varN_const, varN_const_inter, varN_const_inj). The remaining three (pat_uniq, pat_app_uniq, extra_pat) are precisely characterized as false against the current underspecified VInductDecl.WF: pat_uniq/pat_app_uniq need WF to pin rule-shape functionality and constructor-name distinctness; extra_pat needs delta rules registered as .defn pats (a separate registry design). Left as -- IOTA-TODO(soundness).

…fication) Resolves two conflicts: - Theory/Typing/Pattern.lean rename/modify: kept the relocation to Theory/Pattern.lean, ported upstream's v4.33 fixes (Subpattern.varN def->theorem; ; rfl on Matches.uniq / matches_determ app cases). - Verify/Environment/Basic.lean: kept the real AddInduct structure over upstream's stub; upstream's TrEnv' unsafe/mutual/block cases merged in. Untracks local .claude/ and .mcp.json. Proof repair for v4.33 follows.

…ation Repairs the iota additions after the upstream merge (toolchain v4.29-> v4.33-rc2 + master's front-end declaration checking): - Pattern.lean: import Batteries.Tactic.Init (exacts visibility under the new module system); the Theory layer ports with no proof-text changes. - InductiveParams.lean: mutualDef cases for VDecl.WF.pats_eq_or_induct/le and addConsts/addDefEqs pats/le helpers. - AddInduct.value_find ported to deltaValue? (core value? gained allowOpaque / excludes theorems, lean4#12973); import Lean4Lean.Declaration. - Extension.lean: VEnv.LE constructions get the new pats field. Two integration decisions, both natural for the (safe) erasure consumer: - TrEnv.pats_iota gains hsafe : safety <= (recInfo rval).safety. Master's new 'ignore' constructor can skip an *unsafe* recursor without registering its iota rule, which made the old statement false; the guard (satisfied by any safe recursor via le_safe) restores it. This is a correctness improvement the merge surfaced. - TrEnv'.induct is guarded to safety = .safe, matching AddInduct's .safe- only translation and keeping master's .unsafe front-end path inductive-free (TrEnv'.no_inductInfo). Unsafe inductives are future work. Build green on v4.33-rc2; 12 IOTA-TODO sorries unchanged; no new axioms. Handback lemmas: iota_defeq [propext], addInduct_pat [propext,Quot.sound], pats_iota proven (only pre-existing TrProj sorryAx via its TrEnv' type).

Restores the maintainer's original file location; VEnv imports Theory.Typing.Pattern directly (no import cycle — Pattern depends only on VExpr). Reverts an unforced stylistic move that disturbed upstream layout and caused a merge conflict.

Copilot

Pull request overview

This PR introduces ι-reduction support by modelling recursor computation rules as schematic Pattern-based reductions stored in a new VEnv.pats registry, and threads these rules through the verified translation layer (TrEnv/TrEnv') to expose downstream lookup (pats_iota) and definitional-equality replay (iota_defeq).

Changes:

Extend the theory environment and definitional equality with pattern-based reduction rules (VEnv.pats, VEnv.addPat, IsDefEq.pat) plus the supporting Pattern.Check.Realizes bridge.
Implement inductive/recursor rule installation as ι-pattern rules (VEnv.addRecRule, VEnv.addInduct) and add recursor metadata carriers (VRecursor, VRecRule, VInductDecl.recs).
Add verification-layer support for inductive translation via a concrete AddInduct witness, plus exposed recursor-rule lookup and “replay” lemmas (TrEnv.pats_iota, TrEnv.iota_defeq).

Reviewed changes

Copilot reviewed 16 out of 16 changed files in this pull request and generated 7 comments.

Show a summary per file

File	Description
Lean4Lean/Verify/Typing/Expr.lean	Adds `VExpr.mkApps` helper for building application spines.
Lean4Lean/Verify/Environment/Lemmas.lean	Adds const-map WF and recursor-lookup helpers; exposes `pats_iota`/`iota_defeq`; introduces an `Aligned.addInduct` placeholder.
Lean4Lean/Verify/Environment/Extension.lean	Updates monotonicity lemmas for `pats` and adjusts unsafe-path inductive handling; removes local `insertDefs_wf`.
Lean4Lean/Verify/Environment/Basic.lean	Replaces placeholder `AddInduct` with a concrete structure; gates `TrEnv'.induct` to `.safe`.
Lean4Lean/Theory/VExpr.lean	Adds decidability instance for `ClosedN`.
Lean4Lean/Theory/VEnv.lean	Adds `pats` field plus `addPat`, and extends `VEnv.LE` with `pats` monotonicity.
Lean4Lean/Theory/VDecl.lean	Introduces recursor/rule carriers and adds `recs` to inductive declarations.
Lean4Lean/Theory/Typing/Basic.lean	Adds the new definitional equality constructor `.pat`.
Lean4Lean/Theory/Typing/Strong.lean	Propagates `.pat` through strong definitional equality and its structural lemmas (with remaining soundness holes).
Lean4Lean/Theory/Typing/Pattern.lean	Adds `Realizes` bridge, transport lemmas for `.pat`, and ι-rule builders (`varN_pathOf`, `iotaRHS`) plus combinatorics lemmas.
Lean4Lean/Theory/Typing/Lemmas.lean	Extends core lemmas (`closedN'`, `mono`, `levelWF`, `weakN`, `instN`, `instL`, inversions) with `.pat` cases (with remaining inversion holes).
Lean4Lean/Theory/Typing/InductiveParams.lean	New `Params` instance construction from `env.pats`, with several deferred side conditions.
Lean4Lean/Theory/Typing/InductiveLemmas.lean	Adds `addInduct_le` / `addInduct_pat` and supporting fold lemmas; leaves `addInduct_WF` deferred.
Lean4Lean/Theory/Typing/ChurchRosser.lean	Adds `.pat` case stub in `church_rosser`.
Lean4Lean/Theory/Inductive.lean	Implements `VInductDecl.WF`, `VEnv.addRecRule`, and `VEnv.addInduct` (ι-rule installation).
Lean4Lean/Theory.lean	Wires in `Typing.InductiveParams`.

Suppressed comments (1)

Lean4Lean/Theory/Typing/Lemmas.lean:863

This pat case of IsDefEq.sort_inv' is admitted with sorry, so sort inversion is incomplete in the presence of .pat (ι) reductions. This leaves universe well-formedness extraction axiom-dependent for equalities that take a .pat step.

  | pat _ _ _ _ _ ihe _ =>
    obtain eq | eq := eq
    · exact ihe (.inl eq)
    -- IOTA-TODO(soundness): sort-inversion through a pat (ι-)reduction reduct.
    · exact sorry

💡 Add a code-review agent skill or configure MCP servers for context-aware, tailored reviews. Learn more in the docs.

+theorem Aligned.addInduct (H : AddInduct C₁ venv₁ decl C₂ venv₂)
+    (h : Aligned safety C₁ venv₁) : Aligned safety C₂ venv₂ := by
+  -- IOTA-TODO(soundness): `Aligned` has no constructor for `addInduct`'s final
+  -- `addPat` stage, and records no per-step `addConst` witnesses, so the batch
+  -- `AddInduct` cannot rebuild an `Aligned`. `pats_iota` bypasses this (via
+  -- `TrEnv'.constMap_wf`); only the `Aligned`-routed `find?`/`of_value` family is
+  -- tainted.
+  sorry


+  -- IOTA-TODO(soundness): EqUpToLevels of a pat-reduction reduct; needs an
+  -- EqUpToLevels congruence for `RHS.apply`.
+  | pat _ _ _ _ _ ihe _ => exact ⟨ihe.1, sorry⟩


+  | pat _ _ _ _ _ ihe _ =>
+    obtain eq | eq := eq
+    · exact ihe (.inl eq)
+    -- IOTA-TODO(soundness): forallE-inversion through a pat (ι-)reduction reduct.
+    · exact sorry


+@[reducible] def toParams (env : VEnv) (henv : env.WF) (U : Nat) : Params where
+  env := env
+  henv := henv
+  univs := U
+  Pat := env.pats
+  pat_simple := fun hp => henv.pat_simple hp
+  -- IOTA-TODO(soundness): needs functionality of `env.pats` (a pattern determines its
+  -- reduct), false while `VInductDecl.WF` lets two rules register the same iota pattern
+  -- with different reducts; needs `VInductDecl.WF` to pin each rule's shape.
+  pat_uniq := sorry
+  -- `pat_wf` is the genuine content: recover a `Realizes` witness from `Check.OK` and
+  -- feed it to `IsDefEq.pat`.
+  pat_wf := fun {p r e m1 m2 Γ A} hpat hmatch hty hok =>
+    let ⟨_, hr, hall⟩ := hok.exists_realizer (rel := fun a b t => IsDefEq env U Γ a b t)
+    ⟨A, IsDefEq.pat hpat hmatch hty hr hall⟩
+  pat_app_l := fun hp hs => henv.pat_app_l hp hs
+  pat_app_l_uniq := fun hp hp' hs hs' hv => henv.pat_app_l_uniq hp hp' hs hs' hv
+  -- IOTA-TODO(soundness): needs `recN ≠ ru.ctor`, false while `VInductDecl.WF` leaves
+  -- `ru.ctor` an unconstrained `Name`; needs it to require `ru.ctor` be an actual
+  -- constructor (hence a registered constant distinct from recursor names).
+  pat_app_uniq := sorry
+  -- IOTA-TODO(soundness): demands every `env.defeqs df` be realised by a registered
+  -- pattern, but `addInduct` registers only ι patterns, never `SimplePattern.defn` (δ);
+  -- false for any env with a `def`/quot until δ-rule registration also installs `.defn`.
+  extra_pat := sorry


+/-- Soundness of `addInduct`: extending an `Ordered` environment with an inductive
+declaration keeps it `Ordered`.
+
+IOTA-TODO(soundness): not provable as stated. `Ordered` has no constructor for the
+`addPat` stage, and `VInductDecl.WF` does not line up the per-constant `uvars`;
+both need strengthening. -/
 theorem addInduct_WF (henv : Ordered env) (hdecl : decl.WF env)
    (henv' : addInduct env decl = some env') : Ordered env' :=
  sorry


+  | pat _ _ _ _ _ _ _ =>
+    -- IOTA-TODO(soundness): confluence for a pat (ι-)reduction step; needs a bridge
+    -- from `env.pats` to the abstract `Params.Pat` reduction to join via `ParRed.extra`.
+    exact sorry


 theorem Environment.constants_addDefs : ∀ {vs : List DefinitionVal} {env : Environment},
    (vs.foldl (fun e v => Lean.Kernel.Environment.add e (.defnInfo v)) env).constants =
    insertDefs env.constants vs


Comment-only cleanup: shortens the docstrings and IOTA-TODO reasons added for the iota work to match upstream's concise register (drops field-by-field enumerations, rationale essays, and the thesis citation). No code, statement, or proof changed; build green; the 12 IOTA-TODO tags are unchanged.

Strengthens the downstream ι interface after exercising it end-to-end: - AddInduct.rec_find now pins the full recursor telescope split (numMotives/numMinors/numIndices, not just getMajorIdx) and links each rule's model reduct to the kernel rule via TrExprS. The split is what iotaRHS consumes; the link is what a consumer needs to normalise the reduct. AddInduct is still unconstructed, so this strengthens an assumption with no new obligation until addDecl.WF's inductive case lands. - TrEnv.pats_iota' / TrEnv'.pats_iota' expose the registered witness (the concrete iotaRHS pair at the trivial check, over a template translating the kernel reduct) instead of the opaque existential, so the trivial check is instantiable; the plain pats_iota lemmas become corollaries. - TrEnv.iota_rec composes pats_iota' with iota_defeq into the rec-applied- to-constructor ≡ reduct step. Build green; 12 IOTA-TODO(soundness) unchanged; no new axioms; iota_rec / pats_iota' carry only the pre-existing TrProj sorryAx via the TrEnv' type.

barabbs · 2026-08-11T12:15:19Z

Quick follow-up

Since opening this I wired the ι interface into a downstream consumer end-to-end, which surfaced that the two exposed lemmas didn't actually compose as shipped: pats_iota handed back an opaque ∃ r, so there was no way to see the check was trivial and drive iota_defeq with it. The fixes are all contained in iota:

The recursor telescope split and the link from each rule's model reduct to the kernel rule are part of TrRecursor (numParams/numMotives/numMinors/numIndices, and TrExprS envR rval.levelParams [] rule.rhs ru.rhs), from which AddInduct.rec_find is derived. The split is what iotaRHS slices on; the TrExprS link is the only handle a caller has to normalise the reduct back against the kernel rule.rhs. AddInduct is still not constructed from Environment.addInductive (the inductDecl case of addDecl.WF is the remaining boundary), so nothing discharges it yet.
pats_iota' names the registered witness (the concrete iotaRHS pair at the trivial check, over a template translating the kernel reduct) instead of the opaque existential; the plain pats_iota is gone. As before sorryAx only via the existing TrProj.
TrEnv.iota_rec composes pats_iota' with iota_defeq into the rec-applied-to-constructor ≡ reduct step, the end-to-end composition that should have been checked in the first cut; inductiveReduceRecCore.WF now uses it for the ι case of recursor reduction.

Everything else has since moved: VInductDecl.WF is the direct-block specification, its side-conditions and addInduct_WF are proved, and the single remaining obligation is patsStrong (see the updated description above). The δ-as-.defn question is still open on my side. Happy to take any of it on once the way it should go gets established.

Alessandro

Experimental is not a default target, so its IsDefEq/IsDefEqStrong inductions never saw the new pat constructor and its VEnv literals never saw the pats field. Adds the missing pat cases (deferred with sorry, the ι-confluence metatheory, as in the Theory copies) in ParallelReduction (toTyping, church_rosser), Stratified and StratifiedUntyped, and pats _ _ := False to Stronger's VEnv'.out. lake build Lean4Lean.Experimental is green again (only pre-existing + these deferred sorries); no new axioms. Only the inductions over the global IsDefEqStrong needed it; the many Experimental modules with their own local defeq inductives are unaffected.

barabbs · 2026-08-18T16:29:23Z

Just noticed from CI that lake build Lean4Lean.Experimental (which isn't in the default targets) failed due to some missing pat case placeholders: added them now, so everything should pass :)

The reconcile merge 29d67a7 absorbed all five digama commits; the ladder entry is deleted per convention. Section 2 records: remote drift reconciled (watch items PR digama0#43/digama0#32/digama0#27 stand, re-checked at every checkpoint boundary), ladder position = lane phase (Lane R L4L-16N, Lane V checker pre-closure, Lane D D-ladder volume, 16E in slack). The V6 route-map row carries the banked repair recipe and its dependent-match residual (one focused Lane-V session); the collision risk row notes the absorption. reduceProjCore.WF discharge is ledger D022 (upstream-contribution candidate); D012 narrowed; D021 added.

Rework the ι-reduction model so that the Verify-side witness `AddInduct` carries only kernel data (the `InductiveVal`s/`RecursorVal`s, the stage successes, the `TrIndType`/`TrRecursor` translations, freshness and the constant order). The seven fields it previously assumed (`rec_find`, `rec_reg`, `ctor_find`, `value_find`, `find?_mono`, `wf`, `consts`) are now theorems, matching how `AddQuot` carries no trust fields. Theory: - `VExpr.RecShape`/`CtorShape`/`RuleShape`/`MotiveShape`/`MinorFor`: decidable syntactic shapes of recursor types, constructor types and ι reducts (thesis §2.6.3–2.6.4). - `VRecRule.ctorParams` (the constructor's own parameter count, needed by the auxiliary recursors of nested inductives), `VRecursor.getMajorIdx`/`getFirstIndexIdx`. - `VEnv.addInduct` staged as `addTypes`/`addCtors`/`addRecs`/`addRules`; `VInductDecl.WF` types each stage in the environment the kernel checks it in and records the rule bookkeeping (`rules_wf`, `rules_ctor`, `rules_total`, `rules_nodup`, ...). - `VEnv.PatWF := PatTyped ∧ TemplateHeaded`: the checked, monotone admissibility condition of `Ordered.pat`; `Ordered`/`Aligned` gain `pat` clauses. - Proved: `addInduct_WF`, `WF.pat_uniq`, `WF.pat_app_uniq`, `Aligned.addInduct`, `addInduct_le`/`addInduct_pat`; `toParams` takes `DefEqsAsPats` as an explicit hypothesis. - The one ι obligation left open is `VEnv.WF.patsStrong` (subject reduction of ι in the strong system); it is deferred together with the inversion/injectivity metatheory it depends on (`Injectivity.lean`). Verify: - `TrEnv'.induct` is no longer gated on `.safe`. - `addQuot.WF`/`addDecl.WF` take an `Environment.EqSafe` precondition: the previous proof was vacuous through `TrEnv'.no_inductInfo`. `Quot.checkEqType` is unchanged and matches the C++ kernel. - `Tests/IotaShape.lean` validates the shapes and `SimplePattern.iotaRHS` against `inductiveReduceRec` by `rfl`/`decide` over the recursors of 65 inductives. Experimental: the `pat` cases of the stratified/parallel-reduction metatheory stay `sorry` (pre-existing); comments updated. Non-Experimental `sorry` terms go from 33 to 24; no axioms added.

Upstream adds simultaneous substitution for the strong judgment, the primitive-constant verification layer, and the new level algorithm. Both sides had appended helpers to Theory/VExpr.lean; the two blocks are kept side by side (master's `Subst.Fixes`/`ClosedN.subst_eq`/subst lemmas, then the recursor- and constructor-shape helpers). Semantic resolutions: - Three pattern-stability lemmas under substitution in Theory/Typing/ Pattern.lean, mirroring the `instN` family: `Pattern.RHS.subst_apply`, `Pattern.matches_subst` and `Pattern.Check.Realizes.map_subst`. The `fixed` parts of a right-hand side are closed, so `ClosedN.subst_eq` discharges them and a substitution only reaches the holes. - A `pat` case for `IsDefEqStrong.substEq'`, following the `weakN`/`instN` template: the redex and its reduct both substitute, and the side conditions transport by `Realizes.map_subst`. - `OrderedStrong` threaded through the substitution and primitives layers. `IsDefEq.strong` needs subject reduction of the registered reduction rules, so master's substitution theorems (`IsDefEqStrong.substEq'`, `.subst`, `IsDefEq.substDF`, `.subst`, `HasType.subst`, `IsDefEqU.subst`, `IsType.subst`) and the primitives files now take `OrderedStrong` in place of `Ordered`. Every call site holds a `VEnv.WF` and obtains it via `WF.orderedStrong`; the `CoeOut` instance covers the uses that only need `Ordered`. - Verify/Environment/Quot.lean adapts to master's reshaped `checkName.WF` postcondition.

`VExpr.RuleShape` gains `nrec`, the number of arguments the reduct applies to the minor after the fields (thesis §2.6.4 `e_c b v`, `v::δ`), and `VInductDecl.WF.rule_shape` sets it to the minor premise's binders beyond the fields: `nfields ≤ piArity(minor)` and `nrec = piArity(minor) - nfields` — zero for a non-recursive constructor. A count only: the terms `v` are still pinned by nothing but `rules_wf`'s typing. Decidable via `VExpr.eq_mkApps_append_length_iff`. `WF.pats_split` exposes the minor and the count; `addRules_ordered` adapted. `Tests/IotaShape.lean`: `ruleShapeAt` decides the count; negative controls (`Nat.succ` with `nrec` 0 or 2, the case-analysis reduct without its inductive hypothesis, a field applied to the binderless `Nat.zero` minor); and `checkAll` runs every shape clause, `checkMore` (`rec_params`, `rules_own_params`, `rules_nodup`, `rules_ctor`) and the kernel-reduct agreement (`checkIotaAuto`) over 16 adversarial declarations (nested, mutual, reflexive, indexed, dependent, small-eliminating) and a sweep of 49 library inductive types.

VInductDecl.WF was a shape checklist: it omitted the §2.6.1-2.6.4 side conditions on a declaration, and it let a "recursor" range over a type former outside the block whose rules fired on arbitrary constants of the right arity. Both are admissibility gaps. A Prop with two constructors and a Sort u-eliminating recursor passed, and its environment derives (forall p:Prop, p -> p) = (forall p:Prop, p); a rule firing on a hider constant `c : forall (A : Type), A -> T` passes with a redex whose reduct is not typeable at the redex's type, which is what the subject-reduction argument for iota needs. The predicate now specifies a *direct* mutual block: every recursor eliminates one of the block's own type formers and every rule fires on one of that former's constructors. Nested inductives are outside it, as in the thesis, where the kernel's ElimNestedInductive compiles them to direct blocks before checking. New in Theory/Inductive.lean, mirroring Inductive/Add.lean syntactically where the kernel is syntactic and by typing where it infers types: - MentionsConst / ValidIndApp / FieldPositive / CtorPositive: strict positivity, after hasIndOcc, isValidIndApp? and checkPositivity. - CtorResult: the constructor returns its own former applied to the parameter variables in order and then its indices. MajorApp: the same for a recursor's major premise, replacing IndApp in RecShape, which pinned only an index suffix over an arbitrary constant. - LargeElim after isLargeEliminator, with the decidable half LargeElimShape. New fields: universes (one result sort for the block, imax(u, l) <= l for every constructor field, and large elimination only when a recursor asks for the extra universe parameter), ctors_params, ctors_result, ctors_positive, recs_over_block, rec_counts; rules_ctor now names the constructor instead of looking up a constant of the right arity, and subsumes rules_own_params, which becomes a lemma. Dependents: rules_ctor_shape restates the old rules_ctor field over the block's own constructors, so addInduct_rule_ctor and AddInduct.ctor_find are unchanged below it. addInduct_WF, addInduct_pat, WF.pat_uniq, WF.pat_app_uniq, WF.pat_simple, WF.pat_app_l, WF.pat_app_l_uniq and WF.patsIota stay sorry-free. Tests/IotaShape.lean decides the new clauses on the kernel's data for a list of Init/Std inductives, and adds the negative controls: Tree (its node constructor is not positive, its auxiliary recursor is off-block), a hand-built non-positive constructor type, and the two-constructor Prop asking for large elimination. Nested blocks keep their iota-agreement check against inductiveReduceRec.

`VEnv.PatsStrong` demanded subject reduction of every registered rule in every `Ordered` sub-environment of `env`. That quantification was an artefact of `OrderedStrong.strong`, which built `OnTypes env (EnvStrong env)` by `Ordered.induction`, whose motive exposes the environments it passes through only as `Ordered` subsets — arbitrary sub-selections, stronger than the thesis's regularity lemma (which is per system) and than what `Injectivity.lean` targets. The strengthening argument needs subject reduction only where constant types and definitional axioms are strengthened: the well-formed prefixes of `env` and their extensions by constants alone, which carry exactly a prefix's `pats`. `VEnv.WF.strong` now runs the induction over the `WF'` derivation instead, stage by stage — `foldlM_addConst_strong` for the constant folds of `addConsts` and of `addInduct`, `addQuot_chain` for the quotient chain, `addDefEqs_strong` and `addRules_strong` for the remaining steps — and `VEnv.PatsStrong` quantifies over exactly those environments, with `VEnv.WFPrefix` naming the prefix relation. `OrderedStrong` now records `strong : OnTypes env (EnvStrong env)` as a field rather than deriving it, so `OrderedStrong.strong` goes away and `PatsStrongOn` (subject reduction of the rules of `env`, in `env`) replaces the old `pats` field. `IsDefEq.strong`, `CtxStrong.strong` and every `variable! (henv : OrderedStrong env)` lemma keep their statements, so consumers are unchanged. `VDecl.WF.le` moves from `InductiveParams` to `EnvLemmas`, where `WFPrefix.le` needs it.

`VEnv.recSplit?` and its exactness lemma decoded a recursor's telescope split from what a bare `VEnv` retains of an ι entry; nothing in the theory or the verified checker consumes that, and `WF.pats_split` existed only to state it. Delete both, along with the module section that documented them, and keep `WF'.pats_origin`, the first step of the deferred ι subject-reduction proof. The shape, positivity and result-type predicates are used as propositions in the theory and executed only by the tests, so their `Decidable` instances (and the `DecidableEq` derivations and existential-decoding instances they rest on) move to `Lean4Lean.Tests.ShapeDecide`. `decidableExistsLT'` goes: instance search finds `Nat.decidableExistsLT` on its own. Also drop `MinorHeaded.recHeaded` and `iotaRHS_boundary_irrel`, which had no users.

`SMap.WF.find?_insert` repeated the proof of `find?_insert_of_map₂`, which needs less; make it a corollary. The four `find?`-after-insertion lemmas of `Verify/Environment/Basic.lean` are about `SMap`, not about constant maps, so state them there over an arbitrary key and value type; `insertConsts_find?_mono` is then `insertList_find?_mono` at the name projection. `List.Forall₂.append` follows from `append_of_left` instead of repeating its induction. The generic `LocalContext` lemmas about the empty context, one fresh declaration on top of it and `mkForall` as a fold were stated inside the quotient development; move them to `Verify/LocalContext.lean`, dropping `find?_eq_toList`, a restatement of `WF.find?_eq_find?_toList`. The `DecidableEq FVarId` instance they need moves with them and is no longer private.

The quotient telescopes were resolved by a ladder of `L*_wf`/`L*_fresh` lemmas feeding `find?_mkLocalDecl`, whose freshness hypothesis forced a separate `find?`-is-`none` proof for every prefix, and by a `quot_find` macro enumerating seventeen lookup paths through that ladder. Freshness is not needed: `find?` after `mkLocalDecl` is determined by the underlying map's well-formedness alone, which `mkLocalDecl` preserves unconditionally. Restate `LocalContext.find?_mkLocalDecl` over `fvarIdToDecl.WF`, add the two lemmas that produce it, and drop the freshness ladder. `quot_find` then collapses into `quot_simp`, which already rewrote with the `L*_find` ladder and decided the fvar comparisons, so `quot_mem` discharges its membership goals directly. Also wrap the file to 100 columns.

`quot.cpp`'s `check_eq_type` pins the shape of `Eq` but not its safety, and the four quotient constants it then adds carry no safety flag, while `Quot.lift`'s type mentions `Eq`. Initializing quotients over an `unsafe inductive Eq` would leave safe constants depending on an unsafe one, so the environment would have no model at the safe level. `checkEqType` now rejects that, and `checkEqType_ok` reports the safety of `Eq` along with its shape. The obligation was previously discharged by an assumption on the caller, `Environment.EqSafe`; delete it, together with the hypothesis it fed in `addQuot.WF` and `addDecl.WF`, which are now unconditional. Record the divergence.

The `pat` rule of `VEnv.IsDefEq` left four inductions in `Experimental` with an unproved case. `ParallelReduction`'s abstract `Typing` gains `pat_env`, the field `ChurchRosser`'s `Params` already carries: a registered reduction rule is a `Pat` rule. With it, `pat` reduces to the neighbouring `extra` case in both `IsDefEq.toTyping` and `IsDefEqU.church_rosser` — a single parallel step on the redex against no step on the reduct. The stratified systems had no rule to translate an ι step into, so give `IsDefEq1` and `IsDefEqU1` a `pat` constructor mirroring `IsDefEq.pat` (the untyped one dropping the side conditions' types). The strong system annotates its `pat` with the typing of the reduct, so both components of the induction's conclusion are available, exactly as for `extra`.

Cut the module doc of `InductiveLemmas` and the docstrings of `VEnv.PatTyped` and `VEnv.PatWF` down to what they state, dropping the running commentary and the note on how `PatWF` got its name. In the ι interface of `Verify/Environment/Lemmas.lean`, `TrEnv'.pats_iota'` took its recursor and rule hypotheses in the opposite order to `TrEnv.pats_iota'`; align them. Delete `TrEnv'.pats_iota` and `TrEnv.pats_iota`, which restated the primed lemmas with the witness dropped and had no users, and say of `iota_rec` what it is for.

Split `inductiveReduceRec` so that its ι step -- the rule lookup for the major premise's head constructor and the slicing that builds the reduct -- is the pure function `inductiveReduceRecCore`, leaving the whnf of the major and the K-like and structure-η conversions in the caller. The split is behaviour-preserving: the extracted body is the original one, with `getMajorIdx` recomputed where the caller had bound it. Prove `inductiveReduceRecCore.WF`: on a redex whose major premise is a saturated constructor application, the kernel's reduct translates to the redex's own translation. The proof takes the redex's translation apart along the recursor's telescope split, matches it against the ι pattern the translated environment registers for the rule (`TrEnv.iota_rec`), and identifies the model's `SimplePattern.iotaRHS` reduct with the kernel's slicing. Saturation of the major is a hypothesis: it is what makes the two slicings agree -- the kernel takes the last `nfields` arguments of the major, the pattern the ones past the constructor's parameters -- and it follows from the redex being well-typed. Supporting lemmas: `Expr.getAppFn_mkAppList` and its `getAppArgs` companions; `TrExprS.mkAppList_inv`, inverting the translation of an application spine; `TrExpr.mkAppList`, rebuilding one over a well-typed model spine. `reduceRecursor.WF` stays open: its other paths reduce the major by `toCtorWhenK` or `toCtorWhenStruct`, which have no counterpart in `IsDefEq`.

`VEnv.toParams` had no consumer, so nothing showed that its `DefEqsAsPats` hypothesis is satisfiable. Add the `addInduct_defeqs` chain, `inductParams`, and `crDefEq_of_induct`.

barabbs added 11 commits July 21, 2026 15:19

refactor: relocate Pattern core to Theory/Pattern

cb920e1

Pattern/RHS/Check depend only on Theory.VExpr; moving them out of Theory/Typing/ lets VEnv reference the pattern registry without inverting the Theory/Typing layer hierarchy. No semantic change.

Copilot AI lite review requested due to automatic review settings August 8, 2026 09:44

Copilot started reviewing on behalf of barabbs August 8, 2026 09:44 View session

Copilot AI reviewed Aug 8, 2026

View reviewed changes

barabbs force-pushed the iota branch from a01c918 to 349da4b Compare August 8, 2026 09:57

barabbs added 9 commits September 4, 2026 09:36

barabbs added 5 commits September 8, 2026 12:28

docs: exercise the Params instance on an inductive environment

3de1dcb

`VEnv.toParams` had no consumer, so nothing showed that its `DefEqsAsPats` hypothesis is satisfiable. Add the `addInduct_defeqs` chain, `inductParams`, and `crDefEq_of_induct`.

docs: fix a stale lemma name in the ι interface header

38ea0de

Navigation Menu

Iota Reduction - #43

Iota Reduction#43
barabbs wants to merge 28 commits into
digama0:masterfrom
barabbs:iota

barabbs commented Aug 8, 2026 •

edited

Loading

Uh oh!

Copilot AI left a comment

Uh oh!

barabbs commented Aug 11, 2026 •

edited

Loading

Uh oh!

barabbs commented Aug 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Conversation

barabbs commented Aug 8, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What's where

The deferred obligation

Uh oh!

Copilot AI left a comment

Choose a reason for hiding this comment

Pull request overview

Reviewed changes

Uh oh!

barabbs commented Aug 11, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

barabbs commented Aug 18, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

barabbs commented Aug 8, 2026 •

edited

Loading

barabbs commented Aug 11, 2026 •

edited

Loading