toBool

Stream: mathlib4

[Kevin Buzzard]

In mathlib3 we have

theorem to_bool_true {h} : @to_bool true h = tt :=
...

(in data.bool.basic) and this has been translated in mathlib3port to

theorem to_bool_true {h} : @toBool True h = tt :=
...

But this doesn't look right to me: the type of @to_bool in mathlib3 is

decidable.to_bool : Π (p : Prop) [h : decidable p], bool

and in lean 4 we have

Decidable.decide : (p : Prop) → [h : Decidable p] → Bool

and

@toBool : {α : Type u_1} → [self : ToBool α] → α → Bool

which looks like something else; it's a field of the ToBool class, which I'm not sure of the point of. I have paid 0 attention to the mathlib port (and not much attention to Lean 4) until two days ago when it was announced that we could start manually porting files, something which I'm genuinely excited by, so now I'm on the learning curve. Does this mean that something is not "aligned" correctly in the porting program? Should this be fixed? Most (but not all) occurrences of the to_bool -> toBool translation "error" take place in the file I'm manually porting, so I can just change these things myself, unless someone tells me that ToBool is the new Decidable (as I say, I don't really get what ToBool is all about). Sorry for the basic questions, porting files is getting me up to speed quickly but I am trying to find my feet.

[Mario Carneiro]

Yes, this is an alignment problem

[Mario Carneiro]

I'm working on a tool that will make it a lot easier to spot and fix alignment errors (mathport#187)

[Mario Carneiro]

The new advice is the following. There are four kinds of (mis)alignments you can have:

1. A defeq match - lean 3 def/theorem X is defeq to lean 4 def/theorem Y
2. The value is a mismatch but the type of lean 3 X (after translation) is defeq to lean 4 Y
3. The types are not defeq but for reasons like a change in the order of implicit arguments, which usually doesn't matter
4. X and Y are completely different definitions, although they may share the same name (after translation)

• If you are in case 1, mathport will automatically align the definitions if X = Y, and otherwise you need to add #align X Y to get mathport to translate one to the other.
• In case 2/3/4, mathport would previously rename X to Yₓ if it wanted to use the name Y but it was already taken.
• After the refactor, mathport will align X to Y in case 2, and will align X to Y with a warning in cases 3 and 4
• In case 2, you should do the same as case 1: if X = Y you don't have to do anything, otherwise you should add #align X Y
• In case 3, you should use #align X Yₓ. The ₓ has a special meaning now: it will be stripped when printing the lean 4 file, so behind the scenes lean will still think of it as a different definition but re-elaborating the lean 4 file will fix the argument order mismatch and use definition Y instead of Yₓ.
• In case 4, you should use #align X Y'. The ' is not a special character here, it just means we're going to make a separate definition and avoid the collision. This is the situation with toBool - that's an unrelated definition so we should name any theorems something else to avoid collisions.

[Mario Carneiro]

In this particular case, that means we need #align to_bool decide and #align to_bool_true decide_true

[Mario Carneiro]

and #align bool.tt Bool.true, that one doesn't look right either

[Kevin Buzzard]

I am changing a few names because of this, so that involves further alignments, right? For example mathlib3 to_bool_true I renamed to decideTrueand various other examples. If I rename a lemma is it my job to align it somehow? I don't know how to align things.

[Scott Morrison]

You can just leave #align X Y statements in the mathlib4 file itself.

[Scott Morrison]

mathport reads through all of the existing mathlib4 when it reprocess mathlib.

[Scott Morrison]

And yes, if you rename a lemma (please do so sparingly rather than thoroughly!!) you need to leave the #aligns, ideally immediately following the declaration.

[Scott Morrison]

One day (tm) when the port is over, we can go through and discard all the aligns, I guess.

[Mario Carneiro]

Note: to_bool_true is a theorem, so it still gets a snake case name like decide_true rather than decideTrue

[Kevin Buzzard]

Thanks. Can you remind me where to read about the current (and presumably now decided upon) naming conventions?

[Kevin Buzzard]

I have been thrown into confusion by the fact that lean 4 seems to have both and and And, true and True etc

[Mario Carneiro]

I don't have a particular reference to point to (PR's welcome!), but the general pattern is:

• Modules (file names), namespaces and types are in UpperCamelCase
• definitions of "data" are in lowerCamelCase
• theorems (proofs of propositions) are in snake_case

[Kevin Buzzard]

For example I currently don't understand why this theorem shouldn't be called decide_True because it's about True not true

[Mario Carneiro]

I'm still not sure about whether to explicitly lower-case expressions like that when they appear in theorems. I don't think we have come to a final decision on that

[Mario Carneiro]

mathport will lowercase the true but it doesn't have much choice in the matter

[Mario Carneiro]

I would be okay with either decide_true or decide_True

[Mario Carneiro]

lowercasing also leads to a bunch of conflicts about And vs and, for example is and_assoc about associativity of /\ or &&?

[Kevin Buzzard]

I've not thought for more than ten seconds about this but if the idea is that _ is supposed to be distinguishing whether the declaration is a proof or not then what's the harm in And_assoc?

[Kevin Buzzard]

I guess the alternative argument is that there will be vanishingly few examples of when we have both foo and Foo so we come up with some special case scenario

[Kevin Buzzard]

Just rereading last messages and laughing at completely unintentional "case" wordplay in final sentence