Proof search

Stream: new members

[Marko Grdinić]

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]

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

[Floris van Doorn]

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]

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

[Marko Grdinić]

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]

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]

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

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

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]

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

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]

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

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

[Johan Commelin]

@Lucas Allen Hooray! Nice work!

[Marko Grdinić]

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

There is squeeze_simp that will report what the simplifier did.

[Johan Commelin]

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

[Marko Grdinić]

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

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

[Johan Commelin]

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

[Johan Commelin]

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

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

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]

Are you rewriting by smul or smul_add?

[Johan Commelin]

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

[Johan Commelin]

That seems like a useful lemma for you

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Marko Grdinić]

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]

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]

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

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

[Johan Commelin]

Weird

[Marko Grdinić]

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

It's really powerful!

[Marc Huisinga]

maybe some file you imported also imports the algebra files.

[Marc Huisinga]

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

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

[Marko Grdinić]

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]

Lucas Allen Hooray! Nice work!

Thanks :slight_smile:

[Marko Grdinić]

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]

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

[Rob Lewis]

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]

I thought that refine_list made this patch

[Rob Lewis]

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]

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]

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]

Then I hereby warn the reviewers (-;

[Kevin Buzzard]

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

[Lucas Allen]

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]

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

[Scott Morrison]

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

[Lucas Allen]

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]

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

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.