library_search

Stream: general

[Scott Morrison]

... 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]

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]

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]

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

[Patrick Massot]

It's very promising!

[Patrick Massot]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Johan Commelin]

@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]

This is also how I collaborate with Simon

[Johan Commelin]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

we don't know that

[Kenny Lau]

that's just comparison test

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Sebastien Gouezel]

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]

Is it because s should be an implicit argument?

[Sebastien Gouezel]

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

[Simon Hudon]

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]

(don't forget to open tactic)

[Sebastien Gouezel]

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

[Sebastien Gouezel]

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]

... exact neg_inj rfl

[Sebastien Gouezel]

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]

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

[Chris Hughes]

cases f'; refl or ext; refl?

[Sebastien Gouezel]

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]

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

[Floris van Doorn]

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]

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

[Sebastien Gouezel]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

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]

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]

If you view the projections as primitive, they are different

[Floris van Doorn]

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]

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

[Sebastian Ullrich]

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]

Coq also has opt-in definitional eta for structures.

[Abhimanyu Pallavi Sudhir]

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

[Johan Commelin]

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

[Abhimanyu Pallavi Sudhir]

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?

[Patrick Massot]

Yes.

[Patrick Massot]

Or maybe I don't understand the question.

[Johan Commelin]

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]

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]

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]

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

[Marc Huisinga]

plagiarization!

[Mario Carneiro]

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]

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]

While

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

works, of course.

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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]

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]

@Sebastien Gouezel Where do you use ordered_partition2?

[Sebastien Gouezel]

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]

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]

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]

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

[Sebastien Gouezel]

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]

Nope, that sounds like a bug!

[Sebastien Gouezel]

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]

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

[Reid Barton]

indeed

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

[Julian Külshammer]

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]

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

[Shing Tak Lam]

Is this the same bug as #3093?

[Rob Lewis]

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

[Kevin Buzzard]

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]

Aah yes I see now that this has been well diagnosed

[Shing Tak Lam]

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]

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]

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]

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]

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]

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

[Rob Lewis]

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]

Since library_search is where this bug will appear most often.

[Eric Wieser]

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

[Siyuan Yan]

Lean learner here, how do I write my claim and do a library search in the middle of a proof? currently, I write my claim as a separate lemma and it feels too verbose.

[Scott Morrison]

have : X := by library_search

[Siyuan Yan]

that's cool thanks!

[Martin Dvořák]

You can also write stuff like specialize foo x (by library_search) or convert_to foo bar baz, library_search in the middle of your proof.