test(tests/lean/run): add basic ematching tests

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

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