## Stream: new members

### Topic: Proof search

#### Marko Grdinić (Oct 13 2019 at 12:06):

I am working on a little proof and need to rewrite sqr (a - b) into sqr a - 2 * a * b + sqr b. Now of course I could define a postulate for this like I did in the Agda proof I am rewriting, but I am guessing that this is proven in the mathlib and Lean has some kind of proof search. In Coq I could write something like Search (forall a b, sqr (a - b) = sqr a - 2 * a * b + sqr b). What functionality for this sort of thing does Lean have?

#### Chris Hughes (Oct 13 2019 at 13:06):

The ring tactic should solve this. You'll need to use ^2 instead of sqr though.

#### Floris van Doorn (Oct 13 2019 at 13:24):

For searching, library_search is convenient:

import data.rat.basic tactic.library_search

example {a b : ℚ} : (a + b) * (a + b) = a * a + 2 * a * b + b * b :=
by library_search -- exact add_mul_self_eq a b


#### Floris van Doorn (Oct 13 2019 at 13:26):

Oh wait, the minus sign got lost in translation. I don't think that particular lemma is in the library yet.

#### Marko Grdinić (Oct 14 2019 at 15:10):

Let me bring this subject up again as I am having some trouble.

1 goal
c x : ℚ,
l : list ℚ,
E.const_none : ∀ (l : list ℚ), monoid.pow c (list.length l) * rat.inv ↑(list.length l) = c ∨ l = list.nil
⊢ monoid.pow c (1 + list.length l) * rat.inv (1 + ↑(list.length l)) = c


Right now I have something like this in my tactic state and I want to search all the proofs involving monoid.pow. What would be the best way to go about this. library_search is not quite equivalent to Coq's Search as it is a tactic that fails or succeeds. Coq's Search can print out every function in which a term appears.

#### Alex J. Best (Oct 14 2019 at 15:31):

You can also use set_option trace.library_search true to have library_search list of all possible results matching a given type. Alternatively you can make an educated guess at names with a bit of grepping / text searching in vscode or whatever to find things, this is surprisingly effective because the mathlib naming scheme is quite rigid.

#### Kevin Buzzard (Oct 14 2019 at 15:36):

In tactic mode you can try exact monoid.pow and then ctrl-space and then maybe esc and ctrl-space again for good measure. This might give you a list of helpful things.

#### Marko Grdinić (Oct 14 2019 at 15:48):

Coq's Search can print out every function in which a term appears.

Actually, what I meant to write here is that it can print out every function in whose type a term appears which is very useful for searching through theorems of equalities. It is a powerful thing. I am not sure if it is on the requested features list, but if it is not, it definitely should be.

@Alex J. Best

You can also use set_option trace.library_search true to have library_search list of all possible results matching a given type.

I am not sure how to control library_search to just search it for equalities involving monoid.pow. Right now I just tried it and it gave me what seems to be an unordered list of 4k lemmas. It is not really quite the thing I am looking for.

@Kevin Buzzard

In tactic mode you can try exact monoid.pow and then ctrl-space and then maybe esc and ctrl-space again for good measure. This might give you a list of helpful things.

In VS Code that is the trigger for autosuggestion, I am not sure if you are using Emacs what is it there. One thing I do know is that Ctrl + click dives me into the implementation of a function which is useful, but not quite enough for me.

#### Marko Grdinić (Oct 14 2019 at 16:13):

For examples how Coq's Search works, check this out: https://softwarefoundations.cis.upenn.edu/vfa-current/Perm.html

It is the first chapter of vol 3 of Software Foundations.

#### Johan Commelin (Oct 14 2019 at 16:24):

@Marko Grdinic You are trying to prove that c ^ something = c. You want to do this be claiming that something = 1. You can guess the name of the lemma that says c ^ 1 = c: it will/should/must/shall/ought be called pow_one. So you proceed by saying convert pow_one c. Now you are left with proving something = 1.

#### Andrew Ashworth (Oct 14 2019 at 16:35):

Yes. Many of us are aware of how library_search is different from Coq search. Actually there was some brief talk awhile back about ambitious projects like coding up a Hoogle-alike, but it never went anywhere because most people are OK with what we have (some mixture of grep, library_search, and VSCode autocomplete + naming conventions). That is not to say that if you wanted to have a Search tactic in mathlib, that pull request would not be accepted. Although I'm not a maintainer, but generally they are pretty receptive to these things.

#### Scott Morrison (Oct 14 2019 at 23:43):

@Lucas Allen is almost ready with a refine_list tactic, which is like library_search but allows leaving holes. Hopefully it will be helpful!

#### Scott Morrison (Oct 15 2019 at 01:04):

oh, and there it is: https://github.com/leanprover-community/mathlib/pull/1552

#### Johan Commelin (Oct 15 2019 at 01:59):

@Lucas Allen Hooray! Nice work!

#### Marko Grdinić (Oct 15 2019 at 08:47):

@Johan Commelin

You are trying to prove that c ^ something = c. You want to do this be claiming that something = 1. You can guess the name of the lemma that says c ^ 1 = c: it will/should/must/shall/ought be called pow_one. So you proceed by saying convert pow_one c. Now you are left with proving something = 1.

Actually, monoid.pow is misleading here, it really is multiplication under the hood. What I am trying to prove is more like c * (1 + n) / (1 + n) = c. What makes this situation confusing is that the simplifier got it into this strange form using I do not know which rewrites, and I am not sure what the steps for dealing with this should be. It cannot be solved by ring here. Maybe I will try simplifying it step by step in addition to going through the lemmas for rat.

#### Johan Commelin (Oct 15 2019 at 08:48):

There is squeeze_simp that will report what the simplifier did.

#### Johan Commelin (Oct 15 2019 at 08:48):

And I agree that this seems a very crazy end result be the simplifier.

#### Marko Grdinić (Oct 15 2019 at 09:24):

@Johan Commelin
I think I am looking at some bug here. I thought that monoid.pow was multiplication, but it turns out it really is a power function.

theorem list.eq.repeat (c : rat) : ∀ (l : list rat), list.sum (list.map (fun _, c) l) = c * list.length l
| [] := by simp
| (x :: l) :=
by { -- list.sum (list.map (λ (_x : ℚ), c) (x :: l)) = c * ↑(list.length (x :: l))
simp at *, -- add_monoid.smul (1 + list.length l) c = c * (1 + ↑(list.length l))
ring at *, -- add_monoid.smul (list.length l + 1) c = (↑(list.length l) + 1) * c
unfold add_monoid.smul at *, -- monoid.pow c (list.length l + 1) = (↑(list.length l) + 1) * c
unfold monoid.pow, -- c * monoid.pow c (list.length l) = (↑(list.length l) + 1) * c
rw list.eq.repeat, -- c * (↑(list.length l) * c) = (↑(list.length l) + 1) * c
ring, -- c * (c * ↑(list.length l)) = c * ↑(list.length l) + c
}


Something is not right here.

#### Johan Commelin (Oct 15 2019 at 09:27):

What is the output if you replace the first simp with squeeze_simp?

#### Johan Commelin (Oct 15 2019 at 09:28):

You want to rw by add_monoid.smul_add, so probably you can add that to simp

#### Johan Commelin (Oct 15 2019 at 09:29):

The place where everything goes bonkers is unfold add_monoid.smul, because it switches you from additive to multiplicative notation. Reason: add_monoid.smul is defined to be monoid.pow on multiplicative M, where M is your additive monoid.

#### Marko Grdinić (Oct 15 2019 at 09:33):

What is the output if you replace the first simp with squeeze_simp?

variance.lean:72:8: information trace output
simp only [list.repeat,
list.length,
list.sum_repeat,
list.map_const,
nat.cast_one,
list.map] at *


#### Marko Grdinić (Oct 15 2019 at 09:36):

The effect of that is the same as unfolding it like I am doing now.

The place where everything goes bonkers is unfold add_monoid.smul, because it switches you from additive to multiplicative notation.

So what you are saying is that the *s are actually +s on the left side of the equality?

#### Johan Commelin (Oct 15 2019 at 09:36):

Are you rewriting by smul or smul_add?

#### Johan Commelin (Oct 15 2019 at 09:37):

https://github.com/leanprover-community/mathlib/blob/494132e1ebdba300a43d66e19ddc5b724fd20129/src/algebra/group_power.lean#L143

#### Johan Commelin (Oct 15 2019 at 09:38):

That seems like a useful lemma for you

#### Johan Commelin (Oct 15 2019 at 09:38):

It's not tagged as a simp-lemma. So you could add it to the simp-set manually.

#### Johan Commelin (Oct 15 2019 at 09:39):

If you then also add list.eq.repeat (your induction hypothesis) to the simp set, it might be able to close the goal completely

#### Johan Commelin (Oct 15 2019 at 09:41):

Also, your lemma doesn't really use that c is a rat. So you could state it for any semiring I guess

#### Marko Grdinić (Oct 15 2019 at 09:52):

Thanks.

theorem list.eq.repeat (c : rat) : ∀ (l : list rat), list.sum (list.map (fun _, c) l) = c * list.length l
| [] := by simp
| (x :: l) :=
by {
have := list.eq.repeat l,
ring at *,
unfold monoid.pow,
rw this,
ring,
refl
}


This goes through. I still find this confusing though. I have no idea why the notation suddenly changed mid way. How does that work? Is there a way print out the goal without the operators?

#### Alex J. Best (Oct 15 2019 at 10:06):

Is this what you want set_option pp.notation false. Example:

set_option pp.notation false

#check 1 ∈ (@set.univ ℕ)
-- has_mem.mem 1 set.univ : Prop


#### Johan Commelin (Oct 15 2019 at 10:24):

@Marko Grdinic Don't do simp [add_monoid.smul] but put the smul_add there instead. I would hope that it would avoid all the ugly notation.

#### Marko Grdinić (Oct 15 2019 at 13:34):

@Johan Commelin
Putting it there right away does nothing. I need to unfold monoid.pow first.

Weird

#### Marko Grdinić (Oct 15 2019 at 13:51):

-- list.sum (list.map (λ (_x : ℚ), c) (x :: l)) = c * ↑(list.length (x :: l))
rw list.map_const, -- list.sum (list.repeat c (list.length (x :: l))) = c * ↑(list.length (x :: l))
rw list.sum_repeat -- add_monoid.smul (list.length (x :: l)) c = c * ↑(list.length (x :: l))


@[simp] theorem list.sum_repeat : ∀ (a : β) (n : ℕ), (list.repeat a n).sum = n • a is the function that leads into it. It is in algebra.group_power, while map_const is in list.basic. I am not sure why that rewriting is happening considering I had not imported any of the algebra files myself. The only import I have is data.rat. I guess this means that every file in the project can extend the namespace in such a manner.

Hmmm...definitely not what I expected. I expected that imports would be the main mechanism of information exchange between modules, but these extension definitions seem to be entirely separate from that. I am not sure if the manual said anything about this.

#### Johan Commelin (Oct 15 2019 at 13:53):

It's really powerful!

#### Marc Huisinga (Oct 15 2019 at 13:56):

maybe some file you imported also imports the algebra files.

#### Marc Huisinga (Oct 15 2019 at 13:57):

at least according to TPIL, simp only uses tagged lemmas from files that have been imported (https://leanprover.github.io/theorem_proving_in_lean/tactics.html#using-the-simplifier, "Once the attribute is applied, however, there is no way to remove it; it persists in any file that imports the one where the attribute is assigned.")

#### Marko Grdinić (Oct 15 2019 at 14:06):

I guess data.rat must be importing them then at some point.

#### Marko Grdinić (Oct 15 2019 at 14:53):

Here is an easier way of implementing the above function.

theorem list.eq.repeat (c : rat) (l : list rat) : list.sum (list.map (fun _, c) l) = c * list.length l :=
by { simp, rw add_monoid.smul_eq_mul _ c, ring }


All my difficulty here was not really understanding the difference between monoidal and regular multiplication. One can use add_monoid.smul_eq_mul to go between the two.

#### Lucas Allen (Oct 15 2019 at 22:12):

Lucas Allen Hooray! Nice work!

Thanks :slight_smile:

#### Marko Grdinić (Oct 16 2019 at 13:33):

example : ∀ (x : rat), x^2 = x*x := by library_search -- succeeds
example : ∀ (x : rat), x*x = x^2 := by library_search -- fails


library_search should really be adjusted so that both sides of equalities get tested. It has been useful so far though. In cases like looking for add_monoid.smul_eq_mul I was lucky that I got the sides right otherwise I would not even have realized that something was amiss.

#### Johan Commelin (Oct 16 2019 at 13:39):

I think there is currently a PR that tries symmetry in library search

#### Rob Lewis (Oct 16 2019 at 15:08):

I think there is currently a PR that tries symmetry in library search

I see an issue, but not a PR. Am I overlooking something? I'll review soon if I am.

#### Johan Commelin (Oct 16 2019 at 15:14):

I thought that refine_list made this patch

#### Rob Lewis (Oct 16 2019 at 15:18):

I don't see anything in the PR or added documentation that says that. If it does, it should be clarified! (Also it should probably be a separate PR.)

#### Johan Commelin (Oct 16 2019 at 15:18):

I saw <|> symmetry somewhere, and I guessed that was doing this patch. But I don't know meta code. So don't trust me.

#### Rob Lewis (Oct 16 2019 at 15:21):

You could be right. This is a dangerous thing to do. When that's merged, the behavior of library_search will change (and become slower), and it will be very hard to trace the cause, since it isn't mentioned in the commit name or the PR body.

#### Johan Commelin (Oct 16 2019 at 15:23):

Then I hereby warn the reviewers (-;

#### Kevin Buzzard (Oct 16 2019 at 19:34):

@Marko Grdinic the rule of thumb is that the RHS should be "simpler" then the LHS.

#### Lucas Allen (Oct 16 2019 at 22:09):

I think there is currently a PR that tries symmetry in library search

@Scott Morrison added symmetry to the apply_and_solve function in library_search while he was putting some final touches on refine_list.

#### Scott Morrison (Oct 16 2019 at 22:11):

Okay, let's yoink that symmetry back out of this PR, and add it separately later.

#### Scott Morrison (Oct 16 2019 at 22:11):

It really should have a performance optimisation put (run symmetry only once, not once for each lemma we try to apply...) anyway.

#### Lucas Allen (Oct 16 2019 at 22:17):

Okay, let's yoink that symmetry back out of this PR, and add it separately later.

I've removed symmetry from library_search in the refine_list PR.

#### Scott Morrison (Oct 16 2019 at 22:20):

@Lucas Allen, you should still explain in the top post that all the apparent changes to library_search are actually just refactoring so library_search and refine_list can share code, and (assuming this is correct), this PR doesn't change the behaviour of library_search.

#### Lucas Allen (Oct 16 2019 at 22:41):

Lucas Allen, you should still explain in the top post that all the apparent changes to library_search are actually just refactoring so library_search and refine_list can share code, and (assuming this is correct), this PR doesn't change the behaviour of library_search.

OK. I've modified the top post of the refine_list PR, and I made sure to mention what it's doing to library_search.

Last updated: May 06 2021 at 22:13 UTC