feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant

hott/algebra/precategory/morphism.hlean

@@ -105,7 +105,7 @@ namespace morphism
             = retraction_of f ∘ retraction_of g ∘ g ∘ f : assoc
         ... = retraction_of f ∘ ((retraction_of g ∘ g) ∘ f) : aux
         ... = retraction_of f ∘ id ∘ f : {retraction_compose g}
-        ... = retraction_of f ∘ f : id_left f
+        ... = retraction_of f ∘ f : {id_left f}
         ... = id : retraction_compose f)
 
   theorem composition_is_retraction [instance] (Hf : is_retraction f) (Hg : is_retraction g)
@@ -118,7 +118,7 @@ namespace morphism
             = g ∘ f ∘ section_of f ∘ section_of g : assoc
         ... = g ∘ (f ∘ section_of f) ∘ section_of g : aux
         ... = g ∘ id ∘ section_of g : compose_section f
-        ... = g ∘ section_of g : id_left (section_of g)
+        ... = g ∘ section_of g : {id_left (section_of g)}
         ... = id : compose_section)
 
   theorem composition_is_inverse [instance] (Hf : is_iso f) (Hg : is_iso g) : is_iso (g ∘ f) :=

hott/init/equiv.hlean

@@ -102,7 +102,7 @@ namespace is_equiv
       have eq1 : ap f (sec a) = _,
         from calc ap f (sec a)
               = idp ⬝ ap f (sec a) : !concat_1p⁻¹
-          ... = (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : concat_pV
+          ... = (ret (f a) ⬝ (ret (f a)⁻¹)) ⬝ ap f (sec a) : {!concat_pV⁻¹}
           ... = ((ret (fgfa))⁻¹ ⬝ ap (f ∘ g) (ret (f a))) ⬝ ap f (sec a) : {!concat_pA1⁻¹}
           ... = ((ret (fgfa))⁻¹ ⬝ fgretrfa) ⬝ ap f (sec a) : {ap_compose g f _}
           ... = (ret (fgfa))⁻¹ ⬝ (fgretrfa ⬝ ap f (sec a)) : !concat_pp_p,

hott/types/sigma.hlean

@@ -268,7 +268,7 @@ namespace sigma
               : ap (g a⁻¹) !transport_compose
       ... = g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (ap f (sect f a)⁻¹) (g a b)))
            : ap (λ x, g a⁻¹ (transport B' (ap f (sect f a)) (transport B' (x⁻¹) (g a b)))) (adj f a)
-      ... = g a⁻¹ (g a b) : transport_pV
+      ... = g a⁻¹ (g a b) : {!transport_pV}
       ... = b : sect (g a) b
   end
     -- -- "rewrite ap_transport"

library/algebra/ring.lean

@@ -246,7 +246,7 @@ section
           dvd.intro
             (calc
               a * -c = -(a * c) : {!neg_mul_eq_mul_neg⁻¹}
-                ... = -(-b) : H'
+                ... = -(-b) : {H'}
                 ... = b : neg_neg)))
     (assume H : a | b,
       dvd.elim H
@@ -254,7 +254,7 @@ section
           dvd.intro
             (calc
               a * -c = -(a * c) : {!neg_mul_eq_mul_neg⁻¹}
-                ... = -b : H')))
+                ... = -b : {H'})))
 
   theorem neg_dvd_iff_dvd : -a | b ↔ a | b :=
   iff.intro

library/data/fin.lean

@@ -70,12 +70,12 @@ namespace fin
   to_nat_of_nat (p+1) (n+1) h := calc
     to_nat (of_nat (p+1) (n+1) h)
              = succ (to_nat (of_nat p n _)) : rfl
-         ... = succ p                       : to_nat_of_nat p n _
+         ... = succ p                       : {to_nat_of_nat p n _}
 
   theorem of_nat_to_nat : ∀ {n : nat} (f : fin n) (h : to_nat f < n), of_nat (to_nat f) n h = f,
   of_nat_to_nat (fz n) h    := rfl,
   of_nat_to_nat (@fs n f) h := calc
     of_nat (to_nat (fs f)) (succ n) h = fs (of_nat (to_nat f) n _) : rfl
-                                 ...  = fs f                       : of_nat_to_nat f _
+                                 ...  = fs f                       : {of_nat_to_nat f _}
 
 end fin

library/data/int/basic.lean

@@ -43,7 +43,7 @@ inductive int : Type :=
 
 notation `ℤ` := int
 coercion [persistent] int.of_nat
-definition int.of_num [coercion] (n : num) : ℤ := int.of_nat (nat.of_num n)
+definition int.of_num [coercion] [reducible] (n : num) : ℤ := int.of_nat (nat.of_num n)
 
 namespace int
 
@@ -506,7 +506,7 @@ cases_on a
           pmul (repr (neg_succ_of_nat m')) (repr n) =
               (0 * n + succ m' * 0, 0 * 0 + succ m' * n) : rfl
             ... = (0 + succ m' * 0, 0 * 0 + succ m' * n) : zero_mul
-            ... = (0 + succ m' * 0, succ m' * n) : nat.zero_add
+            ... = (0 + succ m' * 0, succ m' * n) : {!nat.zero_add}
             ... = repr (mul (neg_succ_of_nat m') n) : repr_neg_of_nat)⁻¹)
       (take n',
         (calc

library/data/nat/div.lean

@@ -45,7 +45,7 @@ theorem add_div_left {x z : ℕ} (H : z > 0) : (x + z) div z = succ (x div z) :=
 calc
   (x + z) div z = if 0 < z ∧ z ≤ x + z then (x + z - z) div z + 1 else 0 : !divide_def
             ... = (x + z - z) div z + 1 : if_pos (and.intro H (le_add_left z x))
-            ... = succ (x div z)        : add_sub_cancel
+            ... = succ (x div z)        : {!add_sub_cancel}
 
 theorem add_div_right {x z : ℕ} (H : x > 0) : (x + z) div x = succ (z div x) :=
 !add.comm ▸ add_div_left H

src/frontends/lean/calc_proof_elaborator.cpp

@@ -154,7 +154,7 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
                 fn(e);
         }
 
-        auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs) {
+        auto try_alternative = [&](expr const & e, expr const & e_type, constraint_seq fcs, bool conservative) {
             justification new_j            = mk_type_mismatch_jst(e, e_type, meta_type);
             if (!tc->is_def_eq(e_type, meta_type, new_j, fcs))
                 throw unifier_exception(new_j, s);
@@ -166,8 +166,9 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
             cs_buffer.push_back(mk_eq_cnstr(meta, e, j, relax));
 
             unifier_config new_cfg(cfg);
-            new_cfg.m_discard    = false;
+            new_cfg.m_discard      = false;
-            unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg);
+            new_cfg.m_conservative = conservative;
+            unify_result_seq seq   = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg);
             auto p = seq.pull();
             lean_assert(p);
             substitution new_s     = p->first.first;
@@ -183,30 +184,35 @@ constraint mk_calc_proof_cnstr(environment const & env, options const & opts,
         };
 
         if (!get_elaborator_calc_assistant(opts)) {
-            return try_alternative(e, e_type, new_cs);
+            bool conservative = false;
+            return try_alternative(e, e_type, new_cs, conservative);
         } else {
             std::unique_ptr<throwable> saved_ex;
             try {
-                return try_alternative(e, e_type, new_cs);
+                bool conservative = false;
+                return try_alternative(e, e_type, new_cs, conservative);
             } catch (exception & ex) {
                 saved_ex.reset(ex.clone());
             }
 
             constraint_seq symm_cs = new_cs;
-            auto symm = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g);
+            auto symm  = apply_symmetry(env, ctx, ngen, tc, e, e_type, symm_cs, g);
             if (symm) {
-                try { return try_alternative(symm->first, symm->second, symm_cs); } catch (exception &) {}
+                bool conservative = false;
+                try { return try_alternative(symm->first, symm->second, symm_cs, conservative); } catch (exception &) {}
             }
 
             constraint_seq subst_cs = new_cs;
             if (auto subst = apply_subst(env, ctx, ngen, tc, e, e_type, meta_type, subst_cs, g)) {
-                try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {}
+                bool conservative = true;
+                try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {}
             }
 
             if (symm) {
                 constraint_seq subst_cs = symm_cs;
+                bool conservative = true;
                 if (auto subst = apply_subst(env, ctx, ngen, tc, symm->first, symm->second, meta_type, subst_cs, g)) {
-                    try { return try_alternative(subst->first, subst->second, subst_cs); } catch (exception&) {}
+                    try { return try_alternative(subst->first, subst->second, subst_cs, conservative); } catch (exception&) {}
                 }
             }
 

src/library/unifier.cpp

@@ -45,10 +45,15 @@ Author: Leonardo de Moura
 #define LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES false
 #endif
 
+#ifndef LEAN_DEFAULT_UNIFIER_CONSERVATIVE
+#define LEAN_DEFAULT_UNIFIER_CONSERVATIVE false
+#endif
+
 namespace lean {
-static name * g_unifier_max_steps         = nullptr;
+static name * g_unifier_max_steps               = nullptr;
-static name * g_unifier_computation       = nullptr;
+static name * g_unifier_computation             = nullptr;
-static name * g_unifier_expensive_classes = nullptr;
+static name * g_unifier_expensive_classes       = nullptr;
+static name * g_unifier_conservative            = nullptr;
 
 unsigned get_unifier_max_steps(options const & opts) {
     return opts.get_unsigned(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS);
@@ -62,12 +67,17 @@ bool get_unifier_expensive_classes(options const & opts) {
     return opts.get_bool(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES);
 }
 
+bool get_unifier_conservative(options const & opts) {
+    return opts.get_bool(*g_unifier_conservative, LEAN_DEFAULT_UNIFIER_CONSERVATIVE);
+}
+
 unifier_config::unifier_config(bool use_exceptions, bool discard):
     m_use_exceptions(use_exceptions),
     m_max_steps(LEAN_DEFAULT_UNIFIER_MAX_STEPS),
     m_computation(LEAN_DEFAULT_UNIFIER_COMPUTATION),
     m_expensive_classes(LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES),
-    m_discard(discard) {
+    m_discard(discard),
+    m_conservative(LEAN_DEFAULT_UNIFIER_CONSERVATIVE) {
     m_cheap = false;
     m_ignore_context_check = false;
 }
@@ -77,7 +87,8 @@ unifier_config::unifier_config(options const & o, bool use_exceptions, bool disc
     m_max_steps(get_unifier_max_steps(o)),
     m_computation(get_unifier_computation(o)),
     m_expensive_classes(get_unifier_expensive_classes(o)),
-    m_discard(discard) {
+    m_discard(discard),
+    m_conservative(get_unifier_conservative(o)) {
     m_cheap = false;
     m_ignore_context_check = false;
 }
@@ -419,6 +430,11 @@ struct unifier_fn {
             m_tc[1] = m_tc[0];
             m_flex_rigid_tc = m_tc[0];
             m_config.m_computation = false;
+        } else if (m_config.m_conservative) {
+            m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false, OpaqueIfNotReducibleOn);
+            m_tc[1] = m_tc[0];
+            m_flex_rigid_tc = m_tc[0];
+            m_config.m_computation = false;
         } else {
             m_tc[0] = mk_type_checker(env, m_ngen.mk_child(), false);
             m_tc[1] = mk_type_checker(env, m_ngen.mk_child(), true);
@@ -1325,7 +1341,8 @@ struct unifier_fn {
 
         justification a;
         bool relax = relax_main_opaque(c);
-        if (!m_config.m_cheap && (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_reducible_on(m_env, d.get_name()))) {
+        if (!m_config.m_cheap && !m_config.m_conservative &&
+            (m_config.m_computation || module::is_definition(m_env, d.get_name()) || is_reducible_on(m_env, d.get_name()))) {
             // add case_split for t =?= s
             a = mk_assumption_justification(m_next_assumption_idx);
             add_case_split(std::unique_ptr<case_split>(new delta_unfold_case_split(*this, j, c)));
@@ -1871,7 +1888,7 @@ struct unifier_fn {
     */
     bool use_flex_rigid_whnf_split(expr const & lhs, expr const & rhs) {
         lean_assert(is_meta(lhs));
-        if (m_config.m_cheap)
+        if (m_config.m_cheap || m_config.m_conservative)
             return false;
         if (m_config.m_computation)
             return true; // if unifier.computation is true, we always consider the additional whnf split
@@ -2514,12 +2531,15 @@ void initialize_unifier() {
     g_unifier_max_steps         = new name{"unifier", "max_steps"};
     g_unifier_computation       = new name{"unifier", "computation"};
     g_unifier_expensive_classes = new name{"unifier", "expensive_classes"};
+    g_unifier_conservative      = new name{"unifier", "conservative"};
 
     register_unsigned_option(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps");
     register_bool_option(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION,
                          "(unifier) always case-split on reduction/computational steps when solving flex-rigid and delta-delta constraints");
     register_bool_option(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES,
                          "(unifier) use \"full\" higher-order unification when solving class instances");
+    register_bool_option(*g_unifier_conservative, LEAN_DEFAULT_UNIFIER_CONSERVATIVE,
+                         "(unifier) unfolds only constants marked as reducible, avoid expensive case-splits (it is faster but less complete)");
 
     g_dont_care_cnstr = new constraint(mk_eq_cnstr(expr(), expr(), justification(), false));
     g_tmp_prefix      = new name(name::mk_internal_unique_name());
@@ -2531,5 +2551,6 @@ void finalize_unifier() {
     delete g_unifier_max_steps;
     delete g_unifier_computation;
     delete g_unifier_expensive_classes;
+    delete g_unifier_conservative;
 }
 }

src/library/unifier.h

@@ -40,7 +40,15 @@ struct unifier_config {
     // If m_discard is true, then constraints that cannot be solved are discarded (or incomplete methods are used)
     // If m_discard is false, unify returns the set of constraints that could not be handled.
     bool     m_discard;
+    // If m_conservative is true, then the following restrictions are imposed:
+    //     - All constants that are not marked as reducible as treated as
+    //       opaque.
+    //     - Disables case-split on delta-delta constraints.
+    //     - Disables reduction case-split on flex-rigid constraints.
+    // Default is m_conservative == false
+    bool     m_conservative;
     // If m_cheap is true, then expensive case-analysis is not performed (e.g., delta).
+    // It is more restrictive than m_conservative
     // Default is m_cheap == false
     bool     m_cheap;
     // If m_ignore_context_check == true, then occurs-check is skipped.