Zulip Chat Archive

Stream: new members

Topic: help me find lemmas


view this post on Zulip 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

view this post on Zulip Reid Barton (Nov 24 2018 at 00:43):

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

view this post on Zulip Scott Morrison (Nov 24 2018 at 00:50):

Thanks, that'll do fine for the second.

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Nov 24 2018 at 08:36):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:36):

I am sure it's there

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:36):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 08:37):

nat.le_sub_right_of_add_le

view this post on Zulip Scott Morrison (Nov 24 2018 at 08:38):

ah, missing the right, thanks

view this post on Zulip Scott Morrison (Nov 24 2018 at 08:43):

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

view this post on Zulip Scott Morrison (Nov 24 2018 at 08:55):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:01):

nat.sub_lt_right_iff_lt_add

view this post on Zulip Scott Morrison (Nov 24 2018 at 09:11):

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

view this post on Zulip Scott Morrison (Nov 24 2018 at 09:12):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:12):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:47):

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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:47):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:48):

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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:48):

So how does that work for add_assoc?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:49):

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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:49):

It's a comp lemma.

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:49):

well that depends on the parser

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:50):

what's the logic here?

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:50):

honestly I would always write an assoc lemma with explicit parens

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:50):

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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:50):

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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:50):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 09:51):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:52):

I guess that works for mul_add though

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:52):

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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:53):

yeah, just do the old .1 .2

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 24 2018 at 09:54):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 24 2018 at 09:55):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Nov 24 2018 at 09:56):

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

view this post on Zulip Scott Morrison (Nov 24 2018 at 10:03):

...

view this post on Zulip Kevin Buzzard (Nov 24 2018 at 10:16):

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

view this post on Zulip 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 (-;

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Andrew Ashworth (Nov 24 2018 at 19:29):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Nov 25 2018 at 03:59):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Nov 25 2018 at 04:00):

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

view this post on Zulip Scott Morrison (Nov 25 2018 at 04:02):

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

view this post on Zulip 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.

view this post on Zulip 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!.

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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