# Zulip Chat Archive

## 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 `1`

s 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