From 2717adde9485169a2a95af0e8d102f509e8cae2b Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 19 Jan 2015 16:23:29 -0800 Subject: [PATCH] feat(library/unifier): add option 'unifier.conservative', use option by default in the calc_assistant --- hott/algebra/precategory/morphism.hlean | 4 +-- hott/init/equiv.hlean | 2 +- hott/types/sigma.hlean | 2 +- library/algebra/ring.lean | 4 +-- library/data/fin.lean | 4 +-- library/data/int/basic.lean | 4 +-- library/data/nat/div.lean | 2 +- src/frontends/lean/calc_proof_elaborator.cpp | 24 +++++++++----- src/library/unifier.cpp | 35 ++++++++++++++++---- src/library/unifier.h | 8 +++++ 10 files changed, 62 insertions(+), 27 deletions(-) diff --git a/hott/algebra/precategory/morphism.hlean b/hott/algebra/precategory/morphism.hlean index 2c36e8af7..bc7b16b57 100644 --- a/hott/algebra/precategory/morphism.hlean +++ b/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) := diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index 598a7bfcb..758ccbc35 100644 --- a/hott/init/equiv.hlean +++ b/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, diff --git a/hott/types/sigma.hlean b/hott/types/sigma.hlean index cab19dfaf..b568d194c 100644 --- a/hott/types/sigma.hlean +++ b/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" diff --git a/library/algebra/ring.lean b/library/algebra/ring.lean index a6b61a6e6..32d15fa86 100644 --- a/library/algebra/ring.lean +++ b/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 diff --git a/library/data/fin.lean b/library/data/fin.lean index dcb9f3581..05b9b039e 100644 --- a/library/data/fin.lean +++ b/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 diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean index a567336e3..8fc890397 100644 --- a/library/data/int/basic.lean +++ b/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 diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean index d1ad72b6b..538f451a1 100644 --- a/library/data/nat/div.lean +++ b/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 diff --git a/src/frontends/lean/calc_proof_elaborator.cpp b/src/frontends/lean/calc_proof_elaborator.cpp index a1eafb2ec..04e9db15b 100644 --- a/src/frontends/lean/calc_proof_elaborator.cpp +++ b/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; - unify_result_seq seq = unify(env, cs_buffer.size(), cs_buffer.data(), ngen, substitution(), new_cfg); + new_cfg.m_discard = false; + 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 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&) {} } } diff --git a/src/library/unifier.cpp b/src/library/unifier.cpp index 41a838631..401a56a06 100644 --- a/src/library/unifier.cpp +++ b/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_computation = nullptr; -static name * g_unifier_expensive_classes = nullptr; +static name * g_unifier_max_steps = nullptr; +static name * g_unifier_computation = 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(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; } } diff --git a/src/library/unifier.h b/src/library/unifier.h index 7d8e84932..0378622e0 100644 --- a/src/library/unifier.h +++ b/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.