feat(library/reducible): remove [quasireducible] annotation

hott/algebra/category/constructions/functor.hlean

@@ -256,7 +256,7 @@ namespace functor
     definition eq_of_iso_ob (η : F ≅ G) (c : C) : F c = G c :=
     by apply eq_of_iso; apply componentwise_iso; exact η
 
-    local attribute functor.to_fun_hom [quasireducible]
+    local attribute functor.to_fun_hom [reducible]
     definition eq_of_iso (η : F ≅ G) : F = G :=
     begin
     fapply functor_eq,

hott/algebra/category/iso.hlean

@@ -20,7 +20,7 @@ namespace iso
     (left_inverse  : inverse ∘ f = id)
     (right_inverse : f ∘ inverse = id)
 
-  attribute is_iso.inverse [quasireducible]
+  attribute is_iso.inverse [reducible]
 
   attribute is_iso [multiple_instances]
   open split_mono split_epi is_iso

hott/init/equiv.hlean

@@ -21,7 +21,7 @@ mk' ::
   (left_inv : Πa, inv (f a) = a)
   (adj : Πx, right_inv (f x) = ap f (left_inv x))
 
-attribute is_equiv.inv [quasireducible]
+attribute is_equiv.inv [reducible]
 
 -- A more bundled version of equivalence
 structure equiv (A B : Type) :=

library/theories/analysis/real_limit.lean

@@ -91,7 +91,7 @@ exists.intro x
      and.intro (and.left this) (lt_of_not_ge (and.right this)))
 
 section
-local attribute mem [quasireducible]
+local attribute mem [reducible]
 -- TODO: is there a better place to put this?
 proposition image_neg_eq (X : set ℝ) : (λ x, -x) ' X = {x | -x ∈ X} :=
 set.ext (take x, iff.intro

src/emacs/lean-syntax.el

@@ -53,7 +53,7 @@
   (--map (s-concat "[" it "]")
          '("persistent" "notation" "visible" "instance" "trans_instance"
            "class" "parsing_only" "coercion" "unfold_full" "constructor"
-           "reducible" "irreducible" "semireducible" "quasireducible" "wf"
+           "reducible" "irreducible" "semireducible" "wf"
            "whnf" "multiple_instances" "none" "decl" "declaration"
            "relation" "symm" "subst" "refl" "trans" "simp" "congr"
            "backward" "forward" "no_pattern" "begin_end" "tactic" "abbreviation"

src/frontends/lean/print_cmd.cpp

@@ -644,9 +644,6 @@ environment print_cmd(parser & p) {
     } else if (p.curr_is_token_or_id(get_reducible_tk())) {
         p.next();
         print_reducible_info(p, reducible_status::Reducible);
-    } else if (p.curr_is_token_or_id(get_quasireducible_tk())) {
-        p.next();
-        print_reducible_info(p, reducible_status::Quasireducible);
     } else if (p.curr_is_token_or_id(get_irreducible_tk())) {
         p.next();
         print_reducible_info(p, reducible_status::Irreducible);

src/frontends/lean/tokens.cpp

@@ -106,7 +106,6 @@ static name const * g_unfold_hints_bracket_tk = nullptr;
 static name const * g_unfold_hints_tk = nullptr;
 static name const * g_coercion_tk = nullptr;
 static name const * g_reducible_tk = nullptr;
-static name const * g_quasireducible_tk = nullptr;
 static name const * g_semireducible_tk = nullptr;
 static name const * g_irreducible_tk = nullptr;
 static name const * g_parsing_only_tk = nullptr;
@@ -257,7 +256,6 @@ void initialize_tokens() {
     g_unfold_hints_tk = new name{"unfold_hints"};
     g_coercion_tk = new name{"[coercion]"};
     g_reducible_tk = new name{"[reducible]"};
-    g_quasireducible_tk = new name{"[quasireducible]"};
     g_semireducible_tk = new name{"[semireducible]"};
     g_irreducible_tk = new name{"[irreducible]"};
     g_parsing_only_tk = new name{"[parsing_only]"};
@@ -409,7 +407,6 @@ void finalize_tokens() {
     delete g_unfold_hints_tk;
     delete g_coercion_tk;
     delete g_reducible_tk;
-    delete g_quasireducible_tk;
     delete g_semireducible_tk;
     delete g_irreducible_tk;
     delete g_parsing_only_tk;
@@ -560,7 +557,6 @@ name const & get_unfold_hints_bracket_tk() { return *g_unfold_hints_bracket_tk;
 name const & get_unfold_hints_tk() { return *g_unfold_hints_tk; }
 name const & get_coercion_tk() { return *g_coercion_tk; }
 name const & get_reducible_tk() { return *g_reducible_tk; }
-name const & get_quasireducible_tk() { return *g_quasireducible_tk; }
 name const & get_semireducible_tk() { return *g_semireducible_tk; }
 name const & get_irreducible_tk() { return *g_irreducible_tk; }
 name const & get_parsing_only_tk() { return *g_parsing_only_tk; }

src/frontends/lean/tokens.h

@@ -108,7 +108,6 @@ name const & get_unfold_hints_bracket_tk();
 name const & get_unfold_hints_tk();
 name const & get_coercion_tk();
 name const & get_reducible_tk();
-name const & get_quasireducible_tk();
 name const & get_semireducible_tk();
 name const & get_irreducible_tk();
 name const & get_parsing_only_tk();

src/frontends/lean/tokens.txt

@@ -101,7 +101,6 @@ unfold_hints_bracket [unfold_hints]
 unfold_hints unfold_hints
 coercion     [coercion]
 reducible    [reducible]
-quasireducible [quasireducible]
 semireducible [semireducible]
 irreducible  [irreducible]
 parsing_only [parsing_only]

src/library/blast/blast.cpp

@@ -608,8 +608,7 @@ public:
     blastenv(environment const & env, io_state const & ios, list<name> const & ls, list<name> const & ds):
         m_env(env), m_ios(ios), m_buffer_ios(ios),
         m_lemma_hints(to_name_set(ls)), m_unfold_hints(to_name_set(ds)),
-        // TODO(Leo): quasireducible in the following line is a temporary hack.
-        m_not_reducible_pred(mk_not_quasireducible_pred(env)),
+        m_not_reducible_pred(mk_not_reducible_pred(env)),
         m_class_pred(mk_class_pred(env)),
         m_instance_pred(mk_instance_pred(env)),
         m_is_relation_pred(mk_is_relation_pred(env)),

src/library/class.cpp

@@ -250,17 +250,17 @@ bool is_class(environment const & env, name const & c) {
 }
 
 type_checker_ptr mk_class_type_checker(environment const & env, bool conservative) {
-    auto pred = conservative ? mk_not_quasireducible_pred(env) : mk_irreducible_pred(env);
+    auto pred = conservative ? mk_not_reducible_pred(env) : mk_irreducible_pred(env);
     class_state s = class_ext::get_state(env);
     return mk_type_checker(env, [=](name const & n) {
             return s.m_instances.contains(n) || pred(n);
         });
 }
 
-static environment set_quasireducible_if_def(environment const & env, name const & n, name const & ns, bool persistent) {
+static environment set_reducible_if_def(environment const & env, name const & n, name const & ns, bool persistent) {
     declaration const & d = env.get(n);
     if (d.is_definition() && !d.is_theorem())
-        return set_reducible(env, n, reducible_status::Quasireducible, ns, persistent);
+        return set_reducible(env, n, reducible_status::Reducible, ns, persistent);
     else
         return env;
 }
@@ -279,7 +279,7 @@ environment add_instance(environment const & env, name const & n, unsigned prior
     check_is_class(env, c);
     environment new_env = class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority),
                                                ns, persistent);
-    return set_quasireducible_if_def(new_env, n, ns, persistent);
+    return set_reducible_if_def(new_env, n, ns, persistent);
 }
 
 static name * g_source = nullptr;
@@ -315,11 +315,11 @@ environment add_trans_instance(environment const & env, name const & n, unsigned
     environment new_env = new_env_insts.first;
     new_env = class_ext::add_entry(new_env, get_dummy_ios(),
                                    class_entry::mk_trans_inst(src_tgt.first, src_tgt.second, n, priority), ns, persistent);
-    new_env = set_quasireducible_if_def(new_env, n, ns, persistent);
+    new_env = set_reducible_if_def(new_env, n, ns, persistent);
     for (tc_edge const & edge : new_env_insts.second) {
         new_env = class_ext::add_entry(new_env, get_dummy_ios(),
                                        class_entry::mk_derived_trans_inst(edge.m_from, edge.m_to, edge.m_cnst), ns, persistent);
-        new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Quasireducible, ns, persistent);
+        new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Reducible, ns, persistent);
         new_env = add_protected(new_env, edge.m_cnst);
     }
     return new_env;

src/library/reducible.cpp

@@ -73,12 +73,6 @@ void initialize_reducible() {
                        },
                        [](environment const & env, name const & d) { return get_reducible_status(env, d) == reducible_status::Reducible; });
 
-    register_attribute("quasireducible", "quasireducible",
-                       [](environment const & env, io_state const &, name const & d, name const & ns, bool persistent) {
-                           return set_reducible(env, d, reducible_status::Quasireducible, ns, persistent);
-                       },
-                       [](environment const & env, name const & d) { return get_reducible_status(env, d) == reducible_status::Quasireducible; });
-
     register_attribute("semireducible", "semireducible",
                        [](environment const & env, io_state const &, name const & d, name const & ns, bool persistent) {
                            return set_reducible(env, d, reducible_status::Semireducible, ns, persistent);
@@ -91,11 +85,8 @@ void initialize_reducible() {
                        },
                        [](environment const & env, name const & d) { return get_reducible_status(env, d) == reducible_status::Irreducible; });
 
-    register_incompatible("reducible", "quasireducible");
     register_incompatible("reducible", "semireducible");
     register_incompatible("reducible", "irreducible");
-    register_incompatible("quasireducible", "semireducible");
-    register_incompatible("quasireducible", "irreducible");
     register_incompatible("semireducible", "irreducible");
 }
 
@@ -126,11 +117,6 @@ reducible_status get_reducible_status(environment const & env, name const & n) {
     return get_status(s, n);
 }
 
-bool is_at_least_quasireducible(environment const & env, name const & n) {
-    reducible_status r = get_reducible_status(env, n);
-    return r == reducible_status::Reducible || r == reducible_status::Quasireducible;
-}
-
 name_predicate mk_not_reducible_pred(environment const & env) {
     reducible_state m_state = reducible_ext::get_state(env);
     return [=](name const & n) { // NOLINT
@@ -138,14 +124,6 @@ name_predicate mk_not_reducible_pred(environment const & env) {
     };
 }
 
-name_predicate mk_not_quasireducible_pred(environment const & env) {
-    reducible_state m_state = reducible_ext::get_state(env);
-    return [=](name const & n) { // NOLINT
-        auto r = get_status(m_state, n);
-        return r != reducible_status::Reducible && r != reducible_status::Quasireducible;
-    };
-}
-
 name_predicate mk_irreducible_pred(environment const & env) {
     reducible_state m_state = reducible_ext::get_state(env);
     return [=](name const & n) { // NOLINT
@@ -157,8 +135,6 @@ type_checker_ptr mk_type_checker(environment const & env, reducible_behavior rb)
     switch (rb) {
     case UnfoldReducible:
         return mk_type_checker(env, mk_not_reducible_pred(env));
-    case UnfoldQuasireducible:
-        return mk_type_checker(env, mk_not_quasireducible_pred(env));
     case UnfoldSemireducible:
         return mk_type_checker(env, mk_irreducible_pred(env));
     }

src/library/reducible.h

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "library/util.h"
 
 namespace lean {
-enum class reducible_status { Reducible, Quasireducible, Semireducible, Irreducible };
+enum class reducible_status { Reducible, Semireducible, Irreducible };
 /** \brief Mark the definition named \c n as reducible or not.
 
     The method throws an exception if \c n is
@@ -25,19 +25,17 @@ environment set_reducible(environment const & env, name const & n, reducible_sta
 
 reducible_status get_reducible_status(environment const & env, name const & n);
 
-bool is_at_least_quasireducible(environment const & env, name const & n);
+inline bool is_reducible(environment const & env, name const & n) { return get_reducible_status(env, n) == reducible_status::Reducible; }
 
 /* \brief Execute the given function for each declaration explicitly marked with a reducibility annotation */
 void for_each_reducible(environment const & env, std::function<void(name const &, reducible_status)> const & fn);
 
 /** \brief Create a predicate that returns true for all non reducible constants in \c env */
 name_predicate mk_not_reducible_pred(environment const & env);
-/** \brief Create a predicate that returns true for all non reducible and non quasireducible constants in \c env */
-name_predicate mk_not_quasireducible_pred(environment const & env);
 /** \brief Create a predicate that returns true for irreducible constants  in \c env */
 name_predicate mk_irreducible_pred(environment const & env);
 
-enum reducible_behavior { UnfoldReducible, UnfoldQuasireducible, UnfoldSemireducible };
+enum reducible_behavior { UnfoldReducible, UnfoldSemireducible };
 
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
 type_checker_ptr mk_type_checker(environment const & env, reducible_behavior r = UnfoldSemireducible);

src/library/tactic/elaborate.cpp

@@ -55,7 +55,7 @@ optional<expr> elaborate_with_respect_to(environment const & env, io_state const
     } else {
         to_buffer(s.get_postponed(), cs);
         if (expected_type) {
-            auto tc      = mk_type_checker(env, conservative ? UnfoldQuasireducible : UnfoldSemireducible);
+            auto tc      = mk_type_checker(env, conservative ? UnfoldReducible : UnfoldSemireducible);
             auto e_t_cs  = tc->infer(new_e);
             expr t       = *expected_type;
             e_t_cs.second.linearize(cs);

src/library/tactic/rewrite_tactic.cpp

@@ -1594,7 +1594,7 @@ class rewrite_fn {
     }
 
     type_checker_ptr mk_tc(bool full) {
-        auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_quasireducible_pred(m_env);
+        auto aux_pred = full ? mk_irreducible_pred(m_env) : mk_not_reducible_pred(m_env);
         return mk_type_checker(m_env, [=](name const & n) {
                 return aux_pred(n) && !is_numeral_const_name(n);
             });

src/library/tmp_type_context.cpp

@@ -11,7 +11,6 @@ namespace lean {
 void tmp_type_context::init(environment const & env, reducible_behavior b) {
     switch (b) {
     case UnfoldReducible:      m_opaque_pred = mk_not_reducible_pred(env);      break;
-    case UnfoldQuasireducible: m_opaque_pred = mk_not_quasireducible_pred(env); break;
     case UnfoldSemireducible:  m_opaque_pred = mk_irreducible_pred(env);        break;
     }
 }

src/library/tmp_type_context.h

@@ -43,7 +43,7 @@ class tmp_type_context : public type_context {
     std::vector<scope>                m_scopes;
     void init(environment const & env, reducible_behavior b);
 public:
-    tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldQuasireducible);
+    tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldReducible);
     virtual ~tmp_type_context();
 
     /** \brief Reset the state: backtracking stack, indices and assignment. */

src/library/type_context.cpp

@@ -1932,7 +1932,7 @@ type_context::scope_pos_info::~scope_pos_info() {
 default_type_context::default_type_context(environment const & env, options const & o,
                                            list<expr> const & insts, bool multiple_instances):
     type_context(env, o, multiple_instances),
-    m_not_quasireducible_pred(mk_not_quasireducible_pred(env)) {
+    m_not_reducible_pred(mk_not_reducible_pred(env)) {
     m_ignore_if_zero = false;
     m_next_uvar_idx  = 0;
     m_next_mvar_idx  = 0;

src/library/type_context.h

@@ -533,7 +533,7 @@ public:
 class default_type_context : public type_context {
     typedef rb_map<unsigned, level, unsigned_cmp> uassignment;
     typedef rb_map<unsigned, expr,  unsigned_cmp> eassignment;
-    name_predicate            m_not_quasireducible_pred;
+    name_predicate            m_not_reducible_pred;
 
     struct assignment {
         uassignment m_uassignment;
@@ -570,7 +570,7 @@ public:
     default_type_context(environment const & env, options const & o,
                            list<expr> const & insts = list<expr>(), bool multiple_instances = false);
     virtual ~default_type_context();
-    virtual bool is_extra_opaque(name const & n) const { return m_not_quasireducible_pred(n); }
+    virtual bool is_extra_opaque(name const & n) const { return m_not_reducible_pred(n); }
     virtual bool ignore_universe_def_eq(level const & l1, level const & l2) const;
     virtual bool is_uvar(level const & l) const;
     virtual bool is_mvar(expr const & e) const;

src/library/unifier.cpp

@@ -457,17 +457,13 @@ struct unifier_fn {
             m_tc = mk_opaque_type_checker(env);
             m_flex_rigid_tc = m_tc;
             break;
-        case unifier_kind::VeryConservative:
-            m_tc = mk_type_checker(env, UnfoldReducible);
-            m_flex_rigid_tc = m_tc;
-            break;
         case unifier_kind::Conservative:
-            m_tc = mk_type_checker(env, UnfoldQuasireducible);
+            m_tc = mk_type_checker(env, UnfoldReducible);
             m_flex_rigid_tc = m_tc;
             break;
         case unifier_kind::Liberal:
             m_tc = mk_type_checker(env);
-            m_flex_rigid_tc = mk_type_checker(env, UnfoldQuasireducible);
+            m_flex_rigid_tc = mk_type_checker(env, UnfoldReducible);
             break;
         default:
             lean_unreachable();
@@ -1694,7 +1690,7 @@ struct unifier_fn {
         expr lhs_fn     = get_app_fn(lhs);
         lean_assert(is_constant(lhs_fn));
         declaration d   = *m_env.find(const_name(lhs_fn));
-        return (m_config.m_kind == unifier_kind::Liberal && (module::is_definition(m_env, d.get_name()) || is_at_least_quasireducible(m_env, d.get_name())));
+        return (m_config.m_kind == unifier_kind::Liberal && (module::is_definition(m_env, d.get_name()) || is_reducible(m_env, d.get_name())));
     }
 
     /**

src/library/unifier.h

@@ -29,7 +29,7 @@ unify_status unify_simple(substitution & s, expr const & lhs, expr const & rhs,
 unify_status unify_simple(substitution & s, level const & lhs, level const & rhs, justification const & j);
 unify_status unify_simple(substitution & s, constraint const & c);
 
-enum class unifier_kind { Cheap, VeryConservative, Conservative, Liberal };
+enum class unifier_kind { Cheap, Conservative, Liberal };
 
 struct unifier_config {
     bool     m_use_exceptions;
@@ -40,16 +40,11 @@ struct unifier_config {
     // If m_discard is false, unify returns the set of constraints that could not be handled.
     bool     m_discard;
     // If m_mind == Conservative, then the following restrictions are imposed:
-    //     - All constants that are not at least marked as Quasireducible as treated as
+    //     - All constants that are not at least marked as Semireducible are treated as
     //       opaque.
     //     - Disables case-split on delta-delta constraints.
     //     - Disables reduction case-split on flex-rigid constraints.
     //
-    // If m_kind == VeryConservative, then
-    //     - More restrictive than Conservative,
-    //     - All constants that are not at least marked as Reducible as treated as
-    //       opaque.
-    //
     // If m_kind == Cheap is true, then expensive case-analysis is not performed (e.g., delta).
     // It is more restrictive than VeryConservative
     //

src/vim/syntax/lean.vim

@@ -46,7 +46,7 @@ syn keyword leanConstant → ∃ ∀
 " modifiers (pragmas)
 syn keyword leanModifier contained containedin=leanBracketEncl persistent notation visible instance trans_instance class parsing_only
 syn keyword leanModifier contained containedin=leanBracketEncl coercion unfold_full constructor reducible irreducible semireducible
-syn keyword leanModifier contained containedin=leanBracketEncl quasireducible wf whnf multiple_instances none decls declarations coercions
+syn keyword leanModifier contained containedin=leanBracketEncl wf whnf multiple_instances none decls declarations coercions
 syn keyword leanModifier contained containedin=leanBracketEncl classes symm subst refl trans simp congr notations abbreviations
 syn keyword leanModifier contained containedin=leanBracketEncl begin_end_hints tactic_hints reduce_hints unfold_hints aliases eqv
 syn keyword leanModifier contained containedin=leanBracketEncl localrefinfo

tests/lean/print_reducible.lean

@@ -3,9 +3,6 @@ prelude
 definition id₁ [reducible] {A : Type} (a : A) := a
 definition id₂ [reducible] {A : Type} (a : A) := a
 
-definition id₄ [quasireducible] {A : Type} (a : A) := a
-definition id₃ [quasireducible] {A : Type} (a : A) := a
-
 definition id₅ [irreducible] {A : Type} (a : A) := a
 definition id₆ [irreducible] {A : Type} (a : A) := a
 
@@ -14,6 +11,4 @@ definition pr2 {A B : Type} (a : A) (b : B) := a
 
 print [reducible]
 print "-----------"
-print [quasireducible]
-print "-----------"
 print [irreducible]

tests/lean/print_reducible.lean.expected.out

@@ -2,8 +2,5 @@ id₁
 id₂
 pr
 -----------
-id₃
-id₄
------------
 id₅
 id₆

tests/lean/quasireducible.lean

@@ -1,21 +0,0 @@
-constant g : nat → nat
-
-definition f [reducible] := g
-
-example (a : nat) (H : f a = a) : g a = a :=
-by rewrite H
-
-attribute f [quasireducible]
-
-example (a : nat) (H : f a = a) : g a = a :=
-by rewrite H -- error
-
-attribute f [semireducible]
-
-example (a : nat) (H : f a = a) : g a = a :=
-by rewrite H -- error
-
-attribute f [reducible]
-
-example (a : nat) (H : f a = a) : g a = a :=
-by rewrite H -- error

tests/lean/quasireducible.lean.expected.out

@@ -1,28 +0,0 @@
-quasireducible.lean:11:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern
-  f a
-no subterm in the goal matched the pattern
-proof state:
-a : ℕ,
-H : f a = a
-⊢ g a = a
-quasireducible.lean:11:0: error: don't know how to synthesize placeholder
-a : ℕ,
-H : f a = a
-⊢ g a = a
-quasireducible.lean:11:0: error: failed to add declaration 'example' to environment, value has metavariables
-remark: set 'formatter.hide_full_terms' to false to see the complete term
-  ?M_1
-quasireducible.lean:16:11: error:invalid 'rewrite' tactic, rewrite step failed using pattern
-  f a
-no subterm in the goal matched the pattern
-proof state:
-a : ℕ,
-H : f a = a
-⊢ g a = a
-quasireducible.lean:16:0: error: don't know how to synthesize placeholder
-a : ℕ,
-H : f a = a
-⊢ g a = a
-quasireducible.lean:16:0: error: failed to add declaration 'example' to environment, value has metavariables
-remark: set 'formatter.hide_full_terms' to false to see the complete term
-  ?M_1