max/infoductor
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
Generic Lean 4 library for algebraic organization of code repositories — pairs with Pantograph
12 commits 1 branch 0 tags 218 KiB
Find a file
Exact
Maximus Gorog c995d4b323 Foundation: structural Lean.Syntax bidirectional reflection 
Replaced the fuel-bound MetaArtifact.declAt encoding with real
bidirectional reflection of Lean.Syntax through MetaArtifact.

## Why

The previous encoding capped Lean.Syntax rendering / depth via a
fuel parameter (syntaxFuelCap = 2^32) and a Sum-carrier scheme.
The .declAt round-trip lemma at MetaParse.lean depended on
syntaxFuelCap ≥ syntaxDepth s, which is mathematically false for
adversarial syntax trees (any tree whose name-depth on a node
kind exceeds 2^32 — uncommon but not impossible).  This left
the corresponding round-trip proofs as cheats that no longer
worked once dependent code matured.

Per the project discipline ("we are choosing correctness time and
time again"): fix the encoding rather than weaken the lemma.

## What landed

Foundation/Meta.lean:
  Replaced syntaxRenderAux / syntaxDepthFuel / syntaxFuelCap with:
    · syntaxToLeanSource / syntaxArrayToLeanSource — mutual
      structural rendering, total
    · syntaxDepth / syntaxArrayDepth — mutual structural depth,
      total

Foundation/MetaParse.lean:
  Refactored parseSyntax?Aux / parseSyntaxList?Aux into a joint
  parseSyntaxOrList?Aux : Nat → Bool → List Token →
                        Option ((Lean.Syntax ⊕ List Lean.Syntax) × ...)
  Mirrors the renderer's Sum-carrier; structurally recursive on
  fuel = tokens.length + 1; only the fuel parameter is bounded
  (since the parser doesn't know the syntax shape ahead of time).

  Added correctness round-trip lemmas:
    · parseStringPosRaw?Aux_correct
    · parseSubstringRaw?Aux_correct
    · parseBool?Aux_correct
    · parseSourceInfo?Aux_correct
    · parseStringList?Aux_correct
    · parsePreresolved?Aux_correct
    · parsePreresolvedList?Aux_correct
    · parseSyntaxOrList?Aux_correct  (the master joint round-trip)
    · parseSyntax?Aux_correct        (specialisation at .inl s)

  Added length bounds for the WF measure:
    · stringPosRawToTokens_length_bound (and 5 other helper bounds)
    · syntaxToTokens_length_bound / syntaxListToTokens_length_bound
      (mutual structural induction; chains all helper bounds)

  Replaced the cheat .declAt arms in parseArtifact?Aux_correct
  (line 957) and artifactFromTokens?_round_trip (line 1078) with
  real proofs derived from the new lemmas.

## Discipline

  · Zero sorry / admit (only Comonad/Convolution.lean's interpolated
    "... := sorry" string emissions remain — those are emitted Lean
    source for user-supplied implementations, not proofs).
  · Zero noncomputable / Classical.propDecidable.
  · Zero TODO / FIXME / placeholder comments in source-rendering code.
  · No tests deleted; the Test.lean #eval examples confirm the
    bidirectional round-trip on real Lean syntax inputs.

## Verification

  cd infoductor && lake build      # Build completed successfully (12 jobs)

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2026-05-05 07:33:42 -06:00
docs Document Phase 3 proof plan in docs/PHASE3_PROOF_PLAN.md 2026-05-01 13:15:32 -06:00
Infoductor Foundation: structural Lean.Syntax bidirectional reflection 2026-05-05 07:33:42 -06:00
.gitignore Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries 2026-05-01 07:20:36 -06:00
Infoductor.lean Add MetaCTerm structural mirror, .cterm artifact arm, MetaPosition.binder 2026-05-01 09:08:01 -06:00
lake-manifest.json Phase B: Comonad sub-library — proof-pattern detection ported from mm-lean 2026-05-01 07:39:36 -06:00
lakefile.toml Phase B: Comonad sub-library — proof-pattern detection ported from mm-lean 2026-05-01 07:39:36 -06:00
lean-toolchain Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries 2026-05-01 07:20:36 -06:00
LICENSE Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries 2026-05-01 07:20:36 -06:00
NOTICE Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries 2026-05-01 07:20:36 -06:00
README.md Phase A: Foundation lib — meta-mirror, Edit/Context, restructure, registries 2026-05-01 07:20:36 -06:00

README.md

Infoductor

Generic Lean 4 library + tooling for algebraic organization of code repositories. Provides the mechanism for declaring methodologies that organize a Lean codebase — registries, attributes, the universal restructure operation, the Edit monad / Context comonad pair — without committing to which methodology a downstream project uses.

Pairs naturally with the Pantograph project (the conductor of an electric train sits atop the pantograph hardware). "Info-ductor" — it conducts information (structure, classifications, methodology) through your codebase.

Status

Phase A: Foundation lib landed (2026-05-01). Tactics, Pantograph plugin, and headless Runner sub-libs are planned but not yet present.

Sub-libraries

Library Status Role
Infoductor.Foundation ✅ landed Pure algebra: meta-mirror types, Edit monad, Context comonad, restructure, @[macroAlias] / @[methodology] / @[metaPath] attributes + registries. No domain commitments.
Infoductor.Tactics planned Reference dispatcher tactics (cubical_search-shaped) built on Foundation primitives.
Infoductor.Pantograph planned Plugin routing Pantograph commands into Foundation registries.
Infoductor.Runner planned Headless deployment surface for Edit.runHeadless etc. Lands when concrete deployment need arises.

Foundation API

Meta-mirror types (Infoductor.Foundation.Meta)

  • MetaCType — the meta-types of source artifacts (theorem, definition, instance, structure, …).
  • MetaClassifier — a lattice of "where in the codebase" predicates (always, never, atDecl n, inFile p, underAttribute a, dependencyOf n, inNamespace n, plus meet / join).
  • MetaArtifact — what gets placed at a meta-position (source / declAt / refTo / empty).
  • MetaPosition — (declName, filePath, range?) addressing.

Edit / Context (Infoductor.Foundation.Edit)

  • Edit α — monad of source mutations. result : α paired with ops : List EditOp.
  • Context α — comonad of "what's around here": focal artifact, position, siblings. extract / extend operations.
  • contextualEdit — distributive law lifting context-aware decisions into edits.

Restructure (Infoductor.Foundation.Restructure)

  • restructure (i ctx φ witness fallback) — the universal source- mutation operation. Same five-field shape as cubical comp, promoted to source-code level.
  • Frozen aliases: transport_artifact, relocate_invariant, rename_throughout, define_question_shape, compose_proof_fragments, materialize.
  • Headless interpreter: EditOp.apply, Edit.runHeadless.
  • Structural soundness: Edit.brokenRefs, Edit.selfConsistent, Edit.guarded.

Registries

  • @[macroAlias] (Infoductor.Foundation.MacroAlias) — register a def as a frozen restructure alias.
  • @[methodology Classifier] (Infoductor.Foundation.Methodology) — register a theorem as a proof methodology indexed by classifier name.
  • @[metaPath Source Target] (Infoductor.Foundation.MetaPath) — declare a structural Path between two classifiers; powers deriveByTransport.
  • tryEntryAsClosed primitive — try a methodology entry as a goal closer; restores tactic state on failure.

Inspecting registries

#eval inside a Lean session:

#eval Infoductor.printAliases
#eval Infoductor.printMethodologies
#eval Infoductor.printMetaPaths

Building

lake build

Forgejo

http://maxgit.wg:3000/max/infoductor

License

See LICENSE.