mod

Stream: new members

[Alex Zhang]

Has the already been in Lean?
def aux (a b: ℕ): a % b.succ < b.succ := sorry
How can I prove it?

[Johan Commelin]

Does by library_search prove it for you?

[Johan Commelin]

My guess is that it is called nat.mod_lt_self or something like that.

[Johan Commelin]

Maybe just nat.mod_lt

[Alex Zhang]

library_search fails for this example

[Huỳnh Trần Khanh]

def aux (a b: ℕ): a % b.succ < b.succ := @nat.mod_lt a b.succ $ nat.succ_pos b

[Johan Commelin]

Do you need the @?

[Johan Commelin]

docs#nat.mod_lt

[Johan Commelin]

I think a.mod_lt b.succ_pos should maybe also work

[Alex Zhang]

Why doesn't library search work for this case?

[Huỳnh Trần Khanh]

Because, well, it's dumb. You should use gptf instead. It's faster than library_search.

[Johan Commelin]

Alex Zhang said:

Why doesn't library search work for this case?

It has to combine two lemmas from the library. It can only use 1 lemma + local hypotheses to close the goal.

[Johan Commelin]

I guess that by { have := b.succ_pos, library_search } should actually work.

[Huỳnh Trần Khanh]

gptf is library_search on steroids. It finds the proof instantly.
Screenshot-from-2021-06-28-13.23.33.png

[Huỳnh Trần Khanh]

https://github.com/jesse-michael-han/lean-gptf

[Alex Zhang]

What file(s) do I need to import to use it?

[Johan Commelin]

It is not part of mathlib. So you need to follow the instruction in that github repo

[Kevin Buzzard]

It would never have occurred to me to use gptf for this. Is this thing a useful tool for learners?

[Alex Zhang]

Do I have to wait until I have received an API key to use gptf?

[Johan Commelin]

I think so, yes

[Damiano Testa]

Kevin, I do not know if Johan's comment was an answer to your question, but for me, the success rate for library_search increased a lot once I had an expectation of what lemmas it might find. For instance, I now know that with inequalities, if I have < in context and the result follow for \le, then library_search will likely work with have : \le := le_of_lt, but probably not otherwise.

A few months back, I would have simply said: "oh well, library_search is not helping me".

However, I am still intimidated by how to use gptf and, even though I would like to use it, I am afraid of installing it and breaking what I think is a fragile equilibrium of git and lean working at the same time! :upside_down:

[Johan Commelin]

My "yes" was a reply to Alex

[Julian Berman]

gptf can produce non-syntactically valid output (or syntactically valid but nonexistant lemma output), so I suspect it may confuse more than help for very new folks even though it is certainly super cool

[Julian Berman]

I can say though Damiano that I managed not to break anything by just putting it in a separate repository, it wants lean 3.26 anyhow IIRC, so that part at least I think is surmountable, it's definitely cool to play with

[Alex Zhang]

Does anyone know how long I usually need to wait to get an API key before starting trying this?

[Kevin Buzzard]

I think mine took about a week to arrive, I wouldn't hold your breath :-)

[Huỳnh Trần Khanh]

Alex Zhang said:

Does anyone know how long I usually need to wait to get an API key before starting trying this?

a week and the email looks like this, initially i didn't even know that i received an api key lol because the email was... so vague
anyway if you see something like this it means you received an api key and you should follow the instructions Screenshot-from-2021-06-28-15.18.25.png