Kernel tries to reduce WF definitions

[gebner]

The following theorem fails to type-check in the kernel:

theorem y : id (Nat.gcd 314159 10000) = Nat.gcd 314159 10000 := rfl
-- (kernel) deep recursion detected

Presumably this happens because we provide a too constructive proof of Acc (· < ·) 314159, which allows the kernel to unfold the definition 314159 times. (theorized by @digama0)

as reported by @thorimur

[gebner]

Presumably this happens because we provide a too constructive proof of Acc (· < ·) 314159, which allows the kernel to unfold the definition 314159 times.

For some reason, I've never realized this. I've always thought the proofs in well-founded definitions need to reduce, which is infeasible if we had to ensure that for all proofs. But this is of course not the case. The only proof that needs to reduce here is the proof that the relation is well-founded. And for natural numbers this is just induction.

[nomeata]

Just stumbled on this due to a support question. The self-contained #mwe here was

def f (x0 : Nat) : Nat :=
  if h : x0 = 0 then
    1
  else
    4 + f (x0 - 1)
  termination_by  x0
  decreasing_by simp_wf; omega

example : f 10000 = id f (id 10000) := rfl -- deep recusion
example : id f 10000 = id f (id 10000) := rfl -- fine
example : f 10000 + 0 = f (id 10000) + 0 := rfl -- deep recursion
example : f 10000 = f (id 10000) := rfl -- fine

And as Gabriel pointed out: It may be better if the WellFoundedRelation proof doesn’t reduce to easily.

Is there a good an easy way to make a proof term not reduce?

I played around with the identity function as an axiom, and indeed, that allows me to defined a WellFoundedRelation instance where the second field doesn’t reduce, and thus the kernel doesn’t unfold more than it should:

axiom dontReduce {α : Prop} : α → α

def NNat := Nat
instance NNat.lt_wfRel : WellFoundedRelation NNat where
  rel := fun x y => Nat.lt x y
  wf  := dontReduce Nat.lt_wfRel.2

def NNat.ofNat  : Nat → NNat := fun x => x

def g (x0 : Nat) : Nat :=
  if h : x0 = 0 then
    1
  else
    4 + g (x0 - 1)
  termination_by NNat.ofNat x0
  decreasing_by simp_wf; unfold NNat.ofNat; omega

example : g 10000 = id g (id 10000) := rfl
example : id g 10000 = id g (id 10000) := rfl
example : g 10000 + 0 = g (id 10000) + 0 := rfl
example : g 10000 = g (id 10000) := rfl

Can we define dontReduce without using axiom?

And should that be used in the WellFounded definitions to avoid kernel reduction here?

Or better to wait for the kernel to learn about reducibility flags, and/or the module system?

[nomeata]

Ah, of course I can make a reduction blocking id at least without any new axioms, using existing ones, e.g.

theorem dontReduce {P : Prop} (h : P) : P :=
  (Classical.em P).elim (fun h' => h') (fun h' => False.elim (h' h))

So what if we replaced

noncomputable def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
  fixF F x (apply hwf x)

with

noncomputable def fix (hwf : WellFounded r) (F : ∀ x, (∀ y, r y x → C y) → C x) (x : α) : C x :=
  fixF F x (dontReduce (apply hwf x))

Would this have the effect that the kernel never reduces well-founded functions, and would that be desirable? We could even make it so that the kernel unfolds once, so that the base cases still work. Will maybe play around with it.

[nomeata]

First observations:

Yes, using dontReduce helps here, and reliably makes the kernel not reduce definitions by well-founded recursion. It doesn't even need an axiom, we can use

opaque withoutKernelReduction {P : Prop} (h : P) : P := h

But it closes the unseal foo escape hatch, so that breaks existing proofs.

A tedious work-around would be to offer a tactic that unfolds foo to fix, then rewrites to a reducingFix that doesn't use dontReduce and then lets the kernel go wild.

Less tedious would be to let the translation of wf rec functions look at the reducibity setting, and if it's semireducible (or even reducible) use reducingFix, else nonreducingFix, internally. This way one can at least get the old behavior, although only for the function as a whole.

[nomeata]

NB: Since #3772 (merged two weeks ago), rfl will no longer use Kernel.whnf, and the impact of this issue is thus reduced.