Zulip Chat Archive

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: Dec 20 2023 at 11:08 UTC