Kata

This is a marginally more difficult version of Multiples of 3, you say?

We say that a divides b if b is a multiple of a. An inductive definition of this relation could be as follows:

Inductive divides (m : nat) : nat -> Prop :=
| O_divides : divides m O
| add_divides n (H : divides m n) : divides m (m + n).

The Coq stdlib defines this notion as well for both natural numbers and integers, albeit in a non-inductive way.

Now we define a predicate P on the natural numbers such that:

• P 24 holds
• P 40 holds
• P 60 holds
• P (n + m) holds if both P n and P m hold
• P l holds if there exists n, m such that l + n = m and both P n, P m hold

Show that P describes exactly the multiples of some natural number m.

Preloaded

Inductive divides (m : nat) : nat -> Prop :=
| O_divides : divides m O
| add_divides n (H : divides m n) : divides m (m + n).

Inductive P : nat -> Prop :=
| P_24 : P 24
| P_40 : P 40
| P_60 : P 60
| P_sum n m (Hn : P n) (Hm : P m) : P (n + m)
| P_diff l n m (Hl : l + n = m) (Hn : P n) (Hm : P m) : P l.