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

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,
        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