From 5798ac43de7506d2c72296eea7ae70f94892f1c8 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 7 May 2015 09:09:07 -0700
Subject: [PATCH] fix(frontends/lean/structure_cmd): 'structure' command must
 set unfold-c attribute for auxiliary recursors

fixes #582
---
 library/data/rat/basic.lean          | 2 +-
 src/frontends/lean/structure_cmd.cpp | 3 +++
 tests/lean/582.hlean                 | 9 +++++++++
 tests/lean/582.hlean.expected.out    | 9 +++++++++
 4 files changed, 22 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/582.hlean
 create mode 100644 tests/lean/582.hlean.expected.out

diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index 6b4e2a438..c8f27f066 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -109,7 +109,7 @@ theorem num_eq_zero_of_equiv_zero {a : prerat} : a ≡ zero → num a = 0 :=
 by rewrite [↑equiv, ↑zero, ↑of_int, mul_one, zero_mul]; intro H; exact H
 
 theorem inv_zero {d : int} (dp : d > 0) : inv (mk nat.zero d dp) = zero :=
-begin rewrite [↑inv, ↑int.cases_on, ↑cases_on, ▸*] end
+begin rewrite [↑inv, ▸*] end
 
 theorem inv_zero' : inv zero = zero := inv_zero (of_nat_succ_pos nat.zero)
 
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index 649172bd7..bbed73723 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -18,6 +18,7 @@ Author: Leonardo de Moura
 #include "kernel/error_msgs.h"
 #include "kernel/inductive/inductive.h"
 #include "library/scoped_ext.h"
+#include "library/normalize.h"
 #include "library/placeholder.h"
 #include "library/locals.h"
 #include "library/reducible.h"
@@ -725,6 +726,8 @@ struct structure_cmd_fn {
                                              opaque);
         m_env = module::add(m_env, check(m_env, new_decl));
         m_env = set_reducible(m_env, n, reducible_status::Reducible);
+        if (optional<unsigned> idx = has_unfold_c_hint(m_env, rec_on_name))
+            m_env = add_unfold_c_hint(m_env, n, *idx);
         save_def_info(n);
         add_alias(n);
     }
diff --git a/tests/lean/582.hlean b/tests/lean/582.hlean
new file mode 100644
index 000000000..f540a022f
--- /dev/null
+++ b/tests/lean/582.hlean
@@ -0,0 +1,9 @@
+open prod
+variables {A B C : Type} (f : A → B → C) (a : A) (b b' : B)
+
+example (p : b = b') : prod.cases_on (a, b) f = f a b' :=
+begin
+  esimp,
+  state,
+  rewrite p
+end
diff --git a/tests/lean/582.hlean.expected.out b/tests/lean/582.hlean.expected.out
new file mode 100644
index 000000000..57b220832
--- /dev/null
+++ b/tests/lean/582.hlean.expected.out
@@ -0,0 +1,9 @@
+582.hlean:7:2: proof state
+A : Type,
+B : Type,
+C : Type,
+f : A → B → C,
+a : A,
+b b' : B,
+p : b = b'
+⊢ f a b = f a b'