From 7286dfa38a1f1733e17e84a4db3507d9b40ed149 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Mon, 30 Oct 2023 15:00:52 +1100 Subject: [PATCH] feat: withAssignableSyntheticOpaque in assumption (#2596) * feat: withAssignableSyntheticOpaque in assumption * add test --- src/Lean/Elab/Tactic/BuiltinTactic.lean | 5 ++++- tests/lean/2361.lean | 16 ++++++++++++++++ tests/lean/2361.lean.expected.out | 0 3 files changed, 20 insertions(+), 1 deletion(-) create mode 100644 tests/lean/2361.lean create mode 100644 tests/lean/2361.lean.expected.out diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean index e7fb5b0a0d..c9d603d6bc 100644 --- a/src/Lean/Elab/Tactic/BuiltinTactic.lean +++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean @@ -232,7 +232,10 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit := | some msg => withRef stx[0] <| addRawTrace msg @[builtin_tactic Lean.Parser.Tactic.assumption] def evalAssumption : Tactic := fun _ => - liftMetaTactic fun mvarId => do mvarId.assumption; pure [] + -- The `withAssignableSyntheticOpaque` is needed here to accommodate + -- `assumption` after `refine`. + -- See https://github.com/leanprover/lean4/issues/2361 + liftMetaTactic fun mvarId => withAssignableSyntheticOpaque do mvarId.assumption; pure [] @[builtin_tactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun _ => liftMetaTactic fun mvarId => do mvarId.contradiction; pure [] diff --git a/tests/lean/2361.lean b/tests/lean/2361.lean new file mode 100644 index 0000000000..bdae3c34fc --- /dev/null +++ b/tests/lean/2361.lean @@ -0,0 +1,16 @@ +import Lean + +-- This worked before issue #2361 +example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by + constructor + assumption + +example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by + refine ⟨?m, ?c⟩ + -- `?m` is synthetic opaque, so `assumption` needs to be able to assign such metavariables + -- for this to succeed. + case c => assumption + +example {α : Type} {P : α → Prop} (a : α) (h : P a) : ∃ x, P x := by + refine' ⟨_, ?c⟩ + case c => assumption diff --git a/tests/lean/2361.lean.expected.out b/tests/lean/2361.lean.expected.out new file mode 100644 index 0000000000..e69de29bb2