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
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):
nat.sqrt is actually executed by the corresponding
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: Aug 03 2023 at 10:10 UTC