field division and DecidableEq

Stream: mathlib4

[Jz Pan]

Quiz: if F is a field without DecidableEq, can you define a function on it which maps non-zero x to x, and maps 0 to 1? You can't use if x = 0 then 1 else x since there is no DecidableEq.

Answer: it is (x - 1) * x / x + 1, since in Lean anything divide by 0 is 0.

But seems that in order to prove that this function satisfies the property, classical must be used, since you need by_cases h : x = 0.

Any thoughts?

[Floris van Doorn]

Jz Pan said:

But seems that in order to prove that this function satisfies the property, classical must be used, since you need by_cases h : x = 0.

To prove what property? Not to show that f(0)=1 or x \ne 0 \to f(x)=x.

[Jz Pan]

Floris van Doorn said:

Jz Pan said:

But seems that in order to prove that this function satisfies the property, classical must be used, since you need by_cases h : x = 0.

To prove what property?

Prove that (1) it maps non-zero x to x, and maps 0 to 1.

... or prove that (2) it maps any elements to nonzero elements.

[Jz Pan]

Real world scenario: in PR #16864 I defined something depends on some number equal to zero or not: https://github.com/leanprover-community/mathlib4/blob/9e08b117fbd856d22db894716a4df6d39e93d780/Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean#L645 but in order to make it work without classical I have to add a DecidableEq instance. I'm thinking if it worth to use such cheating way to define it bypassing DecidableEq.

[Jz Pan]

in https://github.com/leanprover-community/mathlib4/blob/9e08b117fbd856d22db894716a4df6d39e93d780/Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean#L375 the cheat is successful since in that case I just want 1,0,0,0 if some number is zero, so I don't need to invent some artificial formulas.

[Sébastien Gouëzel]

Is there a reason why you want to avoid classical there?

[Jz Pan]

There are no particular reason, just out of curiosity. I just want the def itself does not depend on classical, since it is an explicit formula written in textbook, so it should be computable. For the proof of the property it satisfies, I'm OK if it requires classical.

[Sébastien Gouëzel]

If there is no particular reason, my advice would be to use classicalfrom the start. The only downside I can think of is if you want to run this on explicit examples using kernel calculations, but it's probably a bad idea anyway.

[Jz Pan]

Sébastien Gouëzel said:

my advice would be to use classicalfrom the start

Thank you for your suggestion!

But I got the contrary comments from reviewers on my previous PRs, they don't like noncomputable section and open scoped Classical in the beginning...

[Sébastien Gouëzel]

open scoped Classical is definitely bad, as you don't know what it can contaminate. For definitions that need it, just do

open Classical in
def foobar ...

And in proofs about foobar, use classical at the beginning of the proofs if needed.

[Eric Wieser]

Sébastien Gouëzel said:

open scoped Classical is definitely bad, as you don't know what it can contaminate. For definitions that need it, just do

open Classical in
def foobar ...

And in proofs about foobar, use classical at the beginning of the proofs if needed.

open scoped Classical in is probably better practice, but the gain over what you have is small compared to the in-free version