Sum.bnot_isLeft and Sum.bnot_isRight

Stream: lean4

[Wrenna Robson]

I think docs#Sum.bnot_isLeft and docs#Sum.bnot_isRight are badly-formed. It looks to me that there's a coercion going wrong somewhere - I think instead of !x.isLeft = x.isRight we should have (!x.isLeft) = x.isRight - that is a much more useful simp lemma. The problem seems to be the priority of the ! operator - it's binding to the whole expression x.isLeft = x.isRight, but I think this cannot be what is intended, surely.

[Wrenna Robson]

If people agree I guess I'll submit a lean4 PR to fix this... am I just missing something as to why this is useful in its current form?

[Eric Wieser]

These are definitely malformed, they should say (!x.isLeft) = x.isRight not (!decide (x.isLeft = x.isRight)) = true

[Eric Wieser]

Separately, maybe the precedence of ! is wrong?

[Wrenna Robson]

Aye, or shifted at some point and that's why this happened (after all, you probably wouldn't notice if these simp lemmas aren't actually used anywhere currently).

[Wrenna Robson]

@[inherit_doc] notation:max "!" b:40 => not b- This is where the notation for ! is defined.

[Eric Wieser]

I wonder if the decide coercion should be considered harmful

[Eric Wieser]

I know @Kyle Miller was annoyed in the past about the bidirectional coercions between Fin and Nat; presumably the bidirectional coercions between Bool and Prop are similarly problematic?

[Wrenna Robson]

I don't much like it. We were discussing earlier that isLeft and isRight are a pain to use and this is one reason for that I think.

[Eric Wieser]

Either way, I think you should just go ahead and fix the statements right now with the current precedence / coercions

[Wrenna Robson]

OK. Always somewhat more of a pain with core to run up a quick PR but I'll do it.

[Eric Wieser]

docs#Bool.not_eq_iff and nearby lemmas are also affected

[Wrenna Robson]

Huh weird. It... may already be fixed? At least, I just synced to the most recent version of core, and that is different.

[Eric Wieser]

Indeed, #check Sum.bnot_isRight looks ok in the nightly web editor

[Wrenna Robson]

Looks like lean4#8849 fixed this on the way past adding grind annotations.

[Eric Wieser]

Eric Wieser said:

docs#Bool.not_eq_iff and nearby lemmas are also affected

These ones are still broken though

[Wrenna Robson]

Aye

[Kyle Miller]

@Eric Wieser The Nat <-> Fin bidirectional coercions are actively harmful, since they can cause silent truncation due to the way arithmetic is elaborated depending on small changes in elaboration order. (As a matter of principle, I think coercions ought to never have data loss. Nat -> Fin should be explicit.)

Going back and forth between Prop and Bool doesn't have the same sort of issue but still, it's not good to have coercion loops. This loss of definitional equality is annoying:

example (b : Bool) : ((b : Prop) : Bool) = b := by simp -- rfl fails

[Wrenna Robson]

Sometimes you have things like, for instance, Sum.isLeft and Sum.isRight which are kind of used like propositions or conclusions. But I would argue it would be better if these were propositions, and then they just had a Decidable instance for when you need to turn them into Bool! They are in core though so maybe that would be an issue.

[Wrenna Robson]

But I do basically feel like Bool should always look like data and a Bool that is used like a proposition is often a code smell.

[Eric Wieser]

I think the "just make things (decidable) propositions" ship has largely sailed

[Wrenna Robson]

Alas, alack.

[Wrenna Robson]

Like if we had (a == b) hypotheses in a theorem that would smell bad to me.

[Eric Wieser]

Maybe there should be a linter that bans prop / bool coercions in theorem statements

[Eric Wieser]

Since they tend to be accidental, or hiding that the statement is much messier than intended

[Wrenna Robson]

Oh no, I've just learned we also use ! for factorial. I mean it's fine, ish, it just makes trying to find more of these errors a bit harder

[Wrenna Robson]

n ! = 1 ↔ n ≤ 1 - this statement does NOT mean what I thought it meant.

[Eric Wieser]

I already did such a search and believe that the ones I mentioned above are exhaustive (at least for mathlib)

[Wrenna Robson]

Great! Thought I would double check. I make three such issues.

[Wrenna Robson]

Also some of the names here are iffy (they should be bnot) but that is out of scope.

[Kyle Miller]

@Joachim Breitner Recently in a code review you suggested that I change f x (!y) z to f x !y z, but the precedence causes that to be parsed as f x !(y z). Do we find this to be surprising that ! has such low precedence?

It's hard to imagine changing ! and reviewing all uses of it in the ecosystem, to make sure programs don't suddenly start having different behavior, but also it would be much harder to make such a change later. I think in practice though we see uses of !f x y z, so I'm not sure it would ever make sense for f x !y z to mean f x (!y) z, but at least it could be bumped up to a precedence right before function application.

[Wrenna Robson]

What should the statement of not_eq_iff be?

[Kyle Miller]

@Wrenna Robson Make sure you check issues/PRs about !. I think I have a few experiments in there about it, to try to help address factorial problems.

[Kyle Miller]

(That's assuming the issues would be about !)

[Wrenna Robson]

A little hard to search but I will try.

[Kyle Miller]

Found them @Wrenna Robson: #5824 #5826

[Wrenna Robson]

Thank you

[Wrenna Robson]

Are those in lean4?

[Wrenna Robson]

lean4#5824, lean4#5826

[Wrenna Robson]

Ah, I gotta go home and then I am on leave for a couple days, so I might not get a fix to those Mathlib lemmas in. I'm glad that the main issue I noticed is fixed in nightly. Having looked at docs#Bool.not_eq_iff for a while I am not actually sure what it is meant to be...

[Wrenna Robson]

Kyle Miller said:

Eric Wieser The Nat <-> Fin bidirectional coercions are actively harmful, since they can cause silent truncation due to the way arithmetic is elaborated depending on small changes in elaboration order. (As a matter of principle, I think coercions ought to never have data loss. Nat -> Fin should be explicit.)

Going back and forth between Prop and Bool doesn't have the same sort of issue but still, it's not good to have coercion loops. This loss of definitional equality is annoying:

example (b : Bool) : ((b : Prop) : Bool) = b := by simp -- rfl fails

If you think coercions should never have data loss, does that mean you are also opposed to, for instance, FunLike-style coercions?

[Kyle Miller]

Good question @Wrenna Robson, and clearly my rule needs refinement. I'm thinking of this from the perspective of Coe as a way to fix defeq failures.

CoeFun is different, since it's more like an interface types can implement to participate in function applications. I don't believe it's ever used to transform individual values, but only in the context of making f x make sense.

[Wrenna Robson]

Yes, a world without it would be a much more annoying world, certainly.

[Kyle Miller]

The mystery of not_eq_iff seems solvable by looking at it in context.

lemma eq_not_iff : ∀ {a b : Bool}, a = !b ↔ a ≠ b := by decide

lemma not_eq_iff : ∀ {a b : Bool}, !a = b ↔ a ≠ b := by decide

Based on eq_not_iff, I'd guess it should be (!a) = b).

[Wrenna Robson]

Oh of course it is. It's obvious now you say it.

[Wrenna Robson]

Still I suppose this is what the poor parser has to cope with.

[Kyle Miller]

There's some sense to having ! parse similarly to \not, but somehow for Bool it's really confusing, since ! seems like it should have high precedence for some reason.

[Wrenna Robson]

To me I think ! for Boolean negation binds far too greedily, yeah.

[Wrenna Robson]

It wants to work more like - I think?

[Kyle Miller]

Yeah, booleans have boolean algebra.

There's also a big tradition of being able to negate atoms easily (e.g. conjunctive normal form)

[Wrenna Robson]

Whereas with propositions you often want to negate quite a complex proposition built out of longer statements.

[Kyle Miller]

Yeah, and definitely it should have lower precedence than any arithmetical operators

[Kyle Miller]

Wrenna Robson said:

Yes, a world without it would be a much more annoying world, certainly.

Just to be clear, I don't think that CoeFun is an exception to the rule for sake of convenience, but rather that "coe" happens to be in the name and it's not the same kind of thing as Coe. It's more like we could imagine that whenever you do f x, the elaborator always asks CoeFun how to resolve it (like Python's __call__). Similarly, CoeSort is an interface for letting terms be on the RHS of :. The Coe system is something different from these, used to patch type mismatches in general.

[Wrenna Robson]

Hmm, but sometimes we do coerce the whole function - consider Function.Injective e, where e is an Equiv, or a MulHom.

[Wrenna Robson]

And that I think is a Coe.

[Kyle Miller]

Ok, then I give up :-)

[Kyle Miller]

Oh, wait, isn't the data in a FunLike generally the underlying function? The coercion to a function doesn't lose data then, only some proofs.

[Wrenna Robson]

I do basically agree with your rule though. Like we should coerce Nat to Int, not Int to Nat, for the same reason. I suppose that is genuinely throwing away data whereas in theory because the coercion in FunLike is injective, you aren't actually losing anything.

[Wrenna Robson]

Ah we had the same thought I think.

[Aaron Liu]

Kyle Miller said:

Oh, wait, isn't the data in a FunLike generally the underlying function? The coercion to a function doesn't lose data then, only some proofs.

Sometimes you are losing data, like the symm of an Equiv

[Wrenna Robson]

It could be reconstructed in theory though.

[Wrenna Robson]

Like you could define an equiv as a function equipped with a proof that it is bijective.

[Wrenna Robson]

You shouldn't. But you could!

[Robin Arnez]

Yeah FunLike comes with a proof of injectivity iirc so you will never lose data (at least in the noncomputable sense)

[Wrenna Robson]

The argument I guess is that all coercions should be injective.

[Kevin Buzzard]

The coercion from naturals to integers mod n isn't injective

[Wrenna Robson]

Or at least injective on the value being coerced (in the case of Fin (n + 1), say, I don't actually have an issue with the Nat 0 being coerced... but partial injectivity feels messy in other ways).

[Wrenna Robson]

Kevin Buzzard said:

The coercion from naturals to integers mod n isn't injective

Yes - I think Kyle's maximalist position would be that it should therefore be barred.

[Kyle Miller]

At least Mathlib doesn't have a ZMod n -> Nat coercion, otherwise that would induce a lot more chaos.

[Kyle Miller]

Lean is missing a way to cast values using a uniform system, casting in the sense of C++.

There's no coercion from Nat to Fin n for example (thankfully not, because there's a coercion Fin n -> Nat), but you have to guess the function to use to lossily turn a Nat into Fin n.

Type ascriptions aren't casts; they indicate the type that you intend a term to have. This could all be done with an extra typeclass and writing terms like cast_to (Fin 2) n. There could be type-ascription-like syntax for this such as (n as Fin 2) (though maybe not stealing as as a keyword).

[Yaël Dillies]

Kyle Miller said:

There's no coercion from Nat to Fin n for example (thankfully not, because there's a coercion Fin n -> Nat)

... although that is a very recent development

[Wrenna Robson]

Is it?

[Kyle Miller]

Yes, I'm very happy about this development :-)

Now (3 : Nat) = (3 : Fin 2) and (3 : Fin 2) = (3 : Nat) both evaluate to false

[Wrenna Robson]

Oh, the no coercion.

[Joachim Breitner]

Kyle Miller schrieb:

Recently in a code review you suggested that I change f x (!y) z to f x !y z, but the precedence causes that to be parsed as f x !(y z). Do we find this to be surprising that ! has such low precedence?

I am certainly surprised :-)

[Eric Wieser]

Wrenna Robson said:

Looks like lean4#8849 fixed this on the way past adding grind annotations.

It's ok, we have 6 more of these: https://github.com/leanprover/lean4/blob/2c13d145dc05899f8ac5928253787d8a495f6c2b/src/Init/Data/Ord.lean#L250-L255

[Eric Wieser]

@loogle !(decide (_ = _))

[loogle]

:search: Nat.not_decide_mod_two_eq_one, Ordering.not_isEq_eq_isNe, and 10 more

[Eric Wieser]

Is a good way to find them

[Wrenna Robson]

Cool. I am focusing on a grant application this week but I'm happy to review a PR if you get there first.

[Eric Wieser]

lean4#9129