From a41aac0e6a19c9ca9c0039eaead9cd491a8dfd23 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 19 Feb 2017 17:27:09 -0800
Subject: [PATCH] feat(library/tools/mini_crush): add tracing messages, and
 more examples

---
 library/tools/mini_crush/default.lean |  34 +++++-
 tests/lean/run/cpdt.lean              |   5 +-
 tests/lean/run/cpdt3.lean             | 161 ++++++++++++++++++++++++++
 3 files changed, 192 insertions(+), 8 deletions(-)
 create mode 100644 tests/lean/run/cpdt3.lean

diff --git a/library/tools/mini_crush/default.lean b/library/tools/mini_crush/default.lean
index d7b9a12a35..874d921fb7 100644
--- a/library/tools/mini_crush/default.lean
+++ b/library/tools/mini_crush/default.lean
@@ -81,20 +81,42 @@ 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
 
+meta def collect_inductive_hyps : tactic (list expr) :=
+local_context >>= mfoldl (λ r h, mcond (is_inductive h) (return $ h::r) (return r)) []
+
 /- Induction -/
 
-meta def try_induction_aux (cont : tactic unit) : list expr → tactic unit
+meta def try_induction_aux (cont : expr → tactic unit) : list expr → tactic unit
 | []      := failed
-| (e::es) := (step (induction e); cont; now) <|> try_induction_aux es
+| (e::es) := (step (induction e); cont e; 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 try_induction (cont : expr → tactic unit) : tactic unit :=
+focus1 $ collect_inductive_hyps >>= try_induction_aux cont
 
-meta def strategy_1 (cfg : simp_config := {}) : tactic unit :=
+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")
+  end
+  >> trace_state >> trace "--------------" >> failed
+
+meta def close_or_fail (s : name) (e : expr) : tactic unit :=
+    now
+<|> triv           <|> reflexivity reducible <|> contradiction
+<|> (rsimp >> now) <|> try_for 1000 reflexivity
+<|> report_failure s (some e)
+
+meta def strategy_1 (cfg : simp_config := {}) (n : name := "strategy 1") : 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))
+   try_induction (λ e, simph_intros_using s cfg >> close_or_fail n e)
+
+meta def strategy_2 (cfg : simp_config := {}) : tactic unit :=
+intros >> strategy_1 cfg "strategy 2"
 
 end mini_crush
 
 meta def mini_crush :=
 mini_crush.strategy_1
+<|>
+mini_crush.strategy_2
diff --git a/tests/lean/run/cpdt.lean b/tests/lean/run/cpdt.lean
index d1812fe9c5..703a77f9e1 100644
--- a/tests/lean/run/cpdt.lean
+++ b/tests/lean/run/cpdt.lean
@@ -1,3 +1,4 @@
+import tools.mini_crush
 /- "Proving in the Large" chapter of CPDT -/
 
 inductive exp : Type
@@ -19,8 +20,8 @@ def times (k : nat) : exp → exp
 
 attribute [simp] exp_eval times mul_add
 
-theorem eval_times (k e) : exp_eval (times k e) = k * exp_eval e :=
-by induction e; simph
+theorem eval_times : ∀ (k e), exp_eval (times k e) = k * exp_eval e :=
+by mini_crush
 
 def reassoc : exp → exp
 | (Const n)    := (Const n)
diff --git a/tests/lean/run/cpdt3.lean b/tests/lean/run/cpdt3.lean
new file mode 100644
index 0000000000..7b755f1838
--- /dev/null
+++ b/tests/lean/run/cpdt3.lean
@@ -0,0 +1,161 @@
+import tools.mini_crush
+/-
+This corresponds to Chapter 2 of CPDT, Some Quick Examples
+-/
+open list
+
+inductive binop : Type
+| Plus
+| Times
+
+open binop
+
+inductive exp : Type
+| Const : nat → exp
+| Binop : binop → exp → exp → exp
+
+open exp
+
+def binop_denote : binop → nat → nat → nat
+| Plus  := add
+| Times := mul
+
+def exp_denote : exp → nat
+| (Const n)       := n
+| (Binop b e1 e2) := (binop_denote b) (exp_denote e1) (exp_denote e2)
+
+inductive instr : Type
+| iConst : ℕ → instr
+| iBinop : binop → instr
+
+open instr
+
+@[reducible]
+def prog := list instr
+def stack := list nat
+
+def instr_denote (i : instr) (s : stack) : option stack :=
+match i with
+| (iConst n) := some (n :: s)
+| (iBinop b) :=
+  match s with
+  | (arg1 :: arg2 :: s') := some ((binop_denote b) arg1 arg2 :: s')
+  | _                    := none
+  end
+end
+
+def prog_denote : prog → stack → option stack
+| nil       s := some s
+| (i :: p') s :=
+  match instr_denote i s with
+  | none := none
+  | (some s') := prog_denote p' s'
+  end
+
+def compile : exp → prog
+| (Const n)       := iConst n :: nil
+| (Binop b e1 e2) := compile e2 ++ compile e1 ++ iBinop b :: nil
+
+/- This example needs a few facts from the list library. -/
+
+@[simp] theorem compile_correct' :
+  ∀ e p s, prog_denote (compile e ++ p) s = prog_denote p (exp_denote e :: s) :=
+by intro; mini_crush
+
+@[simp] theorem compile_correct : ∀ e, prog_denote (compile e) nil = some (exp_denote e :: nil) :=
+by mini_crush
+
+inductive type : Type
+| Nat
+| Bool
+
+open type
+
+inductive tbinop : type → type → type → Type
+| TPlus  : tbinop Nat Nat Nat
+| TTimes : tbinop Nat Nat Nat
+| TEq    : ∀ t, tbinop t t Bool
+| TLt    : tbinop Nat Nat Bool
+
+open tbinop
+
+inductive texp : type → Type
+| TNConst : nat → texp Nat
+| TBConst : bool → texp Bool
+| TBinop  : ∀ {t1 t2 t}, tbinop t1 t2 t → texp t1 → texp t2 → texp t
+
+open texp
+
+def type_denote : type → Type
+| Nat  := nat
+| Bool := bool
+
+/- To simulate CPDT we need the next three operations. -/
+
+def beq_nat (m n : ℕ) : bool := if m = n then tt else ff
+def eqb (b₁ b₂ : bool) : bool := if b₁ = b₂ then tt else ff
+def leb (m n : ℕ) : bool := if m < n then tt else ff
+
+def tbinop_denote : Π {arg1 arg2 res : type},
+  tbinop arg1 arg2 res → type_denote arg1 → type_denote arg2 → type_denote res
+| ._ ._ ._ TPlus      := (add : ℕ → ℕ → ℕ)
+| ._ ._ ._ TTimes     := (mul : ℕ → ℕ → ℕ)
+| ._ ._ ._ (TEq Nat)  := beq_nat
+| ._ ._ ._ (TEq Bool) := eqb
+| ._ ._ ._ TLt        := leb
+
+def texp_denote : Π {t : type}, texp t → type_denote t
+| ._ (TNConst n)             := n
+| ._ (TBConst b)             := b
+| ._ (@TBinop _ _ _ b e1 e2) := (tbinop_denote b) (texp_denote e1) (texp_denote e2)
+
+@[reducible]
+def tstack := list type
+
+inductive tinstr : tstack → tstack → Type
+| TiNConst : Π s, nat → tinstr s (Nat :: s)
+| TiBConst : Π s, bool → tinstr s (Bool :: s)
+| TiBinop  : Π {arg1 arg2 res s}, tbinop arg1 arg2 res → tinstr (arg1 :: arg2 :: s) (res :: s)
+
+open tinstr
+
+inductive tprog : tstack → tstack → Type
+| TNil  : Π {s}, tprog s s
+| TCons : Π {s1 s2 s3}, tinstr s1 s2 → tprog s2 s3 → tprog s1 s3
+
+open tprog
+
+def vstack : tstack → Type
+| nil        := unit
+| (t :: ts') := type_denote t × vstack ts'
+
+def tinstr_denote : Π {ts ts' : tstack}, tinstr ts ts' → vstack ts → vstack ts'
+| ._ ._ (TiNConst ts n)              := λ s, (n, s)
+| ._ ._ (TiBConst ts b)              := λ s, (b, s)
+| ._ ._ (@TiBinop arg1 arg2 res s b) := λ ⟨arg1, ⟨arg2, s'⟩⟩, ((tbinop_denote b) arg1 arg2, s')
+
+def tprog_denote : Π {ts ts' : tstack}, tprog ts ts' → vstack ts → vstack ts'
+| ._ ._ (@TNil _)           := λ s, s
+| ._ ._ (@TCons _ _ _ i p') := λ s, tprog_denote p' (tinstr_denote i s)
+
+def tconcat : Π {ts ts' ts'' : tstack}, tprog ts ts' → tprog ts' ts'' → tprog ts ts''
+| ._ ._ ts'' (@TNil _) p'           := p'
+| ._ ._ ts'' (@TCons _ _ _ i p1) p' := TCons i (tconcat p1 p')
+
+def tcompile : Π {t : type}, texp t → Π ts : tstack, tprog ts (t :: ts)
+| ._ (TNConst n) ts             := TCons (TiNConst _ n) TNil
+| ._ (TBConst b) ts             := TCons (TiBConst _ b) TNil
+| ._ (@TBinop _ _ _ b e1 e2) ts := tconcat (tcompile e2 _)
+      (tconcat (tcompile e1 _) (TCons (TiBinop b) TNil))
+
+@[simp] lemma tconcat_correct : ∀ ts ts' ts'' (p : tprog ts ts') (p' : tprog ts' ts'') (s : vstack ts),
+  tprog_denote (tconcat p p') s = tprog_denote p' (tprog_denote p s) :=
+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
+
+theorem tcompile_correct :
+  ∀ t (e : texp t), tprog_denote (tcompile e nil) () = (texp_denote e, ()) :=
+by mini_crush