forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Restore "fix: make sure
refine
preserves pre-existing natural mvars (…
…leanprover#2435)" This reverts commit a7efe5b.
- Loading branch information
Showing
3 changed files
with
75 additions
and
6 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,53 @@ | ||
import Lean | ||
|
||
/-! Ensures that `refine` does not remove pre-existing natural goals from the goal list. -/ | ||
|
||
open Lean Meta Elab Tactic Term | ||
|
||
elab "add_natural_goal" s:ident " : " t:term : tactic => do | ||
let g ← mkFreshExprMVar (← elabType t) .natural s.getId | ||
appendGoals [g.mvarId!] | ||
|
||
/-! | ||
In the following, `refine` would erroneously close each focused goal, leading to a | ||
`(kernel) declaration has metavariables '_example'` error. | ||
This occurred because `withCollectingNewGoalsFrom` was only erroring on new natural goals (as | ||
determined by `index`), while simultaneously only passing through non-natural goals to construct | ||
the resulting goal list. This orphaned old natural metavariables and closed the goal list | ||
erroneously. | ||
As such, all of the following tests should lead to an `unsolved goals` error, followed by a | ||
`no goals` error (instead of a successful focus). | ||
-/ | ||
|
||
example : Bool × Nat := by | ||
add_natural_goal d : Bool | ||
add_natural_goal e : Nat | ||
· refine (?d,?e) | ||
· refine ?d | ||
· refine ?e | ||
|
||
example : Bool × Bool := by | ||
add_natural_goal d : Bool | ||
add_natural_goal e : Bool | ||
· refine (?d,?e) | ||
· case d => refine ?e | ||
· refine ?e | ||
|
||
/-! | ||
Previously, this would error, as `refine (?d, ?e)` erroneously closed the goal, leading to a | ||
`no goals` error. Instead, this should succeed. | ||
-/ | ||
|
||
example : Bool × Bool := by | ||
add_natural_goal d : Bool | ||
add_natural_goal e : Bool | ||
· refine (?d,?e) | ||
refine ?d | ||
refine ?e -- This unifies `?d` and `?e`, so only one goal remains. | ||
exact true |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,14 @@ | ||
refinePreservesNaturalMVars.lean:29:2-29:3: error: unsolved goals | ||
case d | ||
⊢ Bool | ||
|
||
case e | ||
⊢ Nat | ||
refinePreservesNaturalMVars.lean:30:2-30:3: error: no goals to be solved | ||
refinePreservesNaturalMVars.lean:36:2-36:3: error: unsolved goals | ||
case d | ||
⊢ Bool | ||
|
||
case e | ||
⊢ Bool | ||
refinePreservesNaturalMVars.lean:37:2-37:3: error: no goals to be solved |