Why tactic `decide` cannot solve IsSquare 9 ?

Stream: new members

[ptrl]

My code:

def nine_is_square : IsSquare 9 := by
  decide

screenshot2024-12-05 00.33.25.png

[Eric Wieser]

unseal Nat.sqrt.iter in
def nine_is_square : IsSquare 9 := by
  decide

fixes it

[Eric Wieser]

cc @Joachim Breitner, it would be great to have some documentation in the decide tactic about the interaction with well-founded recursion

[Daniel Weber]

I recall some talk about being allowed to unfold well-founded recursion on ground terms, which could also solve this

[ptrl]

@Eric Wieser May I ask a more further question?
How to solve this by decide? \sqrt 7 will be solved, but \sqrt 7 + 1 not work

unseal Nat.sqrt.iter in
example : Irrational (√7 + 1) := by
  decide

[Eric Wieser]

You can use

#synth Decidable (Irrational √7)

to see that docs#instDecidableIrrationalSqrtOfNatReal is being used, which only applies when there is no addition

[ptrl]

Eric Wieser said:

You can use

#synth Decidable (Irrational √7)

to see that docs#instDecidableIrrationalSqrtOfNatReal is being used, which only applies when there is no addition

Hi, @Eric Wieser
If I want to solve Irrational (√7 + 1), what should I do? I want to use Irrational.rat_add, but 1 is not a rational, it is \R.
And what about Irrational (√7 - 1)? I think it is more difficult

[Matt Diamond]

this works, though I would hope there's a way to do this without the Nat.cast_one rewrite:

import Mathlib

unseal Nat.sqrt.iter in
example : Irrational (√7 + 1) := by
  rw [← Nat.cast_one, irrational_add_nat_iff]
  decide

[Matt Diamond]

and then you can do the same for - 1 using irrational_sub_nat_iff

[Eric Wieser]

We should add an ofNat version of that lemma, and rename that one to natCast

[Mario Carneiro]

Daniel Weber said:

I recall some talk about being allowed to unfold well-founded recursion on ground terms, which could also solve this

Probably decide +kernel, since the kernel doesn't care about irreducibility

[ptrl]

Why \sqrt 4 = 2 cannot be solved by decide? :sob:

unseal Nat.sqrt.iter in
def sqrt4eq2 : √(4 : ℕ) = 2 := by
  decide

[Mario Carneiro]

does decide +kernel work?

[Daniel Weber]

That's not docs#Nat.sqrt, that's docs#Real.sqrt (and reals are noncomputable)

[Mario Carneiro]

theorem sqrt4eq2 : √(4 : ℕ) = 2 := by
  rw [Real.sqrt_eq_iff_eq_sq] <;> norm_num

works

[Mario Carneiro]

perhaps norm_num should have a module for Real.sqrt that does this, although it's obviously limited to rational squares

[Ruben Van de Velde]

I agree