feat(library/class): mark instances as quasireducible by default

quasireducible are also known as lazyreducible.

There is a lot of work to be done.
We still need to revise blast, and add a normalizer for type class
instances. This commit worksaround that by eagerly unfolding
quasireducible.

hott/homotopy/sphere.hlean

@@ -134,7 +134,7 @@ namespace sphere
     -- fapply equiv_change_fun,
     -- {
       revert A, induction n with n IH: intro A,
-      { rewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv},
+      { krewrite [sphere_eq_bool_pointed], apply pmap_bool_equiv},
       { refine susp_adjoint_loop (S. n) A ⬝e !IH ⬝e _, rewrite [loop_space_succ_eq_in]}
     -- },
     -- { intro f, exact apn n f surf},

hott/types/fin.hlean

@@ -383,7 +383,7 @@ begin
     assert H' : is_prop.elim (lt_add_of_lt_right ilt 1) (lt_add_of_lt_right ilt 1) = idp,
       apply is_prop.elim,
     krewrite H' },
-  { intro a, contradiction },
+  { intro a, exact absurd ilt a },
 end
 
 definition elim_succ_maxi_cases_maxi {C : fin (nat.succ n) → Type}
@@ -507,7 +507,7 @@ open prod
 definition fin_prod_equiv (n m : nat) : (fin n × fin m) ≃ fin (n*m) :=
 begin
   induction n,
-  { rewrite nat.zero_mul,
+  { krewrite nat.zero_mul,
     calc fin 0 × fin m ≃ empty × fin m : fin_zero_equiv_empty
                    ... ≃ fin m × empty : prod_comm_equiv
                    ... ≃ empty : prod_empty_equiv

library/data/nat/bigops.lean

@@ -77,7 +77,7 @@ proposition sum_range_eq_sum_interval_aux (m n : ℕ) (f : ℕ → A) :
             (∑ i = m...m+n, f i) = (∑ i ∈ '[m, m + n], f i) :=
 begin
   induction n with n ih,
-    {rewrite [nat.add_zero, sum_range_self, Icc_self, Sum_singleton]},
+    {krewrite [nat.add_zero, sum_range_self, Icc_self, Sum_singleton]},
   have H : m ≤ succ (m + n), from le_of_lt (lt_of_le_of_lt !le_add_right !lt_succ_self),
   have H' : '[m, m + n] ∩ '{succ (m + n)} = ∅, from
     eq_empty_of_forall_not_mem (take x, assume H1,
@@ -168,7 +168,7 @@ proposition prod_range_eq_prod_interval_aux (m n : ℕ) (f : ℕ → A) :
             (∏ i = m...m+n, f i) = (∏ i ∈ '[m, m + n], f i) :=
 begin
   induction n with n ih,
-    {rewrite [nat.add_zero, prod_range_self, Icc_self, Prod_singleton]},
+    {krewrite [nat.add_zero, prod_range_self, Icc_self, Prod_singleton]},
   have H : m ≤ succ (m + n), from le_of_lt (lt_of_le_of_lt !le_add_right !lt_succ_self),
   have H' : '[m, m + n] ∩ '{succ (m + n)} = ∅, from
     eq_empty_of_forall_not_mem (take x, assume H1,

library/theories/combinatorics/choose.lean

@@ -82,7 +82,7 @@ begin
   induction n with [n, ih],
     {intro k,
       cases k with k',
-        {rewrite [*choose_self, one_mul, mul_one]},
+        {krewrite [*choose_self, one_mul, mul_one]},
         {have H : 1 < succ (succ k'), from succ_lt_succ !zero_lt_succ,
          krewrite [one_mul, choose_zero_succ, choose_eq_zero_of_lt H, zero_mul]}},
   intro k,

library/theories/measure_theory/extended_real.lean

@@ -197,7 +197,7 @@ private theorem aux2 : ∀ u : ereal, -u * ∞ = -(u * ∞)
                       by rewrite [ereal.neg_of_real, pos_mul_infty (neg_pos_of_neg H),
                                   neg_mul_infty H])
                    (assume H : x = 0,
-                      by rewrite [H, ereal.neg_zero, *zero_mul_infty, ereal.neg_zero])
+                      by krewrite [H, ereal.neg_zero, *zero_mul_infty, ereal.neg_zero])
                    (assume H : x > 0,
                       by rewrite [ereal.neg_of_real, neg_mul_infty (neg_neg_of_pos H),
                                    pos_mul_infty H])
@@ -238,16 +238,16 @@ lt.by_cases
     lt.by_cases
       (assume H1 : y < 0, by rewrite [infty_mul_neg H, neg_infty, ereal_neg_mul, -of_real_mul,
                                      infty_mul_neg H1, infty_mul_pos (mul_pos_of_neg_of_neg H H1)])
-      (assume H1 : y = 0, by rewrite [H1, *ereal.mul_zero])
+      (assume H1 : y = 0, by krewrite [H1, *ereal.mul_zero])
       (assume H1 : y > 0, by rewrite [infty_mul_neg H, neg_infty, *ereal_neg_mul, -of_real_mul,
                                      infty_mul_pos H1, infty_mul_neg (mul_neg_of_neg_of_pos H H1)]))
   (assume H : x = 0,
-    by rewrite [H, ereal.mul_zero, *ereal.zero_mul, ereal.mul_zero])
+    by krewrite [H, ereal.mul_zero, *ereal.zero_mul, ereal.mul_zero])
   (assume H : x > 0,
     lt.by_cases
       (assume H1 : y < 0, by rewrite [infty_mul_pos H, infty_mul_neg H1, -of_real_mul,
                                      infty_mul_neg (mul_neg_of_pos_of_neg H H1)])
-      (assume H1 : y = 0, by rewrite [H1, *ereal.mul_zero])
+      (assume H1 : y = 0, by krewrite [H1, *ereal.mul_zero])
       (assume H1 : y > 0, by rewrite [infty_mul_pos H, infty_mul_pos H1, -of_real_mul,
                                      infty_mul_pos (mul_pos H H1)]))
 
@@ -275,7 +275,7 @@ protected theorem one_mul : ∀ u : ereal, of_real 1 * u = u
 | -∞          := by rewrite [neg_infty, ereal_mul_neg, pos_mul_infty zero_lt_one]
 
 protected theorem mul_one (u : ereal) : u * 1 = u :=
-by rewrite [ereal.mul_comm, ereal.one_mul]
+by krewrite [ereal.mul_comm, ereal.one_mul]
 
 /- instantiating arithmetic structures -/
 

library/theories/number_theory/bezout.lean

@@ -98,7 +98,7 @@ decidable.by_cases
     have cpx : coprime p x, from coprime_of_prime_of_not_dvd pp this,
     obtain (a b : ℤ) (Hab : a * p + b * x = gcd p x), from Bezout_aux p x,
     assert a * p * y + b * x * y = y,
-      by rewrite [-right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul],
+      by krewrite [-right_distrib, Hab, ↑coprime at cpx, cpx, int.one_mul],
     have p ∣ y,
       begin
         apply dvd_of_of_nat_dvd_of_nat,

src/frontends/lean/structure_cmd.cpp

@@ -19,6 +19,7 @@ Author: Leonardo de Moura
 #include "kernel/error_msgs.h"
 #include "kernel/inductive/inductive.h"
 #include "library/trace.h"
+#include "library/attribute_manager.h"
 #include "library/scoped_ext.h"
 #include "library/normalize.h"
 #include "library/placeholder.h"
@@ -842,7 +843,7 @@ struct structure_cmd_fn {
                     m_env = add_coercion(m_env, m_p.ios(), coercion_name, get_namespace(m_env), true);
                 if (m_modifiers.is_class() && is_class(m_env, parent_name)) {
                     // if both are classes, then we also mark coercion_name as an instance
-                    m_env = add_trans_instance(m_env, coercion_name, get_namespace(m_env), true);
+                    m_env = add_trans_instance(m_env, coercion_name, LEAN_DEFAULT_PRIORITY, get_namespace(m_env), true);
                 }
             }
         }

src/library/blast/blast.cpp

@@ -608,7 +608,8 @@ 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)),
-        m_not_reducible_pred(mk_not_reducible_pred(env)),
+        // TODO(Leo): quasireducible in the following line is a temporary hack.
+        m_not_reducible_pred(mk_not_quasireducible_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,13 +250,21 @@ 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_reducible_pred(env) : mk_irreducible_pred(env);
+    auto pred = conservative ? mk_not_quasireducible_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) {
+    declaration const & d = env.get(n);
+    if (d.is_definition() && !d.is_theorem())
+        return set_reducible(env, n, reducible_status::Quasireducible, ns, persistent);
+    else
+        return env;
+}
+
 environment add_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent) {
     declaration d = env.get(n);
     expr type = d.get_type();
@@ -269,12 +277,9 @@ environment add_instance(environment const & env, name const & n, unsigned prior
     }
     name c = get_class_name(env, get_app_fn(type));
     check_is_class(env, c);
-    return class_ext::add_entry(env, get_dummy_ios(), class_entry(class_entry_kind::Instance, c, n, priority),
-                                ns, persistent);
-}
-
-environment add_instance(environment const & env, name const & n, name const & ns, bool persistent) {
-    return add_instance(env, n, LEAN_DEFAULT_PRIORITY, ns, persistent);
+    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);
 }
 
 static name * g_source = nullptr;
@@ -310,19 +315,16 @@ 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);
     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::Reducible, ns, persistent);
+        new_env = set_reducible(new_env, edge.m_cnst, reducible_status::Quasireducible, ns, persistent);
         new_env = add_protected(new_env, edge.m_cnst);
     }
     return new_env;
 }
 
-environment add_trans_instance(environment const & env, name const & n, name const & ns, bool persistent) {
-    return add_trans_instance(env, n, LEAN_DEFAULT_PRIORITY, ns, persistent);
-}
-
 environment mark_multiple_instances(environment const & env, name const & n, name const & ns, bool persistent) {
     check_class(env, n);
     return class_ext::add_entry(env, get_dummy_ios(), class_entry(n, true), ns, persistent);

src/library/class.h

@@ -11,12 +11,8 @@ namespace lean {
 type_checker_ptr mk_class_type_checker(environment const & env, bool conservative);
 /** \brief Add a new 'class' to the environment (if it is not already declared) */
 environment add_class(environment const & env, name const & n, name const & ns, bool persistent);
-/** \brief Add a new 'class instance' to the environment with default priority. */
-environment add_instance(environment const & env, name const & n, name const & ns, bool persistent);
 /** \brief Add a new 'class instance' to the environment. */
 environment add_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent);
-/** \brief Add a new 'class transitive instance' to the environment with default priority. */
-environment add_trans_instance(environment const & env, name const & n, name const & ns, bool persistent);
 /** \brief Add a new 'class transitive instance' to the environment. */
 environment add_trans_instance(environment const & env, name const & n, unsigned priority, name const & ns, bool persistent);
 /** \brief Return true iff \c c was declared with \c add_class. */

src/library/class_instance_resolution.cpp

@@ -493,7 +493,7 @@ static constraint mk_class_instance_root_cnstr(std::shared_ptr<class_instance_co
         new_cfg.m_discard        = false;
         new_cfg.m_use_exceptions = false;
         new_cfg.m_pattern        = true;
-        new_cfg.m_kind           = C->m_conservative ? unifier_kind::VeryConservative : unifier_kind::Liberal;
+        new_cfg.m_kind           = C->m_conservative ? unifier_kind::Conservative : unifier_kind::Liberal;
 
         auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints {
             substitution new_s = subst;

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 ? UnfoldReducible : UnfoldSemireducible);
+            auto tc      = mk_type_checker(env, conservative ? UnfoldQuasireducible : UnfoldSemireducible);
             auto e_t_cs  = tc->infer(new_e);
             expr t       = *expected_type;
             e_t_cs.second.linearize(cs);

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 = UnfoldReducible);
+    tmp_type_context(environment const & env, options const & o, reducible_behavior b = UnfoldQuasireducible);
     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_reducible_pred(mk_not_reducible_pred(env)) {
+    m_not_quasireducible_pred(mk_not_quasireducible_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_reducible_pred;
+    name_predicate            m_not_quasireducible_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_reducible_pred(n); }
+    virtual bool is_extra_opaque(name const & n) const { return m_not_quasireducible_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;