From 0ceedbe69e80cebbc584eccb2d3d68174054c3b0 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 29 May 2015 15:49:10 -0700 Subject: [PATCH] fix(library/normalize): fixes #640 --- src/kernel/environment.h | 3 +++ src/kernel/hits/hits.cpp | 4 ++++ src/kernel/hits/hits.h | 1 + src/kernel/inductive/inductive.cpp | 4 ++++ src/kernel/inductive/inductive.h | 1 + src/kernel/normalizer_extension.cpp | 5 +++++ src/kernel/normalizer_extension.h | 1 + src/kernel/quotient/quotient.cpp | 4 ++++ src/kernel/quotient/quotient.h | 1 + src/library/normalize.cpp | 2 +- src/tests/kernel/environment.cpp | 1 + tests/lean/640.hlean | 26 ++++++++++++++++++++++++++ tests/lean/640.hlean.expected.out | 17 +++++++++++++++++ 13 files changed, 69 insertions(+), 1 deletion(-) create mode 100644 tests/lean/640.hlean create mode 100644 tests/lean/640.hlean.expected.out diff --git a/src/kernel/environment.h b/src/kernel/environment.h index a970cad061..bd3e586fe1 100644 --- a/src/kernel/environment.h +++ b/src/kernel/environment.h @@ -56,6 +56,7 @@ public: bool eta() const { return m_eta; } bool impredicative() const { return m_impredicative; } normalizer_extension const & norm_ext() const { return *(m_norm_ext.get()); } + bool is_recursor(environment const & env, name const & n) const { return m_norm_ext->is_recursor(env, n); } }; class environment_extension { @@ -134,6 +135,8 @@ public: /** \brief Return true iff the environment assumes Eta-reduction */ bool eta() const { return m_header->eta(); } + bool is_recursor(name const & n) const { return m_header->is_recursor(*this, n); } + /** \brief Return true iff the environment treats universe level 0 as an impredicative Prop */ bool impredicative() const { return m_header->impredicative(); } diff --git a/src/kernel/hits/hits.cpp b/src/kernel/hits/hits.cpp index 2bfbbb3e0c..ed50b742f7 100644 --- a/src/kernel/hits/hits.cpp +++ b/src/kernel/hits/hits.cpp @@ -129,6 +129,10 @@ bool hits_normalizer_extension::supports(name const & feature) const { return feature == *g_hits_extension; } +bool hits_normalizer_extension::is_recursor(environment const &, name const & n) const { + return n == *g_trunc_rec || n == *g_type_quotient_rec; +} + bool is_hits_decl(environment const & env, name const & n) { if (!get_extension(env).m_initialized) return false; diff --git a/src/kernel/hits/hits.h b/src/kernel/hits/hits.h index 38f23d61a3..05eecbcfa8 100644 --- a/src/kernel/hits/hits.h +++ b/src/kernel/hits/hits.h @@ -17,6 +17,7 @@ public: virtual optional> operator()(expr const & e, extension_context & ctx) const; virtual optional is_stuck(expr const & e, extension_context & ctx) const; virtual bool supports(name const & feature) const; + virtual bool is_recursor(environment const & env, name const & n) const; }; /** \brief The following function must be invoked to register the builtin HITs computation rules in the kernel. */ diff --git a/src/kernel/inductive/inductive.cpp b/src/kernel/inductive/inductive.cpp index d8daa683e7..01108161c9 100644 --- a/src/kernel/inductive/inductive.cpp +++ b/src/kernel/inductive/inductive.cpp @@ -953,6 +953,10 @@ auto inductive_normalizer_extension::operator()(expr const & e, extension_contex return some_ecs(r, cs); } +bool inductive_normalizer_extension::is_recursor(environment const & env, name const & n) const { + return static_cast(is_elim_rule(env, n)); +} + template optional is_elim_meta_app_core(Ctx & ctx, expr const & e) { inductive_env_ext const & ext = get_extension(ctx.env()); diff --git a/src/kernel/inductive/inductive.h b/src/kernel/inductive/inductive.h index cccc7f1e73..dc9323c407 100644 --- a/src/kernel/inductive/inductive.h +++ b/src/kernel/inductive/inductive.h @@ -19,6 +19,7 @@ public: virtual optional> operator()(expr const & e, extension_context & ctx) const; virtual optional is_stuck(expr const & e, extension_context & ctx) const; virtual bool supports(name const & feature) const; + virtual bool is_recursor(environment const & env, name const & n) const; }; /** \brief Introduction rule */ diff --git a/src/kernel/normalizer_extension.cpp b/src/kernel/normalizer_extension.cpp index c79f9594d1..a095b36782 100644 --- a/src/kernel/normalizer_extension.cpp +++ b/src/kernel/normalizer_extension.cpp @@ -14,6 +14,7 @@ public: } virtual optional is_stuck(expr const &, extension_context &) const { return none_expr(); } virtual bool supports(name const &) const { return false; } + virtual bool is_recursor(environment const &, name const &) const { return false; } }; std::unique_ptr mk_id_normalizer_extension() { @@ -44,6 +45,10 @@ public: virtual bool supports(name const & feature) const { return m_ext1->supports(feature) || m_ext2->supports(feature); } + + virtual bool is_recursor(environment const & env, name const & n) const { + return m_ext1->is_recursor(env, n) || m_ext2->is_recursor(env, n); + } }; std::unique_ptr compose(std::unique_ptr && ext1, std::unique_ptr && ext2) { diff --git a/src/kernel/normalizer_extension.h b/src/kernel/normalizer_extension.h index 6538258cf6..92b388e2fe 100644 --- a/src/kernel/normalizer_extension.h +++ b/src/kernel/normalizer_extension.h @@ -25,6 +25,7 @@ public: /** \brief Return true iff the extension supports a feature with the given name, this method is only used for sanity checking. */ virtual bool supports(name const & feature) const = 0; + virtual bool is_recursor(environment const & env, name const & n) const = 0; }; inline optional> none_ecs() { return optional>(); } diff --git a/src/kernel/quotient/quotient.cpp b/src/kernel/quotient/quotient.cpp index 5983a9e7eb..a0382b8af4 100644 --- a/src/kernel/quotient/quotient.cpp +++ b/src/kernel/quotient/quotient.cpp @@ -122,6 +122,10 @@ bool quotient_normalizer_extension::supports(name const & feature) const { return feature == *g_quotient_extension; } +bool quotient_normalizer_extension::is_recursor(environment const &, name const & n) const { + return n == *g_quotient_lift || n == *g_quotient_ind; +} + bool is_quotient_decl(environment const & env, name const & n) { if (!get_extension(env).m_initialized) return false; diff --git a/src/kernel/quotient/quotient.h b/src/kernel/quotient/quotient.h index 0d1dce473f..fa885e7c80 100644 --- a/src/kernel/quotient/quotient.h +++ b/src/kernel/quotient/quotient.h @@ -15,6 +15,7 @@ public: virtual optional> operator()(expr const & e, extension_context & ctx) const; virtual optional is_stuck(expr const & e, extension_context & ctx) const; virtual bool supports(name const & feature) const; + virtual bool is_recursor(environment const & env, name const & n) const; }; /** \brief The following function must be invoked to register the quotient type computation rules in the kernel. */ diff --git a/src/library/normalize.cpp b/src/library/normalize.cpp index f8d750dd80..7fdc589774 100644 --- a/src/library/normalize.cpp +++ b/src/library/normalize.cpp @@ -282,7 +282,7 @@ class normalize_fn { if (!modified) return e; expr r = mk_rev_app(f, args); - if (is_constant(f) && inductive::is_elim_rule(env(), const_name(f))) { + if (is_constant(f) && env().is_recursor(const_name(f))) { return normalize(r); } else { return r; diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp index ddaaf77179..c021b21602 100644 --- a/src/tests/kernel/environment.cpp +++ b/src/tests/kernel/environment.cpp @@ -136,6 +136,7 @@ public: } virtual optional is_stuck(expr const &, extension_context &) const { return none_expr(); } virtual bool supports(name const &) const { return false; } + virtual bool is_recursor(environment const &, name const &) const { return false; } }; static void tst3() { diff --git a/tests/lean/640.hlean b/tests/lean/640.hlean new file mode 100644 index 0000000000..8cfc31f34f --- /dev/null +++ b/tests/lean/640.hlean @@ -0,0 +1,26 @@ +import hit.type_quotient + +open type_quotient eq sum + + constants {A : Type} (R : A → A → Type) + + local abbreviation C := type_quotient R + + definition f [unfold-c 2] (a : A) (x : unit) : C := + !class_of a + + inductive S : C → C → Type := + | Rmk {} : Π(a : A) (x : unit), S (f a x) (!class_of a) + + set_option pp.notation false + set_option pp.beta false + + definition rec {P : type_quotient S → Type} (x : type_quotient S) : P x := + begin + induction x with c c c' H, + { induction c with b b b' H, + { apply sorry}, + { apply sorry}}, + { cases H, esimp, induction x, + { state, esimp, state, esimp, state, apply sorry}}, + end diff --git a/tests/lean/640.hlean.expected.out b/tests/lean/640.hlean.expected.out new file mode 100644 index 0000000000..c82f5c9bab --- /dev/null +++ b/tests/lean/640.hlean.expected.out @@ -0,0 +1,17 @@ +640.hlean:25:8: proof state +P : type_quotient S → Type, +c c' : C, +a : A +⊢ pathover P (type_quotient.rec (λ (b : A), sorry) (λ (b b' : A) (H : R b b'), sorry) (f a unit.star)) + (eq_of_rel S (S.Rmk a unit.star)) + sorry +640.hlean:25:22: proof state +P : type_quotient S → Type, +c c' : C, +a : A +⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry +640.hlean:25:36: proof state +P : type_quotient S → Type, +c c' : C, +a : A +⊢ pathover P sorry (eq_of_rel S (S.Rmk a unit.star)) sorry