porting core Lean 3 stuff?

Stream: mathlib4

[Kevin Buzzard]

So I'm in the middle of porting data.bool.basic to mathlib4; here are two hopefully straightforward questions:

1) Core Lean 3 contains a file init.data.bool.lemmas which contains about 50 lemmas about bool most of which I can't find either in core Lean 4 or in Std. Should I also be porting them? Some are used in mathlib3 proofs. If so, what's the procedure? There's a lean3port repo, right? Do I copy this file and put it at the beginning of mathlib4's data.bool.basic or do I put it elsewhere?

2) One of the few lemmas in this file which has been ported, to Std.Logic in std4 is

theorem Bool.ff_ne_tt : false ≠ true := fun.

@Mario Carneiro ported this a month ago and in my mind that theorem has the wrong name, because what the heck is ff in a Lean 4 context? Should I be not changing ff to false in mathlib4's port of data.bool.basic? I feel very unequipped to make decisions about naming.

[Floris van Doorn]

My thoughts:
(1) Yes, if lemmas don't exist yet, it is good to port them to mathlib4. Then Mario can later move them to Std4 if that is more appropriate.
(2) I agree that Bool.ff_ne_tt is misnamed. I think until it is renamed, it is good to add a #align command, so that it is easy to fix once Bool.ff_ne_tt gets properly named.

[Kevin Buzzard]

Would you also agree that the following 40 or so lemmas are misnamed? https://github.com/leanprover-community/mathlib3port/blob/5a66d9b4aff2f94aabca7f3daead2a383d7f2117/Mathbin/Data/Bool/Basic.lean#L121-L233

e.g. bor -> or, bnot -> not etc. Should I rename and #align all of them?

Can you explain to me how to align? I thought I was told yesterday that I could just do it in mathlib4 but I can't get it to work and thinking about it, it doesn't sound like this idea makes too much sense. Where do I #align the examples above?

[Mario Carneiro]

You can put #align directives anywhere in mathlib4 (after importing Mathlib.Mathport.Rename of course), although I suggest you put them in the place where the original lean 3 theorem would have been (or after the translated theorem if one exists). What do you mean by "it didn't work"? There is no immediate effect of the annotation, but it will get picked up by mathport in its next run.

[Mario Carneiro]

And yes, ff_ne_tt is misnamed. I think I was trying to avoid renames at the time

[Mario Carneiro]

There are also a number of alias commands in Logic.Basic which could just be renames instead

[Kevin Buzzard]

What do you mean by "it didn't work"?

I just mean "I didn't have the right import".

[Scott Morrison]

Kevin Buzzard said:

Do I copy this file and put it at the beginning of mathlib4's data.bool.basic or do I put it elsewhere?

I don't think this was answered above. If you are porting a file from Lean 3 core, you should put it in Mathlib/Init/. So init.data.bool.lemmas from Lean 3 core would go in Mathlib/Init/Data/Bool/Lemmas/lean in mathlib4.

[Kevin Buzzard]

Thanks! I've essentially finished the mathlib bool file and I'll start on the lean bool file tomorrow