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:

  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 (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