# Exemple guide 2 : Système de mémoire avec pattern matching
import re
import json
from typing import Dict, List, Optional, Tuple
from dataclasses import dataclass, field
from difflib import SequenceMatcher
@dataclass
class StoredProof:
"""Une preuve stockee avec son contexte."""
theorem_pattern: str
original_theorem: str
proof: str
success_count: int = 1
variables: Dict[str, str] = field(default_factory=dict)
class ProofMemory:
"""
Système de mémoire pour reutiliser les preuves reussies.
Fonctionnalites implementees :
1. Pattern matching pour generaliser les théorèmes
2. Recherche de preuves similaires par similarite
3. Adaptation des preuves au nouveau contexte
4. Persistence (optionnelle) vers fichier JSON
"""
def __init__(self, similarity_threshold: float = 0.7):
self.proofs: Dict[str, StoredProof] = {}
self.similarity_threshold = similarity_threshold
# ------------------------------------------------------------------
# Méthode store()
# ------------------------------------------------------------------
def store(self, theorem: str, proof: str) -> str:
"""
Stocke une preuve reussie.
Etapes :
1. Extraire le pattern et les variables avec self._extract_pattern(theorem)
2. Si le pattern existe deja, incrementer success_count
3. Sinon, creer un nouveau StoredProof dans self.proofs
4. Retourner le pattern
"""
# Etape 1 : extraire le pattern générique et le mapping de variables
pattern, variables = self._extract_pattern(theorem)
# Etape 2 : si le pattern est deja connu, on incremente juste le compteur
if pattern in self.proofs:
self.proofs[pattern].success_count += 1
else:
# Etape 3 : creer une nouvelle entrée
self.proofs[pattern] = StoredProof(
theorem_pattern=pattern,
original_theorem=theorem,
proof=proof,
success_count=1,
variables=variables,
)
# Etape 4 : retourner le pattern utilise comme cle
return pattern
def recall(self, theorem: str) -> Optional[Tuple[str, float]]:
"""
Cherche une preuve similaire pour le theoreme donne.
Returns:
(proof_adaptee, score) si trouvee, None sinon.
"""
pattern, variables = self._extract_pattern(theorem)
# Correspondance exacte
if pattern in self.proofs:
stored = self.proofs[pattern]
adapted = self._adapt_proof(stored.proof, stored.variables, variables)
return adapted, 1.0
# Correspondance par similarite
best_score = 0.0
best_stored = None
for stored_pattern, stored_proof in self.proofs.items():
score = SequenceMatcher(None, pattern, stored_pattern).ratio()
if score > best_score:
best_score = score
best_stored = stored_proof
if best_stored and best_score >= self.similarity_threshold:
_, stored_vars = self._extract_pattern(best_stored.original_theorem)
adapted = self._adapt_proof(best_stored.proof, stored_vars, variables)
return adapted, best_score
return None
# ------------------------------------------------------------------
# Méthodes utilitaires
# ------------------------------------------------------------------
def _extract_pattern(self, theorem: str) -> Tuple[str, Dict[str, str]]:
"""
Remplace les noms concrets par des placeholders génériques.
Exemple :
"theorem foo (n : Nat) : n + 0 = n"
-> pattern : "theorem ?name (?x : Nat) : ?x + 0 = ?x"
-> variables : {"?name": "foo", "?x": "n"}
"""
variables: Dict[str, str] = {}
pattern = theorem
# Nom du théorème
name_match = re.match(r'theorem\s+(\w+)', theorem)
if name_match:
name = name_match.group(1)
variables["?name"] = name
pattern = pattern.replace(f"theorem {name}", "theorem ?name", 1)
# Variables dans la signature, ex: (n : Nat), (a b : Nat)
placeholders = ["?x", "?y", "?z", "?w", "?v", "?u"]
sig_vars = re.findall(r'\((\w+(?:\s+\w+)*)\s*:\s*(\w+)\)', theorem)
idx = 0
for var_group, _ in sig_vars:
for var_name in var_group.split():
if idx < len(placeholders):
ph = placeholders[idx]
variables[ph] = var_name
pattern = re.sub(r'\b' + re.escape(var_name) + r'\b', ph, pattern)
idx += 1
return pattern, variables
def _adapt_proof(
self,
proof: str,
stored_vars: Dict[str, str],
new_vars: Dict[str, str],
) -> str:
"""
Substitue les anciens noms de variables par les nouveaux.
Exemple :
proof = "exact Nat.add_zero n"
stored_vars = {"?x": "n"} -> new_vars = {"?x": "m"}
=> "exact Nat.add_zero m"
"""
adapted = proof
for placeholder, old_var in stored_vars.items():
if placeholder in new_vars:
new_var = new_vars[placeholder]
adapted = re.sub(r'\b' + re.escape(old_var) + r'\b', new_var, adapted)
return adapted
def save(self, filepath: str):
"""Persiste la mémoire dans un fichier JSON."""
data = {
p: {
"theorem_pattern": s.theorem_pattern,
"original_theorem": s.original_theorem,
"proof": s.proof,
"success_count": s.success_count,
"variables": s.variables,
}
for p, s in self.proofs.items()
}
with open(filepath, "w", encoding="utf-8") as f:
json.dump(data, f, indent=2, ensure_ascii=False)
def load(self, filepath: str):
"""Charge la mémoire depuis un fichier JSON."""
with open(filepath, "r", encoding="utf-8") as f:
data = json.load(f)
for pattern, d in data.items():
self.proofs[pattern] = StoredProof(**d)
def get_stats(self) -> dict:
"""Retourne les statistiques de la mémoire."""
if not self.proofs:
return {"patterns_stored": 0, "total_uses": 0, "most_used_pattern": None}
most_used = max(self.proofs.values(), key=lambda p: p.success_count)
return {
"patterns_stored": len(self.proofs),
"total_uses": sum(p.success_count for p in self.proofs.values()),
"most_used_pattern": most_used.theorem_pattern,
}
# ------------------------------------------------------------------
# Tests
# ------------------------------------------------------------------
memory = ProofMemory()
print("Test 1 : stockage de deux preuves")
p1 = memory.store("theorem add_zero_n (n : Nat) : n + 0 = n", "exact Nat.add_zero n")
p2 = memory.store("theorem add_comm_ab (a b : Nat) : a + b = b + a", "exact Nat.add_comm a b")
print(f" Pattern 1 : {p1}")
print(f" Pattern 2 : {p2}")
print("\nTest 2 : recall pour my_add_zero (m : Nat) : m + 0 = m")
result = memory.recall("theorem my_add_zero (m : Nat) : m + 0 = m")
if result:
adapted_proof, score = result
print(f" Preuve adaptee : {adapted_proof} (score: {score:.2f})")
print("\nTest 3 : recall pour my_comm (x y : Nat) : x + y = y + x")
result2 = memory.recall("theorem my_comm (x y : Nat) : x + y = y + x")
if result2:
adapted_proof2, score2 = result2
print(f" Preuve adaptee : {adapted_proof2} (score: {score2:.2f})")
stats = memory.get_stats()
print(f"\nStatistiques : {stats}")