fix(meta/mk_dec_eq_instance): handle indices and ginductives

library/init/list.lean

@@ -125,4 +125,17 @@ foldr (λ a r, p a || r) ff l
 definition all (l : list A) (p : A → bool) : bool :=
 foldr (λ a r, p a && r) tt l
 
+def zip : list A → list B → list (prod A B)
+| []      _       := []
+| _       []      := []
+| (x::xs) (y::ys) := (prod.mk x y) :: zip xs ys
+
+def repeat (a : A) : ℕ → list A
+| 0 := []
+| (succ n) := a :: repeat n
+
+def iota : ℕ → list ℕ
+| 0 := []
+| (succ n) := iota n ++ [succ n]
+
 end list

library/init/meta/environment.lean

@@ -46,6 +46,8 @@ meta constant inductive_num_params : environment → name → nat
 meta constant inductive_num_indices : environment → name → nat
 /- Return tt iff the inductive datatype recursor supports dependent elimination -/
 meta constant inductive_dep_elim : environment → name → bool
+/- Return tt iff the given name is a generalized inductive datatype -/
+meta constant is_ginductive : environment → name → bool
 /- Fold over declarations in the environment -/
 meta constant fold {A :Type} : environment → A → (declaration → A → A) → A
 /- (relation_info env n) returns some value if n is marked as a relation in the given environment.

library/init/meta/mk_dec_eq_instance.lean

@@ -93,18 +93,38 @@ do
 private meta def dec_eq_case_1 (I_name : name) (F_name : name) : tactic unit :=
 intro `w >>= cases >> all_goals (dec_eq_case_2 I_name F_name)
 
-meta def mk_dec_eq_instance : tactic unit :=
+meta def mk_dec_eq_instance_core : tactic unit :=
 do I_name ← get_dec_eq_type_name,
    env ← get_env,
    v_name ← return `_v,
    F_name ← return `_F,
+   num_indices ← return $ inductive_num_indices env I_name,
+   idx_names ← return $ list.map (λ (p : name × nat), mk_num_name p~>fst p~>snd) (list.zip (list.repeat `idx num_indices) (list.iota num_indices)),
+
    -- Use brec_on if type is recursive.
    -- We store the functional in the variable F.
    if is_recursive env I_name
-   then intro1 >>= (λ x, induction_core semireducible x (I_name <.> "brec_on") [v_name, F_name])
+   then intro1 >>= (λ x, induction_core semireducible x (I_name <.> "brec_on") (idx_names ++ [v_name, F_name]))
    else intro v_name >> return (),
+
    -- Apply cases to first element of type (I ...)
    get_local v_name >>= cases,
    all_goals (dec_eq_case_1 I_name F_name)
 
+meta def mk_dec_eq_instance : tactic unit :=
+do env ← get_env,
+   (pi x1 i1 d1 (pi x2 i2 d2 b)) ← target >>= whnf | failed,
+   (const I_name ls) ← return (get_app_fn d1) | failed,
+   when (is_ginductive env I_name ∧ ¬ is_inductive env I_name) $
+      do { d1' ← whnf d1,
+           (app I_basic_const I_idx) ← return d1' | failed,
+           I_idx_type ← infer_type I_idx,
+           new_goal ← to_expr `(∀ (_idx : %%I_idx_type), decidable_eq (%%I_basic_const _idx)),
+           assert `_basic_dec_eq new_goal,
+           swap,
+           to_expr `(_basic_dec_eq %%I_idx) >>= exact,
+           intro1,
+           return () },
+   mk_dec_eq_instance_core
+
 end tactic

src/library/vm/vm_environment.cpp

@@ -6,6 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/type_checker.h"
 #include "kernel/inductive/inductive.h"
+#include "library/inductive_compiler/ginductive.h"
 #include "library/standard_kernel.h"
 #include "library/module.h"
 #include "library/util.h"
@@ -140,6 +141,10 @@ vm_obj environment_inductive_dep_elim(vm_obj const & env, vm_obj const & n) {
     return mk_vm_bool(inductive::has_dep_elim(to_env(env), to_name(n)));
 }
 
+vm_obj environment_is_ginductive(vm_obj const & env, vm_obj const & n) {
+    return mk_vm_bool(static_cast<bool>(is_ginductive(to_env(env), to_name(n))));
+}
+
 vm_obj environment_fold(vm_obj const &, vm_obj const & env, vm_obj const & a, vm_obj const & fn) {
     vm_obj r = a;
     to_env(env).for_each_declaration([&](declaration const & d) {
@@ -198,6 +203,7 @@ void initialize_vm_environment() {
     DECLARE_VM_BUILTIN(name({"environment", "inductive_num_params"}),  environment_inductive_num_params);
     DECLARE_VM_BUILTIN(name({"environment", "inductive_num_indices"}), environment_inductive_num_indices);
     DECLARE_VM_BUILTIN(name({"environment", "inductive_dep_elim"}),    environment_inductive_dep_elim);
+    DECLARE_VM_BUILTIN(name({"environment", "is_ginductive"}),         environment_is_ginductive);
     DECLARE_VM_BUILTIN(name({"environment", "relation_info"}),         environment_relation_info);
     DECLARE_VM_BUILTIN(name({"environment", "refl_for"}),              environment_refl_for);
     DECLARE_VM_BUILTIN(name({"environment", "symm_for"}),              environment_symm_for);

tests/lean/run/mk_dec_eq_instance_indices.lean

@@ -0,0 +1,33 @@
+open tactic
+
+namespace X1
+
+inductive Foo : unit -> Type
+| mk : Foo () -> Foo ()
+
+instance (u : unit) : decidable_eq (Foo u) := by mk_dec_eq_instance
+
+end X1
+
+namespace X2
+
+inductive Foo : bool -> bool -> Type
+| mk₁ : Foo tt tt
+| mk₂ : Foo ff ff -> Foo tt ff
+
+instance (idx₁ idx₂ : bool) : decidable_eq (Foo idx₁ idx₂) := by mk_dec_eq_instance
+
+end X2
+
+namespace X3
+
+constants (C : nat -> Type)
+constants (c : Pi (n : nat), C n)
+
+inductive Foo : Pi (n : nat), C n -> Type
+| mk₁ : Pi (n : nat), Foo n (c n) -> Foo (n+1) (c (n+1))
+| mk₂ : Foo 0 (c 0)
+
+noncomputable instance (n : nat) (c : C n) : decidable_eq (Foo n c) := by mk_dec_eq_instance
+
+end X3

tests/lean/run/mk_dec_eq_instance_nested.lean

@@ -0,0 +1,31 @@
+open tactic
+
+namespace X1
+
+inductive Wrap (A : Type) : Type
+| mk : A -> Wrap
+
+inductive Foo : Type
+| mk : Wrap Foo -> Foo
+
+instance : decidable_eq Foo := by mk_dec_eq_instance
+
+end X1
+
+namespace X2
+
+inductive Foo : Type
+| mk : list Foo -> Foo
+
+instance : decidable_eq Foo := by mk_dec_eq_instance
+
+end X2
+
+namespace X3
+
+inductive Foo : bool -> Type
+| mk : list (list (Foo tt)) -> Foo ff
+
+instance (b : bool) : decidable_eq (Foo b) := by mk_dec_eq_instance
+
+end X3

tests/lean/run/nested_inductive.lean

@@ -125,3 +125,11 @@ inductive foo (A : Type*)
 | mk : A -> wrap' (list' foo) -> foo
 
 end X13
+
+namespace X14
+print "with indices in original"
+
+inductive Foo : bool -> Type
+| mk : list (Foo ff) -> Foo tt
+
+end X14