From 30a962d5e0609d22a57d90b8be0dc5beca4fffec Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 9 Jan 2017 19:26:29 -0800
Subject: [PATCH] test(tests/lean/run): add more tests for the smt_tactic
 framework

---
 tests/lean/run/smt_tests3.lean | 39 ++++++++++++++++++++++++++++++++++
 1 file changed, 39 insertions(+)
 create mode 100644 tests/lean/run/smt_tests3.lean

diff --git a/tests/lean/run/smt_tests3.lean b/tests/lean/run/smt_tests3.lean
new file mode 100644
index 0000000000..e01845e762
--- /dev/null
+++ b/tests/lean/run/smt_tests3.lean
@@ -0,0 +1,39 @@
+def f : nat → nat
+| 0     := 1
+| (n+1) := f n + 1
+
+example (a : nat) : f a ≠ 0 :=
+begin
+  induction a,
+  dsimp [f], intro x, contradiction,
+  dsimp [f],
+  change nat.succ (f a) ≠ 0,
+  apply nat.succ_ne_zero
+end
+
+example (a : nat) : f a ≠ 0 :=
+begin [smt]
+  induction a,
+  { ematch_using [f] },
+  { repeat {ematch_using [f, nat.add_one_eq_succ, nat.succ_ne_zero]}}
+end
+
+example (a : nat) : f (a+1) = f a + 1 :=
+begin [smt]
+  dsimp [f]
+end
+
+example (a : nat) : f (a+1) = f a + 1 :=
+begin [smt]
+  simp [f]
+end
+
+example (a : nat) : f (a+1) = f a + 1 :=
+begin [smt]
+  ematch_using [f]
+end
+
+example (a : nat) : f 0 = 1 :=
+begin [smt]
+  ematch_using [f]
+end