## Stream: new members

### Topic: help me find lemmas

#### Scott Morrison (Nov 24 2018 at 00:39):

Surely these are somewhere?

lemma le_pred_of_lt {n m : ℕ} (h : n < m) : n ≤ m - 1 := sorry
lemma pred_le_self (n : ℕ) : n - 1 ≤ n := sorry


#### Reid Barton (Nov 24 2018 at 00:43):

Second is a special case of nat.sub_le, do you specifically need it for 1?

#### Scott Morrison (Nov 24 2018 at 00:50):

Thanks, that'll do fine for the second.

#### Scott Morrison (Nov 24 2018 at 08:35):

We seem to have le_sub_iff_add_le for commutative groups, but not le_sub_of_add_le for nat?

#### Scott Morrison (Nov 24 2018 at 08:36):

Am I missing something? I want n + k ≤ b implies n ≤ b - k.

#### Mario Carneiro (Nov 24 2018 at 08:36):

I am sure it's there

#### Mario Carneiro (Nov 24 2018 at 08:36):

nat.basic has a really comprehensive list of facts like this

#### Mario Carneiro (Nov 24 2018 at 08:37):

nat.le_sub_right_of_add_le

#### Scott Morrison (Nov 24 2018 at 08:38):

ah, missing the right, thanks

#### Scott Morrison (Nov 24 2018 at 08:43):

I should use find more -- it would have successfully found this lemma, it turns out.

#### Scott Morrison (Nov 24 2018 at 08:55):

H_left : n + k ≤ b,
H_right : b < m + k
⊢ b - k < m


#### Mario Carneiro (Nov 24 2018 at 09:01):

nat.sub_lt_right_iff_lt_add

#### Scott Morrison (Nov 24 2018 at 09:11):

Ah, okay. I just found sub_lt_sub_right_iff and managed to use that.

#### Scott Morrison (Nov 24 2018 at 09:12):

So ... is there some long term plan to avoid me having to memorize all these? :-)

#### Mario Carneiro (Nov 24 2018 at 09:12):

go to nat.basic and browse around, that's what I jst did

#### Kevin Buzzard (Nov 24 2018 at 09:43):

Is the following a crazy idea: we know that we can't just take all the standard results about naturals and mark them as [simp] (some of them are one-way implications for example). Scott is complaining that he cannot find lemmas which are "standard" though. Can we tag a shedload of lemmas in data.nat.basic as "standard" and then instead of Scott having to play guess-the-name (which is still sometimes hard, despite the heroic efforts of the name-that-lemma team), he can just explicitly look for the lemma in the "standard" list. I am not saying that there should be a tactic which attempts to apply more than one standard lemma at once. But I am saying that there could be a standard tactic which literally tries to find exactly which lemma you need from a list, and applies it if it's there, and fails otherwise.

I have had problems recently looking for A -> B if it happens to be the case that A <-> B. I personally never know whether to expect to see A -> B or B -> A or both or neither in the library if A <-> B is in there and I am not sure that there is a rule, especially if one direction needs some random thing I don't care about like decidability. Now I understand the philosophy of the library -- "if it looks standard, it should be there". OK so now let's make it easy to find the standard stuff by tagging it all with standard.

#### Mario Carneiro (Nov 24 2018 at 09:44):

if the bidirectional version is there, the one directional versions should not be there normally, unless the assumptions are different in each direction

#### Mario Carneiro (Nov 24 2018 at 09:45):

if A -> B requires fewer assumptions than B -> A, you will probably find A -> B with a weak assumption and A <-> B with a strong assumption

#### Kevin Buzzard (Nov 24 2018 at 09:47):

Ah so there is some logic to it? I'd not realised this. Of course the other thing is when you look for A <-> B and it turns out that it's B <-> A which is in there.

#### Mario Carneiro (Nov 24 2018 at 09:47):

in that case it's usually up to "simplification order"

#### Kevin Buzzard (Nov 24 2018 at 09:47):

Is that just me not knowing the implicit total order on all predicates...yeah, that.

#### Mario Carneiro (Nov 24 2018 at 09:48):

for stuff involving subtraction vs addition, subtraction is on the left

#### Kevin Buzzard (Nov 24 2018 at 09:48):

So how does that work for add_assoc?

#### Mario Carneiro (Nov 24 2018 at 09:49):

left assoc on the left, right assoc on the right. not much else to go on in that case

#### Kevin Buzzard (Nov 24 2018 at 09:49):

But the thing on the right has more characters in, so it's more complicated.

#### Kevin Buzzard (Nov 24 2018 at 09:49):

It's a comp lemma.

#### Mario Carneiro (Nov 24 2018 at 09:49):

well that depends on the parser

#### Kevin Buzzard (Nov 24 2018 at 09:50):

what's the logic here?

#### Mario Carneiro (Nov 24 2018 at 09:50):

honestly I would always write an assoc lemma with explicit parens

#### Mario Carneiro (Nov 24 2018 at 09:50):

(I should double check that's not a lie)

#### Kevin Buzzard (Nov 24 2018 at 09:50):

Even then I'm looking at it and thinking it's 50-50

#### Mario Carneiro (Nov 24 2018 at 09:50):

it is 50-50, I'm not going to lie

#### Mario Carneiro (Nov 24 2018 at 09:51):

but you have to pick one order, and it was picked way back in core, and we stick with it

#### Kevin Buzzard (Nov 24 2018 at 09:51):

"Something is simpler if it has fewer brackets". Is that just nonsense?

#### Mario Carneiro (Nov 24 2018 at 09:51):

I'm not sure how much stock to put in what the parser thinks is the best order

#### Mario Carneiro (Nov 24 2018 at 09:52):

I guess that works for mul_add though

#### Mario Carneiro (Nov 24 2018 at 09:52):

I don't know, I wouldn't bet on it

#### Kevin Buzzard (Nov 24 2018 at 09:53):

OK, so it is random. The reason I am talking about add_assoc explicitly is that since I learnt that many simp or iff lemmas are of the form A = B, A <-> B with B less complicated than A, I've been able to start guessing which is on the left much better. But I still can't guess for add_assoc, so I just have to do look-up.

#### Mario Carneiro (Nov 24 2018 at 09:53):

yeah, just do the old .1  .2

#### Mario Carneiro (Nov 24 2018 at 09:54):

If I were to list a bunch of bracketing combinations in some order, I would probably start from left assoc, maybe that's just me

#### Scott Morrison (Nov 24 2018 at 09:54):

So far my only idea for escaping "look up the damn lemmas" hell is to experiment with marking them all as back, and calling back a lot.

#### Scott Morrison (Nov 24 2018 at 09:54):

I actually think this will solve a lot of my problems.

#### Scott Morrison (Nov 24 2018 at 09:55):

And back? prints the term-mode proof it finds, so it's easy to replace it if it is slow.

#### Scott Morrison (Nov 24 2018 at 09:55):

However .... all these <-> lemmas cause a problem.

#### Mario Carneiro (Nov 24 2018 at 09:55):

metamath (more accurately, one of it's IDEs) had a one-step automatic proof function. It's a life saver for this stuff

#### Mario Carneiro (Nov 24 2018 at 09:56):

you just write down all the assumptions you need and hit "go" and it finds the lemma

#### Mario Carneiro (Nov 24 2018 at 09:56):

you have to be pretty specific, but it's great for doing lookups in context

...

#### Kevin Buzzard (Nov 24 2018 at 10:16):

https://www.urbandictionary.com/define.php?term=the%20old%20one%20two

#### Johan Commelin (Nov 24 2018 at 15:01):

So ... is there some long term plan to avoid me having to memorize all these? :-)

Yes, the long term goal is that you write some automation so that we can all avoid memorising these (-;

#### Scott Morrison (Nov 24 2018 at 19:16):

The only thing I know how to do for "lemmas involve nat subtraction" is to get back up and running and trying beat problems over the head with that. I suspect it will probably work (back, especially if it calls simp along the way, it's not so far from auto) but it won't be pretty.

#### Kevin Buzzard (Nov 24 2018 at 19:22):

Are these nat subtraction problems solved in Coq? Why are they arising? I am struggling to relate this to $\oplus_{i\in I}M_i$ but I never looked at the big operators paper seriously.

#### Andrew Ashworth (Nov 24 2018 at 19:29):

Nat problems are solved by Omega in coq, aka Cooper in lean

#### Scott Morrison (Nov 24 2018 at 22:51):

The interaction between big operators and (un)natural subtraction is arising for me because I was working with sums of subset of the naturals, because the k in choose n k really ought to be a natural number.

#### Keeley Hoek (Nov 25 2018 at 02:30):

Hey Scott, is there a reason why back @ https://github.com/leanprover/mathlib/pull/410 should still have the WIP tag (not that you decide)/is there any programming work I can do to make it mergeable

#### Scott Morrison (Nov 25 2018 at 03:59):

Yes, I'm sorry this PR has been abandonware for a while.

#### Scott Morrison (Nov 25 2018 at 04:00):

I think the major obstacle is working out what to do with apply_rules. I haven't got around to looking at how apply_rules is used in mathlib yet.

#### Scott Morrison (Nov 25 2018 at 04:00):

Can we just replace all the uses of apply_rules with back?

#### Scott Morrison (Nov 25 2018 at 04:02):

It also needs some consideration of lemmas to tag, perhaps.

#### Scott Morrison (Nov 25 2018 at 04:04):

The actual core code at <https://github.com/leanprover/mathlib/pull/410/files#diff-e8836d95f7cd2f7e1c5ee370e791af03R33> could perhaps be rewritten, it reads a bit spaghetti-like at the moment, but I'm not sure what to do.

#### Scott Morrison (Nov 25 2018 at 04:06):

Something that would probably be easy for you, @Keeley Hoek, but I was confused by, is combining the back and elim attributes into just back and back!.

#### Sebastien Gouezel (Nov 25 2018 at 09:29):

I don't think apply_rules is used anywhere yet, so you can safely remove it. I wrote it for proofs of continuity and limits, where it would be most useful, but there is a bug in Lean 3 apply (which unfolds too much) that prevents apply from working without underscores on continuity lemmas. So that I could never use it efficiently!

#### Keeley Hoek (Nov 25 2018 at 09:39):

@Scott Morrison When back and elim are the same attribute what should their single unified description string be?
but sure, I'll do that and then do a tiny shuffle

#### Scott Morrison (Nov 25 2018 at 09:41):

I forget which way round they go now. One counts as progress even if you don't discharge the goal.

#### Keeley Hoek (Nov 25 2018 at 14:34):

I put in my 2-cents and did the stuff
I got rid of that precedence ?:0 thing that worried you scott too

#### Scott Morrison (Nov 26 2018 at 00:05):

@Keeley Hoek I cleaned up a few things, but also realised the current implementation of back is hopelessly inefficient, and will need to be replaced.

#### Scott Morrison (Nov 26 2018 at 02:28):

(I'll continue this in the PR reviews stream.

Last updated: May 11 2021 at 00:31 UTC