# Zulip Chat Archive

## Stream: general

### Topic: nat.sqrt

#### Johan Commelin (Mar 21 2022 at 17:38):

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 (Mar 21 2022 at 17:41):

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

#### Kyle Miller (Mar 21 2022 at 17:45):

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 (Mar 21 2022 at 17:51):

Then what's the benefit of the complicated definition?

#### Kyle Miller (Mar 21 2022 at 17:51):

There seem to be two notions of computability in lean:

- Can the kernel reduce a term to normal form?
- 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 (Mar 21 2022 at 17:53):

Note that `nat.sqrt`

is actually executed by the corresponding `norm_num`

plugin.

#### Eric Rodriguez (Mar 21 2022 at 17:55):

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 (Mar 21 2022 at 18:01):

If there were multiple definitions for `nat.sqrt`

with proofs that they're equal, `norm_num`

could use the more efficient one

#### Eric Rodriguez (Mar 21 2022 at 18:01):

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

Last updated: Dec 20 2023 at 11:08 UTC