Not sure why decide fails on IsSquare

Stream: new members

[Kevin Cheung]

I am not sure why the first example below throws an error since the documentation shows that Nat.instDecidablePredIsSquare exists:

import Mathlib

-- Why doesn't the following work?
example (n : ℕ) (hn : n = 4) : IsSquare n := by
  rw [hn]
  decide -- throws error

example (n : ℕ) (hn : n = 3) : Nat.Prime n := by
  rw [hn]
  decide -- this works

Here is the error:

tactic 'decide' failed for proposition
  IsSquare 4
since its 'Decidable' instance
  Nat.instDecidablePredIsSquare 4
did not reduce to 'isTrue' or 'isFalse'.

After unfolding the instances 'decidable_of_decidable_of_iff', 'decidable_of_iff'', 'instDecidableEqBool', 'instDecidableEqNat', 'Bool.decEq', 'Nat.decEq', 'Nat.decLe' and 'Nat.instDecidablePredIsSquare', reduction got stuck at the 'Decidable' instance
  match h : (Nat.sqrt 4 * Nat.sqrt 4).beq 4 with
  | true => isTrue ⋯
  | false => isFalse ⋯

[Damiano Testa]

Using with_unfolding_all decide works.

[Kevin Cheung]

Could you explain why that is necessary here?

[Aaron Liu]

docs#Nat.sqrt.iter is irreducible

[Damiano Testa]

So, you could also do a more "aimed" unfolding and use

unseal Nat.sqrt.iter in
example : ...

[Kevin Cheung]

Interesting. Is there a good reason why it is irreducible?

[Aaron Liu]

Functions defined using well-founded recursion are automatically marked irreducible.

[Kevin Cheung]

I see. I find it quite counterintuitive that decide doesn't automatically work on a decidable proposition.

[Aaron Liu]

see lean4#4061

[Aaron Liu]

You can also do decide +kernel to skip elaboration and go straight to the kernel, which ignores definition transparency.

[Kevin Cheung]

Does that mean decide +kernel and with_unfolding_all decide are practically the same?

[Kevin Cheung]

Hmm. decide +kernel doesn't work. Do I need to upgrade to the latest Lean? I'm on 4.13.

[Kevin Cheung]

Looks like the last question is answered by https://lean-lang.org/blog/2024-12-9-lean-4140/

[Aaron Liu]

Kevin Cheung said:

Does that mean decide +kernel and with_unfolding_all decide are practically the same?

These are not the same.
decide +kernel instructs decide to skip checking if the Decidable instance reduces to isTrue, and just let the kernel check.
with_unfolding_all decide instructs decide to try harder to unfold the Decidable instance into isTrue, and then the kernel will check it again.

Both stop decide from getting stuck in reduction.

[Kevin Cheung]

Does that mean plain decide is just elaboration?

[Aaron Liu]

Plain decide will first check if the Decidable instance reduces to isTrue (this is during elaboration). If it succeeds, then it will insert a proof term, and then during kernel typechecking, the kernel will also reduce the Decidable instance to isTrue.

[Aaron Liu]

The code for decide is at docs#Lean.Elab.Tactic.evalDecideCore.

[Kevin Cheung]

I see. Thank you.

[Eric Wieser]

Aaron Liu said:

Functions defined using well-founded recursion are automatically marked irreducible.

I think we could override it for Nat.sqrt?

[Aaron Liu]

Is that a good idea?

[Matthew Ballard]

If these definitions are used to define instances of this class and this class is an argument to some other type-class so that type-class inference will have to unfold these instances to check for definitional equality, then these definitions should be marked @[reducible].

is already in a library note. This seems very much in that vein.

If someone wants to make a PR to batteries to test the impact on mathlib, please ping me

[Joachim Breitner]

Eric Wieser said:

Aaron Liu said:

Functions defined using well-founded recursion are automatically marked irreducible.

I think we could override it for Nat.sqrt?

I don’t think it's a good idea to let the kernel try to reduce the proofs in well-founded definitions. This blows up easily and is hard to debug – just today someone on our team spent far too much time trying to understand a kernel reduction timeout that would have been much easier to diagnose if wf definitions were not reducible. It may work for small numbers as in the example above, but isn’t robust.

[Joachim Breitner]

In fact we might actually make wf definitions never ever reducible for that reason (https://github.com/leanprover/lean4/pull/5182).

[Joachim Breitner]

Most definitions by wf recursion that people want to reduce in the kernel, like sqrt.iter, can be rewritten to use structural recursion using fuel, for example like this:

def sqrt (n : Nat) : Nat :=
  if n ≤ 1 then n else
  iter n (n / 2)
where
  /-- Auxiliary for `sqrt`. If `guess` is greater than the integer square root of `n`,
  returns the integer square root of `n`. -/
  iter (n guess : Nat) : Nat :=
    let next := (guess + n / guess) / 2
    if _h : next < guess then
      iter n next
    else
      guess
  termination_by guess



def sqrt' (n : Nat) : Nat :=
  if n ≤ 1 then n else
  iter n (n / 2) (n / 2 + 1) (by omega)
where
  iter (n guess fuel : Nat) (h : guess < fuel ) : Nat :=
    let next := (guess + n / guess) / 2
    if _ : next < guess then
      match fuel with
      | 0 => by contradiction
      | fuel+1 => iter n next fuel (by omega)
    else
      guess


theorem sqrt'.iter_eq_iter : sqrt'.iter n guess fuel h = sqrt.iter n guess := by
  rw [sqrt.iter, sqrt'.iter]
  split
  · split
    · contradiction
    · apply sqrt'.iter_eq_iter
  · rfl


theorem sqrt'_eq_sqrt : sqrt' = sqrt := by
  ext n
  unfold sqrt sqrt'
  congr
  apply sqrt'.iter_eq_iter


-- Or even

def sqrt'' (n : Nat) : Nat :=
  if n ≤ 1 then n else
  iter n (n / 2) (n / 2 + 1)
where
  iter (n guess fuel : Nat) : Nat :=
    let next := (guess + n / guess) / 2
    if _ : next < guess then
      match fuel with
      | 0 => 0
      | fuel+1 => iter n next fuel
    else
      guess



theorem sqrt''.iter_eq_iter  (h : guess < fuel )  : sqrt''.iter n guess fuel = sqrt.iter n guess := by
  rw [sqrt.iter, sqrt''.iter.eq_def]
  dsimp
  split
  · split
    · contradiction
    · apply sqrt''.iter_eq_iter
      omega
  · rfl

theorem sqrt''_eq_sqrt : sqrt'' = sqrt := by
  ext n
  unfold sqrt sqrt''
  congr
  apply sqrt''.iter_eq_iter
  omega

So if you care about kernel reduction, I suggest to use something like this .

[Eric Wieser]

Is the fuel elided in the runtime version?

[Eric Wieser]

Or do we need both the wf and fuel versions with a csimp lemma?

[Joachim Breitner]

In this case, the latter, I fear. (I never got it to work with some form of Prop-valued fuel or something like that, even though the zero-match is not reachable)

[Joachim Breitner]

There are also variants where you “boost” the accessibility proof to have many Acc.intro constructors, so that reduction works nice for a while. But that leads to large proof terms in the kernel, I believe.

[Kyle Miller]

Kevin Cheung said:

Does that mean decide +kernel and with_unfolding_all decide are practically the same?

From a user's point of view, you could think of these as being more-or-less the same. Aaron mentioned that +kernel skips using elaborator reduction, letting the kernel handle everything instead. The kernel doesn't know about irreducibility, so it's as if everything is unfoldable.

However: the kernel type checker and the elaborator type checker are different, and there are small differences here and there. The elaborator is designed to be at least as strict as the kernel, so some other things might be accepted by decide +kernel. One example that comes to mind is smart unfolding, which is an elaborator feature and not a kernel feature, and which sometimes causes people's rfls to fail. I'm not sure it affects "ground terms", which is what decide requires (goals without free variables or metavariables).

If you know decide will succeed, then decide +kernel is also more efficient (it saves almost 50% of the evaluation time). We don't use +kernel mode by default because decide is supposed to fail fast. Tactics might tentatively try decide to close goals, and in that application reducibility should be respected.

[Kevin Cheung]

I hope that there is a good solution. It's just weird that decide Prime works right out of the box but decide IsSquarerequires jumping through hoops. Students could be confused (as I was).

[Joachim Breitner]

Maybe the fundamental issue is that we have a way to indicate how to efficiently calculate a proposition (the Decidable instance), allowing us to decouple algorithms from definitions, but we don't have something like that for definitions. (And maybe we should have separate ones for kernel reduction and compiled evaluations, although there csimp maybe enough)

[Matthew Ballard]

I think you end up here writing a norm_num extension