From d95c064a291adeef4129f76b5de5ec9c990ba3c4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 26 May 2015 17:19:27 -0700 Subject: [PATCH] feat(library/simplifier/ceqv): add to_ceqv procedure --- src/library/constants.cpp | 16 +++++ src/library/constants.h | 4 ++ src/library/constants.txt | 4 ++ src/library/simplifier/ceqv.cpp | 104 +++++++++++++++++++++++++++++++- src/library/simplifier/ceqv.h | 18 ++++++ src/library/util.cpp | 40 ++++++++++++ src/library/util.h | 4 ++ tests/lean/hott/noc_list.hlean | 3 + 8 files changed, 190 insertions(+), 3 deletions(-) create mode 100644 src/library/simplifier/ceqv.h diff --git a/src/library/constants.cpp b/src/library/constants.cpp index fb72afed9..b7b3c7332 100644 --- a/src/library/constants.cpp +++ b/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; } diff --git a/src/library/constants.h b/src/library/constants.h index e90b95472..a628fc32c 100644 --- a/src/library/constants.h +++ b/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(); diff --git a/src/library/constants.txt b/src/library/constants.txt index dad6536cf..50d25426e 100644 --- a/src/library/constants.txt +++ b/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 diff --git a/src/library/simplifier/ceqv.cpp b/src/library/simplifier/ceqv.cpp index 20c55d133..fe831351f 100644 --- a/src/library/simplifier/ceqv.cpp +++ b/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 mk_singleton(expr const & e, expr const & H) { + return list(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 lift(expr const & local, list 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 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(); + } + } + } +public: + to_ceqs_fn(type_checker & tc):m_env(tc.env()), m_tc(tc) {} + + list operator()(expr const & e, expr const & H) { + return filter(apply(e, H), [&](expr_pair const & p) { return is_ceqv(m_tc, p.first); }); + } +}; + +list 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 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 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 diff --git a/src/library/simplifier/ceqv.h b/src/library/simplifier/ceqv.h new file mode 100644 index 000000000..051a821ba --- /dev/null +++ b/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 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); +} diff --git a/src/library/util.cpp b/src/library/util.cpp index 2db6a6633..98cd020a2 100644 --- a/src/library/util.cpp +++ b/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 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 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(); diff --git a/src/library/util.h b/src/library/util.h index 51d312fe5..23e330d01 100644 --- a/src/library/util.h +++ b/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 (not arg), 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 absurd e not_e : t. */ 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); diff --git a/tests/lean/hott/noc_list.hlean b/tests/lean/hott/noc_list.hlean index be7ff50f8..8b7cc1b02 100644 --- a/tests/lean/hott/noc_list.hlean +++ b/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