doc(tactic/*): doc entries for some missing tactics (#2489)

This covers most of the remaining list in the old issue #450. I've already checked off my additions.



Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Co-authored-by: Scott Morrison <scott@tqft.net>

src/tactic/default.lean

@@ -25,3 +25,5 @@ import tactic.tfae
 import tactic.apply_fun
 import tactic.interval_cases
 import tactic.reassoc_axiom -- most likely useful only for category_theory
+import tactic.slice
+import tactic.subtype_instance

src/tactic/ring2.lean

@@ -477,9 +477,12 @@ open tactic.ring2
 
 local postfix `?`:9001 := optional
 
-/-- Tactic for solving equations in the language of rings.
+/-- `ring2` solves equations in the language of rings.
+
+It supports only the commutative semiring operations, i.e. it does not normalize subtraction or division.
+
   This variant on the `ring` tactic uses kernel computation instead
-  of proof generation. -/
+  of proof generation. In general, you should use `ring` instead of `ring2`. -/
 meta def ring2 : tactic unit :=
 do `[repeat {rw ← nat.pow_eq_pow}],
   `(%%e₁ = %%e₂) ← target
@@ -502,6 +505,12 @@ do `[repeat {rw ← nat.pow_eq_pow}],
       "\n  =?=\n" ++ to_string (horner_expr.of_csexpr r₂)),
   tactic.exact e
 
+add_tactic_doc
+{ name        := "ring2",
+  category    := doc_category.tactic,
+  decl_names  := [`tactic.interactive.ring2],
+  tags        := ["arithmetic", "simplification", "decision procedure"] }
+
 end interactive
 end tactic
 

src/tactic/scc.lean

@@ -296,8 +296,15 @@ meta def prove_eqv_target (cl : closure) : tactic unit :=
 do `(%%p ↔ %%q) ← target >>= whnf,
    cl.prove_eqv p q >>= exact
 
-/-- Use the available equivalences and implications to prove
-a goal of the form `p ↔ q`. -/
+/--
+`scc` uses the available equivalences and implications to prove
+a goal of the form `p ↔ q`.
+
+```lean
+example (p q r : Prop) (hpq : p → q) (hqr : q ↔ r) (hrp : r → p) : p ↔ r :=
+by scc
+```
+-/
 meta def interactive.scc : tactic unit :=
 closure.with_new_closure $ λ cl,
 do impl_graph.mk_scc cl,
@@ -316,4 +323,22 @@ do m ← impl_graph.mk_scc cl,
      do { h ← get_unused_name `h,
           try $ closure.prove_eqv cl x.1 x.2 >>= note h none }
 
+/--
+`scc` uses the available equivalences and implications to prove
+a goal of the form `p ↔ q`.
+
+```lean
+example (p q r : Prop) (hpq : p → q) (hqr : q ↔ r) (hrp : r → p) : p ↔ r :=
+by scc
+```
+
+The variant `scc'` populates the local context with all equivalences that `scc` is able to prove.
+This is mostly useful for testing purposes.
+-/
+add_tactic_doc
+{ name := "scc",
+  category := doc_category.tactic,
+  decl_names := [``interactive.scc, ``interactive.scc'],
+  tags := ["logic"] }
+
 end tactic

src/tactic/slice.lean

@@ -89,3 +89,16 @@ meta def slice_rhs (a b : parse small_nat) (t : conv.interactive.itactic) : tact
 do conv_target' (conv.interactive.to_rhs >> slice a b >> t)
 end interactive
 end tactic
+
+/--
+`slice_lhs a b { tac }` zooms to the left hand side, uses associativity for categorical
+composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
+
+`slice_rhs a b { tac }` zooms to the right hand side, uses associativity for categorical
+composition as needed, zooms in on the `a`-th through `b`-th morphisms, and invokes `tac`.
+-/
+add_tactic_doc
+{ name := "slice",
+  category := doc_category.tactic,
+  decl_names := [`tactic.interactive.slice_lhs, `tactic.interactive.slice_rhs],
+  tags := ["category theory"] }

src/tactic/split_ifs.lean

@@ -88,6 +88,12 @@ tactic.split_ifs names at_
 
 add_hint_tactic "split_ifs"
 
+add_tactic_doc
+{ name := "split_ifs",
+  category := doc_category.tactic,
+  decl_names := [``split_ifs],
+  tags := ["case bashing"] }
+
 end interactive
 
 end tactic

src/tactic/subtype_instance.lean

@@ -60,7 +60,7 @@ class is_submonoid (s : set α) : Prop :=
 
 instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
 by subtype_instance
-````
+```
 -/
 meta def subtype_instance :=
 do t ← target,
@@ -73,6 +73,12 @@ do t ← target,
          sources := src.map to_pexpr },
    refine_struct inst ; derive_field_subtype
 
+add_tactic_doc
+{ name := "subtype_instance",
+  category := doc_category.tactic,
+  decl_names := [``subtype_instance],
+  tags := ["type class", "structures"] }
+
 end interactive
 
 end tactic

src/tactic/wlog.lean

@@ -242,6 +242,12 @@ with_enable_tags $ tactic.focus1 $ do
   | none := skip
   end
 
+add_tactic_doc
+{ name := "wlog",
+  category := doc_category.tactic,
+  decl_names := [``wlog],
+  tags := ["logic"] }
+
 end interactive
 
 end tactic