feat(tactic/delta_instance): handle parameters and use in library (#1483

)

* feat(tactic/core): improve delta_instance handler

* feat(*): use delta_instance derive handler

* feat(tactic/delta_instance): cleaner handling of application under binders

* Revert "feat(tactic/delta_instance): cleaner handling of application under binders"

This reverts commit 4005a2f.

* comment apply_under_pis

* properly get unused name

* feat(tactic/delta_instance): run with high priority and don't run on inductives

* Update src/tactic/core.lean

Co-Authored-By: Floris van Doorn <fpvdoorn@gmail.com>

src/category_theory/comma.lean

@@ -190,14 +190,13 @@ end comma
 
 omit 𝒜 ℬ
 
+@[derive category]
 def over (X : T) := comma.{v₃ 0 v₃} (𝟭 T) (functor.of.obj X)
 
 namespace over
 
 variables {X : T}
 
-instance category : category (over X) := by delta over; apply_instance
-
 @[extensionality] lemma over_morphism.ext {X : T} {U V : over X} {f g : U ⟶ V}
   (h : f.left = g.left) : f = g :=
 by tidy
@@ -254,14 +253,13 @@ end
 
 end over
 
+@[derive category]
 def under (X : T) := comma.{0 v₃ v₃} (functor.of.obj X) (𝟭 T)
 
 namespace under
 
 variables {X : T}
 
-instance : category (under X) := by delta under; apply_instance
-
 @[extensionality] lemma under_morphism.ext {X : T} {U V : under X} {f g : U ⟶ V}
   (h : f.right = g.right) : f = g :=
 by tidy

src/data/nat/modeq.lean

@@ -11,6 +11,7 @@ namespace nat
 
 /-- Modular equality. `modeq n a b`, or `a ≡ b [MOD n]`, means
   that `a - b` is a multiple of `n`. -/
+@[derive decidable]
 def modeq (n a b : ℕ) := a % n = b % n
 
 notation a ` ≡ `:50 b ` [MOD `:50 n `]`:0 := modeq n a b
@@ -24,8 +25,6 @@ variables {n m a b c d : ℕ}
 
 @[trans] protected theorem trans : a ≡ b [MOD n] → b ≡ c [MOD n] → a ≡ c [MOD n] := eq.trans
 
-instance : decidable (a ≡ b [MOD n]) := by unfold modeq; apply_instance
-
 theorem modeq_zero_iff : a ≡ 0 [MOD n] ↔ n ∣ a :=
 by rw [modeq, zero_mod, dvd_iff_mod_eq_zero]
 

src/data/rel.lean

@@ -9,15 +9,13 @@ import tactic.basic data.set.lattice order.complete_lattice
 
 variables {α : Type*} {β : Type*} {γ : Type*}
 
+@[derive lattice.complete_lattice]
 def rel (α : Type*) (β : Type*) := α → β → Prop
 
 namespace rel
 
 variables {δ : Type*} (r : rel α β)
 
-instance : lattice.complete_lattice (rel α β) :=
-by unfold rel; apply_instance
-
 def inv : rel β α := flip r
 
 lemma inv_def (x : α) (y : β) : r.inv y x ↔ r x y := iff.rfl

src/field_theory/mv_polynomial.lean

@@ -200,11 +200,9 @@ namespace mv_polynomial
 universe u
 variables (σ : Type u) (α : Type u) [fintype σ] [discrete_field α] [fintype α]
 
+@[derive [add_comm_group, vector_space α]]
 def R : Type u := restrict_degree σ α (fintype.card α - 1)
 
-instance R.add_comm_group : add_comm_group (R σ α) := by dunfold R; apply_instance
-instance R.vector_space : vector_space α (R σ α) := by dunfold R; apply_instance
-
 noncomputable instance decidable_restrict_degree (m : ℕ) :
   decidable_pred (λn, n ∈ {n : σ →₀ ℕ | ∀i, n i ≤ m }) :=
 by simp only [set.mem_set_of_eq]; apply_instance

src/linear_algebra/dual.lean

@@ -14,18 +14,12 @@ namespace module
 variables (R : Type*) (M : Type*)
 variables [comm_ring R] [add_comm_group M] [module R M]
 
-def dual := M →ₗ[R] R
+@[derive [add_comm_group, module R]] def dual := M →ₗ[R] R
 
 namespace dual
 
 instance : has_coe_to_fun (dual R M) := ⟨_, linear_map.to_fun⟩
 
-instance : add_comm_group (dual R M) :=
-by delta dual; apply_instance
-
-instance : module R (dual R M) :=
-by delta dual; apply_instance
-
 def eval : M →ₗ[R] (dual R (dual R M)) := linear_map.id.flip
 
 lemma eval_apply (v : M) (a : dual R M) : (eval R M v) a = a v :=
@@ -43,7 +37,7 @@ variables {K : Type u} {V : Type v} {ι : Type w}
 variables [discrete_field K] [add_comm_group V] [vector_space K V]
 open vector_space module module.dual submodule linear_map cardinal function
 
-instance dual.vector_space : vector_space K (dual K V) := {..dual.module K V}
+instance dual.vector_space : vector_space K (dual K V) := { ..module.dual.inst K V }
 
 variables [decidable_eq ι]
 variables {B : ι → V} (h : is_basis K B)
@@ -205,7 +199,6 @@ begin
   rcases exists_is_basis_fintype h with ⟨b, hb, ⟨hf⟩⟩,
   resetI,
   rw [← hb.to_dual_to_dual, range_comp, hb.to_dual_range, map_top, to_dual_range _],
-  delta dual_basis,
   apply_instance
 end
 

src/tactic/core.lean

@@ -1154,8 +1154,24 @@ do e ← get_env,
   since it is expensive to execute `get_mathlib_dir` many times. -/
 meta def is_in_mathlib (n : name) : tactic bool :=
 do ml ← get_mathlib_dir, e ← get_env, return $ e.is_prefix_of_file ml n
+
+/-- auxiliary function for apply_under_pis -/
+private meta def apply_under_pis_aux (func arg : pexpr) : ℕ → expr → pexpr
+| n (expr.pi nm bi tp bd) := expr.pi nm bi (pexpr.of_expr tp) (apply_under_pis_aux (n+1) bd)
+| n _ :=
+  let vars := ((list.range n).reverse.map (@expr.var ff)),
+      bd := vars.foldl expr.app arg.mk_explicit in
+  func bd
+
+/--
+Assumes `pi_expr` is of the form `Π x1 ... xn, _`.
+Creates a pexpr of the form `Π x1 ... xn, func (arg x1 ... xn)`.
+All arguments (implicit and explicit) to `arg` should be supplied. -/
+meta def apply_under_pis (func arg : pexpr) (pi_expr : expr) : pexpr :=
+apply_under_pis_aux func arg 0 pi_expr
+
 /--
-Tries to derive unary instances by unfolding the newly introduced type.
+Tries to derive instances by unfolding the newly introduced type and applying type class resolution.
 
 For example,
 ```
@@ -1164,21 +1180,32 @@ For example,
 adds an instance `ring new_int`, defined to be the instance of `ring ℤ` found by `apply_instance`.
 
 Multiple instances can be added with `@[derive [ring, module ℝ]]`.
+
+This derive handler applies only to declarations made using `def`, and will fail on such a
+declaration if it is unable to derive an instance. It is run with higher priority than the built-in
+handlers, which will fail on `def`s.
 -/
-@[derive_handler] meta def delta_instance : derive_handler :=
-λ cls tp,
-(do tp' ← mk_const tp,
-   tgt ← to_expr ``(%%cls %%tp'),
-   (_, v) ← solve_aux tgt (delta_target [tp] >> apply_instance >> done),
-   v ← instantiate_mvars v,
-   nm ← get_unused_name $ tp ++
-     match tgt with
-     | expr.app (expr.const nm _) _ := nm
+@[derive_handler, priority 2000] meta def delta_instance : derive_handler :=
+λ cls new_decl_name,
+do env ← get_env,
+if env.is_inductive new_decl_name then return ff else
+do new_decl_type ← declaration.type <$> get_decl new_decl_name,
+   new_decl_pexpr ← resolve_name new_decl_name,
+   tgt ← to_expr $ apply_under_pis cls new_decl_pexpr new_decl_type,
+   (_, inst) ← solve_aux tgt
+     (intros >> reset_instance_cache >> delta_target [new_decl_name]  >> apply_instance >> done),
+   inst ← instantiate_mvars inst,
+   tgt ← instantiate_mvars tgt,
+   nm ← get_unused_decl_name $ new_decl_name ++
+     match cls with
+     -- the postfix is needed because we can't protect this name. using nm.last directly can
+     -- conflict with open namespaces
+     | (expr.const nm _) := (nm.last ++ "_1" : string)
      | _ := "inst"
      end,
-   add_decl $ mk_definition nm [] tgt v,
+   add_decl $ mk_definition nm inst.collect_univ_params tgt inst,
    set_basic_attribute `instance nm tt,
-   return tt) <|> return ff
+   return tt
 
 /-- `find_private_decl n none` finds a private declaration named `n` in any of the imported files.
 
@@ -1207,9 +1234,9 @@ do env ← get_env,
 
 open lean.parser interactive
 
-/-- `import_private foo from bar` finds a private declaration `foo` in the same file as `bar` 
-    and creates a local notation to refer to it. 
-    
+/-- `import_private foo from bar` finds a private declaration `foo` in the same file as `bar`
+    and creates a local notation to refer to it.
+
     `import_private foo`, looks for `foo` in all imported files. -/
 @[user_command]
 meta def import_private_cmd (_ : parse $ tk "import_private") : lean.parser unit :=

src/topology/uniform_space/compare_reals.lean

@@ -91,9 +91,8 @@ namespace compare_reals
 instead of the metric space one. We proved in rat.uniform_space_eq that they are equal,
 but they are not definitionaly equal, so it would confuse the type class system (and probably
 also human readers). -/
-def Q := ℚ
+@[derive comm_ring] def Q := ℚ
 
-instance : comm_ring Q := by unfold Q ; apply_instance
 instance : uniform_space Q := is_absolute_value.uniform_space (abs : ℚ → ℚ)
 
 /-- Real numbers constructed as in Bourbaki. -/

test/delta_instance.lean

@@ -3,8 +3,9 @@ Copyright (c) 2019 Robert Y. Lewis. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Robert Y. Lewis
 -/
+import data.set
 
-import tactic.core
+@[derive has_coe_to_sort] def X : Type := set ℕ
 
 @[derive ring] def T := ℤ
 
@@ -15,3 +16,9 @@ instance : binclass ℤ ℤ := ⟨_, _⟩
 @[derive [ring, binclass ℤ]] def U := ℤ
 
 @[derive λ α, binclass α ℤ] def V := ℤ
+
+@[derive ring] def id_ring (α) [ring α] : Type := α
+
+@[derive decidable_eq] def S := ℕ
+
+@[derive decidable_eq] inductive P | a | b | c