Zulip Chat Archive

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

Scott Morrison (Nov 24 2018 at 10:03):

...

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 iIMi\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: Dec 20 2023 at 11:08 UTC