where is `Lean.ofReduceNat` used?

Stream: general

[Asei Inoue]

where is Lean.ofReduceNat used?

I find Lean.ofReduceBool when I use native_decide, but I haven't seen Lean.ofReducedNatas an axiom in outputs of #print axioms

[Mario Carneiro]

#new members > Where is the axiom `ofReduceNat` used? @ 💬

[Mario Carneiro]

I am of the opinion that we should remove it

[(deleted)]

yeah bugs hide in unused features as they're less tested. it's been a while and no one has come up with a way to use ofReduceNat

[(deleted)]

there's an argument that ofReduceNat extracts more information from a native call than ofReduceBool. well the thing is it's possible to state all sorts of properties with ofReduceBool already

[(deleted)]

if ofReduceNat reduces a function call to 37, then ofReduceBool can be used to get a proof that that the function call returns 37 instead

[Mario Carneiro]

indeed, as long as you are willing to run the compiled code twice, you can always replace an ofReduceNat proof with ofReduceBool. (Run the function in meta code, observe the result, then assert that the function equals its result using ofReduceBool and let the kernel do the verification.) I don't think you can really avoid having to run the code twice anyway though with ofReduceNat, because if you are creating a call where you really don't know what it's going to reduce to because you have not run the function and will rely on the kernel to do that, then you will have difficulty writing the remainder of the proof in a type correct way because the immediately next lemma application is going to contain the reduced form inside its typing constraints.