refactor(library/simplifier): relax rule for conditional equalities

The idea is to support conditional equations where the left-hand-side does not contain all theorem arguments, but the missing arguments can be inferred using type inference.
For example, we will be able to have the eta theorem as rewrite rule:

theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
:= funext (λ x : A, refl (f x))

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

src/builtin/kernel.lean

@@ -68,7 +68,7 @@ theorem substp {A : TypeU} {a b : A} (P : A → Bool) (H1 : P a) (H2 : a == b) :
 theorem not_intro {a : Bool} (H : a → false) : ¬ a
 := H
 
-theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) == f
+theorem eta {A : TypeU} {B : A → TypeU} (f : ∀ x : A, B x) : (λ x : A, f x) = f
 := funext (λ x : A, refl (f x))
 
 theorem trivial : true

src/library/simplifier/ceq.cpp

@@ -115,33 +115,42 @@ list<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const &
 }
 
 bool is_ceq(ro_environment const & env, expr e) {
-    buffer<bool> in_lhs;
+    buffer<bool> found_args;
+    // Define a procedure for marking arguments found.
+    auto visitor_fn = [&](expr const & e, unsigned offset) {
+        if (is_var(e)) {
+            unsigned vidx = var_idx(e);
+            if (vidx >= offset) {
+                vidx -= offset;
+                if (vidx >= found_args.size()) {
+                    // it is a free variable
+                } else {
+                    found_args[found_args.size() - vidx - 1] = true;
+                }
+            }
+        }
+        return true;
+    };
+
     context ctx;
     while (is_pi(e)) {
+        if (!found_args.empty()) {
+            // Support for dependent types.
+            // We may find the instantiation for the previous variables
+            // by matching the type.
+            for_each(abst_domain(e), visitor_fn);
+        }
         // If a variable is a proposition, than if doesn't need to occurr in the lhs.
         // So, we mark it as true.
-        in_lhs.push_back(env->is_proposition(abst_domain(e), ctx));
+        found_args.push_back(env->is_proposition(abst_domain(e), ctx));
         ctx = extend(ctx, abst_name(e), abst_domain(e));
         e = abst_body(e);
     }
     if (is_eq(e)) {
         expr lhs = arg(e, 2);
         // traverse lhs, and mark all variables that occur there in is_lhs.
-        for_each(lhs, [&](expr const & e, unsigned offset) {
+        for_each(lhs, visitor_fn);
-                if (is_var(e)) {
+        return std::find(found_args.begin(), found_args.end(), false) == found_args.end();
-                    unsigned vidx = var_idx(e);
-                    if (vidx >= offset) {
-                        vidx -= offset;
-                        if (vidx >= in_lhs.size()) {
-                            // it is a free variable
-                        } else {
-                            in_lhs[in_lhs.size() - vidx - 1] = true;
-                        }
-                    }
-                }
-                return true;
-            });
-        return std::find(in_lhs.begin(), in_lhs.end(), false) == in_lhs.end();
     } else {
         return false;
     }

tests/lua/ceq1.lua

@@ -34,7 +34,7 @@ test_ceq("Ax3", 4)
 test_ceq("Ax4", 0)
 test_ceq("Ax5", 1)
 test_ceq("Ax6", 1)
--- test_ceq("eta", 1)
+test_ceq("eta", 1)
 test_ceq("not_not_eq", 1)
 test_ceq("or_comm", 1)
 test_ceq("or_assoc", 1)