Kata

This Kata is a part of a collection of supplementary exercises for Logical Foundations.

Consider the set of all natural numbers that are multiples of 3. A straightforward inductive definition of this set is as follows:

• 0 is a multiple of 3
• For every natural number n that is a multiple of 3, 3 + n is also a multiple of 3

Another possible but rather clumsy inductive definition of the same set is as follows:

• 30 is a multiple of 3
• 21 is a multiple of 3
• For every pair of natural numbers (n, m) that are both multiples of 3, n + m is also a multiple of 3
• For every ordered triple of natural numbers (l, n, m) where n, m are multiples of 3 and l + n = m, l is also a multiple of 3

Prove that both inductive definitions do indeed define the same set.

Preloaded

The full source code for Preloaded.lean is displayed below for your reference:

inductive mult_3 : set ℕ
| mult_3_O :
    mult_3 0
| mult_3_SSS : ∀ n,
    mult_3 n →
    mult_3 (n + 3)

inductive mult_3' : set ℕ
| mult_3'_30 :
    mult_3' 30
| mult_3'_21 :
    mult_3' 21
| mult_3'_sum : ∀ n m,
    mult_3' n →
    mult_3' m →
    mult_3' (n + m)
| mult_3'_difference : ∀ l n m,
    mult_3' n →
    mult_3' m →
    l + n = m →
    mult_3' l

def SUBMISSION := mult_3 = mult_3'
notation `SUBMISSION` := SUBMISSION