From 48de9436785fbb3284b2068718c20cf932fde431 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 1 Dec 2015 12:16:37 -0700 Subject: [PATCH] test(tests/lean/run): add Daniel's example --- tests/lean/run/blast_ematch7.lean | 25 +++++++++++++++++++++++++ 1 file changed, 25 insertions(+) create mode 100644 tests/lean/run/blast_ematch7.lean diff --git a/tests/lean/run/blast_ematch7.lean b/tests/lean/run/blast_ematch7.lean new file mode 100644 index 000000000..aff177afb --- /dev/null +++ b/tests/lean/run/blast_ematch7.lean @@ -0,0 +1,25 @@ +import algebra.ring data.int +open algebra + +variables {A : Type} [s : ring A] (a b : A) +include s + +set_option blast.subst false +set_option blast.simp false +set_option blast.ematch true +attribute zero_mul [forward] + +example : a = 0 → a * b = 0 := +by blast + +open int + +-- Remark: int is a non-recursive datatype. So, the recursor action will +-- destruct it. This is a dumb move, and we need to prove the same theorem 4 times because of that. +-- It also demonstrates we need better heuristics for the recursor action and/or annotations. +set_option blast.recursor false + +definition ex1 (a b : int) : a = 0 → a * b = 0 := +by blast + +print ex1