feat(tactic/observe): have a claim proved by library_search under the…

… hood (#10878)

scripts/lint-style.py

@@ -40,8 +40,7 @@
 ERR_RNT = 5 # reserved notation
 ERR_OPT = 6 # set_option
 ERR_AUT = 7 # malformed authors list
-ERR_OME = 8 # imported tactic.omega
-ERR_TAC = 9 # imported tactic
+ERR_TAC = 9 # imported tactic{,.omega,.observe}
 WRN_IND = 10 # indentation
 WRN_BRC = 11 # curly braces
 
@@ -72,8 +71,6 @@
             exceptions += [(ERR_OPT, path)]
         if errno == "ERR_AUT":
             exceptions += [(ERR_AUT, path)]
-        if errno == "ERR_OME":
-            exceptions += [(ERR_OME, path)]
         if errno == "ERR_TAC":
             exceptions += [(ERR_TAC, path)]
         if errno == "WRN_IND":
@@ -302,9 +299,7 @@ def import_omega_check(lines, path):
         imports = line.split()
         if imports[0] != "import":
             break
-        if imports[1] == "tactic.omega":
-            errors += [(ERR_OME, line_nr, path)]
-        if imports[1] == "tactic":
+        if imports[1] in ["tactic", "tactic.omega", "tactic.observe"]:
             errors += [(ERR_TAC, line_nr, path)]
     return errors
 
@@ -343,10 +338,8 @@ def format_errors(errors):
             output_message(path, line_nr, "ERR_OPT", "Forbidden set_option command")
         if errno == ERR_AUT:
             output_message(path, line_nr, "ERR_AUT", "Authors line should look like: 'Authors: Jean Dupont, Иван Иванович Иванов'")
-        if errno == ERR_OME:
-            output_message(path, line_nr, "ERR_OME", "Files in mathlib cannot import tactic.omega")
         if errno == ERR_TAC:
-            output_message(path, line_nr, "ERR_TAC", "Files in mathlib cannot import the whole tactic folder")
+            output_message(path, line_nr, "ERR_TAC", "Files in mathlib cannot import the whole tactic folder, nor tactic.omega or tactic.observe")
         if errno == WRN_IND:
             output_message(path, line_nr, "WRN_IND", "Probable indentation mistake in proof")
         if errno == WRN_BRC:

src/tactic/observe.lean

@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2021 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import tactic.suggest
+
+/-!
+# observe
+
+The `observe` tactic is mainly intended for demo/educational purposes.
+Calling `observe hp : p` is equivalent to `have hp : p, { library_search }`.
+-/
+
+open tactic tactic.interactive
+setup_tactic_parser
+
+/-- `observe hp : p` asserts the proposition `p`, and tries to prove it using `library_search`.
+If no proof is found, the tactic fails.
+In other words, this tactic is equivalent to `have hp : p, { library_search }`.
+
+If `hp` is omitted, then the placeholder `this` is used.
+
+The variant `observe? hp : p` will emit a trace message of the form `have hp : p := proof_term`.
+This may be particularly useful to speed up proofs. -/
+meta def tactic.interactive.observe (trc : parse $ optional (tk "?"))
+  (h : parse ident?) (t : parse (tk ":" *> texpr)) : tactic unit := do
+  let h' := h.get_or_else `this,
+  t ← to_expr ``(%%t : Prop),
+  assert h' t,
+  s ← focus1 (tactic.library_search { try_this := ff }) <|> fail "observe failed",
+  s ← s.get_rest "Try this: exact ",
+  ppt ← pp t,
+  let pph : string := (h.map (λ n : name, n.to_string ++ " ")).get_or_else "",
+  when trc.is_some $ trace! "Try this: have {pph}: {ppt} := {s}"
+
+add_tactic_doc
+{ name       := "observe",
+  category   := doc_category.tactic,
+  decl_names := [`tactic.interactive.observe],
+  tags       := ["search", "Try this"] }

test/observe.lean

@@ -0,0 +1,7 @@
+import tactic.observe
+
+example (a b c : ℕ) : a * (b * c) = (b * a) * c :=
+begin
+  observe : a * b = b * a,
+  rw [← this, nat.mul_assoc],
+end