From c73398a0b80406cdef10dbb4ed7e0f2a76ba1278 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jan 2014 16:05:57 -0800
Subject: [PATCH] refactor(library/simplifier): relax rule for conditional
 equalities
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

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        |   2 +-
 src/builtin/obj/kernel.olean   | Bin 24895 -> 24905 bytes
 src/library/simplifier/ceq.cpp |  43 ++++++++++++++++++++-------------
 tests/lua/ceq1.lua             |   2 +-
 4 files changed, 28 insertions(+), 19 deletions(-)

diff --git a/src/builtin/kernel.lean b/src/builtin/kernel.lean
index b8c1f7743..3a72115e8 100644
--- a/src/builtin/kernel.lean
+++ b/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
diff --git a/src/builtin/obj/kernel.olean b/src/builtin/obj/kernel.olean
index 09bb74a849a1e91325a196d59d676ecd19806a36..15c4f9d2ed73804dc9305569a579ed36ff56c686 100644
GIT binary patch
delta 26
ecmdmgi1Fkh#tjv0+^P&fpaUWTH&?P9ivj>{o(DVt

delta 16
YcmX?kh;jcR#tjv0j2xSr*^Wg406pXeq5uE@

diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp
index 3ed96a374..75dfd8f7c 100644
--- a/src/library/simplifier/ceq.cpp
+++ b/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) {
-                if (is_var(e)) {
-                    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();
+        for_each(lhs, visitor_fn);
+        return std::find(found_args.begin(), found_args.end(), false) == found_args.end();
     } else {
         return false;
     }
diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua
index 3f9255959..dcedf3ca6 100644
--- a/tests/lua/ceq1.lua
+++ b/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)