user
This task only makes sense for dependently-typed languages and proof assistants, or for languages with a type system strong enough to emulate certain dependent types. It does *not* ask you to implement a theorem prover yourself.

In the following task the word "define" implies the need to build the system of Peano axioms using the language itself, that is a way to construct natural and even natural numbers in the canonical forms, as well as a definition of the rules of addition and a way to construct all other acceptable terms. The word "prove" means that some form of logical unification is used (i.e., it requires a type checker in the case of languages ​​with dependent types and a verifying algorithm in the case of proof assistants). Thus, the metatheory of a language must be expressive enough to allow embedding of the Peano axioms and the opportunity to carry out constructive proofs. Examples of the *trusted* mathematical metatheories can be given: SystemF for Haskell, MLTT for Agda, CoC/CoIC for Coq.

**Task**:

1. To illustrate the possibility of type formation and type introduction:
   1. Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}.
   2. Define a countably infinite set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers.
   3. Define a countably infinite set of odd natural numbers {1, 3, 5, 7, ...} within the previously defined set of natural numbers.
2. To illustrate the possibility of type elimination:
   1. Define the addition on natural numbers.
3. To demonstrate constructive proofs:
   1. Prove that the addition of *any* two even numbers is even.
   2. Prove that the addition is *always* associative.
   3. Prove that the addition is *always* commutative.
   4. Try to prove that the addition of *any* two even numbers is odd (it should be rejected).
4. To demonstrate the ability of disproofs:
   1. Prove that the addition of *any* two even numbers cannot be odd.
   2. Try to prove that the addition of *any* two even numbers cannot be even (it should be rejected).

3. and 4. can't be done using a simple number enumeration since there is a countable many natural numbers which is quantified in propositions.
assistant
Partial attempt only.

```
# 20200807 Raku programming solution (Incomplete)

sub check ($type, @testee) {
   @testee.map: { say "Is\t$_\t∈ ", $type.^name, "\t: ", $_ ~~ $type}
}

# 1.1 natural numbers

subset ℕ of Any where ( $_ ≥ 0 and $_.narrow ~~ Int ); # add constraints to Any
# alternative : subset ℕ of Int where * ≥ 0;

check ℕ, < 0 1 -1 3.3 >;

# 1.2 even natural numbers

subset EvenNatural of ℕ where * %% 2;

check EvenNatural, < 33 66 >;

# 1.3 odd natural numbers

subset OddNatural of ℕ where ( $_ ≠ $_ div 2 × 2 );
# alternative : subset OddNatural of ℕ where * !~~ Even;

check OddNatural, < 33 66 >;

# 2.1 Define the addition on natural numbers  (Translation from #Go)

sub infix:<⊞>(ℕ $a, ℕ $b --> ℕ) {
   return $a if $b == 0;
   return $a.succ ⊞ $b.pred;
}

check ℕ, [ 3 ⊞ 5 ];

# 3.1 Prove that the addition of any two even numbers is even
# 3.2 Prove that the addition is always associative
# 3.3 Prove that the addition is always commutative
# 3.4 Try to prove that the addition of any two even numbers is odd (it should be rejected)

# 4.1 Prove that the addition of any two even numbers cannot be odd
# 4.2 Try to prove that the addition of any two even numbers cannot be even (it should be rejected)

```

Output:

```
Is      0       ∈ ℕ     : True
Is      1       ∈ ℕ     : True
Is      -1      ∈ ℕ     : False
Is      3.3     ∈ ℕ     : False
Is      33      ∈ EvenNatural   : False
Is      66      ∈ EvenNatural   : True
Is      33      ∈ OddNatural    : True
Is      66      ∈ OddNatural    : False
Is      8       ∈ ℕ     : True

```