fix(library/tactic/unfold_rec): support indexed families at unfold_rec

This commit also removes many (now unnecessary) folds from the HoTT
library.

See issue #692

We still have to implement support for recursive definitions based on
brec_on that recurse over inductive families.

hott/algebra/e_closure.hlean

@@ -84,27 +84,16 @@ section
              (ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) t) :=
   begin
     induction t,
-    { unfold [ap_e_closure_elim_h,e_closure.elim],
+    { unfold [ap_e_closure_elim_h, e_closure.elim],
       apply square_of_eq, exact !con.right_inv ⬝ !con.left_inv⁻¹},
     { apply ids},
-    { rewrite [↑e_closure.elim,↓e_closure.elim e r,
+    { unfold [e_closure.elim, ap_e_closure_elim_h],
-               ↑ap_e_closure_elim_h,
+      rewrite [ap_con (ap h)],
-               ↓ap_e_closure_elim_h e p r,
-               ↓ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) r,
-               ↓ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) r,
-               ap_con (ap h)],
       refine (transpose !ap_compose_inv)⁻¹ᵛ ⬝h _,
       rewrite [con_inv,inv_inv,-inv2_inv],
       exact !ap_inv2 ⬝v square_inv2 v_0},
-    { rewrite [↑e_closure.elim,↓e_closure.elim e r, ↓e_closure.elim e r',
+    { unfold [e_closure.elim, ap_e_closure_elim_h],
-               ↑ap_e_closure_elim_h,
+      rewrite [ap_con (ap h)],
-               ↓ap_e_closure_elim_h e p r,
-               ↓ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) r,
-               ↓ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) r,
-               ↓ap_e_closure_elim_h e p r',
-               ↓ap_e_closure_elim_h e (λa a' s, ap_compose h g (e s)) r',
-               ↓ap_e_closure_elim_h e' (λa a' s, (ap (ap h) (p s))⁻¹) r',
-               ap_con (ap h)],
       refine (transpose !ap_compose_con)⁻¹ᵛ ⬝h _,
       rewrite [con_inv,inv_inv,con2_inv],
       refine !ap_con2 ⬝v square_con2 v_0 v_1},

hott/hit/two_quotient.hlean

@@ -273,7 +273,7 @@ namespace two_quotient
     { exact P0 a},
     { exact P1 s},
     { exact abstract [unfold 10] begin induction q with a a' t t' q,
-      rewrite [↑e_closure.elim,↓e_closure.elim P1 t,↓e_closure.elim P1 t'],
+      rewrite [↑e_closure.elim],
       apply con_inv_eq_idp, exact P2 q end end},
   end
   local attribute elim [unfold 8]

src/library/tactic/unfold_rec.cpp

@@ -90,7 +90,8 @@ class unfold_rec_fn : public replace_visitor_aux {
     }
 
     // return true if e is of the form (C.rec ...)
-    bool is_rec_app(expr const & e, buffer<expr> const & locals, name & rec_name, unsigned & main_arg_pos, buffer<unsigned> & rec_arg_pos) {
+    bool is_rec_app(expr const & e, buffer<expr> const & locals, name & rec_name, buffer<unsigned> & indices_pos,
+                    unsigned & main_arg_pos, buffer<unsigned> & rec_arg_pos) {
         buffer<expr> args;
         expr fn = get_app_args(e, args);
         if (!is_constant(fn))
@@ -102,34 +103,58 @@ class unfold_rec_fn : public replace_visitor_aux {
         if (!is_recursive_datatype(m_env, *I))
             return false;
         unsigned major_idx = *inductive::get_elim_major_idx(m_env, const_name(fn));
-        if (major_idx >= args.size())
+        unsigned nindices  = *inductive::get_num_indices(m_env, *I);
-            return false;
+        lean_assert(nindices <= major_idx);
-        if (auto it = get_local_pos(locals, args[major_idx])) {
+        unsigned rel_idx   = major_idx - nindices; // first index we should track
-            main_arg_pos = *it;
+        // Collect position of indices (at least the ones that occur in e)
-            for (unsigned i = major_idx+1; i < args.size(); i++) {
+        while (rel_idx < args.size() && rel_idx < major_idx) {
-                if (auto it2 = get_local_pos(locals, args[i])) {
+            if (auto it2 = get_local_pos(locals, args[rel_idx])) {
-                    rec_arg_pos.push_back(*it2);
+                indices_pos.push_back(*it2);
-                } else {
+            } else {
-                    return false;
+                return false;
-                }
             }
+            rel_idx++;
+        }
+
+        if (major_idx >= args.size()) {
+            // Some indices and the major premise may not occur in e because of eta-reduction
+            main_arg_pos      = locals.size() + major_idx - args.size();
+            for (unsigned i = rel_idx; i < major_idx; i++)
+                indices_pos.push_back(locals.size() + i - args.size());
             return true;
         }
-        return false;
+
+        if (auto it = get_local_pos(locals, args[major_idx])) {
+            main_arg_pos = *it;
+        } else {
+            return false;
+        }
+
+        for (unsigned i = major_idx+1; i < args.size(); i++) {
+            if (auto it2 = get_local_pos(locals, args[i])) {
+                rec_arg_pos.push_back(*it2);
+            } else {
+                return false;
+            }
+        }
+        return true;
     }
 
     enum rec_kind { BREC, REC, NOREC };
 
     // try to detect the kind of recursive definition
-    rec_kind get_rec_kind(expr const & e, buffer<expr> const & locals, name & rec_name, unsigned & main_arg_pos, buffer<unsigned> & rec_arg_pos) {
+    rec_kind get_rec_kind(expr const & e, buffer<expr> const & locals, name & rec_name,
-        if (is_rec_app(e, locals, rec_name, main_arg_pos, rec_arg_pos))
+                          buffer<unsigned> & indices_pos, unsigned & main_arg_pos, buffer<unsigned> & rec_arg_pos) {
+        if (is_rec_app(e, locals, rec_name, indices_pos, main_arg_pos, rec_arg_pos))
             return REC;
         buffer<expr> args;
         expr fn = get_app_args(e, args);
         if (is_constant(fn) && const_name(fn) == inductive::get_elim_name(get_prod_name()) &&
             args.size() >= 5) {
             // try do detect brec_on pattern
-            if (is_rec_app(args[4], locals, rec_name, main_arg_pos, rec_arg_pos)) {
+            if (is_rec_app(args[4], locals, rec_name, indices_pos, main_arg_pos, rec_arg_pos) &&
+                // for brec, eta is not applicable, so main_arg_pos must be < locals.size()
+                main_arg_pos < locals.size()) {
                 for (unsigned i = 5; i < args.size(); i++) {
                     if (auto it2 = get_local_pos(locals, args[i])) {
                         rec_arg_pos.push_back(*it2);
@@ -176,14 +201,16 @@ class unfold_rec_fn : public replace_visitor_aux {
         rec_kind                 m_kind;
         name                     m_rec_name;
         unsigned                 m_major_idx; // position of the major premise in the recursor
+        buffer<unsigned> const & m_indices_pos; // position of the datatype indices in the function being unfolded
         unsigned                 m_main_pos;  // position of the (recursive) argument in the function being unfolded
         buffer<unsigned> const & m_rec_arg_pos; // position of the other arguments that are not fixed in the recursion
         name                     m_prod_rec_name;
 
         fold_rec_fn(type_checker_ptr & tc, expr const & fn, buffer<expr> const & args, rec_kind k, name const & rec_name,
-                    unsigned main_pos, buffer<unsigned> const & rec_arg_pos):
+                    buffer<unsigned> const & indices_pos, unsigned main_pos, buffer<unsigned> const & rec_arg_pos):
             m_tc(tc), m_fn(fn), m_args(args), m_kind(k), m_rec_name(rec_name),
             m_major_idx(*inductive::get_elim_major_idx(m_tc->env(), rec_name)),
+            m_indices_pos(indices_pos),
             m_main_pos(main_pos), m_rec_arg_pos(rec_arg_pos) {
             m_prod_rec_name = inductive::get_elim_name(get_prod_name());
             lean_assert(m_main_pos < args.size());
@@ -197,6 +224,10 @@ class unfold_rec_fn : public replace_visitor_aux {
                 throw fold_failed();
             buffer<expr> new_args;
             new_args.append(m_args);
+            unsigned nindices = m_indices_pos.size();
+            for (unsigned i = 0; i < m_indices_pos.size(); i++) {
+                new_args[m_indices_pos[i]] = args[m_major_idx - nindices + i];
+            }
             new_args[m_main_pos] = args[m_major_idx];
             for (unsigned i = 0; i < m_rec_arg_pos.size(); i++) {
                 new_args[m_rec_arg_pos[i]] = args[m_major_idx + 1 + i];
@@ -265,13 +296,15 @@ class unfold_rec_fn : public replace_visitor_aux {
         }
         name rec_name;
         unsigned main_pos;
+        buffer<unsigned> indices_pos;
         buffer<unsigned> rec_arg_pos;
-        rec_kind k = get_rec_kind(fn_body, fn_locals, rec_name, main_pos, rec_arg_pos);
+        rec_kind k = get_rec_kind(fn_body, fn_locals, rec_name, indices_pos, main_pos, rec_arg_pos);
-        if (k == NOREC) {
+        if (k == NOREC || main_pos >= args.size()) {
             // norecursive definition
             return unfold_simple(fn, args);
         }
-        for (unsigned i = fn_locals.size(); i < args.size(); i++)
+        unsigned rest = main_pos >= fn_locals.size() ? main_pos+1 : fn_locals.size();
+        for (unsigned i = rest; i < args.size(); i++)
             rec_arg_pos.push_back(i);
         auto new_main_cs  = m_tc->whnf(args[main_pos]);
         if (!is_constructor_app(m_env, new_main_cs.first) || new_main_cs.second) {
@@ -294,7 +327,7 @@ class unfold_rec_fn : public replace_visitor_aux {
         //    //head is a recursor... so the unfold is probably not generating a nice result...
         //    throw fold_failed();
         // }
-        return fold_rec_fn(m_tc, fn, args, k, rec_name, main_pos, rec_arg_pos)(new_e);
+        return fold_rec_fn(m_tc, fn, args, k, rec_name, indices_pos, main_pos, rec_arg_pos)(new_e);
     }
 
     bool unfold_cnst(expr const & e) {