nat.sqrt

Stream: general

[Johan Commelin]

I'm looking at #12851. Why does this fail

@[simp] lemma sqrt_one : sqrt 1 = 1 := rfl

We seem to be trying quite hard to make sqrt computable...

[Gabriel Ebner]

It's defined using well-founded recursion, this won't reduce (reliably) in the kernel.

[Kyle Miller]

Mario added a norm_num plugin to deal with this very recently:

import data.nat.sqrt_norm_num

lemma sqrt_one : nat.sqrt 1 = 1 := by norm_num

[Johan Commelin]

Then what's the benefit of the complicated definition?

[Kyle Miller]

There seem to be two notions of computability in lean:

1. Can the kernel reduce a term to normal form?
2. Can the VM compile and evaluate a definition?

The first property is not checked nor indicated to us by Lean, and it affects us all the time since we rely on some amount of reduction when we rely on definitional equality. The second property is pervasively checked (requiring us to put noncomputable in the right places), but in practice we rarely evaluate code except for what supports tactics.

[Gabriel Ebner]

Note that nat.sqrt is actually executed by the corresponding norm_num plugin.

[Eric Rodriguez]

yeah, iirc the execution model of many of these tactics are "use #eval to figure out what the answer should be, and then cook up a proof"

[Kyle Miller]

If there were multiple definitions for nat.sqrt with proofs that they're equal, norm_num could use the more efficient one

[Eric Rodriguez]

isn't that effectively what's happening in Lean4?