From 90eb5c8ca54a0f0cc754b122efc3645935da99d0 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 4 Feb 2015 19:33:08 -0800
Subject: [PATCH] test(tests/lean/hott): add test for rewriter in the HoTT
 version

---
 tests/lean/hott/rewriter1.hlean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)
 create mode 100644 tests/lean/hott/rewriter1.hlean

diff --git a/tests/lean/hott/rewriter1.hlean b/tests/lean/hott/rewriter1.hlean
new file mode 100644
index 000000000..ecc6e97d3
--- /dev/null
+++ b/tests/lean/hott/rewriter1.hlean
@@ -0,0 +1,19 @@
+import algebra.group
+open path_algebra
+
+constant f {A : Type} : A → A → A
+
+theorem test1 {A : Type} [s : add_comm_group A] (a b c : A) : f (a + 0) (f (a + 0) (a + 0)) = f a (f (0 + a) a) :=
+begin
+  rewrite
+    add_right_id at {1 3} -- rewrite 1st and 3rd occurrences
+    [0 + _]add_comm   -- apply commutativity to (0 + _)
+end
+
+axiom Ax {A : Type} [s₁ : has_mul A] [s₂ : has_one A] (a : A) : f (a * 1) (a * 1) = 1
+
+theorem test2 {A : Type} [s : comm_group A] (a b c : A) : f a a = 1 :=
+begin
+  rewrite -(mul_right_id a)  -- - means apply symmetry, rewrite 0 ==> a * 0  at 1st and 2nd occurrences
+          Ax                 -- use Ax as rewrite rule
+end