overlapping cases and well-foundedness

Stream: new members

[Mark Dickinson]

I'm trying to define a simple ℕ → ℕ → ℕ function using well-founded recursion. At top-level, I'm splitting on cases, and those cases overlap:

[Mark Dickinson]

def isqrt_inner : ℕ → ℕ → ℕ
| 0 _ := 0
| 1 _ := 1
| b n :=
    let k := shiftr b 1 in
    let a := have b - k < b, from sorry,
                    isqrt_inner (b - k) (shiftr n (2*k)) in
    shiftl a (k - 1) + (shiftr n (k + 1)) / a

Question: how would I go about replacing the sorry here? I need to be able to use the hypotheses that b is neither 0 nor 1, but I'm not sure how to get at those.

[Kenny Lau]

def isqrt_inner : ℕ → ℕ → ℕ
| 0 _ := 0
| 1 _ := 1
| b@(p+2) n :=
    let k := shiftr b 1 in
    let a := have b - k < b, from _,
                    isqrt_inner (b - k) (shiftr n (2*k)) in
    shiftl a (k - 1) + (shiftr n (k + 1)) / a

[Mark Dickinson]

Beautiful! Thank you.