feat: refine refine tactic

Now `refine stx` reports an error when there are natural unassigned
metavariables after we elaborate syntax `stx`. The idea is that only
synthetic holes `?<hole-name>` become new goals.
The tactic `refine! stx` implements the Lean3 behavior.

src/Lean/Elab/Tactic/ElabTerm.lean

@@ -40,13 +40,25 @@ fun stx => match_syntax stx with
     setGoals gs
   | _ => throwUnsupportedSyntax
 
-def refineCore (mvarId : MVarId) (stx : Syntax) (tagSuffix : Name) : TacticM (List MVarId) :=
+/- If `allowNaturalHoles == true`, then we allow the resultant expression to contain unassigned "natural" metavariables.
+   Recall that "natutal" metavariables are created for explicit holes `_` and implicit arguments. They are meant to be
+   filled by typing constraints.
+   "Synthetic" metavariables are meant to be filled by tactics and are usually created using the synthetic hole notation `?<hole-name>`. -/
+def refineCore (mvarId : MVarId) (stx : Syntax) (tagSuffix : Name) (allowNaturalHoles : Bool := false) : TacticM (List MVarId) :=
 withMVarContext mvarId do
   decl ← getMVarDecl mvarId;
   val  ← elabTermEnsuringType stx decl.type;
   assignExprMVar mvarId val;
   newMVarIds ← getMVarsNoDelayed val;
-  let newMVarIds := newMVarIds.toList;
+  newMVarIds ←
+    if allowNaturalHoles then
+      pure newMVarIds.toList
+    else do {
+      naturalMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure mvarDecl.kind.isNatural };
+      syntheticMVarIds ← newMVarIds.filterM fun mvarId => do { mvarDecl ← getMVarDecl mvarId; pure $ !mvarDecl.kind.isNatural };
+      liftM $ Term.logUnassignedUsingErrorContext naturalMVarIds;
+      pure syntheticMVarIds.toList
+    };
   tagUntaggedGoals decl.userName tagSuffix newMVarIds;
   pure newMVarIds
 
@@ -54,10 +66,20 @@ withMVarContext mvarId do
 fun stx => match_syntax stx with
   | `(tactic| refine $e) => do
     (g, gs) ← getMainGoal;
+    /- Remark: only synthetic holes become new goals (we are using `allowNaturalHoles == false`). -/
     gs' ← refineCore g e `refine;
     setGoals (gs' ++ gs)
   | _ => throwUnsupportedSyntax
 
+@[builtinTactic «refine!»] def evalRefineBang : Tactic :=
+fun stx => match_syntax stx with
+  | `(tactic| refine! $e) => do
+    (g, gs) ← getMainGoal;
+    /- Remark all unassigned metavariables become new goals. We consider delayed assignments as assignments here. -/
+    gs' ← refineCore g e `refine true;
+    setGoals (gs' ++ gs)
+  | _ => throwUnsupportedSyntax
+
 @[builtinTactic Lean.Parser.Tactic.apply] def evalApply : Tactic :=
 fun stx => match_syntax stx with
   | `(tactic| apply $e) => do

src/Lean/MetavarContext.lean

@@ -244,6 +244,10 @@ def MetavarKind.isSyntheticOpaque : MetavarKind → Bool
 | MetavarKind.syntheticOpaque => true
 | _                           => false
 
+def MetavarKind.isNatural : MetavarKind → Bool
+| MetavarKind.natural => true
+| _                   => false
+
 structure MetavarDecl :=
 (userName       : Name := Name.anonymous)
 (lctx           : LocalContext)

tests/lean/run/induction1.lean

@@ -45,7 +45,7 @@ theorem tst5 {p q : Prop } (h : p ∨ q) : q ∨ p :=
 by {
   induction h using elim2 with
   | right h => _
-  | left h  => { refine Or.inr _; exact h };
+  | left h  => { refine Or.inr ?_; exact h };
   case right { exact Or.inl h }
 }
 

tests/lean/run/newfrontend1.lean

@@ -87,14 +87,14 @@ by {
 theorem simple6 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
-  refine Eq.trans _ h1;
+  refine Eq.trans ?_ h1;
   assumption
 }
 
 theorem simple7 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
-  refine Eq.trans ?pre ?post;
+  refine! Eq.trans ?pre ?post;
   exact y;
   { exact h3 };
   { exact h1 }
@@ -103,7 +103,7 @@ by {
 theorem simple8 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intro h1; intro _; intro h3;
-  refine Eq.trans ?pre ?post;
+  refine! Eq.trans ?pre ?post;
   case post { exact h1 };
   case pre { exact h3 };
 }
@@ -112,7 +112,7 @@ theorem simple9 (x y z : Nat) : y = z → x = x → x = y → x = z :=
 by {
   intros h1 _ h3;
   traceState;
-  { refine Eq.trans ?pre ?post;
+  { refine! Eq.trans ?pre ?post;
     (exact h1) <|> (exact y; exact h3; assumption) }
 }