feat(library/tools/mini_crush): improve mini_crush

library/init/data/list/basic.lean

@@ -128,7 +128,7 @@ def filter (p : α → Prop) [decidable_pred p] : list α → list α
 | []     := []
 | (a::l) := if p a then a :: filter l else filter l
 
-definition find [decidable_eq α] : α → list α → nat
+def find [decidable_eq α] : α → list α → nat
 | a []       := 0
 | a (b :: l) := if a = b then 0 else succ (find a l)
 
@@ -142,18 +142,18 @@ def taken : ℕ → list α → list α
 | (succ n) [] := []
 | (succ n) (x :: r) := x :: taken n r
 
-definition foldl (f : α → β → α) : α → list β → α
+def foldl (f : α → β → α) : α → list β → α
 | a []       := a
 | a (b :: l) := foldl (f a b) l
 
-definition foldr (f : α → β → β) : β → list α → β
+def foldr (f : α → β → β) : β → list α → β
 | b []       := b
 | b (a :: l) := f a (foldr b l)
 
-definition any (l : list α) (p : α → bool) : bool :=
+def any (l : list α) (p : α → bool) : bool :=
 foldr (λ a r, p a || r) ff l
 
-definition all (l : list α) (p : α → bool) : bool :=
+def all (l : list α) (p : α → bool) : bool :=
 foldr (λ a r, p a && r) tt l
 
 def bor  (l : list bool) : bool := any l id
@@ -188,10 +188,16 @@ def iota : ℕ → list ℕ :=
 def sum [has_add α] [has_zero α] : list α → α :=
 foldl add zero
 
-definition last : Π l : list α, l ≠ [] → α
-| []          h := absurd rfl h
-| [a]         h := a
-| (a₁::a₂::l) h := last (a₂::l) (λ h, list.no_confusion h)
+def last : Π l : list α, l ≠ [] → α
+| []        h := absurd rfl h
+| [a]       h := a
+| (a::b::l) h := last (b::l) (λ h, list.no_confusion h)
+
+def ilast [inhabited α] : list α → α
+| []        := arbitrary α
+| [a]       := a
+| [a, b]    := b
+| (a::b::l) := ilast l
 
 def intersperse (sep : α) : list α → list α
 | []      := []

library/init/meta/simp_tactic.lean

@@ -299,8 +299,8 @@ meta def intro1_aux : bool → list name → tactic expr
 | tt (n::ns) := intro n
 | _  _       := failed
 
-meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic unit
-| S tt     [] := try (simplify_goal S cfg)
+meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic simp_lemmas
+| S tt     [] := try (simplify_goal S cfg) >> return S
 | S use_ns ns := do
   t ← target,
   if t^.is_napp_of `not 1 then
@@ -320,19 +320,25 @@ meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool
   else do
     new_t ← whnf t reducible,
     if new_t^.is_pi then change new_t >> simp_intro_aux S use_ns ns
-    else (try (simplify_goal S cfg) >> mcond (expr.is_pi <$> target) (simp_intro_aux S use_ns ns) (return ()))
+    else
+      try (simplify_goal S cfg) >>
+      mcond (expr.is_pi <$> target)
+        (simp_intro_aux S use_ns ns)
+        (if use_ns ∧ ¬ns^.empty then failed else return S)
 
 meta def simp_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
-simp_intro_aux cfg ff s ff []
+step $ simp_intro_aux cfg ff s ff []
 
 meta def simph_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
+step $
 do s ← collect_ctx_simps >>= s^.append,
    simp_intro_aux cfg tt s ff []
 
 meta def simp_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
-simp_intro_aux cfg ff s tt ns
+step $ simp_intro_aux cfg ff s tt ns
 
 meta def simph_intro_lst_using (ns : list name) (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
+step $
 do s ← collect_ctx_simps >>= s^.append,
    simp_intro_aux cfg tt s tt ns
 

library/init/meta/tactic.lean

@@ -440,6 +440,9 @@ meta constant kdepends_on (e t : expr) (md := reducible) : tactic bool
 
 open list nat
 
+meta def induction' (h : expr) (ns : list name := []) (rec : option name := none) (md := semireducible) : tactic unit :=
+induction h ns rec md >> return ()
+
 /-- Remark: set_goals will erase any solved goal -/
 meta def cleanup : tactic unit :=
 get_goals >>= set_goals

library/tools/mini_crush/default.lean

@@ -93,30 +93,53 @@ meta def try_induction_aux (cont : expr → tactic unit) : list expr → tactic
 meta def try_induction (cont : expr → tactic unit) : tactic unit :=
 focus1 $ collect_inductive_hyps >>= try_induction_aux cont
 
+meta def report {α : Type} [has_to_tactic_format α] (a : α) : tactic unit :=
+when_tracing `mini_crush $ trace a
+
 meta def report_failure (s : name) (e : option expr := none) : tactic unit :=
 when_tracing `mini_crush $
   match e with
   | none   := trace ("FAILED '" ++ to_string s ++ "' at")
-  | some e := (do p ← pp e, trace (to_fmt "FAILED '" ++ to_fmt s ++ "' processing " ++ p ++ to_fmt " at")) <|> trace ("FAILED '" ++ to_string s ++ "' at")
+  | some e := (do p ← pp e, trace (to_fmt "FAILED '" ++ to_fmt s ++ "' processing '" ++ p ++ to_fmt "' at")) <|> trace ("FAILED '" ++ to_string s ++ "' at")
   end
-  >> trace_state >> trace "--------------" >> failed
+  >> trace_state >> trace "--------------"
 
-meta def close_or_fail (s : name) (e : expr) : tactic unit :=
+meta def close_or_fail (s : name) (e : option expr) : tactic unit :=
     now
 <|> triv           <|> reflexivity reducible <|> contradiction
 <|> (rsimp >> now) <|> try_for 1000 reflexivity
-<|> report_failure s (some e)
+<|> (report_failure s e >> failed)
 
-meta def strategy_1 (cfg : simp_config := {}) (n : name := "strategy 1") : tactic unit :=
-do s ← simp_lemmas.mk_default >>= add_relevant_eqns,
-   try_induction (λ e, simph_intros_using s cfg >> close_or_fail n e)
+meta def simple (s : simp_lemmas) (cfg : simp_config) (s_name : name) (h : option expr) : tactic unit :=
+simph_intros_using s cfg >> close_or_fail s_name h
 
-meta def strategy_2 (cfg : simp_config := {}) : tactic unit :=
-intros >> strategy_1 cfg "strategy 2"
+meta def mk_simp_lemmas (s : option simp_lemmas := none) : tactic simp_lemmas :=
+match s with
+| some s := return s
+| none   := simp_lemmas.mk_default >>= add_relevant_eqns
+end
+
+meta def strategy_1 (cfg : simp_config := {}) (s : option simp_lemmas := none) (s_name : name := "strategy 1") : tactic unit :=
+do s ← mk_simp_lemmas s,
+   try_induction (λ h, simple s cfg s_name (some h))
+
+meta def strategy_2_aux (cfg : simp_config) : simp_lemmas → tactic unit
+| s :=
+  do s ← simp_intro_aux cfg tt s tt [`_], -- Introduce next hypothesis
+     h ← list.ilast <$> local_context,
+     try $ solve1 (mwhen (is_inductive h) $ induction' h; simple s cfg "strategy 2" (some h)),
+     now <|> strategy_2_aux s
+
+meta def strategy_2 (cfg : simp_config := {}) (s : option simp_lemmas := none) : tactic unit :=
+do s ← mk_simp_lemmas s,
+   strategy_2_aux cfg s
 
 end mini_crush
 
-meta def mini_crush :=
-mini_crush.strategy_1
+open tactic mini_crush
+
+meta def mini_crush (cfg : simp_config := {}) :=
+do s ← mk_simp_lemmas,
+strategy_1 cfg (some s)
 <|>
-mini_crush.strategy_2
+strategy_2 cfg (some s)

tests/lean/run/cpdt3.lean

@@ -58,11 +58,11 @@ def compile : exp → prog
 
 /- This example needs a few facts from the list library. -/
 
-@[simp] theorem compile_correct' :
+@[simp] lemma compile_correct' :
   ∀ e p s, prog_denote (compile e ++ p) s = prog_denote p (exp_denote e :: s) :=
-by intro; mini_crush
+by mini_crush
 
-@[simp] theorem compile_correct : ∀ e, prog_denote (compile e) nil = some (exp_denote e :: nil) :=
+@[simp] lemma compile_correct : ∀ e, prog_denote (compile e) nil = some (exp_denote e :: nil) :=
 by mini_crush
 
 inductive type : Type
@@ -154,8 +154,8 @@ by mini_crush
 
 @[simp] lemma tcompile_correct' : ∀ t (e : texp t) ts (s : vstack ts),
   tprog_denote (tcompile e ts) s = (texp_denote e, s) :=
-by intros t e; mini_crush
+by mini_crush
 
-theorem tcompile_correct :
+lemma tcompile_correct :
   ∀ t (e : texp t), tprog_denote (tcompile e nil) () = (texp_denote e, ()) :=
 by mini_crush