max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix: abstractNestedProofs (#7728)

Browse source 
This PR fixes an issue in `abstractNestedProofs`.
We should abstract proofs occurring in the inferred proposition too.
This commit is contained in:
Leonardo de Moura 2025-03-29 16:58:09 -07:00 • committed by GitHub
parent e37bbdbf23
commit 56ba3f245b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 15 additions and 10 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

25
src/Lean/Meta/AbstractNestedProofs.lean
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura
prelude
import Init.Grind.Util
import Lean.Meta.Closure
import Lean.Meta.Transform
namespace Lean.Meta
namespace AbstractNestedProofs
@ -37,16 +38,6 @@ structure State where
abbrev M := ReaderT Context $ MonadCacheT ExprStructEq Expr $ StateRefT State MetaM
private def mkAuxLemma (e : Expr) : M Expr := do
let ctx ← read
let s ← get
let lemmaName ← mkAuxName (ctx.baseName ++ `proof) s.nextIdx
modify fun s => { s with nextIdx := s.nextIdx + 1 }
/- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to
identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step.
It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
mkAuxTheoremFor lemmaName e (zetaDelta := true)
partial def visit (e : Expr) : M Expr := do
if e.isAtomic then
pure e
@ -75,6 +66,20 @@ partial def visit (e : Expr) : M Expr := do
| .proj _ _ b => return e.updateProj! (← visit b)
| .app .. => e.withApp fun f args => return mkAppN (← visit f) (← args.mapM visit)
| _ => pure e
where
mkAuxLemma (e : Expr) : M Expr := do
let ctx ← read
let type ← inferType e
let type ← Core.betaReduce type
let type ← zetaReduce type
/- Ensure proofs nested in type are also abstracted -/
let type ← visit type
let lemmaName ← mkAuxName (ctx.baseName ++ `proof) (← get).nextIdx
modify fun s => { s with nextIdx := s.nextIdx + 1 }
/- We turn on zetaDelta-expansion to make sure we don't need to perform an expensive `check` step to
identify which let-decls can be abstracted. If we design a more efficient test, we can avoid the eager zetaDelta expansion step.
It a benchmark created by @selsam, The extra `check` step was a bottleneck. -/
mkAuxTheorem lemmaName type e (zetaDelta := true)
end AbstractNestedProofs