From c651d3ea2dd141d6900de9382c8497414941295c Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 15 Jan 2014 12:05:14 -0800
Subject: [PATCH] feat(library/simplifier): filter out propositions that cannot
 be used as conditional equations

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/library/simplifier/ceq.cpp | 46 +++++++++++++++++++++++++++++++++-
 src/library/simplifier/ceq.h   | 17 +++++++++++++
 tests/lua/ceq1.lua             | 13 ++++------
 3 files changed, 67 insertions(+), 9 deletions(-)

diff --git a/src/library/simplifier/ceq.cpp b/src/library/simplifier/ceq.cpp
index 9d91d4049..e7d957a0b 100644
--- a/src/library/simplifier/ceq.cpp
+++ b/src/library/simplifier/ceq.cpp
@@ -7,13 +7,17 @@ Author: Leonardo de Moura
 #include "util/list_fn.h"
 #include "kernel/builtin.h"
 #include "kernel/free_vars.h"
+#include "kernel/for_each_fn.h"
 #include "library/expr_pair.h"
 #include "library/ite.h"
 #include "library/kernel_bindings.h"
+#include "library/eq_heq.h"
 
 namespace lean {
 static name g_Hc("Hc"); // auxiliary name for if-then-else
 
+bool is_ceq(ro_environment const & env, expr e);
+
 /**
    \brief Auxiliary functional object for creating "conditional equations"
 */
@@ -96,7 +100,7 @@ public:
     to_ceqs_fn(ro_environment const & env):m_env(env), m_idx(0) {}
 
     list<expr_pair> operator()(expr const & e, expr const & H) {
-        return apply(e, H);
+        return filter(apply(e, H), [&](expr_pair const & p) { return is_ceq(m_env, p.first); });
     }
 };
 
@@ -104,6 +108,39 @@ list<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const &
     return to_ceqs_fn(env)(e, H);
 }
 
+bool is_ceq(ro_environment const & env, expr e) {
+    buffer<bool> in_lhs;
+    context ctx;
+    while (is_pi(e)) {
+        // 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));
+        ctx = extend(ctx, abst_name(e), abst_domain(e));
+        e = abst_body(e);
+    }
+    if (is_eq_heq(e)) {
+        auto lhs_rhs = eq_heq_args(e);
+        // traverse lhs, and mark all variables that occur there in is_lhs.
+        for_each(lhs_rhs.first, [&](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();
+    } else {
+        return false;
+    }
+}
+
 static int to_ceqs(lua_State * L) {
     ro_shared_environment env(L, 1);
     auto r = to_ceqs(env, to_expr(L, 2), to_expr(L, 3));
@@ -121,7 +158,14 @@ static int to_ceqs(lua_State * L) {
     return 1;
 }
 
+static int is_ceq(lua_State * L) {
+    ro_shared_environment env(L, 1);
+    lua_pushboolean(L, is_ceq(env, to_expr(L, 2)));
+    return 1;
+}
+
 void open_ceq(lua_State * L) {
     SET_GLOBAL_FUN(to_ceqs, "to_ceqs");
+    SET_GLOBAL_FUN(is_ceq,  "is_ceq");
 }
 }
diff --git a/src/library/simplifier/ceq.h b/src/library/simplifier/ceq.h
index 64d5ff3f6..c2c040feb 100644
--- a/src/library/simplifier/ceq.h
+++ b/src/library/simplifier/ceq.h
@@ -21,8 +21,25 @@ namespace lean {
    [forall x : A, P]    --->   forall x : A, [P]
 
    P                    --->   P = true   (if none of the rules above apply and P is not an equality)
+
+   \remark if the left-hand-side of an equation does not contain all variables, then it is
+   discarded. That is, all elements in the resultant list satisfy the predicate \c is_ceq.
 */
 list<expr_pair> to_ceqs(ro_environment const & env, expr const & e, expr const & H);
+/**
+   \brief Return true iff \c e is a conditional equation.
+
+   A conditional equation ceq has the form
+   <code>
+         ceq := (forall x : A, ceq)
+             |  lhs = rhs
+             |  lhs == rhs
+   </code>
+
+   Moreover, for <tt>(forall x : A, ceq)</tt>, the variable x must occur in the \c ceq left-hand-size
+   when \c A is not a proposition.
+*/
+bool is_ceq(ro_environment const & env, expr e);
 void open_ceq(lua_State * L);
 }
 
diff --git a/tests/lua/ceq1.lua b/tests/lua/ceq1.lua
index 6a319428a..e08a1be0b 100644
--- a/tests/lua/ceq1.lua
+++ b/tests/lua/ceq1.lua
@@ -1,17 +1,10 @@
 local env  = get_environment()
 
-function is_ceq(e)
-   while e:is_pi() do
-      _, _, e = e:fields()
-   end
-   return e:is_eq() or e:is_heq()
-end
-
 function show_ceqs(ceqs)
    for i = 1, #ceqs do
       print(ceqs[i][1], ceqs[i][2])
       env:type_check(ceqs[i][2])
-      assert(is_ceq(ceqs[i][1]))
+      assert(is_ceq(env, ceqs[i][1]))
    end
 end
 
@@ -29,9 +22,13 @@ parse_lean_cmds([[
    axiom Ax2 : forall x : Nat, x < 0 -> f (f x) = x
    variable g : Nat -> Nat -> Nat
    axiom Ax3 : forall x : Nat, not (x = 1) -> if (x < 0) then (g x x = 0) else (g x x < 0 /\ g x 0 = 1 /\ g 0 x = 2)
+   axiom Ax4 : forall x y : Nat, f x = x
+   axiom Ax5 : forall x y : Nat, f x = y /\ g x y = x
 ]])
 
 test_ceq("Ax1", 2)
 test_ceq("Ax2", 1)
 test_ceq("Ax3", 4)
+test_ceq("Ax4", 0)
+test_ceq("Ax5", 1)