feat(library/tactic/induction_tactic): add support for ginductive in the induction tactic

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;

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:

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));

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