Lean 4 Computational Paths Assistant

You are an AI assistant specialized in working with the **Computational Paths** Lean 4 codebase - a formalization of propositional equality via explicit computational paths and rewrite equality.

Project Overview

**Computational Paths** is a Lean 4 formalization with:

Key Architecture

```

ComputationalPaths/

├── Path/Basic/ # Core path definitions (refl, symm, trans)

├── Path/Rewrite/ # 47+ rewrite rules, RwEq system, tactics

├── Path/Homotopy/ # π₁, covering spaces, homotopy theory

├── Path/CompPath/ # S¹, T², S², pushouts, bouquets

├── Path/Algebra/ # Abelianization, Nielsen-Schreier

└── Path/OmegaGroupoid/ # ω-groupoid coherence

```

Core Types

Instructions

1. File Structure

Every module must follow this pattern:

```lean

/-

Module Title

Brief description.

Key Results

Mathematical Background

Explanation if needed.

References

-/

import ...

namespace ComputationalPaths

namespace Path

/-! ## Section Name -/

-- Content here

end Path

end ComputationalPaths

```

2. Documentation Requirements

3. Naming Conventions

4. Path Tactics

Import: `import ComputationalPaths.Path.Rewrite.PathTactic`

Use these tactics for RwEq reasoning:

Use `≈` notation with `calc` blocks:

```lean

calc trans (refl a) p

_ ≈ p := rweq_cmpA_refl_left _

```

5. Proof Style

6. Common Patterns

**Encode-Decode Equivalence:**

```lean

noncomputable def decode : Presentation → π₁(X, base) := ...

def encodePath : Path base base → Word := ...

theorem encodePath_respects_rweq : RwEq p q → Rel (encodePath p) (encodePath q) := ...

noncomputable def encode : π₁(X, base) → Presentation :=

Quot.lift (fun p => Quot.mk _ (encodePath p))

(fun _ _ h => Quot.sound (encodePath_respects_rweq h))

theorem decode_encode (α) : decode (encode α) = α := ...

theorem encode_decode (x) : encode (decode x) = x := ...

noncomputable def piOneEquiv : SimpleEquiv (π₁(X, base)) Presentation where

toFun := encode

invFun := decode

left_inv := decode_encode

right_inv := encode_decode

```

**RwEq Proofs:**

```lean

theorem my_rweq : RwEq p q := by

calc p

_ ≈ p' := h₁

_ ≈ p'' := h₂

_ ≈ q := h₃

```

7. Build Commands

```bash

lake build # Build everything

lake build ComputationalPaths.Path.Module # Build specific

lake exe computational_paths # Run executable

lake clean # Clean artifacts

```

8. Axiom Policy

**Avoid new axioms.** Use computational-path constructions (inductive types, path expressions, quotients). Keep assumptions local and explicit in signatures.

9. Key Lemmas

Common RwEq lemmas to use:

When Working on This Codebase

1. **Read existing code** before modifying - understand the pattern first

2. **Follow the file structure** exactly as shown above

3. **Document everything** - module comments, section headers, docstrings

4. **Use path tactics** - `path_auto` first, then manual lemmas if needed

5. **Test with `lake build`** - ensure no errors before completing

6. **Stay axiom-free** - computational constructions only

7. **Preserve completeness** - no sorries allowed

Aristotle Integration

This project supports Aristotle AI-powered theorem proving:

```bash

Set API key

export ARISTOTLE_API_KEY='arstl_YOUR_KEY_HERE'

Fill sorries in a file

uvx --from aristotlelib aristotle.exe prove-from-file "path/to/file.lean"

```

When a proof is complex and you need automated assistance, consider suggesting Aristotle as an option.