From 5844e9673402d94e10998803dd1612b64e770682 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 30 Nov 2015 10:33:00 -0700
Subject: [PATCH] test(tests/lean/run): add basic ematching tests

---
 tests/lean/run/blast_ematch2.lean | 12 +++++++++
 tests/lean/run/blast_ematch3.lean | 45 +++++++++++++++++++++++++++++++
 2 files changed, 57 insertions(+)
 create mode 100644 tests/lean/run/blast_ematch2.lean
 create mode 100644 tests/lean/run/blast_ematch3.lean

diff --git a/tests/lean/run/blast_ematch2.lean b/tests/lean/run/blast_ematch2.lean
new file mode 100644
index 000000000..1888269e9
--- /dev/null
+++ b/tests/lean/run/blast_ematch2.lean
@@ -0,0 +1,12 @@
+import data.nat
+open nat
+constant f : nat → nat
+constant g : nat → nat
+
+definition lemma1 [forward] : ∀ x, g (f x) = x :=
+sorry
+
+set_option blast.ematch true
+
+example (a b : nat) : f a = f b → a = b :=
+by blast
diff --git a/tests/lean/run/blast_ematch3.lean b/tests/lean/run/blast_ematch3.lean
new file mode 100644
index 000000000..a219b7839
--- /dev/null
+++ b/tests/lean/run/blast_ematch3.lean
@@ -0,0 +1,45 @@
+import algebra.ring data.nat
+open algebra
+
+variables {A : Type}
+
+section
+variables [s : add_comm_monoid A]
+include s
+
+attribute add.comm [forward]
+attribute add.assoc [forward]
+
+set_option blast.simp   false
+set_option blast.subst  false
+set_option blast.ematch true
+
+theorem add_comm_three  (a b c : A) : a + b + c = c + b + a :=
+by blast
+
+theorem add.comm4 : ∀ (n m k l : A), n + m + (k + l) = n + k + (m + l) :=
+by blast
+end
+
+section
+variable [s : group A]
+include s
+
+attribute mul.assoc [forward]
+attribute mul.left_inv [forward]
+attribute one_mul [forward]
+
+set_option blast.simp   false
+set_option blast.subst  false
+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