Stream: new members

Topic: recursive definitions

ROCKY KAMEN-RUBIO (May 30 2020 at 02:14):

I ready TPIL 8 once but I'm still confused about how lean wants me to structure my recursive definitions. I want to define a function that tells me whether the base 10 representation of a nat is all 1s or not. In a normal programming language like python I'd do something like this

def all_ones (n : ℕ) : Prop := n = 0 ∨  (n % 10 = 1 ∧ (all_ones (n / 10)))


In Haskell I'd do something like this, but I know Lean only lets you pattern match on constructors.

def all_ones (n : ℕ) : Prop
| 0 := ff
| 1 := tt
| (10*k + 1) := all_ones k
| _ := ff


How do I do this? Do I need to use some more extensive base 10 machinery with the nats?

Mario Carneiro (May 30 2020 at 02:48):

You can use a definition roughly analogous to the first one you gave, but you have to first prove the recursion is well founded

Mario Carneiro (May 30 2020 at 02:50):

def all_ones : ℕ → Prop | n :=
if h : n = 0 then true else
have n / 10 < n, from nat.div_lt_self (nat.pos_of_ne_zero h) dec_trivial,
n % 10 = 1 ∧ all_ones (n / 10)


Mario Carneiro (May 30 2020 at 02:52):

but this is more appropriate for a decidable proposition or boolean function. You can easily use the same construction to produce a computable boolean function witnessing this:

def all_ones : ℕ → bool | n :=
if h : n = 0 then true else
have n / 10 < n, from nat.div_lt_self (nat.pos_of_ne_zero h) dec_trivial,
n % 10 = 1 ∧ all_ones (n / 10)


the only difference is that I used bool instead of Prop, and everything else is handled by coercion

Mario Carneiro (May 30 2020 at 02:53):

If you don't care about decidability, there is a much simpler way to express this:

def all_ones (n : ℕ) : Prop := ∃ k : ℕ, 9 * n + 1 = 10 ^ k


Mario Carneiro (May 30 2020 at 02:57):

Does haskell really let you pattern match on 10 * k + 1? If so they must have some special support for this because this is undecidable in general if you put an arbitrary function in there

Bhavik Mehta (May 30 2020 at 03:28):

Mario Carneiro said:

Does haskell really let you pattern match on 10 * k + 1? If so they must have some special support for this because this is undecidable in general if you put an arbitrary function in there

Haskell doesn't let you pattern match like this - there used to be "n+k patterns" which let you match on eg n + 3 but it was removed a while back

Last updated: May 16 2021 at 05:21 UTC