feat(elaborator): add option m_assume_injectivity for getting more concise solutions

We may miss solutions, but the solutions found are much more readable.
For example, without this option, for elaboration problem

Theorem Example4 (a b c d e : N) (H: (a = b ∧ b = e ∧ b = c) ∨ (a = d ∧ d = c)) : (h a c) = (h c a) :=
    DisjCases H
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1))
                   in CongrH AeqC (Symm AeqC))
              (fun H1 : _,
                   let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1)
                   in CongrH AeqC (Symm AeqC))

the elaborator generates

Theorem Example4 (a b c d e : N) (H : a = b ∧ b = e ∧ b = c ∨ a = d ∧ d = c) : (h a c) = (h c a) :=
    DisjCases
        H
        (λ H1 : if
               Bool
               (if Bool (a = b) (if Bool (if Bool (if Bool (b = e) (if Bool (b = c) ⊥ ⊤) ⊤) ⊥ ⊤) ⊥ ⊤) ⊤)
               ⊥
               ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 (Conjunct2 H1)) in CongrH AeqC (Symm AeqC))
        (λ H1 : if Bool (if Bool (a = d) (if Bool (d = c) ⊥ ⊤) ⊤) ⊥ ⊤,
           let AeqC := Trans (Conjunct1 H1) (Conjunct2 H1) in CongrH AeqC (Symm AeqC))

The solution is correct, but it is not very readable. The problem is that the elaborator expands the definitions of \/ and /\.

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

src/frontends/lean/frontend_elaborator.cpp

@@ -325,7 +325,14 @@ public:
             expr new_e_t = m_type_checker.infer_type(new_e, context(), &m_menv, m_ucs);
             m_ucs.push_back(mk_convertible_constraint(context(), new_e_t, new_t,
                                                       mk_def_type_match_justification(context(), n, e)));
+            // for (auto c : m_ucs) {
+            //    formatter fmt = mk_simple_formatter();
+            //    std::cout << c.pp(fmt, options(), nullptr, false) << "\n";
+            // }
             substitution s = elaborate_core();
+            // s.for_each([&](name const & n, expr const & v) {
+            //        std::cout << n << " --> " << v << "\n";
+            //    });
             return mk_pair(instantiate_metavars(new_t, s), instantiate_metavars(new_e, s));
         } else {
             return mk_pair(new_t, new_e);

src/kernel/type_checker.cpp

@@ -244,7 +244,7 @@ class type_checker::imp {
         if (is_convertible_core(new_given, new_expected))
             return true;
         if (m_menv && (has_metavar(new_given) || has_metavar(new_expected))) {
-            m_uc->push_back(mk_convertible_constraint(ctx, new_given, new_expected, mk_justification()));
+            m_uc->push_back(mk_convertible_constraint(ctx, given, expected, mk_justification()));
             return true;
         }
         return false;

src/library/elaborator/elaborator.cpp

@@ -149,10 +149,12 @@ class elaborator::imp {
     // options
     bool                                     m_use_justifications;
     bool                                     m_use_normalizer;
+    bool                                     m_assume_injectivity;
 
     void set_options(options const &) {
         m_use_justifications = true;
         m_use_normalizer     = true;
+        m_assume_injectivity = true;
     }
 
     void reset_quota() {
@@ -1054,8 +1056,21 @@ class elaborator::imp {
             return true;
         }
 
+        if (m_assume_injectivity && is_app(a) && is_app(b) && num_args(a) == num_args(b) && arg(a, 0) == arg(b, 0)) {
+            // If m_assume_injectivity is true, we apply the following rule
+            // ctx |- (f a1 a2) == (f b1 b2)
+            // ===>
+            // ctx |- a1 == b1
+            // ctx |- a2 == b2
+            justification new_jst(new destruct_justification(c));
+            for (unsigned i = 1; i < num_args(a); i++)
+                push_front(mk_eq_constraint(ctx, arg(a, i), arg(b, i), new_jst));
+            return true;
+        }
+
         status r;
-        bool allow_assignment = eq; // at this point, we only assign metavariables if the constraint is an equational constraint.
+        // At this point, we only assign metavariables if the constraint is an equational constraint.
+        bool allow_assignment = eq;
         r = process_metavar(c, a, b, true, allow_assignment);
         if (r != Continue) { return r == Processed; }
         r = process_metavar(c, b, a, false, allow_assignment);