From d2be42e0a03f8ebbd081fc388f62e1b224f138f3 Mon Sep 17 00:00:00 2001 From: Vasily Ilin Date: Fri, 23 Oct 2026 18:44:22 +0000 Subject: [PATCH] perf(Incompleteness): avoid kernel reduction in term construction proofs --- .../Arithmetization/ISigmaOne/Metamath/Term/Basic.lean | 8 +++++++- .../ISigmaOne/Metamath/Term/Functions.lean | 8 +++++++- 2 files changed, 14 insertions(+), 2 deletions(-) diff --git a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean index 9336861da9..5f67146a4f 100644 --- a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean +++ b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Basic.lean @@ -803,7 +803,13 @@ def construction : Language.TermRec.Construction V L (blueprint pL) where func (_ _ _ _ v') := listMax v' bvar_defined := by intro v; simp [blueprint] fvar_defined := by intro v; simp [blueprint] - func_defined := by intro v; simp [blueprint] + func_defined := by + intro v + simp only [blueprint] + -- Avoid reducing the large encoded formula during kernel conversion. + rw [HierarchySymbol.Semiformula.val_mkSigma] + rw [Semiformula.eval_substs] + simp end BV end IsUTerm diff --git a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean index 67d8b298e9..3d235e9a70 100644 --- a/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean +++ b/LeanPool/Incompleteness/Arithmetization/ISigmaOne/Metamath/Term/Functions.lean @@ -42,7 +42,13 @@ def construction : Language.TermRec.Construction V L (blueprint pL) where bvar (param z) := (param 1).[z] fvar (_ x) := ^&x func (_ k f _ v') := ^func k f v' - bvar_defined := by intro v; simp [blueprint] + bvar_defined := by + intro v + simp only [blueprint] + -- Avoid reducing the large encoded formula during kernel conversion. + rw [HierarchySymbol.Semiformula.val_mkSigma] + rw [Semiformula.eval_substs] + simp fvar_defined := by intro v; simp [blueprint] func_defined := by intro v; simp [blueprint]