feat: false_or_by_contra tactic (#460)

Std.lean

@@ -129,6 +129,7 @@ import Std.Tactic.Congr
 import Std.Tactic.Exact
 import Std.Tactic.Ext
 import Std.Tactic.Ext.Attr
+import Std.Tactic.FalseOrByContra
 import Std.Tactic.GuardExpr
 import Std.Tactic.GuardMsgs
 import Std.Tactic.HaveI

Std/Tactic/FalseOrByContra.lean

@@ -0,0 +1,45 @@
+/-
+Copyright (c) 2023 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+import Std.Lean.Expr
+import Std.Lean.Meta.Basic
+
+/-!
+# `false_or_by_contra` tactic
+
+Changes the goal to `False`, retaining as much information as possible:
+
+If the goal is `False`, do nothing.
+If the goal is `¬ P`, introduce `P`.
+If the goal is `x ≠ y`, introduce `x = y`.
+Otherwise, for a goal `P`, replace it with `¬ ¬ P` and introduce `¬ P`.
+-/
+
+open Lean
+
+/--
+Changes the goal to `False`, retaining as much information as possible:
+
+If the goal is `False`, do nothing.
+If the goal is `¬ P`, introduce `P`.
+If the goal is `x ≠ y`, introduce `x = y`.
+Otherwise, for a goal `P`, replace it with `¬ ¬ P` and introduce `¬ P`.
+-/
+syntax (name := false_or_by_contra) "false_or_by_contra" : tactic
+
+open Meta Elab Tactic
+
+@[inherit_doc false_or_by_contra]
+def falseOrByContra (g : MVarId) : MetaM MVarId := do
+  match ← whnfR (← g.getType) with
+  | .const ``False _ => pure g
+  | .app (.const ``Not _) _
+  | .app (.const ``Ne _) _ => pure (← g.intro1).2
+  | _ =>
+    let [g] ← g.applyConst ``Classical.byContradiction | panic! "expected one sugoal"
+    pure (← g.intro1).2
+
+@[inherit_doc falseOrByContra]
+elab "false_or_by_contra" : tactic => liftMetaTactic1 (falseOrByContra ·)

test/false_or_by_contra.lean

@@ -0,0 +1,25 @@
+import Std.Tactic.FalseOrByContra
+import Std.Tactic.GuardExpr
+
+example (h : False) : False := by
+  false_or_by_contra
+  guard_target = False
+  exact h
+
+example (h : False) : x ≠ y := by
+  false_or_by_contra <;> rename_i h
+  guard_hyp h : x = y
+  guard_target = False
+  simp_all
+
+example (h : False) : ¬ P := by
+  false_or_by_contra <;> rename_i h
+  guard_hyp h : P
+  guard_target = False
+  simp_all
+
+example (h : False) : P := by
+  false_or_by_contra <;> rename_i h
+  guard_hyp h : ¬ P
+  guard_target = False
+  simp_all