Zulip Chat Archive

Stream: new members

Topic: recursive definitions


view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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