# Memory Patterns and Examples

This document provides detailed examples of memory operations for the lean4-memories skill.

## Memory Entity Schemas

### ProofPattern Entity

```json
{
  "entity_type": "ProofPattern",
  "name": "pi_system_uniqueness_for_measures",
  "attributes": {
    "project": "/Users/freer/work/exch-repos/exchangeability-cursor",
    "skill": "lean4-memories",
    "goal_pattern": "Show two measures equal via finite marginals",
    "goal_type_signature": "μ₁ = μ₂",
    "hypothesis_patterns": [
      "∀ n, μ₁.map (prefixProj n) = μ₂.map (prefixProj n)"
    ],
    "tactics_sequence": [
      "apply measure_eq_of_fin_marginals_eq",
      "intro n",
      "simp [prefixProj]"
    ],
    "helper_lemmas": [
      "isPiSystem_prefixCylinders",
      "generateFrom_prefixCylinders",
      "measure_eq_on_piSystem"
    ],
    "domain": "measure_theory",
    "difficulty": "medium",
    "lines_of_proof": 54,
    "confidence": 0.9,
    "file": "Exchangeability/Core.lean",
    "theorem_name": "measure_eq_of_fin_marginals_eq",
    "success_count": 3,
    "timestamp": "2025-10-19T14:30:00Z"
  },
  "relations": [
    {"type": "uses", "target": "isPiSystem_prefixCylinders"},
    {"type": "similar_to", "target": "fullyExchangeable_via_pathLaw"}
  ]
}
```

### FailedApproach Entity

```json
{
  "entity_type": "FailedApproach",
  "name": "simp_condExp_mul_comm_loop",
  "attributes": {
    "project": "/Users/freer/work/exch-repos/exchangeability-cursor",
    "skill": "lean4-memories",
    "failed_tactic": "simp only [condExp_indicator, mul_comm]",
    "error_type": "infinite_loop",
    "error_message": "deep recursion was detected",
    "context": "Conditional expectation with indicator function",
    "goal_pattern": "condExp μ m (indicator S f) = ...",
    "file": "Exchangeability/DeFinetti/ViaL2.lean",
    "line": 2830,
    "alternative_approach": "simp only [condExp_indicator], then use ring",
    "alternative_success": true,
    "time_wasted": "20 minutes",
    "confidence": 0.95,
    "timestamp": "2025-10-17T09:15:00Z"
  },
  "relations": [
    {"type": "avoided_in", "target": "condIndep_of_condExp_eq"}
  ]
}
```

### ProjectConvention Entity

```json
{
  "entity_type": "ProjectConvention",
  "name": "measure_theory_instance_declaration",
  "attributes": {
    "project": "/Users/freer/work/exch-repos/exchangeability-cursor",
    "skill": "lean4-memories",
    "convention_type": "proof_structure",
    "pattern": "haveI : MeasurableSpace Ω := inferInstance",
    "description": "All measure theory proofs require explicit MeasurableSpace instance",
    "domain": "measure_theory",
    "frequency": 15,
    "files": [
      "Exchangeability/DeFinetti/ViaL2.lean",
      "Exchangeability/Core.lean",
      "Exchangeability/Contractability.lean"
    ],
    "confidence": 0.95,
    "timestamp": "2025-10-15T10:00:00Z"
  }
}
```

### UserPreference Entity

```json
{
  "entity_type": "UserPreference",
  "name": "verbose_script_output",
  "attributes": {
    "project": "/Users/freer/work/exch-repos/exchangeability-cursor",
    "skill": "lean4-memories",
    "preference_type": "script_usage",
    "setting": "verbose_output",
    "value": true,
    "context": "User prefers --verbose flag for all automation scripts",
    "scripts_affected": [
      "search_mathlib.sh",
      "find_instances.sh",
      "smart_search.sh"
    ],
    "confidence": 0.8,
    "timestamp": "2025-10-10T16:20:00Z"
  }
}
```

### TheoremDependency Entity

```json
{
  "entity_type": "TheoremDependency",
  "name": "permutation_extension_lemma_usage",
  "attributes": {
    "project": "/Users/freer/work/exch-repos/exchangeability-cursor",
    "skill": "lean4-memories",
    "helper_theorem": "exists_perm_extending_strictMono",
    "dependent_theorems": [
      "exchangeable_iff_contractable",
      "fullyExchangeable_iff_exchangeable"
    ],
    "usage_pattern": "Extend finite permutation to full permutation",
    "domain": "combinatorics",
    "importance": "high",
    "confidence": 1.0,
    "timestamp": "2025-10-12T11:00:00Z"
  },
  "relations": [
    {"type": "critical_for", "target": "exchangeable_iff_contractable"}
  ]
}
```

## Storage Operation Examples

### Example 1: Store Successful Proof Pattern

**Scenario:** Just completed proof of `condIndep_iff_condexp_eq` using conditional expectation uniqueness.

**Storage operation:**
```python
# Pseudocode for MCP memory operation
memory.create_entity(
    entity_type="ProofPattern",
    name="condExp_unique_for_conditional_independence",
    content={
        "project": os.getcwd(),  # /Users/freer/work/exch-repos/exchangeability-cursor
        "skill": "lean4-memories",
        "goal_pattern": "Prove conditional independence via conditional expectation equality",
        "goal_type": "CondIndep X Y m ↔ condExp m X = condExp m Y",
        "tactics_sequence": [
            "apply condExp_unique",
            "intro s hs",
            "show_ae_eq",
            "measurability"
        ],
        "helper_lemmas": [
            "condExp_unique",
            "ae_eq_condExp_of_forall_setIntegral_eq",
            "setIntegral_condExp"
        ],
        "domain": "probability_theory",
        "subdomain": "conditional_independence",
        "difficulty": "large",
        "lines_of_proof": 85,
        "sorry_count": 0,
        "confidence": 0.9,
        "file": "Exchangeability/DeFinetti/ViaL2.lean",
        "theorem_name": "condIndep_iff_condexp_eq",
        "timestamp": datetime.now().isoformat()
    }
)

memory.create_relations([
    {"source": "condIndep_iff_condexp_eq", "type": "uses", "target": "condExp_unique"},
    {"source": "condIndep_iff_condexp_eq", "type": "similar_to", "target": "condProb_eq_of_eq_on_pi_system"}
])
```

### Example 2: Store Failed Approach

**Scenario:** Attempted to use `tsum_congr` with `condExp` but got type mismatch.

**Storage operation:**
```python
memory.create_entity(
    entity_type="FailedApproach",
    name="tsum_condExp_direct_exchange",
    content={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "failed_tactic": "apply tsum_congr; intro i; rw [condExp_indicator]",
        "error_type": "type_mismatch",
        "error_message": "expected condExp to be measurable, but got ae-measurable",
        "context": "Trying to exchange tsum and condExp directly",
        "goal_pattern": "condExp (∑' i, f i) = ∑' i, condExp (f i)",
        "why_failed": "condExp output is only ae-measurable, not point-wise measurable",
        "file": "Exchangeability/DeFinetti/ViaL2.lean",
        "line": 643,
        "alternative_approach": "Use restricted measure trick: switch to μ.restrict S",
        "alternative_detail": "integral_condExp on restricted measure with set = univ",
        "alternative_success": true,
        "time_wasted": "45 minutes",
        "learning": "Cannot exchange condExp with series directly; need measure restriction",
        "confidence": 0.95,
        "timestamp": datetime.now().isoformat()
    }
)
```

### Example 3: Store Project Convention

**Scenario:** Observed consistent pattern of hypothesis naming across 10+ files.

**Storage operation:**
```python
memory.create_entity(
    entity_type="ProjectConvention",
    name="hypothesis_naming_pattern",
    content={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "convention_type": "naming",
        "category": "hypotheses",
        "pattern": "h{property_name}",
        "examples": [
            "hExchangeable : Exchangeable μ X",
            "hMeasurable : Measurable f",
            "hIntegrable : Integrable f μ",
            "hContract : Contractable μ X"
        ],
        "description": "Hypotheses prefixed with 'h' followed by property name",
        "exceptions": [
            "ih for induction hypothesis",
            "hs for set membership (h_s avoided)"
        ],
        "frequency": 120,
        "files_surveyed": 15,
        "confidence": 0.95,
        "timestamp": datetime.now().isoformat()
    }
)
```

### Example 4: Store User Preference

**Scenario:** User consistently requests ripgrep output format.

**Storage operation:**
```python
memory.create_entity(
    entity_type="UserPreference",
    name="search_tool_preference",
    content={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "preference_type": "tool_usage",
        "tool": "search_mathlib.sh",
        "setting": "output_format",
        "preferred_value": "with_context",
        "reasoning": "User wants to see surrounding code for search results",
        "explicit_request": true,
        "frequency": 8,
        "confidence": 0.9,
        "timestamp": datetime.now().isoformat()
    }
)
```

## Retrieval Operation Examples

### Example 1: Retrieve Similar Proof Patterns

**Scenario:** About to prove `fullyExchangeable_iff_X` which requires showing measure equality.

**Retrieval query:**
```python
# Query for similar patterns
results = memory.search_entities(
    query="measure equality finite marginals",
    entity_type="ProofPattern",
    filters={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "confidence": {">=": 0.7}
    },
    limit=5
)

# Expected result:
# ProofPattern: pi_system_uniqueness_for_measures
# - Tactics: [apply measure_eq_of_fin_marginals_eq, ...]
# - Confidence: 0.9
# - Success count: 3

# Suggested action:
# "This goal is similar to measure_eq_of_fin_marginals_eq"
# "Try π-system uniqueness approach: apply measure_eq_of_fin_marginals_eq"
```

### Example 2: Check for Known Failures

**Scenario:** About to apply `simp only [condExp_indicator, mul_comm]`.

**Retrieval query:**
```python
# Query for known issues with this tactic
results = memory.search_entities(
    query="simp condExp_indicator mul_comm",
    entity_type="FailedApproach",
    filters={
        "project": os.getcwd(),
        "skill": "lean4-memories"
    }
)

# Expected result:
# FailedApproach: simp_condExp_mul_comm_loop
# - Error: infinite_loop
# - Alternative: simp only [condExp_indicator], then ring

# Suggested action:
# ⚠️ WARNING: This tactic combination causes infinite loop
# Alternative approach: Use simp only [condExp_indicator] without mul_comm, then ring
```

### Example 3: Retrieve Project Conventions

**Scenario:** Starting new theorem in measure theory file.

**Retrieval query:**
```python
# Query for measure theory conventions
results = memory.search_entities(
    query="measure theory proof structure",
    entity_type="ProjectConvention",
    filters={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "domain": "measure_theory"
    }
)

# Expected result:
# ProjectConvention: measure_theory_instance_declaration
# - Pattern: haveI : MeasurableSpace Ω := inferInstance
# - Frequency: 15 occurrences

# Suggested action:
# "Based on project conventions, start with:"
# haveI : MeasurableSpace Ω := inferInstance
```

### Example 4: Find Helpful Lemmas

**Scenario:** Stuck on proof, need helper lemmas.

**Retrieval query:**
```python
# Query for theorems that helped with similar goals
results = memory.search_entities(
    query="conditional expectation uniqueness",
    entity_type="TheoremDependency",
    filters={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "domain": "probability_theory"
    }
)

# Expected result:
# TheoremDependency: condExp_unique_usage_pattern
# - Helper: condExp_unique
# - Used in: [condIndep_iff_condexp_eq, condProb_eq_of_eq_on_pi_system]
# - Pattern: "Test equality on measurable sets via integrals"

# Suggested action:
# "Consider using condExp_unique - it helped with similar proofs"
# "Pattern: Show ae_eq by testing on measurable sets"
```

## Memory Maintenance Examples

### Update Memory with New Success

**Scenario:** Used `pi_system_uniqueness` pattern successfully again.

```python
# Retrieve existing memory
pattern = memory.get_entity("pi_system_uniqueness_for_measures")

# Update success count and confidence
pattern.attributes["success_count"] += 1
pattern.attributes["confidence"] = min(1.0, pattern.attributes["confidence"] + 0.05)
pattern.attributes["last_used"] = datetime.now().isoformat()

memory.update_entity(pattern)
```

### Deprecate Outdated Memory

**Scenario:** Found better approach than stored pattern.

```python
# Mark old pattern as deprecated
old_pattern = memory.get_entity("old_approach_name")
old_pattern.attributes["deprecated"] = true
old_pattern.attributes["deprecation_reason"] = "Better approach found: new_approach_name"
old_pattern.attributes["replaced_by"] = "new_approach_name"

memory.update_entity(old_pattern)

# Store new pattern
memory.create_entity(
    entity_type="ProofPattern",
    name="new_approach_name",
    content={...}
)
```

### Prune Low-Confidence Memories

**Scenario:** Periodic cleanup of unreliable memories.

```python
# Query for low-confidence, old memories
candidates = memory.search_entities(
    entity_type="ProofPattern",
    filters={
        "project": os.getcwd(),
        "skill": "lean4-memories",
        "confidence": {"<": 0.5},
        "timestamp": {"<": one_month_ago}
    }
)

# Review and delete if not used
for pattern in candidates:
    if pattern.attributes["success_count"] == 0:
        memory.delete_entity(pattern.name)
```

## Integration Patterns

### Pattern 1: Pre-Proof Memory Check

Before starting a proof, check memories:

```python
def pre_proof_memory_check(goal_description):
    # 1. Check for similar successful patterns
    similar = memory.search_entities(
        query=goal_description,
        entity_type="ProofPattern",
        filters={"project": os.getcwd(), "confidence": {">=": 0.7}}
    )

    # 2. Check for known failures with this goal type
    failures = memory.search_entities(
        query=goal_description,
        entity_type="FailedApproach",
        filters={"project": os.getcwd()}
    )

    # 3. Get relevant conventions
    conventions = memory.search_entities(
        query=extract_domain(goal_description),
        entity_type="ProjectConvention",
        filters={"project": os.getcwd()}
    )

    return {
        "similar_proofs": similar,
        "known_failures": failures,
        "conventions": conventions
    }
```

### Pattern 2: Post-Proof Memory Storage

After completing a proof, store the pattern:

```python
def post_proof_memory_store(proof_info):
    # Only store non-trivial proofs
    if proof_info["lines"] < 10:
        return

    # Only store if confidence is reasonable
    if proof_info["sorry_count"] > 0:
        confidence = 0.5
    elif proof_info["warnings"] > 0:
        confidence = 0.7
    else:
        confidence = 0.9

    memory.create_entity(
        entity_type="ProofPattern",
        name=generate_pattern_name(proof_info),
        content={
            "project": os.getcwd(),
            "skill": "lean4-memories",
            "goal_pattern": proof_info["goal"],
            "tactics_sequence": proof_info["tactics"],
            "helper_lemmas": proof_info["lemmas_used"],
            "difficulty": estimate_difficulty(proof_info["lines"]),
            "confidence": confidence,
            **proof_info
        }
    )
```

### Pattern 3: Tactic Suggestion with Memory

Enhance tactic suggestions with memory:

```python
def suggest_tactics_with_memory(goal):
    # Get base suggestions from goal pattern
    base_suggestions = analyze_goal_pattern(goal)

    # Enhance with memory
    memory_patterns = memory.search_entities(
        query=goal,
        entity_type="ProofPattern",
        filters={"project": os.getcwd(), "confidence": {">=": 0.7}}
    )

    # Prioritize tactics from successful memories
    for pattern in memory_patterns:
        for tactic in pattern.attributes["tactics_sequence"]:
            if tactic not in base_suggestions:
                base_suggestions.append({
                    "tactic": tactic,
                    "source": "memory",
                    "confidence": pattern.attributes["confidence"]
                })

    # Filter out known failures
    failures = memory.search_entities(
        query=goal,
        entity_type="FailedApproach",
        filters={"project": os.getcwd()}
    )

    for failure in failures:
        base_suggestions = [
            s for s in base_suggestions
            if s["tactic"] != failure.attributes["failed_tactic"]
        ]

    return sorted(base_suggestions, key=lambda x: x.get("confidence", 0.5), reverse=True)
```

## Best Practices

### When to Store Memories

**DO store:**
- ✅ Proofs with >10 lines (non-trivial)
- ✅ Approaches that failed after >10 minutes of trying
- ✅ Patterns observed 3+ times
- ✅ Project-specific insights not in mathlib docs

**DON'T store:**
- ❌ One-line proofs (rfl, simp, exact)
- ❌ Obvious applications of standard lemmas
- ❌ Temporary hacks or workarounds
- ❌ General Lean knowledge

### Confidence Scoring Guidelines

- **0.9-1.0:** Clean proof, no warnings, used successfully multiple times
- **0.7-0.9:** Works well, minor issues or single use
- **0.5-0.7:** Works but has problems, needs refinement
- **0.3-0.5:** Hacky solution, use only if nothing else works
- **0.0-0.3:** Experimental, likely needs replacement

### Memory Scoping Guidelines

Always scope by:
1. **Project path** (absolute path to repository)
2. **Skill** ("lean4-memories")
3. **Entity type** (ProofPattern, FailedApproach, etc.)

Never mix memories across projects unless explicitly linked.