Reducibility and decreasing_by

Stream: general

[Violeta Hernández]

While trying to minimize a related issue related to decidable instances, I came across the following odd behavior:

import Mathlib.Data.Nat.Basic

def foo (_m _n : ℕ) : Prop := True

theorem notSorry (m n : ℕ) (h : m ≠ 0) : Prod.Lex (· < ·) (· < ·) (m - 1, n) (m, n) := by
  apply Prod.Lex.left
  exact Nat.pred_lt h

@[reducible]
def decFoo {m n : ℕ} : Decidable (foo m n) :=
  if m = 0 then isTrue ⟨⟩ else
    letI : Decidable (foo (m - 1) n) := decFoo
    decidable_of_iff (foo (m - 1) n) Iff.rfl
termination_by (m, n)
decreasing_by apply notSorry; assumption

instance : DecidableRel foo := @decFoo

example : foo 2 2 := by decide

Here, foo 2 2 is successfully proven. But if we replace the code within decreasing_by by sorry, it fails.

Is this a known/intended behavior? I would have imagined that since proofs are erased, any sorry (or whatever other axiom) would be ignored while reducing the decidability instance.

[Violeta Hernández]

(Even more perplexingly, if we get rid of the second argument n throughout, the decide works with or without a sorry)

[Violeta Hernández]

Came up with a simpler example, this one confuses me even more

def bar (n : Nat) : Prop := True

noncomputable def decBar (n : Nat) : Decidable (bar n) :=
  WellFounded.fix (r := (· < ·)) Nat.lt_wfRel.wf (fun _ _ ↦ isTrue ⟨⟩) n

noncomputable instance : DecidablePred bar := decBar

-- This works?
example : bar 5 := by decide

[Violeta Hernández]

How can this possibly work if Lean also complains about how decBar is noncomputable?

[Violeta Hernández]

And, how come this breaks if you replace Nat.lt_wfRel.wf by sorry?

[Violeta Hernández]

And also how come Lean doesn't complain about computability when using termination_by but it does complain here?

[suhr]

Violeta Hernández said:

How can this possibly work if Lean also complains about how decBar is noncomputable?

noncomputable does not prevent reduction, it only matters for code generation.

[Joachim Breitner]

When reducing a definition defined by well founded recursion, the kernel does have to reduce the termination proof, and may get stuck on the sorry axiom. Proofs erasure is a concept of the compiler, not the kernel and it's concept of reduction.

Generally I'd strongly suggest to not rely on the reduction behavior of well-founded recursion, and use rewriting (simp, rw, unfold) instead of rfl or decide.

[Violeta Hernández]

That's a bit unfortunate given I wanted to prove decidability of a relation defined through well-founded recursion.

[François G. Dorais]

Joachim Breitner said:

Generally I'd strongly suggest to not rely on the reduction behavior of well-founded recursion, and use rewriting (simp, rw, unfold) instead of rfl or decide.

Don't simp and rw use rfl sometimes?

[Sebastian Ullrich]

Recall that wfrec defs are irreducible by default

[Joachim Breitner]

Violeta Hernández said:

That's a bit unfortunate given I wanted to prove decidability of a relation defined through well-founded recursion.

You can still prove it, in a way, but if you then want to efficiently decide relations using decide you’ll have to work around this limitation.

You can use by native_decide if you are fine with the caveats. Then you can get very efficient decision procedures.

The next best option is to define a variant of your function, provably equivlaent, that uses Nat.rec with lots of fuel, and define the Decidable instance using that. Something along these lines

def lots_of_fuel : Nat := 9223372036854775807

def rsimp_iterate {α : Sort u} (x : α) (f : α → α) : α :=
  Nat.rec x (fun _ ih => f ih) lots_of_fuel

theorem reduce_with_fuel {α : Sort u} {x : α} {f : α → α} (h : x = f x) :
    x = rsimp_iterate x f := by
    unfold rsimp_iterate
    exact Nat.rec rfl (fun _ ih => h.trans (congrArg f ih)) lots_of_fuel

def Nat.gcd' : (n m : Nat) → Nat :=
  rsimp_iterate Nat.gcd fun gcd m n =>
    if m = 0 then n else gcd (n % m) m

theorem Nat.gcd'_eq_gcd : Nat.gcd = Nat.gcd' :=
  reduce_with_fuel Nat.gcd.eq_unfold