## Stream: general

### Topic: library_search

#### Scott Morrison (Mar 05 2019 at 12:13):

... a present coming soon:

Here's a randomly chosen short mathlib proof:

lemma div_dvd_of_dvd {a b : ℕ} (h : b ∣ a) : (a / b) ∣ a :=
⟨b, (nat.div_mul_cancel h).symm⟩


Now, let's try

lemma div_dvd_of_dvd {a b : ℕ} (h : b ∣ a) : (a / b) ∣ a :=
by library_search


wait a few seconds, and observe the trace message div_dvd_of_dvd h, which is interesting I guess, but not that awesome.

However:

lemma div_dvd_of_dvd {a b : ℕ} (h : b ∣ a) : (a / b) ∣ a :=
by library_search [-div_dvd_of_dvd]


gives dvd.intro b (nat.div_mul_cancel h).

There were no hints here, just scraping all the imported declarations, and doing a neither-depth-nor-breadth-first search of the tree of applications of lemmas to the goal.

#### Scott Morrison (Mar 05 2019 at 12:15):

Now, this is pretty sensitive to how much you have imported! With just data.nat.prime imported, this example takes a second or so, but with everything-and-the-kitchen-sink imported it spirals out to 40s, which is obviously unacceptable. But I've barely started optimising / trimming the search tree, so it's possible this will still improve a lot.

#### Scott Morrison (Mar 05 2019 at 12:16):

Other examples are much less sensitive to the amount imported. For example I can find the proof of example {a b c : ℕ} (h₁ : a ∣ c) (h₂ : a ∣ b + c) : a ∣ b in about 1s with small imports, and 2s with lots of imports.

#### Scott Morrison (Mar 05 2019 at 12:17):

(That proof is (nat.dvd_add_iff_left h₁).mpr h₂)

#### Patrick Massot (Mar 05 2019 at 12:18):

It's very promising!

#### Patrick Massot (Mar 05 2019 at 12:18):

It's very exciting to see you are back to tactic writing!

#### Scott Morrison (Mar 05 2019 at 12:19):

Attempting to prepare examples for my students was getting discouraging. Also they are already upset about not being able to find lemmas. :-)

#### Scott Morrison (Mar 05 2019 at 12:19):

Also -- thanks to Simon and Keeley for help at key points, and Johan's constant encouragement. :-)

#### Scott Morrison (Mar 05 2019 at 12:19):

But there's still some work to get this polished, it's a mess at the moment!

#### Johan Commelin (Mar 05 2019 at 16:12):

@Scott Morrison I'm glad you interpret my nagging and whining as encouragement (-;
I'm very excited to see this! I really hope we will have a back in mathlib soon.

#### Patrick Massot (Mar 05 2019 at 17:37):

This is also how I collaborate with Simon

#### Johan Commelin (Apr 30 2019 at 17:49):

I had some people in my office today who attended Kevin's talk. They had never used Lean before, but they wanted to try it. I helped them setup the system, and they dove in. First thing they wanted to try: prove that the derivative of exp is exp. After we had the statement formalised, I told them about some basic tactics, and library_search. They loved it. It worked surprisingly often, which kept them addicted. Of course, when we got to the meat of the theorem, we gut stuck. But nevertheless: chapeau @Scott Morrison!
(I think Kevin would say that they went in instant Isabelle-mode.)

#### Kevin Buzzard (Apr 30 2019 at 18:17):

Proving the derivative of exp is exp is not something we can currently do, right?

#### Kevin Buzzard (Apr 30 2019 at 18:17):

We need that a power series can be differentiated term by term

#### Patrick Massot (Apr 30 2019 at 18:17):

we don't know that

#### Kenny Lau (Apr 30 2019 at 18:17):

that's just comparison test

#### Kevin Buzzard (Apr 30 2019 at 18:19):

Why doesn't someone do it if it's easy? We have done so much algebra. We need some analysts!

#### Mario Carneiro (Apr 30 2019 at 18:27):

we have basic exp inequalities already, right? so that's not needed

#### Mario Carneiro (Apr 30 2019 at 18:27):

In this case you need that exp x - 1 - x is O(x^2)

#### Sebastien Gouezel (May 20 2019 at 19:23):

library_search works extremely well most of the time (many thanks for this). However, I just got the following strange behavior

lemma continuous_at.preimage_mem_nhds {f : α → β} {x : α} {s : set β} (h : continuous_at f x)
(hs : s ∈ nhds (f x)) : f ⁻¹' s ∈ nhds x :=
begin
library_search
end


the output of library_search is exact mem_def.mpr (h s hs), which does not work. It should be exact mem_def.mpr (h hs) (or simply exact h hs).

#### Simon Hudon (May 20 2019 at 19:26):

Is it because s should be an implicit argument?

#### Sebastien Gouezel (May 20 2019 at 19:37):

It's complicated to say: there is a lot of nontrivial unfolding to be done.

#### Simon Hudon (May 20 2019 at 19:43):

You can see the function type of h by putting this into your proof script:

   do { get_local h >>= infer_type >>= whnf >>= trace }


#### Simon Hudon (May 20 2019 at 19:43):

(don't forget to open tactic)

#### Sebastien Gouezel (May 20 2019 at 19:51):

semi-implicit argument: ∀ ⦃a : set β⦄, a ∈ (nhds (f x)).sets → a ∈ (filter.map f (nhds x)).sets

#### Sebastien Gouezel (Nov 27 2019 at 19:34):

How would you prove

lemma no_way {𝕜 : Type*} [normed_field 𝕜]
{E : Type*} [normed_group E] [vector_space 𝕜 E] [normed_space 𝕜 E]
{F : Type*} [normed_group F] [vector_space 𝕜 F] [normed_space 𝕜 F] (f' : E →L[𝕜] F) :
f'.comp continuous_linear_map.id = f' :=


by simp doesn't work (obvious gap in the library that I will fill right away), so I tried library_search. It worked, giving me the following proof...

#### Sebastien Gouezel (Nov 27 2019 at 19:34):

... exact neg_inj rfl

#### Sebastien Gouezel (Nov 27 2019 at 19:35):

where neg_inj is

theorem neg_inj : ∀ {α : Type u} [_inst_1 : add_group α] {a b : α}, -a = -b → a = b


Lean is way too clever for me here to see a relationship between the question I ask and the answer I get.

#### Sebastien Gouezel (Nov 27 2019 at 19:38):

Indeed, - f'.comp continuous_linear_map.id = - f'is rfl, but f'.comp continuous_linear_map.id = f'is not...

#### Chris Hughes (Nov 27 2019 at 19:39):

cases f'; refl or ext; refl?

#### Sebastien Gouezel (Nov 27 2019 at 19:45):

Yes, the natural proof I would use is ext, refl, and it works fine. I was just amazed by the answer of library_search.

#### Johan Commelin (Nov 27 2019 at 20:49):

Isn't it nice that Lean is getting clever? That's what all the mathematicians want, right?

#### Floris van Doorn (Nov 27 2019 at 20:53):

This is one of the strange artifacts from Lean not having the definitional eta rule for structures. The eta rule for (say) products states that x : prod A B is definitionally equal to (x.1, x.2). A rule like this makes sense. After all, the first and second projections of both x and (x.1, x.2) are already definitionally equal in Lean, so it makes sense to say that they are definitionally equal.

In your case you have again two structures, where all projections are definitionally equal. This means that if you perform any transformation on both the LHS and the RHS that only take projections into account (like neg), you get something definitionally equal, which is why the proof that library_search found works.

Originally the reason that Lean didn't get this rule was that the developers saw no compelling reason to add it. A while later I stated some (IMO) compelling reasons, but it never got added.

#### Patrick Massot (Nov 27 2019 at 20:54):

This behavior of product never ceases to catch me by surprise.

#### Sebastien Gouezel (Nov 27 2019 at 21:04):

Even if you added this rule for structures, I guess it would not ensure that id and lambda x, (x.1, x.2) are defeq, right? (in manifolds, it would have helped me a lot if this had been true).

#### Sebastien Gouezel (Nov 27 2019 at 21:10):

I think it is the first time I understand what this eta rule for structures is. Thanks! Now I just need to understand alpha, beta, gamma, delta, and how many others do you have?

#### Johan Commelin (Nov 27 2019 at 21:11):

Ooh, and then there are Y and S and K combinators, in case you get bored....

#### Kevin Buzzard (Nov 27 2019 at 21:27):

I learnt about these alpha beta things when I was trying to get automation working in the definition of the complex numbers

#### Kevin Buzzard (Nov 27 2019 at 21:28):

All proofs of eg associativity of multiplication are "check on real and imaginary parts" so it was precisely these projections in a very concrete situation

#### Floris van Doorn (Nov 27 2019 at 21:57):

Here is a cheat sheet:

α-equivalence: λ x, f x ≡ λ y, f y
β-reduction: (λ x, f x) a ≡ f a
δ-reduction: id ≡ λ {α : Sort*} (x : α), x (i.e. unfold a definition)
η-reduction: λ x, f x ≡ f (η-expansion is in the other direction)
ι-reduction: nat.rec P₀ Pₛ 0 ≡ P₀ and nat.rec P₀ Pₛ n.succ ≡ Pₛ n (nat.rec P₀ Pₛ n)
ζ-reduction: (let x := a in f x) ≡ f a
β-reduction (for records): (x, y).1 ≡ x and (x, y).2 ≡ y
η-reduction (for records): (x.1, x.2) ≡ x


all reduction rules are directed (from left to right), but if you take the congruence closure (that is, the smallest equivalence relation that respects all ways to make a term), you get the corresponding equivalence. "Definitional equality" is the smallest congruence closure containing all of the above relations (except η-reduction for records).

#### Floris van Doorn (Nov 27 2019 at 21:58):

Usually they are written a bit differently, using substitution instead of function application, but that will probably be more confusing. But just to be clear: something like β-reduction also applies if the term inside the lambda is not a application - so something like (λ x, x) a ≡ a is an instance of β-reduction

#### Chris Hughes (Nov 27 2019 at 22:25):

Why do the two etas and betas have the same name? Isn't the second beta just a combination of delta and iota?

#### Mario Carneiro (Nov 27 2019 at 22:46):

If you view the projections as primitive, they are different

#### Floris van Doorn (Nov 27 2019 at 22:53):

Yes, the second beta is indeed a combination of delta and iota in Lean. This is because products are defined as a inductive type. If records are primitive (not special cases of inductive types) then it could be its own rule.

Sometimes ι-reduction is also called "β-reduction for inductive types". To explain this terminology, we have to take a step back.
In type theory, to each type former, there is a number of rules associated to it. I will explain these rules by using the natural numbers as an example.

• (Type) formation rules: when can I form this type? For natural numbers, we have nat : Type
• (Term) introduction rules: when can I form an element of this type? For natural numbers: 0 : nat and if n : nat then n.succ : nat
• (Term) elimination rules: how can I eliminate out of this type? For natural numbers this is nat.rec.
• Then there are computation rules. These have two flavors

- What happens if I apply an elimination rule to an introduction rule? In general, this is sometimes called beta-reduction (since it corresponds to beta-reduction when talking about functions). For natural numbers, these are the iota-reduction rules mentioned above.
- What happens if I apply an introduction rule to an elimination rule? These are called eta-conversion rules. The natural numbers don't really have them (I think you can write something like an eta-rule down, but it's not that useful). For functions and products, it's the eta rule I mentioned above.

This is the reason that different rules have the name beta/eta-reductions: they are the corresponding reduction rules for those type formers.

#### Floris van Doorn (Nov 27 2019 at 22:54):

If you want more information than my summary, you can look e.g. here: https://ncatlab.org/nlab/show/type+theory#Syntax

#### Sebastian Ullrich (Nov 28 2019 at 12:43):

Just for comparison, Agda has definitional eta for some structures. Some termination (for coinductive structures, so not very relevant) and performance (even for pairs, unsolved?) issues are documented at https://github.com/agda/agda/issues/2436.

#### Reid Barton (Nov 28 2019 at 15:28):

Coq also has opt-in definitional eta for structures.

#### Abhimanyu Pallavi Sudhir (Dec 12 2019 at 18:08):

Does library_search check for every possible paranthetic nesting structure of the hypothesis? Or just superficial combinations and repetitions?

#### Johan Commelin (Dec 12 2019 at 18:16):

I don't think it does anything with associativity, if that is what you mean. The goal has to match perfectly.

#### Abhimanyu Pallavi Sudhir (Dec 12 2019 at 18:19):

I mean, if we have hypothesis H1 H2 H3 and goal G, and we have a library theorem L such that L (H1 H2) H3 = G, will the tactic find L?

Yes.

#### Patrick Massot (Dec 12 2019 at 18:22):

Or maybe I don't understand the question.

#### Johan Commelin (Dec 12 2019 at 18:58):

I'm actually not sure if library_search will close that. suggest hopefully will do it. But as far as I know library_search only tries to close the immediate hypotheses of L with existing hypotheses in your context. There is no recursion.

#### Johan Commelin (Dec 12 2019 at 18:59):

suggest wouldn't close the goal either, but would hopefully suggest refine L _ H3. And after that suggest and library_search should both close the goal via solve_by_elim

#### Sebastien Gouezel (Mar 01 2020 at 11:37):

I am always amazed by library_search. I thought it was only supposed to try to apply all lemmas in the library, filling them with things in the context. But look at what happens in the following situation:

lemma card (n : ℕ) : fintype.card (ordered_partition2 n) = fintype.card (finset (fin (n-1))) :=
begin
let : ordered_partition2 n ≃ finset (fin (n - 1)) := order_partition2_equiv n,
library_search
end


I wanted to get the name of the lemma saying that if one has an equiv between two fintypes they have the same cardinal, so I asked library_search in my context. Its answer is:

Try this: exact list.length_map
⇑{to_fun := ⇑(equiv.symm (order_partition2_equiv n)),
inj := fintype.of_bijective._proof_1 ⇑(equiv.symm (order_partition2_equiv n))
(equiv.bijective (equiv.symm (order_partition2_equiv n)))}
(list.pmap finset.mk (multiset.powerset_aux (list.fin_range (n - 1))) (finset.powerset._proof_1 finset.univ))


and it works perfectly well :) (Still, I will rather go with exact fintype.card_congr this)

#### Mario Carneiro (Mar 01 2020 at 12:26):

I think it unfolded some proof in the library to get that

plagiarization!

#### Mario Carneiro (Mar 01 2020 at 12:33):

I don't know what order_partition2 is so I can't completely reverse engineer it but the last bit, list.pmap finset.mk ... is the list that results if you ask what list enumerates finset.powerset (@finset.univ (fin (n-1)))

#### Sebastien Gouezel (Mar 01 2020 at 12:38):

order_partition2 n is a structure, defined as

structure ordered_partition2 (n : ℕ) :=
(boundaries : finset (fin n.succ))
(zero_mem   : (0 : fin n.succ) ∈ boundaries)
(last_mem   : (fin.last n ∈ boundaries))


I constructed an equiv between this and finset (fin (n-1)) (the one that is used in the proof). So, I am not surprised that an enumeration of the powerset of fin (n-1) shows up in the proof found by library_search.

On an unrelated note, I was surprised that I could not prove that this is a fintype directly. Even

structure my_struct (n : ℕ) :=
(my_finset : finset (fin n))

instance (n : ℕ) : fintype (my_struct n) := by apply_instance


fails...

#### Sebastien Gouezel (Mar 01 2020 at 12:39):

While

instance inst2 (n : ℕ) : fintype (finset (fin n)) := by apply_instance


works, of course.

#### Mario Carneiro (Mar 01 2020 at 12:40):

There is no tactic for proving arbitrary inductive types to be finite. (I think @Jeremy Avigad was working on something like this...) You have to manually cobble together the constructions in fintype.lean

#### Mario Carneiro (Mar 01 2020 at 12:41):

Certainly apply_instance will not work, there is no typeclass instance to find

#### Mario Carneiro (Mar 01 2020 at 12:42):

Conceivably it might work with a hypothetical @[derive fintype] on the definition of order_partition2

#### Mario Carneiro (Mar 01 2020 at 12:45):

But if you just use the existing constructors instead of defining a new type, typeclass inference works fine:

instance foo (n : ℕ) : fintype {
boundaries : finset (fin n.succ) //
(0 : fin n.succ) ∈ boundaries ∧
(fin.last n ∈ boundaries)} := by apply_instance


#### Mario Carneiro (Mar 01 2020 at 12:49):

and that is also the easiest method of proof:

instance foo (n : ℕ) : fintype (ordered_partition2 n) :=
fintype.of_equiv {boundaries : finset (fin n.succ) //
(0 : fin n.succ) ∈ boundaries ∧ (fin.last n ∈ boundaries)}
⟨λ ⟨a,b,c⟩, ⟨a,b,c⟩, λ ⟨a,b,c⟩, ⟨a,b,c⟩, λ ⟨a,b,c⟩, rfl, λ ⟨a,b,c⟩, rfl⟩


#### Sebastien Gouezel (Mar 01 2020 at 13:19):

Sure, I know how to do it with a subtype. But since I need the exact cardinality, I have anyway to construct the equiv with fin (n-1). I was just surprised the fintype instance didn't work out of the box, because in general almost everything works out of the box!

#### Mario Carneiro (Mar 01 2020 at 14:26):

Well, my point is that as you wrote it it's impossible to have anything work out of the box unless you go into lean to change how the structure command works. You would have to put a @[derive fintype] annotation or trigger a tactic by some similar method... and someone would have to write that tactic

#### Jeremy Avigad (Mar 01 2020 at 20:03):

No, I am not working on tactics for inductive types. What Mario is thinking of is this: there is a general strategy for showing finitely branching inductive types are encodable: https://github.com/leanprover-community/mathlib/blob/master/archive/examples/prop_encodable.lean. There is a lot of boilerplate involved, but that sort of thing can also be automated. (But I am not planning to do it.)

#### Yury G. Kudryashov (Mar 02 2020 at 02:13):

@Sebastien Gouezel Where do you use ordered_partition2?

#### Sebastien Gouezel (Mar 02 2020 at 06:53):

I am working on analytic functions (in good generality, i.e., possibly on Banach spaces). These are the functions that have locally an expansion f(x + h) = \Sigma_n f_n(h, ..., h) where f_n is a continuous n-multilinear map. To show that the composition of analytic functions is analytic, you need to write the composition of two such things as a series of multilinear maps, which is kind of dirty. I use ordered_partition2 there.

#### Kenny Lau (Apr 09 2020 at 10:42):

I would like to personally thank @Scott Morrison for creating this incredibly useful library_search tactic (and others who contributed to this tactic).

#### Kenny Lau (Apr 09 2020 at 10:44):

I typed:

theorem real.exists_one_div (r : ℝ) (hr : 0 < r) : ∃ n : ℕ, (1/(n+1) : ℝ) < r :=
by library_search


and then I found exactly the name of the lemma exists_nat_one_div_lt that I couldn't find by trying real.exists_ and other real. prefixes

#### Scott Morrison (Apr 09 2020 at 10:48):

You're welcome. I really should get back to work on it; I think it easily could be better still.

#### Sebastien Gouezel (Jul 13 2020 at 11:54):

I am surprised that library_search fails on that one:

import analysis.analytic.basic

example : (0 : ennreal) ≤ 1 :=
begin
-- library_search!, fails
exact zero_le _,
end


@Scott Morrison , does it look normal to you?

#### Scott Morrison (Jul 13 2020 at 11:54):

Nope, that sounds like a bug!

#### Sebastien Gouezel (Jul 15 2020 at 07:52):

It seems that something is broken currently with library_search. Here is another example where it doesn't work:

import analysis.analytic.basic

lemma foo : is_open (set.Ioo (0 : ℝ) 1) :=
begin
-- library_search!,  -- fails
exact is_open_Ioo
end


It turns out that it fails for essentially all one-liners like this in the manifold exercises for Friday. It is not a real problem, though, because we have a wonderful naming convention, and people should get used to it sooner than later :-)

#### Reid Barton (Jul 15 2020 at 11:33):

This one looks like the apply bug, and potentially the one above as well

#### Reid Barton (Jul 15 2020 at 11:34):

indeed

{ le          := λ o₁ o₂ : option α, ∀ a ∈ o₂, ∃ b ∈ o₁, b ≤ a }


#### Julian Külshammer (Jul 17 2020 at 09:42):

Here is another bug report from Kevin's breakout room, this time regarding library_search:

import topology.metric_space.basic

open_locale classical filter topological_space

namespace lftcm
open filter set

def at_top : filter ℕ :=
{ sets := {s | ∃ a, ∀ b, a ≤ b → b ∈ s},
univ_sets := begin
sorry
end,
sets_of_superset := begin
rintros x y ⟨a, ha⟩ hxy,
use a,
intros b hb,
library_search
end,
inter_sets := begin
sorry
end}

end lftcm


Lean suggests exact hxy b (ha b hb) which doesn't work (removing the b makes it work).

#### Rob Lewis (Jul 17 2020 at 09:43):

This was just discovered in exactly the same context :) #3422

#### Shing Tak Lam (Jul 17 2020 at 09:45):

Is this the same bug as #3093?

#### Rob Lewis (Jul 17 2020 at 09:46):

Oh, yes, I'm pretty sure it is!

#### Kevin Buzzard (Jul 17 2020 at 10:40):

As far as I can see, It's because \subseteq unfolds to \forall {{a}}, ... and library_search inserts the variable but Lean doesn't want it

#### Kevin Buzzard (Jul 17 2020 at 10:41):

Aah yes I see now that this has been well diagnosed

#### Shing Tak Lam (Jul 17 2020 at 11:26):

Now I don't think the bug is in library_search. Here's an example which doesn't use library_search which I think does the same thing for this goal.

import tactic

open tactic

namespace tactic.interactive

meta def st : tactic unit :=
do
g ← get_goals,
tactic.solve_by_elim,
trace g

end tactic.interactive

example (α : Type) (S T : set α) (a : α) (ha : a ∈ S) (hst : S ⊆ T) : a ∈ T :=
begin
st -- Output: [hst a ha]
end


#### Shing Tak Lam (Jul 17 2020 at 11:28):

This also has the same behaviour (and the same if tauto is replaced by solve_by_elim)

example (α : Type) (S T : set α) (a : α) (ha : a ∈ S) (hst : S ⊆ T) : a ∈ T :=
begin
show_term { tauto } -- exact hst a ha
end


#### Shing Tak Lam (Jul 17 2020 at 11:36):

and the same even if I provide the term to use with exact

example (α : Type) (S T : set α) (a : α) (ha : a ∈ S) (hst : S ⊆ T) : a ∈ T :=
begin
show_term { exact hst ha } -- exact hst a ha
end


#### Shing Tak Lam (Jul 17 2020 at 11:38):

in fact, this works without any mathlib imports, so it's probably an issue in core Lean

open tactic

meta def st : tactic unit :=
do
g :: _ ← get_goals,
e ← to_expr (hst ha),
tactic.exact e,
trace g

example (α : Type) (S T : set α) (a : α) (ha : a ∈ S) (hst : S ⊆ T) : a ∈ T :=
begin
st
end


#### Rob Lewis (Jul 17 2020 at 11:41):

Yes, I think Gabriel saw this in #3093:

This looks like a bug in the pretty-printer, which apparently prints hst ha incorrectly.

The pretty printer affects everything you've shown and is part of the Lean system.

#### Shing Tak Lam (Jul 17 2020 at 11:42):

So should I close the mathlib issue and make one in leanprover-community/lean instead?

#### Rob Lewis (Jul 17 2020 at 11:43):

Definitely make an issue in the lean repo and link the mathlib one! But I think you can leave the mathlib one open.

#### Rob Lewis (Jul 17 2020 at 11:43):

Since library_search is where this bug will appear most often.

#### Eric Wieser (Jul 17 2020 at 15:36):

I think github lets you move issues between repos in the same org

Last updated: May 10 2021 at 19:16 UTC