feat(library/definitional/projection): add auxiliary function for simplifying expressions containing projections and constructors

src/frontends/lean/structure_cmd.cpp

@@ -62,19 +62,6 @@ static name * g_gen_proj_mk = nullptr;
 bool get_structure_eta_thm(options const & o) { return o.get_bool(*g_gen_eta, LEAN_DEFAULT_STRUCTURE_ETA); }
 bool get_structure_proj_mk_thm(options const & o) { return o.get_bool(*g_gen_proj_mk, LEAN_DEFAULT_STRUCTURE_ETA); }
 
-/** \brief Return true iff the type named \c S can be viewed as
-    a structure in the given environment.
-
-    If not, generate an error message using \c pos.
-*/
-bool is_structure(environment const & env, name const & S) {
-    optional<inductive::inductive_decls> idecls = inductive::is_inductive_decl(env, S);
-    if (!idecls || length(std::get<2>(*idecls)) != 1)
-        return false;
-    inductive::inductive_decl decl   = head(std::get<2>(*idecls));
-    return length(inductive::inductive_decl_intros(decl)) == 1 && *inductive::get_num_indices(env, S) == 0;
-}
-
 /** \brief Return the universe parameters, number of parameters and introduction rule for the given parent structure
 
     \pre is_structure(env, S)

src/library/definitional/projection.cpp

@@ -77,6 +77,91 @@ void finalize_projection() {
     delete g_ext;
 }
 
+/** \brief Return true iff the type named \c S can be viewed as
+    a structure in the given environment.
+
+    If not, generate an error message using \c pos.
+*/
+bool is_structure(environment const & env, name const & S) {
+    optional<inductive::inductive_decls> idecls = inductive::is_inductive_decl(env, S);
+    if (!idecls || length(std::get<2>(*idecls)) != 1)
+        return false;
+    inductive::inductive_decl decl   = head(std::get<2>(*idecls));
+    return length(inductive::inductive_decl_intros(decl)) == 1 && *inductive::get_num_indices(env, S) == 0;
+}
+
+/** \brief If \c is a constructor application, then return the name of the constructor.
+    Otherwise, return none.
+*/
+optional<name> is_constructor_app(environment const & env, expr const & e) {
+    expr const & fn = get_app_fn(e);
+    if (is_constant(fn))
+        if (auto I = inductive::is_intro_rule(env, const_name(fn)))
+            return optional<name>(const_name(fn));
+    return optional<name>();
+}
+
+/** \brief If \c d is the name of a definition of the form
+            Fun (a : A), t
+    where t is a constructor application, then return the name of the constructor.
+*/
+optional<name> is_constructor_app_def(environment const & env, name const & d) {
+    if (auto decl = env.find(d)) {
+        expr const * it = &decl->get_value();
+        while (is_lambda(*it))
+            it = &binding_body(*it);
+        return is_constructor_app(env, *it);
+    }
+    return optional<name>();
+}
+
+/** \brief Return the name of constructor and projection functions iff \c e is of the form
+
+        (mk ... (pr ...) ...)
+
+    where \c mk is a constructor of a structure, and at least of the arguments is a projection \c pr
+    where \c pr is not necessarily a projection associated with \c mk.
+    In this case, the name of \c pr is returned. Otherwise, none is returned.
+*/
+optional<pair<name, name>> is_constructor_of_projections(environment const & env, expr const & e) {
+    expr const & fn = get_app_fn(e);
+    if (is_constant(fn)) {
+        if (auto I = inductive::is_intro_rule(env, const_name(fn))) {
+            if (is_structure(env, *I)) {
+                expr const * it = &e;
+                while (is_app(*it)) {
+                    expr const & arg = app_arg(*it);
+                    expr const & pr  = get_app_fn(arg);
+                    if (is_constant(pr)) {
+                        if (auto info = get_projection_info(env, const_name(pr))) {
+                            if (info->m_nparams + 1 == get_app_num_args(arg))
+                                return some(mk_pair(const_name(pr), const_name(pr)));
+                        }
+                    }
+                    it = &app_fn(*it);
+                }
+            }
+        }
+    }
+    return optional<pair<name, name>>();
+}
+
+/** \brief Return the name of constructor and projection functions iff \c d is the name of a definition of the form
+
+       Fun (a : A), t
+
+    where is_constructor_of_projections(env, t)
+ */
+optional<pair<name, name>> is_constructor_of_projections_def(environment const & env, name const & d) {
+    if (auto decl = env.find(d)) {
+        expr const * it = &decl->get_value();
+        while (is_lambda(*it))
+            it = &binding_body(*it);
+        return is_constructor_of_projections(env, *it);
+    }
+    return optional<pair<name, name>>();
+}
+
 [[ noreturn ]] static void throw_ill_formed(name const & n) {
     throw exception(sstream() << "projection generation, '" << n << "' is an ill-formed inductive datatype");
 }

src/library/definitional/projection.h

@@ -11,6 +11,13 @@ namespace lean {
 environment mk_projections(environment const & env, name const & n, buffer<name> const & proj_names, bool inst_implicit = false);
 environment mk_projections(environment const & env, name const & n, bool inst_implicit = false);
 
+/** \brief Return true iff the type named \c S can be viewed as
+    a structure in the given environment.
+
+    If not, generate an error message using \c pos.
+*/
+bool is_structure(environment const & env, name const & S);
+
 /** \brief Auxiliary information attached to projections. This information
     is used to simplify projection over constructor (efficiently)