From 03f6b87647ae79cdca92c5de87a84603eba78b06 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 9 Apr 2022 11:57:27 -0700
Subject: [PATCH] feat: add hand-written `rfl` tactic

It requires update stage0
---
 src/Init/Notation.lean                  |  6 +++--
 src/Lean/Elab/Tactic/BuiltinTactic.lean |  4 +++
 src/Lean/Meta/Reduce.lean               |  3 +++
 src/Lean/Meta/Tactic.lean               |  1 +
 src/Lean/Meta/Tactic/Refl.lean          | 35 +++++++++++++++++++++++++
 5 files changed, 47 insertions(+), 2 deletions(-)
 create mode 100644 src/Lean/Meta/Tactic/Refl.lean

diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean
index 11f13c1421..4d5bf0706d 100644
--- a/src/Init/Notation.lean
+++ b/src/Init/Notation.lean
@@ -348,8 +348,10 @@ macro "try " t:tacticSeq : tactic => `(first | $t | skip)
 /-- `tac <;> tac'` runs `tac` on the main goal and `tac'` on each produced goal, concatenating all goals produced by `tac'`. -/
 macro:1 x:tactic " <;> " y:tactic:0 : tactic => `(tactic| focus ($x:tactic; all_goals $y:tactic))
 
-/-- `rfl` is a shorthand for `exact rfl`. -/
-macro "rfl" : tactic => `(exact rfl)
+/-- `rfl` is equivalent to `exact rfl`, but has a few optimizatons. -/
+syntax (name := refl) "rfl" : tactic
+
+macro_rules | `(tactic| rfl) => `(tactic| exact rfl)
 
 /--
   Similar to `rfl`, but disables smart unfolding and unfolds all kinds of definitions,
diff --git a/src/Lean/Elab/Tactic/BuiltinTactic.lean b/src/Lean/Elab/Tactic/BuiltinTactic.lean
index a8a47a3504..55b0158651 100644
--- a/src/Lean/Elab/Tactic/BuiltinTactic.lean
+++ b/src/Lean/Elab/Tactic/BuiltinTactic.lean
@@ -3,6 +3,7 @@ Copyright (c) 2021 Microsoft Corporation. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 -/
+import Lean.Meta.Tactic.Refl
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
 
@@ -144,6 +145,9 @@ partial def evalChoiceAux (tactics : Array Syntax) (i : Nat) : TacticM Unit :=
 @[builtinTactic Lean.Parser.Tactic.contradiction] def evalContradiction : Tactic := fun stx =>
   liftMetaTactic fun mvarId => do Meta.contradiction mvarId; pure []
 
+@[builtinTactic Lean.Parser.Tactic.refl] def evalRefl : Tactic := fun stx =>
+  liftMetaTactic fun mvarId => do Meta.refl mvarId; pure []
+
 @[builtinTactic Lean.Parser.Tactic.intro] def evalIntro : Tactic := fun stx => do
   match stx with
   | `(tactic| intro)                   => introStep none `_
diff --git a/src/Lean/Meta/Reduce.lean b/src/Lean/Meta/Reduce.lean
index 066659cc08..77c0c47770 100644
--- a/src/Lean/Meta/Reduce.lean
+++ b/src/Lean/Meta/Reduce.lean
@@ -41,4 +41,7 @@ partial def reduce (e : Expr) (explicitOnly skipTypes skipProofs := true) : Meta
         | _                  => return e
   visit e |>.run
 
+def reduceAll (e : Expr) : MetaM Expr :=
+  reduce e false false false
+
 end Lean.Meta
diff --git a/src/Lean/Meta/Tactic.lean b/src/Lean/Meta/Tactic.lean
index ad670f2f14..67ec272fe4 100644
--- a/src/Lean/Meta/Tactic.lean
+++ b/src/Lean/Meta/Tactic.lean
@@ -27,3 +27,4 @@ import Lean.Meta.Tactic.Unfold
 import Lean.Meta.Tactic.Rename
 import Lean.Meta.Tactic.LinearArith
 import Lean.Meta.Tactic.AC
+import Lean.Meta.Tactic.Refl
diff --git a/src/Lean/Meta/Tactic/Refl.lean b/src/Lean/Meta/Tactic/Refl.lean
new file mode 100644
index 0000000000..77ecaee423
--- /dev/null
+++ b/src/Lean/Meta/Tactic/Refl.lean
@@ -0,0 +1,35 @@
+/-
+Copyright (c) 2022 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Meta.Reduce
+import Lean.Meta.Tactic.Util
+
+namespace Lean.Meta
+
+def refl (mvarId : MVarId) (reduceIfGround := true) : MetaM Unit := do
+  withMVarContext mvarId do
+    checkNotAssigned mvarId `apply
+    let targetType ← getMVarType' mvarId
+    unless targetType.isAppOfArity ``Eq 3 do
+      throwTacticEx `rfl mvarId "equality expected{indentExpr targetType}"
+    let lhs ← instantiateMVars targetType.appFn!.appArg!
+    let rhs ← instantiateMVars targetType.appArg!
+    let success ←
+      if (← useReduceAll lhs rhs) then
+        pure ((← reduceAll lhs) == (← reduceAll rhs))
+      else
+        isDefEq lhs rhs
+    unless success do
+      throwTacticEx `rfl mvarId "equality left-hand-side{indentExpr lhs}\nis not definitionally equal right-hand-side{indentExpr rhs}"
+    let us := targetType.getAppFn.constLevels!
+    let α := targetType.appFn!.appFn!.appArg!
+    assignExprMVar mvarId (mkApp2 (mkConst ``Eq.refl  us) α lhs)
+where
+  useReduceAll (lhs rhs : Expr) : MetaM Bool := do
+    if !reduceIfGround then return false
+    else if lhs.hasFVar || lhs.hasMVar || lhs.hasFVar || lhs.hasMVar then return false
+    else return (← getTransparency) matches TransparencyMode.default | TransparencyMode.all
+
+end Lean.Meta