`vcgen frames` fails on types with abbreviation
Maintainers usually reply within 1 day
Nobody has claimed this yet.
Assessment
- Difficulty
- 5/5
- Estimated time
- Over a week
- Newbie friendliness
- 15/100
- Issue type
- Bug
- Clarity
- Mostly clear
- Activity status
- Active
- Domain
- compilers
Research direction
The failing case is the vcgen frames tactic with an abbrev type alias, reproduced by the Lean snippet in the issue body. The reporter suspects the abbrev is not reduced before it enters the hash-consing table of Sym, so the proof term fails to match. Reproduce by running the example with set_option experimental.vcgen true, then compare it with the eta-expanded variant that passes. Done means the first example compiles without the kernel application type mismatch error.
Written by the indexing model from the issue text.
Description
Description
Please check the Lean Web
import Std.WP
set_option experimental.vcgen true
open Lean.Order Std.WP
abbrev S := Nat
def tick [Monad m] [MonadStateOf S m] : m Unit := pure ()
@[spec] theorem tick_spec : ⦃ fun _ => True ⦄ (tick : StateM S Unit) ⦃ fun _ _ => True ⦄ := by
unfold tick; vcgen
def F : S → Prop := fun _ => True
@[grind .] theorem frames_F : WP.Frames meet (tick : StateM S Unit) F P :=
WP.frames_of_conjunctive (by unfold tick F; vcgen with finish) (fun _ => meet_le_right _ _)
/-- error: (kernel) application type mismatch -/
#guard_msgs (error, substring := true) in
example : ⦃ F ⦄ (tick : StateM S Unit) ⦃ fun _ _ => True ⦄ := by
vcgen frames | tick => F with finish
-- The same frame, eta-expanded, passes.
example : ⦃ F ⦄ (tick : StateM S Unit) ⦃ fun _ _ => True ⦄ := by
vcgen frames | tick => fun s => F s with finish
For some reason, if abbrev is used in the program, vcgen framesblows up, unless the abbrev is eta-expanded. I guess the abbrev is not reduced properly before it goes to the hash-consing table of Sym, so later symbolic matching fails to pick up the proof of correct type.
- Dominant language
- Lean
- Stars
- 9.7k
- Forks
- 1.1k
- Avg merge
- 20h 27m
- Merged PRs (30d)
- 314
Getting set up
- No Dockerfile or Docker Compose file
- Has a pull request template
- Read the contributing guide
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
More from leanprover/lean4
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
leanprover/lean4#15982 · 2 comments ·
Maintainers usually reply within 1 day
-
bug: `isExclusiveUnsafe` should be marked `@[never_extract]`Possibly taken A pull request linked to this issue is open or already merged. Openbug
Difficulty 1/5 Under an hour Newbie friendliness 85/100
leanprover/lean4#15925 ·
Maintainers usually reply within 1 day
-
`IO.appPath` fails when `/proc` belongs to another PID namespacePossibly taken @treiher claimed this 8 days ago. Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 72/100
leanprover/lean4#15692 · 3 reactions ·
Maintainers usually reply within 1 day
-
`IO.FS.realPath` reports every failure as `noFileOrDirectory` instead of classifying by `errno`Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 66/100
leanprover/lean4#15683 ·
Maintainers usually reply within 1 day
-
`Child.pid` leaks the `Child` and its pipe file descriptors (owned argument treated as borrowed)Openbug
Difficulty 2/5 1-3 hours Newbie friendliness 70/100
leanprover/lean4#15681 ·
Maintainers usually reply within 1 day
All issues in leanprover/lean4
Similar issues
-
bug intrinsic medium priority rt_lib
Difficulty 2/5 1-3 hours Newbie friendliness 75/100
Maintainers usually reply within 1 day
-
area:codegen backend:metal bug direction:output
Difficulty 2/5 1-3 hours Newbie friendliness 79/100
Maintainers usually reply within 1 day
-
JS_SetPropertyInternal2 loses the value when a lazy property on the prototype runs out of memoryOpen
Difficulty 2/5 1-3 hours Newbie friendliness 78/100
quickjs-ng/quickjs#1852 ·
Maintainers usually reply within 2 days
-
Difficulty 2/5 1-3 hours Newbie friendliness 74/100
matter-labs/era-compiler-llvm#978 · 3 comments ·
Maintainers usually reply within 5 days
-
Difficulty 2/5 1-3 hours Newbie friendliness 77/100
manuscript-lang/manuscript#1604 ·
Maintainers usually reply within 1 day