Where is the axiom `ofReduceNat` used?

Stream: new members

[Isak Colboubrani]

I'm looking for a concrete instance where the ofReduceNat axiom is actually used in Lean code—whether that's in the Lean 4 source code, Mathlib, or a an existing third-party library.

I'm trying to falsify the claim that this axiom is currently unused, but so far, I've been unable to find any references to it. Perhaps I'm missing something basic.

Can anyone point me to an example of ofReduceNat being used?

[Yaël Dillies]

What happens if you make a version of Lean core with that axiom removed? Can you still build all of mathlib?

[Isak Colboubrani]

@Yaël Dillies Yes, both Lean core and Mathlib builds successfully.

[Yaël Dillies]

Ah well, that's most of your answer then :sweat_smile:

[Isak Colboubrani]

Yes, that's what I suspected. I just wanted to make sure there wasn't anything fundamental I was overlooking. It's certainly surprising to find an axiom that doesn't seem to be used at all!

[Isak Colboubrani]

I've searched extensively for third-party libraries that use it, but I haven't found a single example anywhere.

[Damiano Testa]

You could look at the code for checking "classical" axioms and modify it to check for ofReduceNat and then run it on all the declarations in the environment under import Mathlib.

[Damiano Testa]

(Sorry for the lack of references: I'm on mobile, since my computer is refusing to start up this morning.)

[Isak Colboubrani]

One question I have is the following: given …

% cd mathlib4/
% git checkout master
% git grep ofReduceNat
% cd ..
% cd lean4/
% git checkout master
% git grep ofReduceNat
src/Init/Core.lean:The axiom `ofReduceNat` is used to perform proofs by reflection. See `reduceBool`.
src/Init/Core.lean:axiom ofReduceNat (a b : Nat) (h : reduceNat a = b) : a = b
%

… could there still be any uses of ofReduceNat in Lean or Mathlib? If so, where?

[Henrik Böving]

Isak Colboubrani said:

I'm looking for a concrete instance where the ofReduceNat axiom is actually used in Lean code—whether that's in the Lean 4 source code, Mathlib, or a an existing third-party library.

I'm trying to falsify the claim that this axiom is currently unused, but so far, I've been unable to find any references to it. Perhaps I'm missing something basic.

Can anyone point me to an example of ofReduceNat being used?

Just because the axiom is currently unused doesnt mean we should remove it. It took years for ofReduceBool to have more than one user and as ofReduceNat allows us to extract a lot more information from a single call to a native function than ofReduceBool there is no reason to remove it just because we can.

[Isak Colboubrani]

I see, thanks!

Is the following claim correct? The ofReduceNat axiom is not currently unused in Lean 4 and Mathlib, but it may be used in the future.

[Henrik Böving]

ofReduceNat is currently unused in Lean 4 and Mathlib but may be used in the future. Also note that if you were to delete the axiom the entire mechanism around ofReduceNat should be deleted as well which requires touching some kernel code etc.

[Isak Colboubrani]

Thanks! That answers my question.