Proof: Difference between revisions
added Raku programming solution (Incomplete)
m (→{{header|Phix}}: replaced a "test" with "axiom") |
(added Raku programming solution (Incomplete)) |
||
Line 1,069:
The fact that there's no error indicates that all proofs are verified.
=={{header|Raku}}==
Partial attempt only.
<lang perl6># 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)
</lang>
{{out}}
<pre>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
</pre>
=={{header|Salmon}}==
| |||