From 1cd44e894b8ea3b30f30abe01dee2b8fcb5c97ff Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 24 Feb 2015 14:09:20 -0800 Subject: [PATCH] feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible closes #442 --- hott/algebra/precategory/yoneda.hlean | 2 ++ hott/init/axioms/funext_of_ua.hlean | 1 + hott/init/axioms/funext_varieties.hlean | 3 +++ hott/init/logic.hlean | 11 +++++---- hott/init/nat.hlean | 2 +- hott/init/trunc.hlean | 2 +- hott/types/trunc.hlean | 1 + library/data/int/order.lean | 8 +++++-- library/data/nat/bquant.lean | 4 ++-- library/init/logic.lean | 12 ++++++---- library/init/nat.lean | 2 +- library/logic/examples/instances_test.lean | 2 ++ src/library/tactic/class_instance_synth.cpp | 23 +++++++++++++++++- tests/lean/hott/class_loop.hlean | 26 +++++++++++++++++++++ tests/lean/interactive/whnfinst.lean | 2 +- tests/lean/run/group4.lean | 2 +- tests/lean/run/group5.lean | 2 +- tests/lean/run/whnfinst.lean | 2 +- 18 files changed, 87 insertions(+), 20 deletions(-) create mode 100644 tests/lean/hott/class_loop.hlean diff --git a/hott/algebra/precategory/yoneda.hlean b/hott/algebra/precategory/yoneda.hlean index 733678e21..7cf686a82 100644 --- a/hott/algebra/precategory/yoneda.hlean +++ b/hott/algebra/precategory/yoneda.hlean @@ -15,6 +15,8 @@ open is_trunc.trunctype funext precategory.ops prod.ops set_option pp.beta true namespace yoneda + set_option class.conservative false + definition representable_functor_assoc [C : Precategory] {a1 a2 a3 a4 a5 a6 : C} (f1 : a5 ⟶ a6) (f2 : a4 ⟶ a5) (f3 : a3 ⟶ a4) (f4 : a2 ⟶ a3) (f5 : a1 ⟶ a2) : (f1 ∘ f2) ∘ f3 ∘ (f4 ∘ f5) = f1 ∘ (f2 ∘ f3 ∘ f4) ∘ f5 := calc (f1 ∘ f2) ∘ f3 ∘ f4 ∘ f5 = f1 ∘ f2 ∘ f3 ∘ f4 ∘ f5 : assoc diff --git a/hott/init/axioms/funext_of_ua.hlean b/hott/init/axioms/funext_of_ua.hlean index 0fd5278cc..3b612d1be 100644 --- a/hott/init/axioms/funext_of_ua.hlean +++ b/hott/init/axioms/funext_of_ua.hlean @@ -77,6 +77,7 @@ context (λ xy, prod.rec_on xy (λ b c p, eq.rec_on p idp)))) + set_option class.conservative false theorem nondep_funext_from_ua {A : Type} {B : Type} : Π {f g : A → B}, f ∼ g → f = g := (λ (f g : A → B) (p : f ∼ g), diff --git a/hott/init/axioms/funext_varieties.hlean b/hott/init/axioms/funext_varieties.hlean index 96b3f5cf1..476f60942 100644 --- a/hott/init/axioms/funext_varieties.hlean +++ b/hott/init/axioms/funext_varieties.hlean @@ -78,6 +78,8 @@ context @transport _ (λ gh, Q (pr1 gh) (pr2 gh)) (sigma.mk f (homotopy.refl f)) (sigma.mk g h) (@center_eq _ is_contr_sigma_homotopy _ _) d + + local attribute weak_funext [reducible] local attribute homotopy_ind [reducible] definition homotopy_ind_comp : homotopy_ind f (homotopy.refl f) = d := (@hprop_eq _ _ _ _ !center_eq idp)⁻¹ ▹ idp @@ -87,6 +89,7 @@ end -- Now the proof is fairly easy; we can just use the same induction principle on both sides. universe variables l k +local attribute weak_funext [reducible] theorem funext_of_weak_funext (wf : weak_funext.{l k}) : funext.{l k} := funext.mk (λ A B f g, let eq_to_f := (λ g' x, f = g') in diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index 1b326021a..450368e04 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -267,12 +267,15 @@ section (assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq))) (assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp)) - definition iff.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ↔ q) := _ + definition iff.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ↔ q) := + show decidable (prod (p → q) (q → p)), from _ end -definition decidable_pred {A : Type} (R : A → Type) := Π (a : A), decidable (R a) -definition decidable_rel {A : Type} (R : A → A → Type) := Π (a b : A), decidable (R a b) -definition decidable_eq (A : Type) := decidable_rel (@eq A) +definition decidable_pred [reducible] {A : Type} (R : A → Type) := Π (a : A), decidable (R a) +definition decidable_rel [reducible] {A : Type} (R : A → A → Type) := Π (a b : A), decidable (R a b) +definition decidable_eq [reducible] (A : Type) := decidable_rel (@eq A) +definition decidable_ne [instance] {A : Type} (H : decidable_eq A) : decidable_rel (@ne A) := +show ∀ x y : A, decidable (x = y → empty), from _ definition ite (c : Type) [H : decidable c] {A : Type} (t e : A) : A := decidable.rec_on H (λ Hc, t) (λ Hnc, e) diff --git a/hott/init/nat.hlean b/hott/init/nat.hlean index aed5bd40c..81d9683b7 100644 --- a/hott/init/nat.hlean +++ b/hott/init/nat.hlean @@ -19,7 +19,7 @@ namespace nat notation a < b := lt a b - definition le (a b : nat) : Type₀ := a < succ b + definition le [reducible] (a b : nat) : Type₀ := a < succ b notation a ≤ b := le a b diff --git a/hott/init/trunc.hlean b/hott/init/trunc.hlean index 4cf72e01c..f5ac3a532 100644 --- a/hott/init/trunc.hlean +++ b/hott/init/trunc.hlean @@ -53,7 +53,7 @@ namespace is_trunc definition minus_two_le (n : trunc_index) : -2 ≤ n := star definition empty_of_succ_le_minus_two {n : trunc_index} (H : n .+1 ≤ -2) : empty := H end trunc_index - definition trunc_index.of_nat [coercion] (n : nat) : trunc_index := + definition trunc_index.of_nat [coercion] [reducible] (n : nat) : trunc_index := nat.rec_on n (-1.+1) (λ n k, k.+1) /- truncated types -/ diff --git a/hott/types/trunc.hlean b/hott/types/trunc.hlean index 36e0f4eb8..768ca229d 100644 --- a/hott/types/trunc.hlean +++ b/hott/types/trunc.hlean @@ -99,6 +99,7 @@ namespace is_trunc imp (λp, p ▹ refl a) + local attribute not [reducible] definition is_hset_of_double_neg_elim {A : Type} (H : Π(a b : A), ¬¬a = b → a = b) : is_hset A := is_hset_of_relation (λa b, ¬¬a = b) _ (λa n, n idp) H diff --git a/library/data/int/order.lean b/library/data/int/order.lean index ff93fb170..ff402ff37 100644 --- a/library/data/int/order.lean +++ b/library/data/int/order.lean @@ -25,6 +25,7 @@ infix <= := int.le infix ≤ := int.le infix < := int.lt +local attribute nonneg [reducible] private definition decidable_nonneg [instance] (a : ℤ) : decidable (nonneg a) := int.cases_on a _ _ definition decidable_le [instance] (a b : ℤ) : decidable (a ≤ b) := decidable_nonneg _ definition decidable_lt [instance] (a b : ℤ) : decidable (a < b) := decidable_nonneg _ @@ -242,8 +243,11 @@ section port_algebra infix >= := int.ge infix ≥ := int.ge infix > := int.gt - definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) := _ - definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := _ + + definition decidable_ge [instance] (a b : ℤ) : decidable (a ≥ b) := + show decidable (b ≤ a), from _ + definition decidable_gt [instance] (a b : ℤ) : decidable (a > b) := + show decidable (b < a), from _ theorem le_of_eq_of_le : ∀{a b c : ℤ}, a = b → b ≤ c → a ≤ c := @algebra.le_of_eq_of_le _ _ theorem le_of_le_of_eq : ∀{a b c : ℤ}, a ≤ b → b = c → a ≤ c := @algebra.le_of_le_of_eq _ _ diff --git a/library/data/nat/bquant.lean b/library/data/nat/bquant.lean index 12233bb57..3abd4073b 100644 --- a/library/data/nat/bquant.lean +++ b/library/data/nat/bquant.lean @@ -19,10 +19,10 @@ More importantly, they can be reduced inside of the Lean kernel. import data.nat.order namespace nat - definition bex (n : nat) (P : nat → Prop) : Prop := + definition bex [reducible] (n : nat) (P : nat → Prop) : Prop := ∃ x, x < n ∧ P x - definition ball (n : nat) (P : nat → Prop) : Prop := + definition ball [reducible] (n : nat) (P : nat → Prop) : Prop := ∀ x, x < n → P x definition not_bex_zero (P : nat → Prop) : ¬ bex 0 P := diff --git a/library/init/logic.lean b/library/init/logic.lean index f9ab4baef..7e7a115bf 100644 --- a/library/init/logic.lean +++ b/library/init/logic.lean @@ -315,12 +315,16 @@ section (assume Hnq : ¬q, inr (assume H : p → q, absurd (H Hp) Hnq))) (assume Hnp : ¬p, inl (assume Hp, absurd Hp Hnp)) - definition iff.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ↔ q) := _ + definition iff.decidable [instance] (Hp : decidable p) (Hq : decidable q) : decidable (p ↔ q) := + show decidable ((p → q) ∧ (q → p)), from _ + end -definition decidable_pred {A : Type} (R : A → Prop) := Π (a : A), decidable (R a) -definition decidable_rel {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b) -definition decidable_eq (A : Type) := decidable_rel (@eq A) +definition decidable_pred [reducible] {A : Type} (R : A → Prop) := Π (a : A), decidable (R a) +definition decidable_rel [reducible] {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b) +definition decidable_eq [reducible] (A : Type) := decidable_rel (@eq A) +definition decidable_ne [instance] {A : Type} (H : decidable_eq A) : Π (a b : A), decidable (a ≠ b) := +show Π x y : A, decidable (x = y → false), from _ inductive inhabited [class] (A : Type) : Type := mk : A → inhabited A diff --git a/library/init/nat.lean b/library/init/nat.lean index 30330cda1..03f31d28a 100644 --- a/library/init/nat.lean +++ b/library/init/nat.lean @@ -19,7 +19,7 @@ namespace nat notation a < b := lt a b - definition le (a b : nat) : Prop := a < succ b + definition le [reducible] (a b : nat) : Prop := a < succ b notation a ≤ b := le a b diff --git a/library/logic/examples/instances_test.lean b/library/logic/examples/instances_test.lean index df8cf504f..bce5a40d1 100644 --- a/library/logic/examples/instances_test.lean +++ b/library/logic/examples/instances_test.lean @@ -16,6 +16,8 @@ open eq.ops example (a b : Prop) (H : a ↔ b) (H1 : a) : b := mp H H1 +set_option class.conservative false + example (a b c d e : Prop) (H1 : a ↔ b) (H2 : a ∨ c → ¬(d → a)) : b ∨ c → ¬(d → b) := subst iff H1 H2 diff --git a/src/library/tactic/class_instance_synth.cpp b/src/library/tactic/class_instance_synth.cpp index b9969c2b7..8405968a1 100644 --- a/src/library/tactic/class_instance_synth.cpp +++ b/src/library/tactic/class_instance_synth.cpp @@ -37,10 +37,15 @@ Author: Leonardo de Moura #define LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH 32 #endif +#ifndef LEAN_DEFAULT_CLASS_CONSERVATIVE +#define LEAN_DEFAULT_CLASS_CONSERVATIVE true +#endif + namespace lean { static name * g_class_unique_class_instances = nullptr; static name * g_class_trace_instances = nullptr; static name * g_class_instance_max_depth = nullptr; +static name * g_class_conservative = nullptr; [[ noreturn ]] void throw_class_exception(char const * msg, expr const & m) { throw_generic_exception(msg, m); } [[ noreturn ]] void throw_class_exception(expr const & m, pp_fn const & fn) { throw_generic_exception(m, fn); } @@ -49,6 +54,7 @@ void initialize_class_instance_elaborator() { g_class_unique_class_instances = new name{"class", "unique_instances"}; g_class_trace_instances = new name{"class", "trace_instances"}; g_class_instance_max_depth = new name{"class", "instance_max_depth"}; + g_class_conservative = new name{"class", "conservative"}; register_bool_option(*g_class_unique_class_instances, LEAN_DEFAULT_CLASS_UNIQUE_CLASS_INSTANCES, "(class) generate an error if there is more than one solution " @@ -59,12 +65,16 @@ void initialize_class_instance_elaborator() { register_unsigned_option(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH, "(class) max allowed depth in class-instance resolution"); + + register_bool_option(*g_class_conservative, LEAN_DEFAULT_CLASS_CONSERVATIVE, + "(class) use conservative unification (only unfold reducible definitions, and avoid delta-delta case splits)"); } void finalize_class_instance_elaborator() { delete g_class_unique_class_instances; delete g_class_trace_instances; delete g_class_instance_max_depth; + delete g_class_conservative; } bool get_class_unique_class_instances(options const & o) { @@ -79,6 +89,10 @@ unsigned get_class_instance_max_depth(options const & o) { return o.get_unsigned(*g_class_instance_max_depth, LEAN_DEFAULT_CLASS_INSTANCE_MAX_DEPTH); } +bool get_class_conservative(options const & o) { + return o.get_bool(*g_class_conservative, LEAN_DEFAULT_CLASS_CONSERVATIVE); +} + /** \brief Context for handling class-instance metavariable choice constraint */ struct class_instance_context { io_state m_ios; @@ -88,6 +102,7 @@ struct class_instance_context { bool m_relax; bool m_use_local_instances; bool m_trace_instances; + bool m_conservative; unsigned m_max_depth; char const * m_fname; optional m_pos; @@ -95,12 +110,16 @@ struct class_instance_context { name const & prefix, bool relax, bool use_local_instances): m_ios(ios), m_ngen(prefix), - m_tc(mk_type_checker(env, m_ngen.mk_child(), relax)), m_relax(relax), m_use_local_instances(use_local_instances) { m_fname = nullptr; m_trace_instances = get_class_trace_instances(ios.get_options()); m_max_depth = get_class_instance_max_depth(ios.get_options()); + m_conservative = get_class_conservative(ios.get_options()); + if (m_conservative) + m_tc = mk_type_checker(env, m_ngen.mk_child(), false, OpaqueIfNotReducibleOn); + else + m_tc = mk_type_checker(env, m_ngen.mk_child(), m_relax); options opts = m_ios.get_options(); opts = opts.update_if_undef(get_pp_purify_metavars_name(), false); opts = opts.update_if_undef(get_pp_implicit_name(), true); @@ -324,6 +343,7 @@ constraint mk_class_instance_root_cnstr(std::shared_ptr unifier_config new_cfg(cfg); new_cfg.m_discard = false; new_cfg.m_use_exceptions = false; + new_cfg.m_conservative = C->m_conservative; auto to_cnstrs_fn = [=](substitution const & subst, constraints const & cnstrs) -> constraints { substitution new_s = subst; @@ -435,6 +455,7 @@ optional mk_class_instance(environment const & env, io_state const & ios, unifier_config new_cfg(cfg); new_cfg.m_discard = true; new_cfg.m_use_exceptions = true; + new_cfg.m_conservative = C->m_conservative; try { auto p = unify(env, 1, &c, C->m_ngen.mk_child(), substitution(), new_cfg).pull(); lean_assert(p); diff --git a/tests/lean/hott/class_loop.hlean b/tests/lean/hott/class_loop.hlean new file mode 100644 index 000000000..df4c62db8 --- /dev/null +++ b/tests/lean/hott/class_loop.hlean @@ -0,0 +1,26 @@ +constant (A : Type₁) +constant (hom : A → A → Type₁) +constant (id : Πa, hom a a) + +structure is_iso [class] {a b : A} (f : hom a b) := +(inverse : hom b a) +open is_iso + +set_option pp.metavar_args true +set_option pp.purify_metavars false + +definition inverse_id [instance] {a : A} : is_iso (id a) := +is_iso.mk (id a) (id a) + +definition inverse_is_iso [instance] {a b : A} (f : hom a b) (H : is_iso f) : is_iso (@inverse a b f H) := +is_iso.mk (inverse f) f + +constant a : A + +set_option class.trace_instances true + +definition foo := inverse (id a) + +set_option pp.implicit true + +print definition foo diff --git a/tests/lean/interactive/whnfinst.lean b/tests/lean/interactive/whnfinst.lean index ab5a457f7..cec0576cf 100644 --- a/tests/lean/interactive/whnfinst.lean +++ b/tests/lean/interactive/whnfinst.lean @@ -1,7 +1,7 @@ import logic open decidable -definition decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) +definition decidable_bin_rel [reducible] {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) section variable {A : Type} diff --git a/tests/lean/run/group4.lean b/tests/lean/run/group4.lean index 9ac8b8271..3a0856e03 100644 --- a/tests/lean/run/group4.lean +++ b/tests/lean/run/group4.lean @@ -120,7 +120,7 @@ calc ... = a * b * (c * d) : mul_assoc -- for test4b to work, we need instances at the level of the bundled structures as well -definition Monoid_Semigroup [coercion] (M : Monoid) : Semigroup := +definition Monoid_Semigroup [coercion] [reducible] (M : Monoid) : Semigroup := Semigroup.mk (Monoid.carrier M) _ theorem test4 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := diff --git a/tests/lean/run/group5.lean b/tests/lean/run/group5.lean index 0c3996dbd..9cb0f67c0 100644 --- a/tests/lean/run/group5.lean +++ b/tests/lean/run/group5.lean @@ -118,7 +118,7 @@ calc ... = a * b * (c * d) : !mul_assoc -- for test4b to work, we need instances at the level of the bundled structures as well -definition Monoid_Semigroup [coercion] (M : Monoid) : Semigroup := +definition Monoid_Semigroup [coercion] [reducible] (M : Monoid) : Semigroup := Semigroup.mk (Monoid.carrier M) _ theorem test4 {M : Monoid} (a b c d : M) : a * (b * c) * d = a * b * (c * d) := diff --git a/tests/lean/run/whnfinst.lean b/tests/lean/run/whnfinst.lean index ab5a457f7..cec0576cf 100644 --- a/tests/lean/run/whnfinst.lean +++ b/tests/lean/run/whnfinst.lean @@ -1,7 +1,7 @@ import logic open decidable -definition decidable_bin_rel {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) +definition decidable_bin_rel [reducible] {A : Type} (R : A → A → Prop) := Πx y, decidable (R x y) section variable {A : Type}