xor

Stream: mathlib4

[Kevin Buzzard]

I was about to whinge that xor should be the Bool function and not the Prop version (in my version of mathlib4 xor was a Proppy xor), but when I was composing the whinge I created a link to github and discovered that as of 19 hours ago it has been changed to Xor'. What's the point of the ' @Mario Carneiro ? I'm going to add xor on Bools in the WIP branch kbuzzard-data-bool-basic.

[Mario Carneiro]

The ', as ever, is a disambiguation marker: Xor refers to the notation typeclass from core which supplies the notation ^^^ for "bitwise XOR". I'm thinking of PR'ing to change that to XorOp instead (to make it consistent with AndOp and OrOp which have similar conflicts to deal with)

[Violeta Hernández]

Out of curiosity, what's going on with docs#Xor' ? Is it something one should be using? If so, how come I barely ever see it? Why don't we have notation for it? And, why not just write p ≠ q?

[Edward van de Meent]

One reason for not using Ne is that you may want to avoid unnecessary uses of propext

[Edward van de Meent]

(which is an axiom)

[Yury G. Kudryashov]

Most of Mathlib uses classical reasoning, so this is not a valid point in terms of Mathlib coding style discussion.

[Edward van de Meent]

mathlib coding style does not tell you how to decide between formulations which are equivalent up to axioms, so your point about my point being invalid is invalid. (in particular, it doesn't say to use the formulation which uses and/or forces the use of the most of mathlibs acceptable axioms)

[Edward van de Meent]

anywho, the reason why you don't come across it might be that p ↔ ¬q is a more common spelling

[Yury G. Kudryashov]

E.g., we actively remove [Decidable _] assumptions from theorems that don't need them for the statement (and don't live in a namespace like Decidable or Encodable).

[Edward van de Meent]

indeed, but that's not applicable here

[Edward van de Meent]

the coding style doesn't tell you to write ∀ x, f x = g x or f = g.

[Edward van de Meent]

in particular, the style guide basically says "there should be a consistent choice made", but doesn't say how to decide which one is right

[Jireh Loreaux]

When Yury says "coding style" he's not referring to #style. Perhaps a more precise phrase would have been "Mathlib coding practice". His point is that in Mathlib, there is absolutely no reason to avoid uses of propext.

[Edward van de Meent]

other than code golf

[Eric Wieser]

It's nice to be able to avoid writing propext literally in a golfed proof where its noise, but I don't think there is any interest in "golfing" it away from the list of axioms

[Edward van de Meent]

indeed, but my point still stands: "if it helps write a shorter proof, avoid propext" definitely seems to be among code practice to me?

[Edward van de Meent]

That aside, saying that "X reason is invalid" simply because 'code practice' doesn't motivate X seems very narrow-minded to me; contributors can have many reasons for design decisions other than those which follow from 'code practice', and saying it's "invalid" completely dismisses the opinion as not worth considering

[Mario Carneiro]

Edward van de Meent said:

indeed, but my point still stands: "if it helps write a shorter proof, avoid propext" definitely seems to be among code practice to me?

Not really, you could stop at "if it helps write a shorter proof, do it". The interesting case of axiom elimination is when it requires writing longer proofs, and in this case there is no evidence of mathlib practice supporting doing a longer proof in order to save on axioms

[Mario Carneiro]

I personally think that small increases in proof length in exchange for axiom reduction is acceptable but by no means required or on any review checklist

[Kim Morrison]

Personally I think we should use propext as much as possible, to make it clear we are not interested in axiom reduction in Mathlib. :-)

But seriously, let's not waste oxygen on propext of all things.

[Mario Carneiro]

Personally I think we should use propext as much as possible, to make it clear we are not interested in axiom reduction in Mathlib. :-)

I know you say this as a joke, but I really don't want people doing this even as a joke. Ambivalence I can take, but active action against people who actually look at what #print axioms prints and do some basic cause/effect analysis just to... stick it to the man or something... is not nice.

[Mario Carneiro]

believe it or not, there are reasons to avoid propext. It breaks canonicity (all axioms do)

[Mario Carneiro]

I generally tell people that lean doesn't have canonicity, but this is technically only true for lean-with-axioms. For Lean-without-axioms it's an open question but could well be true. (I don't usually spend much effort looking at lean-without-axioms because it's not very interesting to the community, but it is a lot closer to a type theory that a type theorist can get behind, so I should probably figure it out at some point. In particular I'd love to know if it's equiconsistent with Lean-with-axioms - my gut feeling is yes, most of the axiomatically strong things in lean already happen in lean-without-axioms, like big inductive types like docs#PSet and impredicative Prop.)

[Kim Morrison]

Agreed, it was a joke, and I wouldn't want to people to do that either as a joke or otherwise.

But I do want to make sure that no one in reviews, or golf suggestions, etc, brings up the topic of reducing axioms unless the original author has expressly indicated they are interested in this. Doing so would be just be unnecessary noise.