help me find lemmas

Stream: new members

[Scott Morrison]

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]

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

[Scott Morrison]

Thanks, that'll do fine for the second.

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

I am sure it's there

[Mario Carneiro]

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

[Mario Carneiro]

nat.le_sub_right_of_add_le

[Scott Morrison]

ah, missing the right, thanks

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

nat.sub_lt_right_iff_lt_add

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Kevin Buzzard]

So how does that work for add_assoc?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

It's a comp lemma.

[Mario Carneiro]

well that depends on the parser

[Kevin Buzzard]

what's the logic here?

[Mario Carneiro]

honestly I would always write an assoc lemma with explicit parens

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

I guess that works for mul_add though

[Mario Carneiro]

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

[Kevin Buzzard]

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]

yeah, just do the old .1 .2

[Mario Carneiro]

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]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

...

[Kevin Buzzard]

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

[Johan Commelin]

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]

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]

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]

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

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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

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

[Keeley Hoek]

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]

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

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