feat(library/type_context): add mk_tmp_local that allows us to specify the pretty printing name

We also modify the type inference procedure to preserve the binder names.

src/library/blast/blast.cpp

@@ -58,6 +58,11 @@ class blastenv {
             return blast::mk_local(n, n, type, bi);
         }
 
+        virtual expr mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
+            name n = m_benv.m_ngen.next();
+            return blast::mk_local(n, pp_n, type, bi);
+        }
+
         virtual bool is_tmp_local(expr const & e) const {
             return blast::is_local(e);
         }

src/library/tmp_type_context.cpp

@@ -50,6 +50,13 @@ expr tmp_type_context::mk_tmp_local(expr const & type, binder_info const & bi) {
     return lean::mk_local(n, n, type, bi);
 }
 
+expr tmp_type_context::mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
+    unsigned idx = m_next_local_idx;
+    m_next_local_idx++;
+    name n(*g_prefix, idx);
+    return lean::mk_local(n, pp_n, type, bi);
+}
+
 bool tmp_type_context::is_tmp_local(expr const & e) const {
     if (!is_local(e))
         return false;

src/library/tmp_type_context.h

@@ -63,6 +63,7 @@ public:
 
     virtual bool is_extra_opaque(name const & n) const { return m_opaque_pred(n); }
     virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info());
+    virtual expr mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi = binder_info());
     virtual bool is_tmp_local(expr const & e) const;
     virtual bool is_uvar(level const & l) const;
     virtual bool is_mvar(expr const & e) const;

src/library/type_context.cpp

@@ -597,7 +597,7 @@ bool type_context::is_def_eq_binding(expr e1, expr e2) {
             // local is used inside t or s
             if (!var_e1_type)
                 var_e1_type = instantiate_rev(binding_domain(e1), subst.size(), subst.data());
-            subst.push_back(mk_tmp_local(*var_e1_type));
+            subst.push_back(mk_tmp_local(binding_name(e1), *var_e1_type));
         } else {
             expr const & dont_care = mk_Prop();
             subst.push_back(dont_care);
@@ -712,7 +712,7 @@ bool type_context::process_assignment(expr const & ma, expr const & v) {
                 return false;
             lean_assert(i <= locals.size());
             if (i == locals.size())
-                locals.push_back(mk_tmp_local(binding_domain(m_type)));
+                locals.push_back(mk_tmp_local_from_binding(m_type));
             lean_assert(i < locals.size());
             m_type = instantiate(binding_body(m_type), locals[i]);
         }
@@ -981,7 +981,7 @@ expr type_context::infer_lambda(expr e) {
         es.push_back(e);
         ds.push_back(binding_domain(e));
         expr d = instantiate_rev(binding_domain(e), ls.size(), ls.data());
-        expr l = mk_tmp_local(d, binding_info(e));
+        expr l = mk_tmp_local(binding_name(e), d, binding_info(e));
         ls.push_back(l);
         e = binding_body(e);
     }
@@ -1111,7 +1111,7 @@ optional<name> type_context::constant_is_class(expr const & e) {
 optional<name> type_context::is_full_class(expr type) {
     type = whnf(type);
     if (is_pi(type)) {
-        return is_full_class(instantiate(binding_body(type), mk_tmp_local(binding_domain(type))));
+        return is_full_class(instantiate(binding_body(type), mk_tmp_local_from_binding(type)));
     } else {
         expr f = get_app_fn(type);
         if (!is_constant(f))
@@ -1341,7 +1341,7 @@ bool type_context::try_instance(ci_stack_entry const & e, expr const & inst, exp
             mvar_type = whnf(mvar_type);
             if (!is_pi(mvar_type))
                 break;
-            expr local  = mk_tmp_local(binding_domain(mvar_type));
+            expr local  = mk_tmp_local_from_binding(mvar_type);
             locals.push_back(local);
             mvar_type = instantiate(binding_body(mvar_type), local);
         }
@@ -1687,6 +1687,13 @@ expr default_type_context::mk_tmp_local(expr const & type, binder_info const & b
     return lean::mk_local(n, n, type, bi);
 }
 
+expr default_type_context::mk_tmp_local(name const & pp_n, expr const & type, binder_info const & bi) {
+    unsigned idx = m_next_local_idx;
+    m_next_local_idx++;
+    name n(*g_prefix, idx);
+    return lean::mk_local(n, pp_n, type, bi);
+}
+
 bool default_type_context::is_tmp_local(expr const & e) const {
     if (!is_local(e))
         return false;

src/library/type_context.h

@@ -223,6 +223,15 @@ public:
     /** \brief Create a temporary local constant */
     virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info()) = 0;
 
+    /** \brief Create a temporary local constant using the given pretty print name.
+        The pretty printing name has not semantic significance. */
+    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info()) = 0;
+
+    /** \brief Create a temporary local constant based on the domain of the given binding (lambda/Pi) expression */
+    expr mk_tmp_local_from_binding(expr const & b) {
+        return mk_tmp_local(binding_name(b), binding_domain(b), binding_info(b));
+    }
+
     /** \brief Return true if \c e was created using \c mk_tmp_local */
     virtual bool is_tmp_local(expr const & e) const = 0;
 
@@ -419,7 +428,8 @@ public:
     virtual ~default_type_context();
     virtual bool is_extra_opaque(name const & n) const { return m_not_reducible_pred(n); }
     virtual bool ignore_universe_def_eq(level const & l1, level const & l2) const;
-    virtual expr mk_tmp_local(expr const & type, binder_info const & bi);
+    virtual expr mk_tmp_local(expr const & type, binder_info const & bi = binder_info());
+    virtual expr mk_tmp_local(name const & pp_name, expr const & type, binder_info const & bi = binder_info());
     virtual bool is_tmp_local(expr const & e) const;
     virtual bool is_uvar(level const & l) const;
     virtual bool is_mvar(expr const & e) const;

tests/lean/binder_overload.lean.expected.out

@@ -1,7 +1,7 @@
 {x : ℕ ∈ S | x > 0} : set ℕ
 {x : ℕ ∈ s | x > 0} : finset ℕ
 @set.sep.{1} nat (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0) S : set.{1} nat
-@finset.sep.{1} nat (λ (x x_1 : nat), nat.has_decidable_eq x x_1) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0)
+@finset.sep.{1} nat (λ (a b : nat), nat.has_decidable_eq a b) (λ (x : nat), @gt.{1} nat 11.source.to.has_lt x 0)
-  (λ (x : nat), nat.decidable_lt 0 x)
+  (λ (a : nat), nat.decidable_lt 0 a)
   s :
   finset.{1} nat

tests/lean/finset_induction_bug.lean.expected.out

@@ -22,12 +22,12 @@ l' : list A,
 IH : ∀ (x : @nodup A l'), P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' x)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
-H3 : @eq (list A) (@list.insert A (λ (x x_1 : A), h x x_1) a l') (@cons A a l'),
+H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
 P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
 H4 :
   P
-    (@insert A (λ (x x_1 : A), h x x_1) a
+    (@insert A (λ (a b : A), h a b) a
        (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
 ⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:30:45: error: don't know how to synthesize placeholder
@@ -44,12 +44,12 @@ l' : list A,
 IH : ∀ (x : @nodup A l'), P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' x)),
 nodup_al' : @nodup A (@cons A a l'),
 anl' : not (@list.mem A a l'),
-H3 : @eq (list A) (@list.insert A (λ (x x_1 : A), h x x_1) a l') (@cons A a l'),
+H3 : @eq (list A) (@list.insert A (λ (a b : A), h a b) a l') (@cons A a l'),
 nodup_l' : @nodup A l',
 P_l' : P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')),
 H4 :
   P
-    (@insert A (λ (x x_1 : A), h x x_1) a
+    (@insert A (λ (a b : A), h a b) a
        (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) l' nodup_l')))
 ⊢ P (@quot.mk (nodup_list A) (nodup_list_setoid A) (@subtype.tag (list A) (@nodup A) (@cons A a l') nodup_al'))
 finset_induction_bug.lean:16:5: error: failed to add declaration 'finset.induction₂' to environment, value has metavariables