docs: update README and add ARCHITECTURE.md

Author: Arthur Freitas Ramos

README.md

@@ -1,10 +1,9 @@
 # Metatheory
 
 [![Lean 4](https://img.shields.io/badge/Lean-4.24.0-blue.svg)](https://lean-lang.org/)
-[![Mathlib](https://img.shields.io/badge/Mathlib-v4.24.0-green.svg)](https://github.com/leanprover-community/mathlib4)
 [![License: MIT](https://img.shields.io/badge/License-MIT-yellow.svg)](https://opensource.org/licenses/MIT)
 
-A comprehensive **programming language metatheory library for Lean 4**, providing formally verified proofs of fundamental results in rewriting theory and type systems.
+A comprehensive **programming language metatheory library for Lean 4**, now spanning **130+ Lean files and 58K+ lines** of mechanized proofs and metatheoretic case studies.
 
 ## Overview
 
@@ -20,6 +19,15 @@ Metatheory formalizes core results from programming language theory:
 - **System F** (Polymorphic Lambda Calculus): Subject reduction with type substitution
 - **Term/String Rewriting**: Confluence via Newman's lemma, critical pair analysis, and first-order TRS completion (KBO/LPO)
 - **TRS Proof Comparison**: Diamond vs Newman confluence for a tiny deterministic TRS
+- **Extended Formalizations**: 78 standalone modules covering type systems, semantics, compilation, effects, logic, macros, and automation
+
+### Project Scale
+
+- **Tracked Lean files**: 155 (`git ls-files '*.lean'`)
+- **Tracked Lean LOC**: 58,126
+- **Lean files under `Metatheory/`**: 153
+- **Standalone modules under `Metatheory/*.lean`**: 78
+- **Top-level dependency model**: no Mathlib requirement in `lakefile.toml`; many standalone modules are self-contained
 
 
 ### Why Metatheory?
@@ -29,7 +37,7 @@ Metatheory formalizes core results from programming language theory:
 | **Multiple proof techniques** | Learn different approaches to confluence (Diamond, Newman, Hindley-Rosen) |
 | **Layered architecture** | Generic framework instantiated by specific systems |
 | **De Bruijn indices** | Capture-avoiding substitution without alpha-equivalence |
-| **Mathlib integration** | Uses Mathlib for standard lemmas; core theorems axiom-free |
+| **Dependency-light design** | Top-level build has no Mathlib requirement; many modules are self-contained |
 | **Axiom/placeholder free** | No `axiom`/`constant` declarations and no `sorry`/`admit` |
 | **Extensively documented** | Docstrings, references, and proof explanations |
 
@@ -39,7 +47,6 @@ Metatheory formalizes core results from programming language theory:
 
 - [Lean 4](https://lean-lang.org/lean4/doc/setup.html) (version 4.24.0 or compatible)
 - [Lake](https://github.com/leanprover/lake) (included with Lean)
-- [Mathlib](https://github.com/leanprover-community/mathlib4) (automatically fetched by Lake)
 
 ### Building
 
@@ -191,6 +198,109 @@ example {M : Term} {τ : Ty} (h : ⊢ M : τ) : M.IsValue ∨ ∃ N, M.Step N :=
   progress h
 ```
 
+## Extended Formalizations (Standalone Modules)
+
+In addition to the layered core directories (`Rewriting/`, `Lambda/`, `CL/`, `TRS/`, `StringRewriting/`, `STLC/`, `STLCext/`, `STLCextBool/`, `SystemF/`), the project includes **78 standalone modules** at `Metatheory/*.lean`.
+
+### Type systems and typing disciplines
+
+- `AbstractionSafety.lean` — Safety-oriented typing relation with abstraction-preservation lemmas.
+- `AffineTypes.lean` — Affine ownership typing inspired by Rust-style single-use resources.
+- `Bidirectional.lean` — Bidirectional typing (synthesis/checking) for concise typing derivations.
+- `ContractTypes.lean` — Contract-annotated typing with interface-level guarantees.
+- `DependentPattern.lean` — Dependently typed pattern matching and indexed elimination structure.
+- `EffectSystems.lean` — Type-and-effect judgments with explicit effect labels.
+- `Gradual.lean` — Gradual typing with dynamic type and consistency relations.
+- `GradedTypeTheory.lean` — Graded modality/type usage tracking (0/1/ω-style discipline).
+- `InformationFlow.lean` — Security typing over a lattice of confidentiality levels.
+- `Intersection.lean` — Intersection type operators and associated metatheoretic lemmas.
+- `LinearTypes.lean` — Linear usage-sensitive typing and structural control.
+- `PolymorphismVariants.lean` — Comparative formalization of polymorphism design variants.
+- `QuantitativeTypes.lean` — Quantitative type usage accounting for resource-aware typing.
+- `RecursiveTypes.lean` — Recursive type constructors with unfold/fold metatheory.
+- `Refinement.lean` — Refinement-annotated base types with predicate-indexed judgments.
+- `RefinementTypes.lean` — Predicate subtyping and refinement typing rules.
+- `RowPoly.lean` — Row polymorphism for extensible typing contexts/signatures.
+- `SecrecyTypes.lean` — Secrecy/security labels integrated into typing judgments.
+- `SessionTypes.lean` — Binary session type protocols for typed communication.
+- `SizedTypes.lean` — Size indices for termination/productivity-aware typing.
+- `TemporalTypes.lean` — Temporal type structure over trace-indexed behavior.
+- `TypeClasses.lean` — Type-class declarations and resolution-oriented typing scaffolding.
+- `TypeInference.lean` — Constraint-based type inference for monomorphic fragments.
+- `TypeInhabitance.lean` — Constructive inhabitation results (type-to-term witness style).
+- `TypePreservation.lean` — Standalone substitution and preservation theorems.
+- `UniversePolymorphism.lean` — Universe-level expressions and polymorphic universe handling.
+
+### Semantics, normalization, and equivalence
+
+- `AbstractInterpretation.lean` — Abstract interpretation skeletons with soundness-oriented structure.
+- `AbstractMachines.lean` — CEK/Krivine/SECD-style machine encodings and transitions.
+- `CallByPushValue.lean` — Call-by-push-value syntax, translation, and metatheory lemmas.
+- `CategorySemantics.lean` — Categorical semantics building blocks for typed languages.
+- `Coinduction.lean` — Coinductive streams/processes and bisimulation-style reasoning.
+- `DomainTheory.lean` — Domain/path-style order-theoretic lemmas for denotational settings.
+- `Erasure.lean` — Erasure translation preserving key typing/evaluation structure.
+- `GameSemantics.lean` — Game-semantic traces/plays with compositional properties.
+- `LogicalRelations.lean` — Logical-relations framework for normalization/equivalence proofs.
+- `ModalTypeTheory.lean` — Modal type-theoretic syntax and proof obligations.
+- `NormByEval.lean` — Normalization by evaluation (NbE) core constructions.
+- `Normalization.lean` — Generic normalization-oriented lemmas and structures.
+- `ObservationalEquality.lean` — Observational/contextual equality formulations.
+- `ParallelReduction.lean` — Parallel reduction relation and confluence-support infrastructure.
+- `Parametricity.lean` — Relational parametricity setup for polymorphic calculi.
+- `ProgramEquivalence.lean` — Program equivalence relations and congruence toolkit.
+- `Realizability.lean` — Realizability semantics over combinatory-style structures.
+- `Termination.lean` — Well-founded termination analysis and accessibility lemmas.
+
+### Compilation and transformation pipeline
+
+- `ANFRegAlloc.lean` — ANF conversion plus register-allocation metatheory.
+- `CPS.lean` — CPS-focused typed syntax and proof support.
+- `CPSTransformation.lean` — Source-to-CPS transformation and simulation lemmas.
+- `CompilerOptimizations.lean` — Verified optimization rewrites for a small compiler core.
+- `ElaborationAlgorithm.lean` — Surface-to-core elaboration algorithm components.
+- `StackMachineCompilation.lean` — Compilation to stack machine code with correctness statements.
+- `StackMachines.lean` — Stack machine semantics and execution lemmas.
+- `SyntaxTransformers.lean` — Generic syntax transformer combinators and properties.
+
+### Effects, concurrency, and resource management
+
+- `AlgebraicEffects.lean` — Algebraic effects with handlers and effect-row-style structure.
+- `EffectHandlers.lean` — Typed handler interfaces and operational effect handling.
+- `ConcurrencyTypes.lean` — Typing-oriented concurrency process/rewrite structure.
+- `MemoryManagement.lean` — Memory-aware terms/types and management invariants.
+- `SessionProc.lean` — Session-typed process calculus fragments and safety scaffolding.
+
+### Logic, proof theory, and structural systems
+
+- `Focusing.lean` — Focused proof search structure with polarized connectives.
+- `LinearLogic.lean` — Linear logic formulae and proof-theoretic infrastructure.
+- `ModalLogic.lean` — Modal proof system lemmas and formula structure.
+- `OTT.lean` — OTT-style syntax/typing support definitions.
+- `ProofIrrelevance.lean` — Proof irrelevance principles and consequences.
+- `ProofNets.lean` — Proof-net representation for linear logic fragments.
+- `ResourceLogic.lean` — Resource-sensitive logic connectives and judgments.
+- `SeparationLogic.lean` — Separation logic structures and composition lemmas.
+- `Sequent.lean` — Sequent calculus style rewriting/judgment relations.
+- `Substructural.lean` — Substructural logic framework controlling structural rules.
+
+### Macros, metaprogramming, and proof automation
+
+- `HigherOrderUnification.lean` — Higher-order unification syntax and solving scaffolding.
+- `HygienicMacros.lean` — Hygienic macro expansion and scope-safety metatheory.
+- `InductionRecursion.lean` — Induction-recursion universes and code interpretations.
+- `MacroSystems.lean` — Macro system core with scoped marks and expansion relations.
+- `MacroTyping.lean` — Macro typing/staging rules for typed expansion.
+- `TacticFrameworks.lean` — Lightweight tactic framework formalization hooks.
+
+### Project scaffolding and integration modules
+
+- `Basic.lean` — Minimal sandbox module used for local sanity checks.
+- `Confluence.lean` — Standalone confluence/closure helper development.
+- `DeBruijn.lean` — De Bruijn-indexed substitution/renaming infrastructure.
+- `Metrics.lean` — Project metrics and theorem inventory checks.
+- `MetatheoryGrandTour.lean` — Grand tour module connecting major components.
+
 ## Key Theorems
 
 ### Generic Rewriting Framework
@@ -292,6 +402,7 @@ example {M : Term} {τ : Ty} (h : ⊢ M : τ) : M.IsValue ∨ ∃ N, M.Step N :=
 Metatheory/
 ├── Metatheory.lean              # Main entry point
 ├── Metrics.lean                 # Project statistics and theorem summary
+├── *.lean (78 standalone modules) # Extended formalizations; see section above
 │
 ├── Rewriting/                   # Layer 0: Generic ARS Framework
 │   ├── Basic.lean               # Star, Plus, Joinable, Diamond, Confluent

docs/ARCHITECTURE.md

@@ -0,0 +1,188 @@
+# Metatheory Architecture
+
+This document summarizes the architecture of the `Metatheory` Lean 4 project after reviewing all tracked `.lean` files in the repository.
+
+## 1) Two-tier architecture
+
+Metatheory has two distinct layers:
+
+### A. Core formalized modules (tightly coupled)
+
+Core directories:
+
+- `Metatheory/Rewriting`
+- `Metatheory/Lambda`
+- `Metatheory/CL`
+- `Metatheory/TRS`
+- `Metatheory/StringRewriting`
+- `Metatheory/STLC`
+- `Metatheory/STLCext`
+- `Metatheory/STLCextBool`
+- `Metatheory/SystemF`
+
+Characteristics:
+
+- Deep interdependencies across modules (especially through `Rewriting` and between typed/untyped calculi).
+- Shared proof infrastructure (`Star`, `Confluent`, `Diamond`, termination, normal forms).
+- Generic-to-specific proof reuse (e.g., proving a local property once, then lifting to confluence through generic theorems).
+- Mathlib-facing interoperability via `Rewriting/Compat.lean` (mathlib-style naming), plus targeted Mathlib imports in advanced TRS components.
+
+### B. Extended standalone modules (broad, mostly self-contained)
+
+At `Metatheory/*.lean`, there are about ~70+ standalone modules (currently 78 files) covering topics like effects, macro systems, abstract interpretation, domain/game/category semantics, compilation, and advanced type disciplines.
+
+Characteristics:
+
+- Usually self-contained, with light or no imports.
+- Repeated use of a lightweight **computational paths** style (`Step`/`Path`) rather than depending on the full generic rewriting stack.
+- Local proof algebra built from path composition and symmetry (`trans`, `symm`) and context lifting (`congrArg`-style transport).
+
+---
+
+## 2) Core module dependency graph
+
+Directory-level dependencies (cross-module):
+
+```text
+Rewriting      -> (foundation; no core dependency)
+Lambda         -> Rewriting
+CL             -> Rewriting
+TRS            -> Rewriting
+StringRewriting-> Rewriting
+STLC           -> Lambda, Rewriting
+STLCext        -> Rewriting
+STLCextBool    -> STLCext, Rewriting
+SystemF        -> Rewriting
+```
+
+Mermaid view:
+
+```mermaid
+graph TD
+  Rewriting --> Lambda
+  Rewriting --> CL
+  Rewriting --> TRS
+  Rewriting --> StringRewriting
+  Rewriting --> STLC
+  Rewriting --> STLCext
+  Rewriting --> STLCextBool
+  Rewriting --> SystemF
+  Lambda --> STLC
+  STLCext --> STLCextBool
+```
+
+Representative internal pipelines:
+
+- **Lambda:** `Term → Beta → MultiStep → Parallel → Complete → Diamond → Confluence/Generic`
+- **STLCext:** `Types/Terms/Reduction/Parallel/Complete → Confluence`
+- **SystemF:** `Types/Terms/Typing → SubjectReduction + StrongReduction + StrongNormalization → Parallel/Complete/Diamond → Confluence`
+- **TRS/StringRewriting:** `Syntax/Rules → local confluence + termination → Newman-based confluence`
+
+---
+
+## 3) Core types and relations
+
+| Name | Location | Role |
+|---|---|---|
+| `Term` | `Lambda/Term.lean`, `CL/Syntax.lean`, `SystemF/Terms.lean`, `STLCext*/Terms.lean`, `TRS/FirstOrder/Syntax.lean` | Object language terms (de Bruijn in lambda/system F; first-order terms over signatures in TRS). |
+| `Ty` | `STLC/Types.lean`, `STLCext/Types.lean`, `STLCextBool/Types.lean`, `SystemF/Types.lean` | Type grammars for each calculus. |
+| `Subst` | `TRS/FirstOrder/Syntax.lean` (`Nat → Term sig`), `SystemF/StrongNormalization.lean` | Substitution models for first-order and higher-order developments. |
+| `Signature` | `TRS/FirstOrder/Syntax.lean` | Function symbols + arity for first-order TRS. |
+| `Rule` / `RuleSet` | `TRS/FirstOrder/Rules.lean` | Rewrite rules and rule predicates. |
+| `HasType` | `STLC/Typing.lean`, `STLCext/Typing.lean`, `STLCextBool/Typing.lean`, `SystemF/Typing.lean` | Typing judgments. |
+| `Step` | multiple modules | One-step reduction relation. |
+| `ParRed` | `Lambda/Parallel.lean`, `CL/Parallel.lean`, `STLCext/Parallel.lean`, `STLCextBool/Parallel.lean`, `SystemF/Parallel.lean` | Parallel reduction for diamond-style confluence proofs. |
+| `Star`, `Plus`, `Joinable`, `Diamond`, `Confluent`, `Terminating` | `Rewriting/Basic.lean` | Generic ARS closure/confluence/termination framework. |
+
+---
+
+## 4) Key theorems across the project
+
+### Generic rewriting framework
+
+- `Rewriting.confluent_of_diamond` (`Rewriting/Diamond.lean`)
+- `Rewriting.confluent_of_terminating_localConfluent` (`Rewriting/Newman.lean`)
+- `Rewriting.confluent_union` (Hindley-Rosen, `Rewriting/HindleyRosen.lean`)
+- Normal-form uniqueness/existence results in `Rewriting/Basic.lean`
+
+### Lambda calculus / CL
+
+- `Lambda.confluence` (Church-Rosser, `Lambda/Confluence.lean`)
+- `Lambda.parRed_diamond` (`Lambda/Generic.lean`)
+- `CL.parRed_diamond`, `CL.confluent`, `CL.church_rosser` (`CL/Confluence.lean`)
+
+### TRS / String rewriting
+
+- `TRS.local_confluent`, `TRS.step_terminating`, TRS confluence via Newman (`TRS/Confluence.lean`)
+- `StringRewriting.local_confluent`, `StringRewriting.step_terminating`, and confluence (`StringRewriting/Confluence.lean`)
+
+### STLC / extended STLC / booleans / System F
+
+- `STLC.subject_reduction`, `STLC.strong_normalization`
+- `STLCext.subject_reduction`, `STLCext.strong_normalization`, `STLCext.confluence`
+- `STLCextBool.subject_reduction`, `STLCextBool.strong_normalization`, `STLCextBool.confluence`
+- `SystemF.subject_reduction`, `SystemF.strong_normalization`, `SystemF.confluence`
+
+---
+
+## 5) Computational paths pattern in standalone modules
+
+Many standalone modules use a recurring lightweight proof kernel:
+
+```lean
+inductive Step (α : Type) : α → α → Type
+inductive Path (α : Type) : α → α → Type
+def Path.trans : Path α a b → Path α b c → Path α a c
+def Path.symm : Path α a b → Path α b a
+def Path.congrArg ...
+```
+
+Interpretation:
+
+- `Step`: named atomic rewrite/equational moves.
+- `Path`: explicit proof object for multi-step chains.
+- `trans`: composition of chains (path concatenation).
+- `symm`: reversible reasoning.
+- `congrArg` (and variants): lift paths through context/formers.
+
+This functions as a local, domain-specific rewriting/equality framework without requiring the full generic ARS stack in each standalone file.
+
+---
+
+## 6) Design decisions
+
+### De Bruijn indices
+
+- Used in `Lambda`, `STLC`-adjacent term layers, and `SystemF`.
+- Avoids alpha-conversion bureaucracy and gives direct structural recursion for substitution/shift lemmas.
+
+### Parallel reduction for confluence
+
+- Core confluence strategy in `Lambda`, `CL`, `STLCext`, `STLCextBool`, and `SystemF`.
+- Standard pipeline: define `ParRed` + `complete` development, prove diamond, then apply generic `confluent_of_diamond`.
+
+### Tait/logical-relations method for strong normalization
+
+- Used in `STLC/Normalization.lean`, `STLCext/Normalization.lean`, and `SystemF/StrongNormalization.lean`.
+- Main shape: reducibility candidates / reducibility predicate / fundamental lemma / SN corollary.
+
+---
+
+## 7) Future work and currently parked pieces
+
+### TRS FirstOrder case-study modules are intentionally parked
+
+The following files contain TODO comment blocks around substantial proof/code regions tied to missing dependency alignment (e.g., `Fin.cons`, `List.Shortlex`, related Mathlib APIs):
+
+- `TRS/FirstOrder/GroupTheory.lean`
+- `TRS/FirstOrder/BooleanCaseStudy.lean`
+- `TRS/FirstOrder/DependencyPairs.lean`
+
+Related TODO marker:
+
+- `TRS/FirstOrder/Examples.lean` includes a restoration note for `Ordering/DependencyPairs`.
+
+### STLCext confluence is already present
+
+`Metatheory/STLCext/Confluence.lean` exists and proves confluence (Church-Rosser form) using the same parallel-reduction + diamond architecture as other core calculi.
+