lint structure projections

Stream: std4

[James Gallicchio]

Thoughts on a linter that disallows numerical structure projections? E.g. for e : Iff _ _ I find e.1 and e.2 much less readable than .mp and .mpr. I feel like the only case where I use the numbers is for tuples.

[James Gallicchio]

Not sure how much that syntax is used in Std/Mathlib at the moment, but it feels like bad style to me

[François G. Dorais]

@Mario Carneiro appears to be a fan of numerical projections. Personally, I am not a fan but I am not against it. That said, .mp and .mpr are pretty obscure for non-logicians (FYI: "modus ponens" and "modus ponens reverse", which should probably be .mpc or .mpv to avoid mixing Latin and English. This name choice goes back to Lean 2 and perhaps Lean 1.)

[Mario Carneiro]

yes, especially for .mp and .mpr I don't find the names much more than a waste of space

[James Gallicchio]

..really? what if you change the order of the fields in a structure? if it's just to save characters I'm not really convinced of the utility

[Mario Carneiro]

I disagree about renaming them to full latin though, modus ponens is the very standard name for this operation

[Mario Carneiro]

For iff specifically, that isn't going to happen

[Mario Carneiro]

for other structures, maybe not, but for And and Iff the field order is absolutely a stable promise

[François G. Dorais]

That was a joke, of course!

[Mario Carneiro]

also sigma and subtype

[Mario Carneiro]

I can't think of too many other structures where the field order is part of the primary interface

[Mario Carneiro]

All the basic logic operators really

[James Gallicchio]

For And/Sigma I totally see the justification, because they're tuples, and the structure names are fst/snd anyways. But Iff could be written in either order, the fields aren't fst and snd

[Mario Carneiro]

Iff is to be thought of as a conjunction (P -> Q) /\ (Q -> P)

[Mario Carneiro]

I think it was actually defined as this once

[Mario Carneiro]

and the order of conjuncts there is important: forward direction first, then backward

[Mario Carneiro]

if you changed the field order you would not only break .1 and .2 but also \<_, _\> and every proof using constructor

[Mario Carneiro]

the only thing that wouldn't break is { mp := _, mpr := _ } and literally no one writes that

[James Gallicchio]

I dunno. Not gonna shed any tears over it, just seems weird to me. Maybe we have some annotation on structures that should never change field order and then lint for number projections for all other structures.

[Mario Carneiro]

Also I think .1 on any one element structure should be okay

[Mario Carneiro]

Before rolling out any lint along these lines I would want data on how often it is actually violated, excepting the cases I mentioned

[François G. Dorais]

Mario Carneiro said:

I think it was actually defined as this once

I don't think it was but I do think it should be.

I'm pretty sure I used iff.mp and iff.mpr back in the Lean 2 days but I'm too lazy to go an check that far in time. (It might have been defined as a conjunction in Lean 1, I wasn't around back then.) Though it could be that these were theorems, but dot notation didn't work as well as now back then so I'm thinking they were actual projections.

In any case, since dot notation works really well by now, I think it makes perfect sense to define Iff a b as a -> b /\ b -> a and then add Iff.mp and Iff.mpr as theorems so nothing breaks downstream. The current definition is, I believe, just a historical artifact.

[Mario Carneiro]

those declarations definitely existed, but that's not inconsistent with the definition being a conjunction

[Mario Carneiro]

or.intro_left and or.inl both existed as well but only one is the constructor

[Mario Carneiro]

dot notation has worked on arbitrary declarations as long as I can remember, although it wasn't always a dot, it was e^.left back in the day because of ambiguity with namespaced names (which is still the case, we just developed a more sophisticated system to handle the ambiguity)

[Kyle Miller]

I'd be wary of defining Iff as an And just to be sure tactics never accidentally unfold it, and also to make sure that dot notation will always refer to the Iff namespace.

[Mario Carneiro]

Lean 4 has been trending towards more structures and less defs, so I think the split is deliberate

[Mario Carneiro]

what kyle said

[Kyle Miller]

More fun would be structure Iff (p q : Prop) extends And (p → q) (q → p) :smile:

[Kyle Miller]

(I'm not seriously suggesting this! It's just interesting that it'd be possible, though with differences, like how .1 gives you the Iff as an And.)

[François G. Dorais]

You're totally right Mario! https://github.com/leanprover/lean2/blob/master/library/init/logic.lean#L291C3-L291C3

[François G. Dorais]

Going back to the Latin/English issue: it's now possible to have Iff.by and Iff.of! Not that I think there is any reason to change Iff.mp and Iff.mpr at this point or ever...

[Alex Keizer]

I'm also not a really big fan of having two ways to refer to the same thing (numerical and named projections). IMO, it would be nice to make the numerical projections opt-in, say with a tuple attribute. This would serve as an explicit promise that a structure is intended to be used like a tuple, and that fields won't be re-ordered

[James Gallicchio]

Yeah, I'm curious how many structures would need to be opted in for mathlib to compile. I suspect constructor/langlerangle are pretty heavily used but maybe only on a small subset of structures.

[Notification Bot]

27 messages were moved from this topic to #std4 > isn't "iff" obscure? by Kyle Miller.

[François G. Dorais]

I've got a case where this kind of linting would be useful.

I was testing a std4 PR against Mathlib to see what would break. I found this example in Mathlib.Analysis.BoxIntegral.Basic:

  have A : l.bHenstock := hl.2.1.resolve_left (by decide)
  HasIntegral.of_bRiemann_eq_false_of_forall_isLittleO (hl.1.resolve_right (by decide)) B hB0 _ s hs
    (fun _ => A) H₁ <| by simpa only [A, true_imp_iff] using H₂

There seems to be a coercion involved which makes resolving the issue extremely difficult. Some hidden definition has changed in my PR so that resolve_left and resolve_right no longer make sense. I still haven't figured it out!

[Mario Carneiro]

Those are almost certainly docs4#Or.resolve_left and docs4#Or.resolve_right

[Kevin Buzzard]

One nice Lean 4 gotcha is that in theorem Or.thing ... you can refer to Or.resolve_left just as resolve_left, but if you change the name of the theorem to theorem Or_thing ... then this no longer works.

[Mario Carneiro]

Does it make things clearer to add

have hl : (_ ∨ _) ∧ (_ ∨ _) ∧ _ := hl

at the top of the proof?

[François G. Dorais]

The issue is that the ors are no longer ors after the PR. The ands are still ands but it's not easy to figure out what they are from the relevant definition:

/-- Auxiliary equivalence with a product type used to lift an order. -/
def equivProd : IntegrationParams ≃ Bool × Boolᵒᵈ × Boolᵒᵈ where
  toFun l := ⟨l.1, OrderDual.toDual l.2, OrderDual.toDual l.3⟩
  invFun l := ⟨l.1, OrderDual.ofDual l.2.1, OrderDual.ofDual l.2.2⟩
  left_inv _ := rfl
  right_inv _ := rfl
#align box_integral.integration_params.equiv_prod BoxIntegral.IntegrationParams.equivProd

instance : PartialOrder IntegrationParams :=
  PartialOrder.lift equivProd equivProd.injective

[Mario Carneiro]

the or is coming from src4#Bool.linearOrder

[Mario Carneiro]

a <= b on bool is defined as a = false \/ b = true apparently

[Mario Carneiro]

TBH I don't think that's a very good definition, a = true -> b = true would be better

[Mario Carneiro]

but that's a whole refactor I'm sure

[François G. Dorais]

Actually, std4#183 fixes a lot of this (but not with that definition, I used leOfOrd forward thinking to an upcoming Ord rehash). This issue came up while attempting to make a Mathlib patch for that std4 PR.

[Mario Carneiro]

I figured that was why you were having porting pains

[Mario Carneiro]

Why do we need a LE instance on bool?

[Eric Wieser]

Presumably mathlib wants one so that it provide a BooleanAlgebra instance

[François G. Dorais]

We at least need an Ord instance so that deriving Ord works properly.

[Eric Wieser]

But that's of course not a reason for Std4

[François G. Dorais]

Also Ord should give default LE and LT as in <https://github.com/leanprover/lean4/issues/1777>

[François G. Dorais]

And that would mean that leOfOrd and ltOfOrd are the default implementations...

[Mario Carneiro]

actually since false < true in rust, haskell, C, python I think it's probably good enough to have this instance in std

[François G. Dorais]

I think so too, but my reasoning is based on making <https://github.com/leanprover/lean4/issues/1777> work with minimal pain.

[Mario Carneiro]

I don't think it is necessarily a goal to have the implementations be defeq to leOfOrd

[François G. Dorais]

No, but then we can just delete the definition and everything will still work.

[Mario Carneiro]

lean4#1777 hasn't been implemented yet. Until it is we have to make do with the class we have

[Mario Carneiro]

which means a LawfulOrd style class

[Mario Carneiro]

or rather, whatever classes exist in core/std already for lawful ordering

[Mario Carneiro]

and leave anything else for mathlib

[François G. Dorais]

I know, but it's apparently a life goal of mine to make lean4#1777 happen! :wink:

[François G. Dorais]

I think you need to learn the joy of programming with Ord! :smile:

[Mario Carneiro]

I don't disagree with the sentiment but I don't really want to write code "as if" we had Ord when we actually don't

[Mario Carneiro]

in particular, in a hypothetical future with such a class there won't be any requirement that LE is derived from Ord, they will be separate fields with a compatibility theorem

[François G. Dorais]

Yes, but this is not a disruptive decision. It makes a lot of ugly stuff in Mathlib cleaner. The issue here is the first annoying one I ran into where it strongly relied on the definition of le for Bool to be an Or. That's a bad idea anyway, so I don't think it's an issue to fix that.

[Mario Carneiro]

sure but changing the defeq for bool LE is a mathlib refactor that requires discussion

[François G. Dorais]

My patch is almost done, you can look at it tomorrow.

[Mario Carneiro]

I'm fairly sure that leOfOrd doesn't give you the a = true -> b = true definition either

[François G. Dorais]

No, but that is never used, and the Or definition is only used in obscure places.

[Mario Carneiro]

instead you get something awkward like

(match a, b with
| false, true => .lt
| true, false => .gt
| _, _ => .eq) = .lt

[François G. Dorais]

On the other hand, it makes min and max behave normally.

[François G. Dorais]

You'll see the patch tomorrow when I'm done...

[Mario Carneiro]

if the argument is "it's fine because you shouldn't care about the defeq anyway" then it shouldn't need to be changed in the first place

[Eric Wieser]

Mario Carneiro said:

sure but changing the defeq for bool LE is a mathlib refactor that requires discussion

I think changing to a = true -> b = true (aka (a = true) <= (b = true)) would be uncontroversial, as it means le is preserved under casting to/from bool by defeq

[François G. Dorais]

It's not a change, it's a move to Std. We're arguing about hypotheticals where both of us have partial info, so let's resume tomorrow after you see the patch. I don't take such decisions lightly, which is why I'm working through the patch for std#183.

[Mario Carneiro]

right, but François G. Dorais is changing the defeq to something else in his refactor

[Mario Carneiro]

I'm pretty sure the result of unfolding leOfOrd is what I posted above

[Mario Carneiro]

@François G. Dorais It's not a move, AFAICT almost all of the code in std4#183 is new code, not copied from mathlib or else modified heavily such that I can't see the relation

[Mario Carneiro]

that's not necessarily a bad thing but it makes review a bit harder

[Mario Carneiro]

and to the extent that it forces mathlib to change its definitions to be consistent with std, it is a change to mathlib

[Mario Carneiro]

mathlib could make a definition of LE on bool which is different from the std one but this will cause the same kind of confusion as the overridden Div Int instance in std

[François G. Dorais]

As I said, that's why I'm working through the Mathlib patch...

[Ruben Van de Velde]

I think if we're adding things to std4 that are intended to replace things in mathlib but don't match exactly, the easiest approach is to make a PR to mathlib first. Then we're sure the std4 dependency update will only require removing code

[François G. Dorais]

I rushed the patch and here it is: <https://github.com/leanprover-community/mathlib4/tree/fgdorais-bool>

It will take an hour or so for the CI to get done. It compiles fine on my machine but I haven't run linters and such yet. Look at the next to last commit, the last commit is just to point std to the branch std4#183 is on. For some reason that I can't recall at the moment, I included the patch for std#184 in that one commit. It's not hard tell which is which, but it makes the patch uselessly bigger since std4#184 will be obsoleted by std4#200.

As you can see the changes are mostly deletions. It also nicely cleans up the mess discussed on Zulip a long while ago. There was exactly one file in Mathlib that relied on le for Bool being an Or, and that was fixed nicely using lemmas that were already in Mathlib.

So, like I said before, all we need is more information. There is no harm to Mathlib nor Std, in fact, there are benefits to both!

[François G. Dorais]

Actually, this uses a slightly outdated version of std4#183 (that's the price of rushing it...) but it should work fine with the more recent version except for xor which should just become an export Bool (xor) in Mathlib.Init.Bool.Basic.

[François G. Dorais]

Oh bummer, compilation is fine but it looks like there's a bunch of simp redundancies that were found by the simp linter... I don't intend to get around to that since std4#200 is more important for now.