feat(library/simplifier/ceqv): add to_ceqv procedure

src/library/constants.cpp

@@ -33,7 +33,11 @@ name const * g_heq_refl = nullptr;
 name const * g_heq_to_eq = nullptr;
 name const * g_iff = nullptr;
 name const * g_iff_refl = nullptr;
+name const * g_iff_false_intro = nullptr;
+name const * g_iff_true_intro = nullptr;
 name const * g_implies = nullptr;
+name const * g_implies_of_if_pos = nullptr;
+name const * g_implies_of_if_neg = nullptr;
 name const * g_ite = nullptr;
 name const * g_lift = nullptr;
 name const * g_lift_down = nullptr;
@@ -165,7 +169,11 @@ void initialize_constants() {
     g_heq_to_eq = new name{"heq", "to_eq"};
     g_iff = new name{"iff"};
     g_iff_refl = new name{"iff", "refl"};
+    g_iff_false_intro = new name{"iff_false_intro"};
+    g_iff_true_intro = new name{"iff_true_intro"};
     g_implies = new name{"implies"};
+    g_implies_of_if_pos = new name{"implies_of_if_pos"};
+    g_implies_of_if_neg = new name{"implies_of_if_neg"};
     g_ite = new name{"ite"};
     g_lift = new name{"lift"};
     g_lift_down = new name{"lift", "down"};
@@ -298,7 +306,11 @@ void finalize_constants() {
     delete g_heq_to_eq;
     delete g_iff;
     delete g_iff_refl;
+    delete g_iff_false_intro;
+    delete g_iff_true_intro;
     delete g_implies;
+    delete g_implies_of_if_pos;
+    delete g_implies_of_if_neg;
     delete g_ite;
     delete g_lift;
     delete g_lift_down;
@@ -430,7 +442,11 @@ name const & get_heq_refl_name() { return *g_heq_refl; }
 name const & get_heq_to_eq_name() { return *g_heq_to_eq; }
 name const & get_iff_name() { return *g_iff; }
 name const & get_iff_refl_name() { return *g_iff_refl; }
+name const & get_iff_false_intro_name() { return *g_iff_false_intro; }
+name const & get_iff_true_intro_name() { return *g_iff_true_intro; }
 name const & get_implies_name() { return *g_implies; }
+name const & get_implies_of_if_pos_name() { return *g_implies_of_if_pos; }
+name const & get_implies_of_if_neg_name() { return *g_implies_of_if_neg; }
 name const & get_ite_name() { return *g_ite; }
 name const & get_lift_name() { return *g_lift; }
 name const & get_lift_down_name() { return *g_lift_down; }

src/library/constants.h

@@ -35,7 +35,11 @@ name const & get_heq_refl_name();
 name const & get_heq_to_eq_name();
 name const & get_iff_name();
 name const & get_iff_refl_name();
+name const & get_iff_false_intro_name();
+name const & get_iff_true_intro_name();
 name const & get_implies_name();
+name const & get_implies_of_if_pos_name();
+name const & get_implies_of_if_neg_name();
 name const & get_ite_name();
 name const & get_lift_name();
 name const & get_lift_down_name();

src/library/constants.txt

@@ -28,7 +28,11 @@ heq.refl
 heq.to_eq
 iff
 iff.refl
+iff_false_intro
+iff_true_intro
 implies
+implies_of_if_pos
+implies_of_if_neg
 ite
 lift
 lift.down

src/library/simplifier/ceqv.cpp

@@ -5,13 +5,111 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/type_checker.h"
+#include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
+#include "library/constants.h"
+#include "library/expr_pair.h"
 #include "library/util.h"
 #include "library/relation_manager.h"
 #include "library/occurs.h"
+#include "library/simplifier/ceqv.h"
 
 namespace lean {
+bool is_ceqv(type_checker & tc, expr e);
+
+/** \brief Auxiliary functional object for creating "conditional equations" */
+class to_ceqs_fn {
+    environment const &   m_env;
+    type_checker &        m_tc;
+
+    static list<expr_pair> mk_singleton(expr const & e, expr const & H) {
+        return list<expr_pair>(mk_pair(e, H));
+    }
+
+    bool is_type(expr const & e) {
+        return is_sort(m_tc.whnf(m_tc.infer(e).first).first);
+    }
+
+    bool is_equivalence(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);
+    }
+
+    list<expr_pair> lift(expr const & local, list<expr_pair> const & l) {
+        lean_assert(is_local(local));
+        return map(l, [&](expr_pair const & e_H) {
+                return mk_pair(Pi(local, e_H.first), Fun(local, e_H.second));
+            });
+    }
+
+    list<expr_pair> apply(expr const & e, expr const & H) {
+        expr c, Hdec, A, arg1, arg2;
+        if (is_equivalence(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());
+            expr new_H = mk_app(mk_constant(get_iff_false_intro_name()), arg1, H);
+            return mk_singleton(new_e, new_H);
+        } else if (is_standard(m_env) && is_and(e, arg1, arg2)) {
+            // TODO(Leo): we can extend this trick to any type that has only one constructor
+            expr H1 = mk_app(mk_constant(get_and_elim_left_name()), arg1, arg2, H);
+            expr H2 = mk_app(mk_constant(get_and_elim_right_name()), arg1, arg2, H);
+            auto r1 = apply(arg1, H1);
+            auto r2 = apply(arg2, H2);
+            return append(r1, r2);
+        } else if (is_pi(e)) {
+            expr local = mk_local(m_tc.mk_fresh_name(), binding_name(e), binding_domain(e), binding_info(e));
+            expr new_e = instantiate(binding_body(e), local);
+            expr new_H = mk_app(H, local);
+            auto r = apply(new_e, new_H);
+            unsigned len = length(r);
+            if (len == 0) {
+                return r;
+            } else if (len == 1 && head(r).first == new_e && head(r).second == new_H) {
+                return mk_singleton(e, H);
+            } else {
+                return lift(local, r);
+            }
+        } else if (is_standard(m_env) && is_ite(e, c, Hdec, A, arg1, arg2)) {
+            // TODO(Leo): support HoTT mode if users request
+            expr not_c = mk_not(m_tc, c);
+            expr Hc    = mk_local(m_tc.mk_fresh_name(), c);
+            expr Hnc   = mk_local(m_tc.mk_fresh_name(), not_c);
+            expr H1    = mk_app({mk_constant(get_implies_of_if_pos_name()),
+                                 c, arg1, arg2, Hdec, e, Hc});
+            expr H2    = mk_app({mk_constant(get_implies_of_if_neg_name()),
+                                 c, arg1, arg2, Hdec, e, Hnc});
+            auto r1    = lift(Hc, apply(arg1, H1));
+            auto r2    = lift(Hnc, apply(arg2, H2));
+            return append(r1, r2);
+        } else {
+            constraint_seq cs;
+            expr new_e = m_tc.whnf(e, cs);
+            if (new_e != e && !cs) {
+                return apply(new_e, H);
+            } else if (is_standard(m_env)) {
+                expr new_e = mk_iff(e, mk_true());
+                expr new_H = mk_app(mk_constant(get_iff_true_intro_name()), arg1, H);
+                return mk_singleton(new_e, new_H);
+            } else {
+                return list<expr_pair>();
+            }
+        }
+    }
+public:
+    to_ceqs_fn(type_checker & tc):m_env(tc.env()), m_tc(tc) {}
+
+    list<expr_pair> operator()(expr const & e, expr const & H) {
+        return filter(apply(e, H), [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); });
+    }
+};
+
+list<expr_pair> to_ceqs(type_checker & tc, expr const & e, expr const & H) {
+    return to_ceqs_fn(tc)(e, H);
+}
+
 bool is_equivalence(environment const & env, expr const & e, expr & rel, expr & lhs, expr & rhs) {
     buffer<expr> args;
     rel = get_app_args(e, args);
@@ -30,7 +128,7 @@ bool is_equivalence(environment const & env, expr const & e, expr & lhs, expr &
     return is_equivalence(env, e, rel, lhs, rhs);
 }
 
-bool is_ceqv(environment const & env, name_generator && ngen, expr e) {
+bool is_ceqv(type_checker & tc, expr e) {
     if (has_expr_metavar(e))
         return false;
     name_set to_find;
@@ -45,8 +143,8 @@ bool is_ceqv(environment const & env, name_generator && ngen, expr e) {
             return true;
         }
     };
+    environment const & env = tc.env();
     bool is_std = is_standard(env);
-    type_checker tc(env, ngen.mk_child());
     buffer<expr> hypotheses; // arguments that are propositions
     while (is_pi(e)) {
         if (!to_find.empty()) {
@@ -55,7 +153,7 @@ bool is_ceqv(environment const & env, name_generator && ngen, expr e) {
             // by matching the type.
             for_each(binding_domain(e), visitor_fn);
         }
-        expr local = mk_local(ngen.next(), binding_domain(e));
+        expr local = mk_local(tc.mk_fresh_name(), binding_domain(e));
         if (binding_info(e).is_inst_implicit()) {
             // If the argument can be instantiated by type class resolution, then
             // we don't need to find it in the lhs

src/library/simplifier/ceqv.h

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+#include "kernel/type_checker.h"
+
+namespace lean {
+/** \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.
+*/
+list<expr_pair> to_ceqs(type_checker & tc, expr const & e, expr const & H);
+bool is_ceqv(type_checker & tc, expr e);
+bool is_permutation_ceqv(environment const & env, expr e);
+}

src/library/util.cpp

@@ -306,6 +306,15 @@ bool is_not(environment const & env, expr const & e, expr & a) {
     }
 }
 
+expr mk_not(type_checker & tc, expr const & e) {
+    if (is_standard(tc.env())) {
+        return mk_app(mk_constant(get_not_name()), e);
+    } else {
+        level l = sort_level(tc.ensure_type(e).first);
+        return mk_app(mk_constant(get_not_name(), {l}), e);
+    }
+}
+
 expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & not_e) {
     level t_lvl  = sort_level(tc.ensure_type(t).first);
     expr  e_type = tc.infer(e).first;
@@ -364,6 +373,21 @@ expr mk_true_intro() {
     return *g_true_intro;
 }
 
+bool is_and(expr const & e, expr & arg1, expr & arg2) {
+    if (get_app_fn(e) == *g_and) {
+        buffer<expr> args; get_app_args(e, args);
+        if (args.size() == 2) {
+            arg1 = args[0];
+            arg2 = args[1];
+            return true;
+        } else {
+            return false;
+        }
+    } else {
+        return false;
+    }
+}
+
 expr mk_and(expr const & a, expr const & b) {
     return mk_app(*g_and, a, b);
 }
@@ -427,6 +451,22 @@ expr mk_pair(type_checker & tc, expr const & a, expr const & b, bool prop) {
 expr mk_pr1(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_left(tc, p) : mk_pr1(tc, p); }
 expr mk_pr2(type_checker & tc, expr const & p, bool prop) { return prop ? mk_and_elim_right(tc, p) : mk_pr2(tc, p); }
 
+bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f) {
+    expr const & fn = get_app_fn(e);
+    if (is_constant(fn) && const_name(fn) == get_ite_name()) {
+        buffer<expr> args;
+        get_app_args(e, args);
+        if (args.size() == 5) {
+            c = args[0]; H = args[1]; A = args[2]; t = args[3]; f = args[4];
+            return true;
+        } else {
+            return true;
+        }
+    } else {
+        return false;
+    }
+}
+
 bool is_iff(expr const & e) {
     expr const & fn = get_app_fn(e);
     return is_constant(fn) && const_name(fn) == get_iff_name();

src/library/util.h

@@ -111,6 +111,7 @@ expr instantiate_univ_param (expr const & e, name const & p, level const & l);
 
 expr mk_true();
 expr mk_true_intro();
+bool is_and(expr const & e, expr & arg1, expr & arg2);
 expr mk_and(expr const & a, expr const & b);
 expr mk_and_intro(type_checker & tc, expr const & Ha, expr const & Hb);
 expr mk_and_elim_left(type_checker & tc, expr const & H);
@@ -145,6 +146,7 @@ expr mk_false_rec(type_checker & tc, expr const & f, expr const & t);
 /** \brief Return true if \c e is of the form <tt>(not arg)</tt>, and store \c arg in \c a.
      Return false otherwise */
 bool is_not(environment const & env, expr const & e, expr & a);
+expr mk_not(type_checker & tc, expr const & e);
 
 /** \brief Create the term <tt>absurd e not_e : t</tt>. */
 expr mk_absurd(type_checker & tc, expr const & t, expr const & e, expr const & not_e);
@@ -163,6 +165,8 @@ bool is_eq_a_a(type_checker & tc, expr const & e);
 bool is_heq(expr const & e);
 bool is_heq(expr const & e, expr & A, expr & lhs, expr & B, expr & rhs);
 
+bool is_ite(expr const & e, expr & c, expr & H, expr & A, expr & t, expr & f);
+
 bool is_iff(expr const & e);
 expr mk_iff(expr const & lhs, expr const & rhs);
 expr mk_iff_refl(expr const & a);

tests/lean/hott/noc_list.hlean

@@ -1,3 +1,6 @@
+set_option pp.universes true
+check @not
+
 inductive list (A : Type) : Type :=
 | nil {} : list A
 | cons   : A → list A → list A