feat(frontends/lean/frontend_elaborator): use is_convertible to minimize number of coercions

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/frontends/lean/frontend_elaborator.cpp

@@ -172,6 +172,14 @@ class frontend_elaborator::imp {
             }
         }
 
+        bool is_convertible(expr const & from, expr const & to) {
+            try {
+                return m_ref.m_type_checker.is_convertible(from, to);
+            } catch (exception &) {
+                return false;
+            }
+        }
+
         /**
            \brief Make sure f_t is a Pi, if it is not, then return none_expr()
         */
@@ -363,7 +371,7 @@ class frontend_elaborator::imp {
                             new_a = add_coercion_mvar_app(coercions, new_a, *new_a_t, ctx, a);
                         } else {
                             expr expected = abst_domain(*f_t);
-                            if (expected != *new_a_t) {
+                            if (!is_convertible(*new_a_t, expected)) {
                                 optional<expr> c = find_coercion(coercions, expected);
                                 if (c) {
                                     new_a = mk_app(*c, new_a); // apply coercion

tests/lean/norm_tac.lean

@@ -1,8 +1,11 @@
 SetOption pp::implicit true
+SetOption pp::coercion true
+SetOption pp::notation false
 Variable vector (A : Type) (sz : Nat) : Type
 Variable read {A : Type} {sz : Nat} (v : vector A sz) (i : Nat) (H : i < sz) : A
 Variable V1 : vector Int 10
 Definition D := read V1 1 (by trivial_tac)
+Show Environment 1
 Variable b : Bool
 Definition a := b
 Theorem T : b => a := (by (** imp_tac() .. normalize_tac() .. assumption_tac() **))

tests/lean/norm_tac.lean.expected.out

@@ -1,10 +1,13 @@
   Set: pp::colors
   Set: pp::unicode
   Set: lean::pp::implicit
+  Set: lean::pp::coercion
+  Set: lean::pp::notation
   Assumed: vector
   Assumed: read
   Assumed: V1
   Defined: D
+Definition D : ℤ := @read ℤ 10 V1 1 Trivial
   Assumed: b
   Defined: a
   Proved: T