## Stream: new members

### Topic: overlapping cases and well-foundedness

#### Mark Dickinson (Oct 21 2018 at 17:05):

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 (Oct 21 2018 at 17:06):

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 (Oct 21 2018 at 17:10):

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 (Oct 21 2018 at 17:12):

Beautiful! Thank you.

Last updated: May 12 2021 at 05:19 UTC