feat(library/tactic/class_instance_synth): conservative class-instance resolution: expand only definitions marked as reducible

closes #442

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

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),

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

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_pred [reducible] {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_rel  [reducible] {A : Type} (R : A → A → Type) := Π (a b : A), decidable (R a b)
-definition decidable_eq   (A : Type) := decidable_rel (@eq A)
+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)

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
 

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 -/

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

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 _ _

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 :=

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_pred [reducible] {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_rel  [reducible] {A : Type} (R : A → A → Prop) := Π (a b : A), decidable (R a b)
-definition decidable_eq   (A : Type) := decidable_rel (@eq A)
+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

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
 

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
 

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<pos_info>        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<class_instance_context>
         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<expr> 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);

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

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}

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) :=

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) :=

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}