feat(tactic/tidy): add tidy tactic (#285)

docs/tactics.md

@@ -294,3 +294,22 @@ effectively be defined and re-defined later, by tagging definitions with `@[foo]
   definition of `foo`, and provides access to the previous definition via `old`.
   (The argument can also be an `option (tactic unit)`, which is provided as `none` if
   this is the first definition tagged with `@[foo]` since `def_replacer` was invoked.)
+
+## tidy
+
+`tidy` attempts to use a variety of conservative tactics to solve the goals.
+In particular, `tidy` uses the `chain` tactic to repeatedly apply a list of tactics to
+the goal and recursively on new goals, until no tactic makes further progress.
+
+`tidy` can report the tactic script it found using `tidy { trace_result := tt }`. As an example
+```
+example : ∀ x : unit, x = unit.star := 
+begin
+  tidy {trace_result:=tt} -- Prints the trace message: "intros x, exact dec_trivial"
+end
+```
+
+The default list of tactics can be found by looking up the definition of 
+[`default_tidy_tactics`](https://github.com/leanprover/mathlib/blob/master/tactic/tidy.lean).
+
+This list can be overriden using `tidy { tactics :=  ... }`. (The list must be a list of `tactic string`.)

tactic/auto_cases.lean

@@ -0,0 +1,46 @@
+-- Copyright (c) 2017 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison
+
+import tactic.basic
+import data.option
+
+open tactic
+
+-- FIXME we need to be able to add more cases here...
+-- Alternatively, just put `pempty` into mathlib and I'll survive.
+meta def auto_cases_at (h : expr) : tactic string :=
+do t' ← infer_type h,
+  t' ← whnf t',
+  let use_cases := match t' with
+  | `(unit)      := tt
+  | `(punit)     := tt
+  | `(ulift _)   := tt
+  | `(plift _)   := tt
+  | `(prod _ _)  := tt
+  | `(and _ _)   := tt
+  | `(sigma _)   := tt
+  | `(subtype _) := tt
+  | `(Exists _)  := tt
+  | `(fin 0)     := tt
+  | `(sum _ _)   := tt -- This is perhaps dangerous!
+  | `(or _ _)    := tt -- This is perhaps dangerous!
+  | _            := ff
+  end,
+  if use_cases then
+    do cases h, pp ← pp h, return ("cases " ++ pp.to_string)
+  else
+    match t' with
+    -- `cases` can be dangerous on `eq` and `quot`, producing mysterious errors during type checking.
+    -- instead we attempt `induction`
+    | `(eq _ _)        := (do induction h, pp ← pp h, return ("induction " ++ pp.to_string))
+    | `(quot _)        := do induction h, pp ← pp h, return ("induction " ++ pp.to_string)
+    | _                := failed
+    end
+
+/-- Applies `cases` or `induction` on certain hypotheses. -/
+meta def auto_cases : tactic string :=
+do l ← local_context,
+   results ← successes (l.reverse.map(λ h, auto_cases_at h)),
+   when (results.empty) (fail "`auto_cases` did not find any hypotheses to apply `cases` or `induction` to"),
+   return (string.intercalate ", " results)

tactic/basic.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Simon Hudon
+Authors: Mario Carneiro, Simon Hudon, Scott Morrison
 -/
 import data.dlist.basic category.basic
 
@@ -54,6 +54,13 @@ e.fold [] (λ e' _ es, if e'.is_local_constant then insert e' es else es)
 meta def list_meta_vars (e : expr) : list expr :=
 e.fold [] (λ e' _ es, if e'.is_meta_var then insert e' es else es)
 
+meta def list_names_with_prefix (pre : name) (e : expr) : name_set := 
+e.fold mk_name_set $ λ e' _ l,
+  match e' with
+  | expr.const n _ := if n.get_prefix = pre then l.insert n else l
+  | _ := l
+  end
+
 /- only traverses the direct descendents -/
 meta def {u} traverse {m : Type → Type u} [applicative m]
   {elab elab' : bool} (f : expr elab → m (expr elab')) :
@@ -422,4 +429,60 @@ do
   tactic.fail_if_no_goals,
   solve_by_elim_aux opt.discharger opt.restr_hyp_set opt.max_rep
 
+meta def metavariables : tactic (list expr) :=
+do r ← result,
+   pure (r.list_meta_vars)
+
+/-- Succeeds only if the current goal is a proposition. -/
+meta def propositional_goal : tactic unit :=
+do goals ← get_goals,
+   let current_goal := goals.head,
+   current_goal_type ← infer_type current_goal,
+   p ← is_prop current_goal_type,
+   guard p
+
+variable {α : Type}
+
+private meta def iterate_aux (t : tactic α) : list α → tactic (list α)
+| L := (do r ← t, iterate_aux (r :: L)) <|> return L
+
+meta def iterate' (t : tactic α) : tactic (list α) := 
+list.reverse <$> iterate_aux t []
+
+meta def iterate1 (t : tactic α) : tactic (α × list α) :=
+do r ← t | fail "iterate1 failed: tactic did not succeed",
+   L ← iterate' t,
+   return (r, L)
+
+meta def intros1 : tactic (list expr) :=
+iterate1 intro1 >>= λ p, return (p.1 :: p.2)
+
+/-- `successes` invokes each tactic in turn, returning the list of successful results. -/
+meta def successes {α} (tactics : list (tactic α)) : tactic (list α) := 
+list.filter_map id <$> monad.sequence (tactics.map (λ t, try_core t))
+
+/-- Return target after instantiating metavars and whnf -/
+private meta def target' : tactic expr :=
+target >>= instantiate_mvars >>= whnf
+
+/--
+Just like `split`, `fsplit` applies the constructor when the type of the target is an inductive data type with one constructor.
+However it does not reorder goals or invoke `auto_param` tactics.
+-/
+-- FIXME check if we can remove `auto_param := ff`
+meta def fsplit : tactic unit :=
+do [c] ← target' >>= get_constructors_for | tactic.fail "fsplit tactic failed, target is not an inductive datatype with only one constructor",
+   mk_const c >>= λ e, apply e {new_goals := new_goals.all, auto_param := ff} >> skip
+
+run_cmd add_interactive [`fsplit]
+
+/-- Calls `injection` on each hypothesis, and then, for each hypothesis on which `injection`
+    succeeds, clears the old hypothesis. -/
+meta def injections_and_clear : tactic unit :=
+do l ← local_context,
+   results ← successes $ l.map $ λ e, injection e >> clear e,
+   when (results.empty) (fail "could not use `injection` then `clear` on any hypothesis")
+
+run_cmd add_interactive [`injections_and_clear]
+
 end tactic

tactic/chain.lean

@@ -0,0 +1,151 @@
+-- Copyright (c) 2018 Scott Morrison. All rights reserved.
+-- Released under Apache 2.0 license as described in the file LICENSE.
+-- Authors: Scott Morrison, Mario Carneiro
+
+import tactic
+import data.option
+
+open interactive
+
+namespace tactic
+
+/-
+This file defines a `chain` tactic, which takes a list of tactics, and exhaustively tries to apply them
+to the goals, until no tactic succeeds on any goal.
+
+Along the way, it generates auxiliary declarations, in order to speed up elaboration time
+of the resulting (sometimes long!) proofs.
+
+This tactic is used by the `tidy` tactic.
+-/
+
+-- α is the return type of our tactics. When `chain` is called by `tidy`, this is string,
+-- describing what that tactic did as an interactive tactic.
+variable {α : Type}
+
+/-
+Because chain sometimes pauses work on the first goal and works on later goals, we need a method
+for combining a list of results generated while working on a later goal into a single result.
+This enables `tidy {trace_result := tt}` to output faithfully reproduces its operation, e.g.
+````
+intros,
+simp,
+apply lemma_1,
+work_on_goal 2 {
+  dsimp,
+  simp
+},
+refl
+````
+-/
+
+namespace interactive
+open lean.parser
+meta def work_on_goal : parse small_nat → itactic → tactic unit
+| n t := do goals ← get_goals,
+            let earlier_goals := goals.take n,
+            let later_goals := goals.drop (n+1),
+            set_goals (goals.nth n).to_list,
+            t,
+            new_goals ← get_goals,
+            set_goals (earlier_goals ++ new_goals ++ later_goals)
+end interactive
+
+inductive tactic_script (α : Type) : Type
+| base : α → tactic_script
+| work (index : ℕ) (first : α) (later : list tactic_script) (closed : bool) : tactic_script
+
+meta def tactic_script.to_string : tactic_script string → string
+| (tactic_script.base a) := a
+| (tactic_script.work n a l c) := "work_on_goal " ++ (to_string n) ++ " { " ++ (", ".intercalate (a :: l.map(λ m : tactic_script string, m.to_string))) ++ " }"
+
+meta instance : has_to_string (tactic_script string) := 
+{ to_string := λ s, s.to_string }
+
+meta instance tactic_script_unit_has_to_string : has_to_string (tactic_script unit) := 
+{ to_string := λ s, "[chain tactic]" }
+
+meta def abstract_if_success {α} (tac : expr → tactic α) (g : expr) : tactic α :=
+do 
+  type ← infer_type g,
+  is_lemma ← is_prop type,
+  if is_lemma then -- there's no point making the abstraction, and indeed it's slower
+    tac g
+  else do
+    m ← mk_meta_var type,
+    a ← tac m,
+    do {
+      val ← instantiate_mvars m,
+      guard (val.list_meta_vars = []),
+      c  ← new_aux_decl_name,
+      gs ← get_goals,
+      set_goals [g],
+      add_aux_decl c type val ff >>= unify g,
+      set_goals gs }
+    <|> unify m g,
+    return a
+
+/-- 
+`chain_many tac` recursively tries `tac` on all goals, working depth-first on generated subgoals,
+until it no longer succeeds on any goal. `chain_many` automatically makes auxiliary definitions.
+-/
+meta mutual def chain_single, chain_many, chain_iter {α} (tac : tactic α)
+with chain_single : expr → tactic (α × list (tactic_script α)) | g :=
+do set_goals [g],
+  a ← tac,
+  l ← get_goals >>= chain_many,
+  return (a, l)
+with chain_many : list expr → tactic (list (tactic_script α))
+| [] := return []
+| [g] := do {
+  (a, l) ← chain_single g,
+  return (tactic_script.base a :: l) } <|> return []
+| gs := chain_iter gs []
+with chain_iter : list expr → list expr → tactic (list (tactic_script α))
+| [] _ := return []
+| (g :: later_goals) stuck_goals := do {
+  (a, l) ← abstract_if_success chain_single g,
+  new_goals ← get_goals,
+  let w := tactic_script.work stuck_goals.length a l (new_goals = []),
+  let current_goals := stuck_goals.reverse ++ new_goals ++ later_goals,
+  set_goals current_goals, -- we keep the goals up to date, so they are correct at the end
+  l' ← chain_many current_goals,
+  return (w :: l') } <|> chain_iter later_goals (g :: stuck_goals)
+
+meta def chain_core {α : Type} [has_to_string (tactic_script α)] (tactics : list (tactic α)) : tactic (list string) :=
+do results ← (get_goals >>= chain_many (first tactics)),
+   when (results.empty) (fail "`chain` tactic made no progress"),
+   return (results.map (λ r : tactic_script α, to_string r))
+
+variables [has_to_string (tactic_script α)] [has_to_format α]
+
+declare_trace chain
+
+meta def trace_output (t : tactic α) : tactic α :=
+do tgt ← target,
+   r ← t,
+   name ← decl_name,
+   trace format!"`chain` successfully applied a tactic during elaboration of {name}:",
+   tgt ← pp tgt,
+   trace format!"previous target: {tgt}",
+   trace format!"tactic result: {r}",
+   tgt ← try_core target,
+   tgt ← match tgt with
+          | (some tgt) := pp tgt
+          | none       := return "no goals"
+          end,
+   trace format!"new target: {tgt}",
+   pure r
+
+private meta def chain_handle_trace (tactics : list (tactic α)) : tactic (list string) :=
+if is_trace_enabled_for `chain then
+  chain_core (tactics.map trace_output)
+else 
+  chain_core tactics
+
+meta def chain (tactics : list (tactic α)) : tactic (list string) :=
+do sequence ← chain_handle_trace tactics,
+   when (sequence.empty) (fail "`chain` tactic made no progress"),
+   pure sequence
+
+end tactic

tactic/interactive.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2017 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Mario Carneiro, Simon Hudon, Sebastien Gouezel
+Authors: Mario Carneiro, Simon Hudon, Sebastien Gouezel, Scott Morrison
 -/
 import data.dlist data.dlist.basic data.prod category.basic
   tactic.basic tactic.rcases tactic.generalize_proofs
@@ -157,16 +157,20 @@ meta def unfold_coes (loc : parse location) : tactic unit :=
 unfold [``coe,``lift_t,``has_lift_t.lift,``coe_t,``has_coe_t.coe,``coe_b,``has_coe.coe,
         ``coe_fn, ``has_coe_to_fun.coe, ``coe_sort, ``has_coe_to_sort.coe] loc
 
+/-- Unfold auxiliary definitions associated with the currently declaration. -/
+meta def unfold_aux : tactic unit :=
+do tgt ← target,
+   name ← decl_name,
+   let to_unfold := (tgt.list_names_with_prefix name),
+   guard (¬ to_unfold.empty),
+   -- should we be using simp_lemmas.mk_default?
+   simp_lemmas.mk.dsimplify to_unfold.to_list tgt >>= tactic.change
+
 /-- For debugging only. This tactic checks the current state for any
 missing dropped goals and restores them. Useful when there are no
 goals to solve but "result contains meta-variables". -/
 meta def recover : tactic unit :=
-do r ← tactic.result,
-   tactic.set_goals $ r.fold [] $ λ e _ l,
-     match e with
-     | expr.mvar _ _ _ := insert e l
-     | _ := l
-     end
+metavariables >>= tactic.set_goals 
 
 /-- Like `try { tac }`, but in the case of failure it continues
 from the failure state instead of reverting to the original state. -/