Excluded middle proof

Stream: lean4

[James Smith]

Hi, I was looking at Lean's proof of Classical.em and I think it can be simplified a bit. It seems that the two Prop → Props U and V are being chosen as a trick to make them equal iff p.

I think it would be much more direct to just take Bool and quotient it by p, giving us a projection π : Bool → A. Then, the proof that π true = π false iff p is trivial and comes from Quotient.sound and Quotient.exact. Using choice, we get a section σ : A → Bool, and we can decide p by deciding σ (π true) = σ (π false), since Bool has decidable equality.

I think that such a proof shows what's really going on better and is easier to follow. I made a PR here to show my idea: https://github.com/leanprover/lean4/pull/2625

What are your thoughts?

[Kevin Buzzard]

Aren't you supposed to make an RFC before a PR?

Does the current proof use the Quotient.sound axiom?

[James Smith]

Sorry, I can make an RFC. I thought it would be easier to just show the new proof since it's a small change.

The current proof uses Quotient.sound indirectly through funext. The new one does not use funext.

[Chris Hughes]

I think the current proof is kind of like your one, if you think of the set {U, V} as a funny construction of the quotient of {True, False} (not Prop) by p (in fact it's just the traditional set theoretic construction of the quotient).

Personally I do prefer the proof using Quot, but I think this is a matter of taste and other people might prefer the current proof.