feat(library/tools): add mini_crush

library/init/meta/rb_map.lean

@@ -50,6 +50,9 @@ map f m
 meta def filter {A B} [has_ordering A] (m : rb_map A B) (f : B → Prop) [decidable_pred f] :=
 fold m (mk _ _) $ λa b m', if f b then insert m' a b else m'
 
+meta def mfold {key data α :Type} {m : Type → Type} [monad m] (mp : rb_map key data) (a : α) (fn : key → data → α → m α) : m α :=
+mp^.fold (return a) (λ k d act, act >>= fn k d)
+
 end rb_map
 
 meta def mk_rb_map {key data : Type} [has_ordering key] : rb_map key data :=
@@ -163,6 +166,9 @@ s^.size
 meta def fold {key α : Type} (s : rb_set key) (a : α) (fn : key → α → α) : α :=
 s^.fold a (λ k _ a, fn k a)
 
+meta def mfold {key α :Type} {m : Type → Type} [monad m] (s : rb_set key) (a : α) (fn : key → α → m α) : m α :=
+s^.fold (return a) (λ k act, act >>= fn k)
+
 meta def to_list {key : Type} (s : rb_set key) : list key :=
 s^.fold [] list.cons
 
@@ -193,4 +199,8 @@ meta instance : has_to_format name_set :=
 
 meta def of_list (l : list name) : name_set :=
 list.foldl name_set.insert mk_name_set l
+
+meta def mfold {α :Type} {m : Type → Type} [monad m] (ns : name_set) (a : α) (fn : name → α → m α) : m α :=
+ns^.fold (return a) (λ k act, act >>= fn k)
+
 end name_set

library/init/meta/simp_tactic.lean

@@ -300,7 +300,7 @@ meta def intro1_aux : bool → list name → tactic expr
 | _  _       := failed
 
 meta def simp_intro_aux (cfg : simp_config) (updt : bool) : simp_lemmas → bool → list name → tactic unit
-| S tt     [] := return ()
+| S tt     [] := try (simplify_goal S cfg)
 | S use_ns ns := do
   t ← target,
   if t^.is_napp_of `not 1 then
@@ -320,7 +320,7 @@ 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 return ()
+    else (try (simplify_goal S cfg) >> mcond (expr.is_pi <$> target) (simp_intro_aux S use_ns ns) (return ()))
 
 meta def simp_intros_using (s : simp_lemmas) (cfg : simp_config := {}) : tactic unit :=
 simp_intro_aux cfg ff s ff []

library/tools/mini_crush/default.lean

@@ -0,0 +1,100 @@
+/-
+Copyright (c) 2017 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+We implement a crush-like strategy using simplifier,
+SMT gadgets, and robust simplifier.
+
+This is just a demo.
+-/
+declare_trace mini_crush
+
+namespace mini_crush
+open tactic
+
+meta def size (e : expr) : nat :=
+e^.fold 1 (λ e _ n, n+1)
+
+/- Collect relevant functions -/
+
+meta def is_auto_construction : name → bool
+| (name.mk_string "brec_on" p)      := tt
+| (name.mk_string "cases_on" p)     := tt
+| (name.mk_string "rec_on" p)       := tt
+| (name.mk_string "no_confusion" p) := tt
+| (name.mk_string "below" p)        := tt
+| _                                 := ff
+
+meta def is_relevant_fn (n : name) : tactic bool :=
+do env ← get_env,
+   if ¬env^.is_definition n ∨ is_auto_construction n then return ff
+   else if env^.in_current_file n then return tt
+   else in_open_namespaces n
+
+meta def collect_revelant_fns_aux : name_set → expr → tactic name_set
+| s e :=
+e^.mfold s $ λ t _ s,
+  match t with
+  | expr.const c _ :=
+    if s^.contains c then return s
+    else mcond (is_relevant_fn c)
+      (do new_s ← return $ if c^.is_internal then s else s^.insert c,
+          d     ← get_decl c,
+          collect_revelant_fns_aux new_s d^.value)
+      (return s)
+  | _              := return s
+  end
+
+meta def collect_revelant_fns : tactic name_set :=
+do ctx ← local_context,
+   s₁  ← mfoldl (λ s e, infer_type e >>= collect_revelant_fns_aux s) mk_name_set ctx,
+   target >>= collect_revelant_fns_aux s₁
+
+meta def add_relevant_eqns (s : simp_lemmas) : tactic simp_lemmas :=
+do fns ← collect_revelant_fns,
+   fns^.mfold s (λ fn s, get_eqn_lemmas_for tt fn >>= mfoldl simp_lemmas.add_simp s)
+
+/- Collect terms that are inductive datatypes -/
+
+meta def is_inductive (e : expr) : tactic bool :=
+do type ← infer_type e,
+   C    ← return type^.get_app_fn,
+   env  ← get_env,
+   return $ C^.is_constant && env^.is_inductive C^.const_name
+
+meta def collect_inductive_aux : expr_set → expr → tactic expr_set
+| S e :=
+  if S^.contains e then return S
+  else do
+    new_S ← mcond (is_inductive e) (return $ S^.insert e) (return S),
+    match e with
+    | expr.app _ _    := fold_explicit_args e new_S collect_inductive_aux
+    | expr.pi _ _ d b := if e^.is_arrow then collect_inductive_aux S d >>= flip collect_inductive_aux b else return new_S
+    | _               := return new_S
+    end
+
+meta def collect_inductive : expr → tactic expr_set :=
+collect_inductive_aux mk_expr_set
+
+meta def collect_inductive_from_target : tactic (list expr) :=
+do S ← target >>= collect_inductive,
+   return $ list.qsort (λ e₁ e₂, size e₁ < size e₂) $ S^.to_list
+
+/- Induction -/
+
+meta def try_induction_aux (cont : tactic unit) : list expr → tactic unit
+| []      := failed
+| (e::es) := (step (induction e); cont; now) <|> try_induction_aux es
+
+meta def try_induction (cont : tactic unit) : tactic unit :=
+focus1 $ collect_inductive_from_target >>= mfilter (λ e, return $ e^.is_local_constant) >>= try_induction_aux cont
+
+meta def strategy_1 (cfg : simp_config := {}) : tactic unit :=
+do s ← simp_lemmas.mk_default >>= add_relevant_eqns,
+   try_induction (simph_intros_using s cfg >> (now <|> triv <|> reflexivity reducible <|> contradiction <|> rsimp <|> try_for 1000 reflexivity))
+
+end mini_crush
+
+meta def mini_crush :=
+mini_crush.strategy_1

tests/lean/run/cpdt2.lean

@@ -0,0 +1,107 @@
+/-
+CPDT Chapter 2, Introducing Inductive Types
+-/
+import tools.mini_crush
+universe variable u
+
+export nat (succ)
+
+def is_zero : ℕ → bool
+| 0        := tt
+| (succ _) := ff
+
+def plus : ℕ → ℕ → ℕ
+| 0 m         := m
+| (succ n') m := succ (plus n' m)
+
+theorem n_plus_0 (n : ℕ) : plus n 0 = n :=
+by mini_crush
+
+lemma plus_S (n1 n2 : nat) : plus n1 (succ n2) = succ (plus n1 n2) :=
+by mini_crush
+
+inductive nat_list : Type
+| NNil  : nat_list
+| NCons : nat → nat_list → nat_list
+
+open nat_list
+
+def nlength : nat_list → ℕ
+| NNil          := 0
+| (NCons _ ls') := succ (nlength ls')
+
+def napp : nat_list → nat_list → nat_list
+| NNil ls2 := ls2
+| (NCons n ls1') ls2 := NCons n (napp ls1' ls2)
+
+theorem nlength_napp (ls1 ls2 : nat_list) : nlength (napp ls1 ls2) = plus (nlength ls1) (nlength ls2) :=
+by mini_crush
+
+inductive nat_btree : Type
+| NLeaf : nat_btree
+| NNode : nat_btree → ℕ → nat_btree → nat_btree
+
+open nat_btree
+
+def nsize : nat_btree → ℕ
+| NLeaf             := succ 0
+| (NNode tr1 _ tr2) := plus (nsize tr1) (nsize tr2)
+
+def nsplice : nat_btree → nat_btree → nat_btree
+| NLeaf tr2               := NNode tr2 0 NLeaf
+| (NNode tr1' n tr2') tr2 := NNode (nsplice tr1' tr2) n tr2'
+
+@[simp] theorem plus_assoc (n1 n2 n3 : nat) : plus (plus n1 n2) n3 = plus n1 (plus n2 n3) :=
+by mini_crush
+
+theorem nsize_nsplice (tr1 tr2 : nat_btree) : nsize (nsplice tr1 tr2) = plus (nsize tr2) (nsize tr1) :=
+by mini_crush
+
+export list (nil cons)
+
+def length {α : Type u} : list α → ℕ
+| nil          := 0
+| (cons _ ls') := succ (length ls')
+
+def app {α : Type u} : list α → list α → list α
+| nil ls2           := ls2
+| (cons x ls1') ls2 := cons x (app ls1' ls2)
+
+theorem length_app {α : Type u} (ls1 ls2 : list α) : length (app ls1 ls2) = plus (length ls1) (length ls2) :=
+by mini_crush
+
+inductive pformula : Type
+| Truth : pformula
+| Falsehood : pformula
+| Conjunction : pformula → pformula → pformula.
+
+open pformula
+
+def pformula_denote : pformula → Prop
+| Truth               := true
+| Falsehood           := false
+| (Conjunction f1 f2) := pformula_denote f1 ∧ pformula_denote f2
+
+open pformula
+
+inductive formula : Type
+| Eq     : nat → nat → formula
+| And    : formula → formula → formula
+| Forall : (nat → formula) → formula
+
+open formula
+
+example forall_refl : formula := Forall (λ x, Eq x x)
+
+def formula_denote : formula → Prop
+| (Eq n1 n2)  := n1 = n2
+| (And f1 f2) := formula_denote f1 ∧ formula_denote f2
+| (Forall f') := ∀ n : nat, formula_denote (f' n)
+
+def swapper : formula → formula
+| (Eq n1 n2)  := Eq n2 n1
+| (And f1 f2) := And (swapper f2) (swapper f1)
+| (Forall f') := Forall (λ n, swapper (f' n))
+
+theorem swapper_preserves_truth (f) : formula_denote f → formula_denote (swapper f) :=
+by mini_crush