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

fix: bug in markNestedProofs within grind (#6500)

Browse source 
This PR fixes a bug in the `markNestedProofs` used in `grind`. See new
test.
This commit is contained in:
Leonardo de Moura 2025-01-02 03:14:45 +01:00 • committed by GitHub
parent a8d09dad1b
commit c0d67e2a65
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 9 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/Lean/Meta/Tactic/Grind/MarkNestedProofs.lean
View file

@ -28,9 +28,9 @@ where
| .bvar .. => unreachable!
-- See comments on `Canon.lean` for why we do not visit these cases.
| .letE .. | .forallE .. | .lam ..
| .const .. | .lit .. | .mvar .. | .sort .. | .fvar ..
| .proj ..
| .mdata .. => return e
| .const .. | .lit .. | .mvar .. | .sort .. | .fvar .. => return e
| .proj _ _ b => return e.updateProj! (← visit b)
| .mdata _ b => return e.updateMData! (← visit b)
-- We only visit applications
| .app .. =>
-- Check whether it is cached

6
tests/lean/run/grind_nested_proof_issue.lean Normal file
View file

@ -0,0 +1,6 @@
example (as bs : Array α) (v : α)
(i : Nat)
(h₁ : i < as.size)
(h₂ : bs = as.set i v)
: (as.set i v).size = as.size → as.size = bs.size := by
grind