refactor(tactic/interactive): rename tactic.interactive.triv to tacti…

…c.interactive.trivial' (#11643)

The difference between `tactic.interactive.trivial` and `tactic.interactive.triv` is that the latter expands only reducible constants; the first uses `tactic.triv` and the latter uses `tactic.triv'`. This name change is to improve consistency.

Also (slipping in a new feature) add `tactic.interactive.triv`, which is the old `tactic.interactive.triv` but does not run `contradiction`. This is useful for teaching.

src/algebraic_geometry/Gamma_Spec_adjunction.lean

@@ -171,7 +171,7 @@ lemma to_stalk_stalk_map_to_Γ_Spec (x : X) : to_stalk _ _ ≫
 begin
   rw PresheafedSpace.stalk_map,
   erw ← to_open_germ _ (basic_open (1 : Γ.obj (op X)))
-    ⟨X.to_Γ_Spec_fun x, by rw basic_open_one; triv⟩,
+    ⟨X.to_Γ_Spec_fun x, by rw basic_open_one; trivial⟩,
   rw [← category.assoc, category.assoc (to_open _ _)],
   erw stalk_functor_map_germ,
   rw [← category.assoc (to_open _ _), X.to_Γ_Spec_SheafedSpace_app_spec 1],

src/data/qpf/multivariate/constructions/fix.lean

@@ -300,7 +300,7 @@ begin
   intros i j,
   cases i,
   { apply ih },
-  { triv },
+  { trivial },
 end
 
 instance mvqpf_fix : mvqpf (fix F) :=

src/tactic/interactive.lean

@@ -630,22 +630,38 @@ add_tactic_doc
   tags       := ["testing"] }
 
 /--
-A weaker version of `trivial` that tries to solve the goal using a canonical proof of `true` or the
-`reflexivity` tactic (unfolding only `reducible` constants, so can fail faster than `trivial`),
-and otherwise tries the `contradiction` tactic. -/
+Tries to solve the goal using a canonical proof of `true` or the `reflexivity` tactic.
+Unlike `trivial` or `trivial'`, does not the `contradiction` tactic.
+-/
 meta def triv : tactic unit :=
-tactic.triv' <|> tactic.reflexivity reducible <|> tactic.contradiction <|> fail "triv tactic failed"
+tactic.triv <|> tactic.reflexivity <|> fail "triv tactic failed"
 
 add_tactic_doc
 { name       := "triv",
   category   := doc_category.tactic,
   decl_names := [`tactic.interactive.triv],
   tags       := ["finishing"] }
 
+/--
+A weaker version of `trivial` that tries to solve the goal using a canonical proof of `true` or the
+`reflexivity` tactic (unfolding only `reducible` constants, so can fail faster than `trivial`),
+and otherwise tries the `contradiction` tactic. -/
+meta def trivial' : tactic unit :=
+tactic.triv'
+  <|> tactic.reflexivity reducible
+  <|> tactic.contradiction
+  <|> fail "trivial' tactic failed"
+
+add_tactic_doc
+{ name       := "trivial'",
+  category   := doc_category.tactic,
+  decl_names := [`tactic.interactive.trivial'],
+  tags       := ["finishing"] }
+
 /--
 Similar to `existsi`. `use x` will instantiate the first term of an `∃` or `Σ` goal with `x`. It
-will then try to close the new goal using `triv`, or try to simplify it by applying `exists_prop`.
-Unlike `existsi`, `x` is elaborated with respect to the expected type.
+will then try to close the new goal using `trivial'`, or try to simplify it by applying
+`exists_prop`. Unlike `existsi`, `x` is elaborated with respect to the expected type.
 `use` will alternatively take a list of terms `[x0, ..., xn]`.
 
 `use` will work with constructors of arbitrary inductive types.
@@ -684,7 +700,7 @@ by use [100, tt, 4, 3]
 meta def use (l : parse pexpr_list_or_texpr) : tactic unit :=
 focus1 $
   tactic.use l;
-  try (triv <|> (do
+  try (trivial' <|> (do
         `(Exists %%p) ← target,
         to_expr ``(exists_prop.mpr) >>= tactic.apply >> skip))