extend rfl to proof iff statement #18

Game/Tactic/Rfl.lean

@@ -6,10 +6,24 @@ import Lean.Elab.Tactic.Basic
 Added `withReducible` to prevent `rfl` proving stuff like `n + 0 = n`.
 -/
 
-namespace MyNat
-
 open Lean Meta Elab Tactic
 
+/--
+Close given goal using `Iff.refl`.
+-/
+def Lean.MVarId.iffRefl (mvarId : MVarId) : MetaM Unit := do
+  mvarId.withContext do
+    mvarId.checkNotAssigned `iffRefl
+    let targetType ← mvarId.getType'
+    let some (lhs, rhs) := Expr.app2? targetType ``Iff
+      | throwTacticEx `iffRefl mvarId m!"iff expected"
+    unless ← isDefEq lhs rhs do
+      throwTacticEx `iffRefl mvarId
+        m!"lhs{indentD lhs}\nis not definitionally equal to rhs{indentD rhs}"
+    mvarId.assign (.app (mkConst ``Iff.refl) lhs)
+
+namespace MyNat
+
 -- @[match_pattern] def MyNat.rfl {α : Sort u} {a : α} : Eq a a := Eq.refl a
 
 /-- Modified `rfl` tactic.
@@ -20,9 +34,13 @@ Note that the version for this game is somewhat weaker than the real one. -/
 syntax (name := rfl) "rfl" : tactic
 
 @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
-  liftMetaTactic fun mvarId => do withReducible <| mvarId.refl; pure []
--- TODO: `rfl` should be able to prove `R ↔ R`!
-
+  liftMetaTactic fun mvarId => withReducible do
+    let targetType ← mvarId.getType'
+    match targetType.getAppFn with
+      | .const ``Eq .. => mvarId.refl
+      | .const ``Iff .. => mvarId.iffRefl
+      | _ => throwTacticEx `rfl mvarId "expecting an equality or iff"
+    pure []
 
 -- @[tactic MyNat.rfl] def evalRfl : Tactic := fun _ =>
 --   liftMetaTactic fun mvarId => do mvarId.refl; pure []

test/tactic.lean

@@ -0,0 +1,5 @@
+import Game.Tactic.Rfl
+
+/- Custom `rfl` should close `A ↔ A`. -/
+example (A : Prop) : A ↔ A := by
+  rfl