Zulip Chat Archive

Stream: new members

Topic: Proof search


view this post on Zulip 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?

view this post on Zulip Chris Hughes (Oct 13 2019 at 13:06):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Oct 15 2019 at 01:04):

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

view this post on Zulip Johan Commelin (Oct 15 2019 at 01:59):

@Lucas Allen Hooray! Nice work!

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 15 2019 at 08:48):

There is squeeze_simp that will report what the simplifier did.

view this post on Zulip Johan Commelin (Oct 15 2019 at 08:48):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 15 2019 at 09:27):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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 *

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Oct 15 2019 at 09:36):

Are you rewriting by smul or smul_add?

view this post on Zulip Johan Commelin (Oct 15 2019 at 09:37):

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

view this post on Zulip Johan Commelin (Oct 15 2019 at 09:38):

That seems like a useful lemma for you

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Marko Grdinić (Oct 15 2019 at 13:34):

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

view this post on Zulip Johan Commelin (Oct 15 2019 at 13:35):

Weird

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 15 2019 at 13:53):

It's really powerful!

view this post on Zulip Marc Huisinga (Oct 15 2019 at 13:56):

maybe some file you imported also imports the algebra files.

view this post on Zulip 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.")

view this post on Zulip Marko Grdinić (Oct 15 2019 at 14:06):

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

view this post on Zulip 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.

view this post on Zulip Lucas Allen (Oct 15 2019 at 22:12):

Lucas Allen Hooray! Nice work!

Thanks :slight_smile:

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 16 2019 at 13:39):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 16 2019 at 15:14):

I thought that refine_list made this patch

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 16 2019 at 15:23):

Then I hereby warn the reviewers (-;

view this post on Zulip Kevin Buzzard (Oct 16 2019 at 19:34):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Oct 16 2019 at 22:11):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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