recursive definitions

Stream: new members

[ROCKY KAMEN-RUBIO]

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]

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]

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]

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]

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]

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]

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