Proof: Difference between revisions
Content added Content deleted
Line 220: | Line 220: | ||
=={{header|ATS}}== |
=={{header|ATS}}== |
||
=== An unusual use of ATS === |
|||
The following seems similar, at least, to a completion of the task. |
|||
Although probably I could do more precisely what is asked, and encode some formal logic in the ATS proofs language, that is not what I do below. '''(Footnote: I am currently at work on the task.)''' Rosetta Code is here to show what a language can do, and so it seems better to show a bit of how ATS ''actually'' would be used. |
|||
<lang ATS>(* Let us do a little of the formal logic in ATS, even though this is |
|||
NOT an intended use of the facilities. However, I DO consider the |
|||
task a good didactic exercise. *) |
|||
(* 1. Define the natural numbers, the even numbers, and the odd |
|||
numbers. I shall do so by recursive "prop". *) |
|||
dataprop NATURAL (i : int) = |
|||
| ZERO (0) |
|||
| {0 <= i} S (i + 1) of NATURAL i |
|||
(* Even and odd are restrictions on the recursion indices. *) |
|||
propdef EVEN (i : int) = NATURAL (2 * i) |
|||
propdef ODD (i : int) = NATURAL ((2 * i) + 1) |
|||
(* 2.1 Define addition constructively (as a total function). *) |
|||
(* Let us define addition as the triple |
|||
(NATURAL i, NATURAL j, NATURAL (i + j)) *) |
|||
prfn |
|||
addition {i, j : nat} () :<prf> |
|||
(NATURAL i, NATURAL j, NATURAL (i + j)) = |
|||
let |
|||
prfun |
|||
add {i, j : nat} |
|||
{k : nat | k <= j} .<j - k>. |
|||
(partial_sum : NATURAL (i + k)) :<prf> NATURAL (i + j) = |
|||
sif k == j then |
|||
partial_sum |
|||
else |
|||
add {i, j} {k + 1} (S partial_sum) |
|||
prval i = add {0, i} {0} (ZERO ()) |
|||
prval j = add {0, j} {0} (ZERO ()) |
|||
prval sum = add {i, j} {0} i |
|||
in |
|||
(i, j, sum) |
|||
end |
|||
(* 3.1 Prove the sum of evens is even. *) |
|||
prfn |
|||
sum_of_evens {i, j : nat} () :<prf> |
|||
(EVEN i, EVEN j, EVEN (i + j)) = |
|||
addition {2 * i, 2 * j} () |
|||
(* 3.2 Prove addition is associative. *) |
|||
prfn |
|||
associativity {i, j, k : nat} () :<prf> |
|||
((NATURAL (i + j), NATURAL k, NATURAL (i + j + k)), |
|||
(NATURAL i, NATURAL (j + k), NATURAL (i + j + k))) = |
|||
(addition {i + j, k} (), |
|||
addition {i, j + k} ()) |
|||
(* 3.3 Prove addition is commutative. *) |
|||
prfn |
|||
commutativity {i, j : nat} () :<prf> |
|||
((NATURAL i, NATURAL j, NATURAL (i + j)), |
|||
(NATURAL j, NATURAL i, NATURAL (i + j))) = |
|||
(addition {i, j} (), |
|||
addition {j, i} ()) |
|||
(* 3.4 Try to prove that sum of two evens is odd. *) |
|||
#if 0 (* Change to 1 to see the attempted proof rejected. *) |
|||
#then |
|||
prfn |
|||
sum_of_evens_is_odd {i, j : nat} () :<prf> |
|||
(EVEN i, EVEN j, ODD (i + j)) = |
|||
(addition {i, j} (), |
|||
addition {j, i} ()) |
|||
#endif |
|||
(* 4.1 Prove the sum of evens is not odd. *) |
|||
prfn |
|||
sum_of_evens_isnot_odd {i, j : nat} () :<prf> |
|||
(* Some might--and SHOULD--object to the use of the remainder |
|||
function here, but ATS is not really made for doing |
|||
mathematical logic. It is a systems programming language, with |
|||
some limited proof capability included as a programming aid. *) |
|||
[k : nat | k mod 2 <> 1] |
|||
(EVEN i, EVEN j, NATURAL k) = |
|||
addition {2 * i, 2 * j} () |
|||
(* 4.2 Try to prove the sum of evens is not even. *) |
|||
#if 0 (* Change to 1 to see the attempted proof rejected. *) |
|||
#then |
|||
prfn |
|||
sum_of_evens_isnot_odd {i, j : nat} () :<prf> |
|||
[k : nat | k mod 2 <> 0] |
|||
(EVEN i, EVEN j, NATURAL k) = |
|||
addition {2 * i, 2 * j} () |
|||
#endif |
|||
(* A little main program, for your enjoyment. *) |
|||
implement |
|||
main0 () = |
|||
println! ("Success!")</lang> |
|||
{{out}} |
|||
<pre>$ patscc proof-primitively.dats && ./a.out |
|||
Success!</pre> |
|||
=== A more usual use of ATS === |
|||
Rosetta Code is here to show what a language can do, and so it seems better to show a bit of how ATS ''actually'' would be used. |
|||
In that case, addition is a poor operation upon which to base the demonstration. ''Multiplication'' would be much better, because ATS has relatively little built-in knowledge of multiplication; the operation has to be defined by axioms or recursively from addition. But I shall stick with addition, just the same. |
In that case, addition is a poor operation upon which to base the demonstration. ''Multiplication'' would be much better, because ATS has relatively little built-in knowledge of multiplication; the operation has to be defined by axioms or recursively from addition. But I shall stick with addition, just the same. |