Proof: Difference between revisions
→{{header|ATS}}
Line 220:
=={{header|ATS}}==
=== An unusual use of ATS ===
The following seems similar, at least, to a completion of the task.
<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.
| |||