minFac is computable but depends on choice

Stream: mathlib4

[Christoph Spiegel]

This is probably a silly question, but how is this possible:

-- `Nat.minFac` uses `Classical.choice` ...
#print axioms Nat.minFac
-- ... but is computable
#eval Nat.minFac 9

Is there just a wasted call to Classical.choice somewhere in the foundations of mathlib that gets pulled into Nat.minFacbut is not actually executed or why does #eval not trip over the noncomputable / axiom?

[Kevin Buzzard]

If it's used in a proof that some computable function has a certain property, then this should be fine, no?

[Kevin Buzzard]

Looks to me that the data part of the definition of docs#Nat.minFacAux is computable but the proof that the "definition is well-defined", i.e. that the algorithm always terminates on any input, uses axioms.

[Kevin Buzzard]

axiom foo : ∀ x, x < 9

def a : {n // n < 9} := ⟨37, foo 37⟩

#eval a -- 37

#print axioms a -- foo

[Christoph Spiegel]

Ah, that does make sense. Thanks for the example!