From 3cb8568fb5b243d46d58a3c5eb38c47a7d785593 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 12 Jul 2015 14:24:05 -0400
Subject: [PATCH] feat(library/simplifier): we can "rewrite" with transitive
 relations

The simplifier does not really need the relation to be an equivalence.
Transitivity is the main required property (we need to chain rewrites
together).
---
 src/library/simplifier/ceqv.cpp             | 18 +++++++++---------
 src/library/simplifier/ceqv.h               |  2 +-
 src/library/simplifier/rewrite_rule_set.cpp |  2 +-
 3 files changed, 11 insertions(+), 11 deletions(-)

diff --git a/src/library/simplifier/ceqv.cpp b/src/library/simplifier/ceqv.cpp
index 44254f2cc..6656f2747 100644
--- a/src/library/simplifier/ceqv.cpp
+++ b/src/library/simplifier/ceqv.cpp
@@ -31,10 +31,10 @@ class to_ceqvs_fn {
         return is_sort(m_tc.whnf(m_tc.infer(e).first).first);
     }
 
-    bool is_equivalence(expr const & e) {
+    bool is_transitive(expr const & e) {
         if (!is_app(e)) return false;
         expr const & fn = get_app_fn(e);
-        return is_constant(fn) && ::lean::is_equivalence(m_env, const_name(fn)) && is_type(e);
+        return is_constant(fn) && ::lean::is_trans_relation(m_env, const_name(fn)) && is_type(e);
     }
 
     list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
@@ -46,7 +46,7 @@ class to_ceqvs_fn {
 
     list<expr_pair> apply(expr const & e, expr const & H) {
         expr c, Hdec, A, arg1, arg2;
-        if (is_equivalence(e)) {
+        if (is_transitive(e)) {
             return mk_singleton(e, H);
         } else if (is_standard(m_env) && is_not(m_env, e, arg1)) {
             expr new_e = mk_iff(e, mk_false());
@@ -110,10 +110,10 @@ list<expr_pair> to_ceqvs(type_checker & tc, expr const & e, expr const & H) {
     return to_ceqvs_fn(tc)(e, H);
 }
 
-bool is_equivalence(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
+bool is_transitive(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
     buffer<expr> args;
     rel = get_app_args(e, args);
-    if (!is_constant(rel) || !is_equivalence(env, const_name(rel)))
+    if (!is_constant(rel) || !is_trans_relation(env, const_name(rel)))
         return false;
     relation_info const * rel_info = get_relation_info(env, const_name(rel));
     if (!rel_info || rel_info->get_lhs_pos() >= args.size() || rel_info->get_rhs_pos() >= args.size())
@@ -123,9 +123,9 @@ bool is_equivalence(environment const & env, expr const & e, expr & rel, expr &
     return true;
 }
 
-bool is_equivalence(environment const & env, expr const & e, expr & lhs, expr & rhs) {
+bool is_transitive(environment const & env, expr const & e, expr & lhs, expr & rhs) {
     expr rel;
-    return is_equivalence(env, e, rel, lhs, rhs);
+    return is_transitive(env, e, rel, lhs, rhs);
 }
 
 bool is_ceqv(type_checker & tc, expr e) {
@@ -167,7 +167,7 @@ bool is_ceqv(type_checker & tc, expr e) {
         e = instantiate(binding_body(e), local);
     }
     expr lhs, rhs;
-    if (!is_equivalence(env, e, lhs, rhs))
+    if (!is_transitive(env, e, lhs, rhs))
         return false;
     // traverse lhs, and remove found variables from to_find
     for_each(lhs, visitor_fn);
@@ -230,7 +230,7 @@ bool is_permutation_ceqv(environment const & env, expr e) {
         num_args++;
     }
     expr lhs, rhs;
-    if (is_equivalence(env, e, lhs, rhs)) {
+    if (is_transitive(env, e, lhs, rhs)) {
         buffer<optional<unsigned>> permutation;
         permutation.resize(num_args);
         return is_permutation(lhs, rhs, 0, permutation);
diff --git a/src/library/simplifier/ceqv.h b/src/library/simplifier/ceqv.h
index cac61d38b..81f161818 100644
--- a/src/library/simplifier/ceqv.h
+++ b/src/library/simplifier/ceqv.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/type_checker.h"
 
 namespace lean {
-bool is_equivalence(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs);
+bool is_transitive(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs);
 /** \brief Given (H : e), return a list of (h_i : e_i) where e_i can be viewed as
     a "conditional" rewriting rule. Any equivalence relation registered using
     the relation_manager is considered.
diff --git a/src/library/simplifier/rewrite_rule_set.cpp b/src/library/simplifier/rewrite_rule_set.cpp
index b29ed8ac2..a4565c43e 100644
--- a/src/library/simplifier/rewrite_rule_set.cpp
+++ b/src/library/simplifier/rewrite_rule_set.cpp
@@ -117,7 +117,7 @@ rewrite_rule_sets add_core(type_checker & tc, rewrite_rule_sets const & s,
             new_e = instantiate(binding_body(new_e), mvar);
         }
         expr rel, lhs, rhs;
-        if (is_equivalence(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
+        if (is_transitive(env, new_e, rel, lhs, rhs) && is_constant(rel)) {
             new_s.insert(const_name(rel), rewrite_rule(id, univ_metas, to_list(metas), lhs, rhs, new_h, is_perm));
         }
     }