From 4f06e91ce52040e57f934d65fd063a8da45d14c5 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 1 Dec 2015 11:59:14 -0700
Subject: [PATCH] test(tests/lean/run): add new test

---
 tests/lean/run/blast_ematch3.lean |  7 -------
 tests/lean/run/blast_ematch6.lean | 30 ++++++++++++++++++++++++++++++
 2 files changed, 30 insertions(+), 7 deletions(-)
 create mode 100644 tests/lean/run/blast_ematch6.lean

diff --git a/tests/lean/run/blast_ematch3.lean b/tests/lean/run/blast_ematch3.lean
index a219b7839..25b7c897e 100644
--- a/tests/lean/run/blast_ematch3.lean
+++ b/tests/lean/run/blast_ematch3.lean
@@ -35,11 +35,4 @@ set_option blast.ematch true
 
 theorem inv_mul_cancel_left (a b : A) : a⁻¹ * (a * b) = b :=
 by blast
-
-attribute mul_one [forward]
-attribute inv_mul_cancel_right [forward]
-
--- TODO(Leo): check if qfc can get this one
--- theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
--- by blast
 end
diff --git a/tests/lean/run/blast_ematch6.lean b/tests/lean/run/blast_ematch6.lean
new file mode 100644
index 000000000..0ce360390
--- /dev/null
+++ b/tests/lean/run/blast_ematch6.lean
@@ -0,0 +1,30 @@
+import algebra.ring data.nat
+open algebra
+
+variables {A : Type}
+
+section
+variable [s : group A]
+include s
+
+set_option blast.simp   false
+set_option blast.subst  false
+set_option blast.ematch true
+
+attribute mul_one      [forward]
+attribute mul.assoc    [forward]
+attribute mul.left_inv [forward]
+attribute one_mul      [forward]
+
+theorem inv_eq_of_mul_eq_one {a b : A} (H : a * b = 1) : a⁻¹ = b :=
+-- This is the kind of theorem that can be easily proved using superposition,
+-- but cannot to be proved using E-matching.
+-- To prove it using E-matching, we must provide the following auxiliary assertion.
+-- E-matching can prove it automatically, and then it is trivial to prove the conclusion
+-- using it.
+-- Remark: this theorem can also be proved using model-based quantifier instantiation (MBQI) available in Z3.
+-- So, we may be able to prove it using qcf.
+assert a⁻¹ * 1 = b, by blast,
+by blast
+
+end