raku-rosettacode/programming_tasks/P/Proof.md

Proof

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