From d6b72ef4d700b3ad0f8d32c85a6066ef73da8df6 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 20 May 2015 23:23:05 -0700
Subject: [PATCH] feat(library/tactic/induction_tactic): try available
 recursors until one works

closes #615
---
 src/library/tactic/induction_tactic.cpp | 17 +++++++++++++++--
 tests/lean/hott/615.hlean               | 21 +++++++++++++++++++++
 2 files changed, 36 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/hott/615.hlean

diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index 8cb2c56ec..93a8c1e59 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -332,8 +332,21 @@ public:
                     return execute(g, H, H_type, *m_rec_name);
                 } else if (inductive::is_inductive_decl(m_env, const_name(I))) {
                     return execute(g, H, H_type, inductive::get_elim_name(const_name(I)));
-                } else if (auto rs = get_recursors_for(m_env, const_name(I))) {
-                    return execute(g, H, H_type, head(rs));
+                } else if (list<name> rs = get_recursors_for(m_env, const_name(I))) {
+                    while (rs) {
+                        name r = head(rs);
+                        rs     = tail(rs);
+                        if (!rs) {
+                            // last one
+                            return execute(g, H, H_type, r);
+                        } else {
+                            try {
+                                flet<list<name>>     save_ids(m_ids, m_ids);
+                                flet<constraint_seq> save_cs(m_cs, m_cs);
+                                return execute(g, H, H_type, r);
+                            } catch (exception &) {}
+                        }
+                    }
                 }
             }
             throw tactic_exception(sstream() << "invalid 'induction' tactic, hypothesis '" << m_h_name
diff --git a/tests/lean/hott/615.hlean b/tests/lean/hott/615.hlean
new file mode 100644
index 000000000..d712a7deb
--- /dev/null
+++ b/tests/lean/hott/615.hlean
@@ -0,0 +1,21 @@
+-- HoTT
+import hit.circle
+open circle eq int
+
+attribute circle.rec circle.elim [recursor 4]
+
+protected definition my_code (x : circle) : Type₀ :=
+begin
+  induction x,
+  { exact ℤ},
+  { apply ua, apply equiv_succ}
+end
+
+protected definition my_decode {x : circle} : my_code x → base = x :=
+begin
+  induction x,
+  { exact power loop},
+  { apply eq_of_homotopy, intro a,
+    refine !arrow.arrow_transport ⬝ !transport_eq_r ⬝ _,
+    rewrite [transport_code_loop_inv,power_con,succ_pred]}
+end