fix(library/elaborator): missing condition

The elaborator was missing solutions because of the missing condition at is_simple_ho_match.

This commit also adds a new test that exposes the problem.

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

src/library/elaborator/elaborator.cpp

@@ -739,7 +739,7 @@ class elaborator::imp {
        \brief See \c process_simple_ho_match
     */
     bool is_simple_ho_match(context const & ctx, expr const & a, expr const & b, bool is_lhs, unification_constraint const & c) {
-        return is_meta_app(a) && are_args_vars(ctx, a) && closed(b) &&
+        return is_meta_app(a) && !has_local_context(arg(a, 0)) && are_args_vars(ctx, a) && closed(b) &&
             (is_eq(c) || (is_lhs && !is_actual_upper(b)) || (!is_lhs && !is_actual_lower(b)));
     }
 

tests/lean/exists4.lean

@@ -0,0 +1,16 @@
+Variable N : Type
+Variables a b c : N
+Variables P : N -> N -> N -> Bool
+Axiom H3 : P a b c
+
+Theorem T1 : exists x y z : N, P x y z := ExistsIntro::explicit N (fun x : N, exists y z : N, P x y z) a
+                                              (ExistsIntro::explicit N _ b
+                                                 (ExistsIntro::explicit N (fun z : N, P a b z) c H3))
+
+Theorem T2 : exists x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
+
+Theorem T3 : exists x y z : N, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H3))
+
+Theorem T4 (H : P a a b) : exists x y z, P x y z := ExistsIntro _ (ExistsIntro _ (ExistsIntro _ H))
+
+Show Environment 4

tests/lean/exists4.lean.expected.out

@@ -0,0 +1,25 @@
+  Set: pp::colors
+  Set: pp::unicode
+  Assumed: N
+  Assumed: a
+  Assumed: b
+  Assumed: c
+  Assumed: P
+  Assumed: H3
+  Proved: T1
+  Proved: T2
+  Proved: T3
+  Proved: T4
+Theorem T1 : ∃ x y z : N, P x y z :=
+    ExistsIntro::explicit
+        N
+        (λ x : N, ∃ y z : N, P x y z)
+        a
+        (ExistsIntro::explicit
+             N
+             (λ x : N, if ((λ x::1 : N, if (P a x x::1) ⊥ ⊤) == (λ x : N, ⊤)) ⊥ ⊤)
+             b
+             (ExistsIntro::explicit N (λ z : N, P a b z) c H3))
+Theorem T2 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
+Theorem T3 : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro b (ExistsIntro c H3))
+Theorem T4 (H : P a a b) : ∃ x y z : N, P x y z := ExistsIntro a (ExistsIntro a (ExistsIntro b H))