Buggy structure matching in monads

Stream: lean4

[Gareth Ma]

import Mathlib.Data.Nat.Basic

def works (a b : ℕ) : (ℕ × ℤ) := Id.run do
  if h : (b % a) < a then
    let c := works (b % a) a
    return (a, c.2)
  else
    return (0, 1)

/- Two errors:
1. the `.match_1` (i.e. the `let (x, y) := ...`) is noncomputable
2. Well-foundedness is not proven automatically
-/
def fails (a b : ℕ) : (ℕ × ℤ) := Id.run do
  if h : (b % a) < a then
    let (x, y) := fails (b % a) a
    return (a, y)
  else
    return (0, 1)

[Gareth Ma]

The structure matching makes the code noncomputable and makes determining well-foundedness fail, which sounds buggy to me.

[Scott Morrison]

Please try to post a #mwe (in particular, you have imports missing here, or need to replace ℕ with Nat, etc)

[Scott Morrison]

I suspect this is a known issue, but I'm not finding an open issue. Let me ping @Joachim Breitner, who has been working on recursion recently, and may know off-hand.

It would be good to have an issue tracking this. It should include also the non-monadic code, to show that the issue is specific to the do notation.

[Scott Morrison]

I think also your termination_by and decreasing_by clauses should be removed from the example.

[Gareth Ma]

Fixed both. I will wait for Joachim's response and one of us can open an issue then

[Gareth Ma]

I always forget that \N is not in Lean haha

[Gareth Ma]

Here's a non-monadic example:

def works_again (a b : ℕ) : ℕ × ℤ := by
  by_cases h : (b % a) < a
  · let ⟨x, y⟩ := works_again (b % a) a
    exact (a, y)
  · exact (0, 1)

[Joachim Breitner]

Marking it as noncomputable makes the well-foundness proof go through. Is that expected or strange?

This is the supposedly non-computable definition, looks computable to me:

def fails.match_1.{u_1} : (motive : ℕ × ℤ → Sort u_1) → (x : ℕ × ℤ) → ((x : ℕ) → (y : ℤ) → motive (x, y)) → motive x :=
fun motive x h_1 => Prod.casesOn x fun fst snd => h_1 fst snd

and

def foo := fails.match_1

doesn't complain about non-computability.

So maybe the problem is that these auxillary definitoins are not compiled early enough for something that’s happening in the well-foundedness proof?

I haven’t seen an issue about this (but I don't know all the issues); feel free to report (ideally minimized to have no imports)