# Zulip Chat Archive

## 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, add_comm, list.sum_repeat, list.map_const, nat.cast_add, nat.cast_one, list.map] at *

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

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

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

#### 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, simp [add_monoid.smul] at *, ring at *, unfold monoid.pow, rw this, ring, simp [add_monoid.smul_add], 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.

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

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: Dec 20 2023 at 11:08 UTC