From d50da0feb7af567f811147caec9b62f91cf365c9 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sat, 4 Mar 2017 14:54:45 -0800
Subject: [PATCH] feat(library/tactic/induction_tactic): add support for
 ginductive in the induction tactic

---
 src/library/inductive_compiler/ginductive.cpp |  9 ++++++++
 src/library/inductive_compiler/ginductive.h   |  3 +++
 src/library/tactic/induction_tactic.cpp       |  4 ++--
 .../lean/run/ginductive_induction_tactic.lean | 21 +++++++++++++++++++
 4 files changed, 35 insertions(+), 2 deletions(-)
 create mode 100644 tests/lean/run/ginductive_induction_tactic.lean

diff --git a/src/library/inductive_compiler/ginductive.cpp b/src/library/inductive_compiler/ginductive.cpp
index af05eb71b4..ab2574af38 100644
--- a/src/library/inductive_compiler/ginductive.cpp
+++ b/src/library/inductive_compiler/ginductive.cpp
@@ -15,6 +15,15 @@ Author: Daniel Selsam
 #include "library/kernel_serializer.h"
 
 namespace lean {
+expr whnf_ginductive(type_context & ctx, expr const & e) {
+    return ctx.whnf_head_pred(e, [&](expr const & e) {
+            if (is_macro(e)) return true;
+            expr const & fn = get_app_fn(e);
+            if (!is_constant(fn)) return true;
+            return !is_ginductive(ctx.env(), const_name(fn));
+        });
+}
+
 static unsigned compute_idx_number(expr const & e) {
     buffer<expr> args;
     unsigned idx = 0;
diff --git a/src/library/inductive_compiler/ginductive.h b/src/library/inductive_compiler/ginductive.h
index 2796319c91..8818d44db5 100644
--- a/src/library/inductive_compiler/ginductive.h
+++ b/src/library/inductive_compiler/ginductive.h
@@ -29,6 +29,9 @@ unsigned get_ginductive_num_params(environment const & env, name const & ind_nam
 /* \brief Returns the names of all types that are mutually inductive with \e ind_name */
 list<name> get_ginductive_mut_ind_names(environment const & env, name const & ind_name);
 
+/* Return \c e until it is in weak head normal form OR the head is a ginductive datatype. */
+expr whnf_ginductive(type_context & ctx, expr const & e);
+
 /* \brief Returns the offset of a simulated introduction rule.
 
 Example:
diff --git a/src/library/tactic/induction_tactic.cpp b/src/library/tactic/induction_tactic.cpp
index cf6d88b38c..3107790a15 100644
--- a/src/library/tactic/induction_tactic.cpp
+++ b/src/library/tactic/induction_tactic.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/vm/vm_expr.h"
 #include "library/vm/vm_name.h"
 #include "library/vm/vm_list.h"
+#include "library/inductive_compiler/ginductive.h"
 #include "library/tactic/tactic_state.h"
 #include "library/tactic/revert_tactic.h"
 #include "library/tactic/intro_tactic.h"
@@ -350,8 +351,7 @@ vm_obj tactic_induction(vm_obj const & H, vm_obj const & ns, vm_obj const & rec,
     if (is_none(rec)) {
         try {
             type_context ctx = mk_type_context_for(s, m);
-            /* Remark: should we support the inductive compiler */
-            expr type = ctx.relaxed_whnf(ctx.infer(to_expr(H)));
+            expr type = whnf_ginductive(ctx, ctx.infer(to_expr(H)));
             expr C    = get_app_fn(type);
             if (is_constant(C)) {
                 name C_rec = get_dep_recursor(ctx.env(), const_name(C));
diff --git a/tests/lean/run/ginductive_induction_tactic.lean b/tests/lean/run/ginductive_induction_tactic.lean
new file mode 100644
index 0000000000..b2da5b455f
--- /dev/null
+++ b/tests/lean/run/ginductive_induction_tactic.lean
@@ -0,0 +1,21 @@
+mutual inductive {u} foo, bla (α : Type u)
+with foo : Type u
+| mk₁ : α → bla → foo
+with bla : Type u
+| mk₂ : α → bla → bla
+| mk₃ : list foo → bla
+
+def cidx {α} : bla α → nat
+| (bla.mk₂ _ _) := 1
+| (bla.mk₃ _) := 2
+
+def to_list {α} : bla α → list (foo α)
+| (bla.mk₂ _ _)  := []
+| (bla.mk₃ ls) := ls
+
+lemma ex {α} (b : bla α) (h : cidx b = 2) : b = bla.mk₃ (to_list b) :=
+begin
+  induction b using bla.rec,
+  {simp [cidx] at h, exact absurd h (dec_trivial)},
+  {simp [to_list]}
+end