From a96aed6dfe987f62bfd2dc69ba853a7b18554cd9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 16 Nov 2015 22:38:33 -0800
Subject: [PATCH] test(tests/lean): add tests for simp priorities

---
 tests/lean/simplifier20.lean              | 31 +++++++++++++++++++++++
 tests/lean/simplifier20.lean.expected.out |  5 ++++
 tests/lean/simplifier21.lean              | 28 ++++++++++++++++++++
 tests/lean/simplifier21.lean.expected.out |  4 +++
 4 files changed, 68 insertions(+)
 create mode 100644 tests/lean/simplifier20.lean
 create mode 100644 tests/lean/simplifier20.lean.expected.out
 create mode 100644 tests/lean/simplifier21.lean
 create mode 100644 tests/lean/simplifier21.lean.expected.out

diff --git a/tests/lean/simplifier20.lean b/tests/lean/simplifier20.lean
new file mode 100644
index 000000000..bb9b6584d
--- /dev/null
+++ b/tests/lean/simplifier20.lean
@@ -0,0 +1,31 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+constants a b c : nat
+axiom H1 : a = b
+axiom H2 : a = c
+
+attribute H1 [simp]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp] [priority 20000]
+
+#simplify eq env 0 a -- b
+
+attribute H2 [simp] [priority 30000]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp] [priority 20000]
+
+#simplify eq env 0 a -- c
+
+attribute H2 [simp] [priority 20000]
+attribute H1 [simp] [priority 20001]
+
+#simplify eq env 0 a -- b
+
+end test_congr
diff --git a/tests/lean/simplifier20.lean.expected.out b/tests/lean/simplifier20.lean.expected.out
new file mode 100644
index 000000000..bd0911c16
--- /dev/null
+++ b/tests/lean/simplifier20.lean.expected.out
@@ -0,0 +1,5 @@
+c
+b
+c
+c
+b
diff --git a/tests/lean/simplifier21.lean b/tests/lean/simplifier21.lean
new file mode 100644
index 000000000..866ad4ca6
--- /dev/null
+++ b/tests/lean/simplifier21.lean
@@ -0,0 +1,28 @@
+/- Basic rewriting with eq and generic congruence, with no conditionals -/
+
+namespace test_congr
+
+constants a b c : nat
+axiom H1 : a = b
+axiom H2 : a = c
+
+attribute H1 [simp]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- c
+
+attribute H1 [simp]
+
+#simplify eq env 0 a -- b
+
+attribute H1 [simp] [priority std.priority.default+1]
+attribute H2 [simp]
+
+#simplify eq env 0 a -- b
+
+attribute H2 [simp] [priority std.priority.default+2]
+attribute H1 [simp] [priority std.priority.default+1]
+
+#simplify eq env 0 a -- c
+
+end test_congr
diff --git a/tests/lean/simplifier21.lean.expected.out b/tests/lean/simplifier21.lean.expected.out
new file mode 100644
index 000000000..02c2efff3
--- /dev/null
+++ b/tests/lean/simplifier21.lean.expected.out
@@ -0,0 +1,4 @@
+c
+b
+b
+c