feat(library/inductive): scaffold for inductive type manager

src/library/CMakeLists.txt

@@ -14,7 +14,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   attribute_manager.cpp error_handling.cpp unification_hint.cpp
   local_context.cpp metavar_context.cpp type_context.cpp export_decl.cpp delayed_abstraction.cpp
   fun_info.cpp congr_lemma.cpp defeq_canonizer.cpp scope_pos_info_provider.cpp
-  mpq_macro.cpp arith_instance_manager.cpp
+  inductive.cpp mpq_macro.cpp arith_instance_manager.cpp
 
   # Legacy -- The following files will be eventually deleted
   normalize.cpp justification.cpp constraint.cpp metavar.cpp choice.cpp locals.cpp

src/library/inductive.cpp

@@ -0,0 +1,42 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+#include "kernel/environment.h"
+#include "library/inductive.h"
+
+namespace lean {
+
+bool is_inductive(environment const & env, name const & ind_name) {
+    throw exception("TODO(dhs): implement");
+}
+
+list<name> get_intro_rule_names(environment const & env, name const & ind_name) {
+    throw exception("TODO(dhs): implement");
+}
+
+optional<name> is_intro_rule_name(environment const & env, name const & ir_name) {
+    throw exception("TODO(dhs): implement");
+}
+
+/* For basic inductive types, we can prove this lemma using <ind_name>.no_confusion.
+
+   For non-basic inductive types, we first create a function <ind_name>.cidx that maps
+   each element of \e ind_type to a natural number depending only on its constructor.
+   We then prove the lemma <tt>forall c1 c2, cidx c1 != cidx c2 -> c1 != c2</tt> and
+   use it to prove the desired theorem.
+*/
+expr prove_intro_rules_disjoint(environment const & env, name const & ir_name1, name const & ir_name2) {
+    throw exception("TODO(dhs): implement");
+}
+
+unsigned get_inductive_num_params(environment const & env, name const & ind_name) {
+    throw exception("TODO(dhs): implement");
+}
+
+void initialize_library_inductive() {}
+void finalize_library_inductive() {}
+
+}

src/library/inductive.h

@@ -0,0 +1,69 @@
+/*
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Daniel Selsam
+*/
+#pragma once
+#include "kernel/environment.h"
+
+/* This file presents a unified interface to all (user-facing) inductive types,
+   which include the basic inductive types understood by the kernel, as well as
+   mutual inductive types and nested inductive types that are compiled to basic
+   inductive types behind the scenes.
+
+   For every inductive type \e ind_name with intro rule \e ir_name recognized
+   by this module, the following are guaranteed to be in the environment:
+
+   1. <ind_name>.cases_on
+   2. <ind_name>.size_of
+   3. <ind_name>.has_size_of [instance]
+   4. <ind_name>.<ir_name>.size_of_spec
+   5. <ind_name>.<ir_name>.injective
+
+   Suppose <ind_name> has parameters (A : Type) and <ir_name> has non-recursive arguments X
+   and recursive arguments Y1 ... Yn.
+
+   Then <ir_name>.size_of_spec is a proof of:
+
+     forall C A x y1 ... yn,
+       let k := size_of (<ir_name> A x y1 ... yn) in
+         (k > size_of y1 -> ... -> k > size_of yn -> C) -> C
+
+
+   and <ir_name>.injective is a proof of:
+
+     forall C A x y x' y',
+       <ir_name> A x y = <ir_name> A x' y' -> (x = x' -> y = y' -> C) -> C
+*/
+
+namespace lean {
+
+/* \brief Returns true if \e ind_name is the name of a (user-facing) inductive type,
+   whether it is basic, mutual, or nested. */
+bool is_inductive(environment const & env, name const & ind_name);
+
+/* \brief Returns the names of the introduction rules for the inductive type \e ind_name. */
+list<name> get_intro_rule_names(environment const & env, name const & ind_name);
+
+/* \brief Returns the name of the inductive type if \e ir_name is indeed an introduction rule. */
+optional<name> is_intro_rule_name(environment const & env, name const & ir_name);
+
+/* \brief Given the names of two introduction rules for the same inductive type, returns a
+   proof that they are disjoint.
+
+   \example For an inductive type \e I with parameters (A : Type) and two introduction rules
+   c1 : X1 -> I and c2 : X2 -> I, returns a proof of the following theorem:
+
+   forall (A : Type), forall (x1 : X1) (x2 : X2), @c1 A x1 = @c2 A x2 -> false.
+
+   \remark When there are indices, the equality will need to be heterogenous.
+*/
+expr prove_intro_rules_disjoint(environment const & env, name const & ir_name1, name const & ir_name2);
+
+/* \brief Returns the number of parameters for the given inductive type \e ind_name. */
+unsigned get_inductive_num_params(environment const & env, name const & ind_name);
+
+void initialize_library_inductive();
+void finalize_library_inductive();
+}

src/library/init_module.cpp

@@ -49,6 +49,7 @@ Author: Leonardo de Moura
 #include "library/delayed_abstraction.h"
 #include "library/app_builder.h"
 #include "library/fun_info.h"
+#include "library/inductive.h"
 #include "library/mpq_macro.h"
 #include "library/arith_instance_manager.h"
 
@@ -128,6 +129,7 @@ void initialize_library_module() {
     initialize_unification_hint();
     initialize_type_context();
     initialize_delayed_abstraction();
+    initialize_library_inductive();
     initialize_mpq_macro();
     initialize_arith_instance_manager();
 }
@@ -135,6 +137,7 @@ void initialize_library_module() {
 void finalize_library_module() {
     finalize_arith_instance_manager();
     finalize_mpq_macro();
+    finalize_library_inductive();
     finalize_delayed_abstraction();
     finalize_type_context();
     finalize_unification_hint();