Proof: Difference between revisions
→An unusual use of ATS
Line 225:
<lang ATS>(* Let us do a little
Line 241:
propdef ODD (i : int) = NATURAL ((2 * i) + 1)
(* To construct a number. *)
(* 2.1 Define addition constructively (as a total function). *)▼
(NATURAL i, NATURAL j, NATURAL (i + j)) *)▼
prfn
(NATURAL i, NATURAL j, NATURAL (i + j)) =▼
let
prfun
sif k ==
else
in
loop (ZERO ())
end
prfn
make_even {i : nat} () :<prf> EVEN i =
make_natural {2 * i} ()
prfn
make_odd {i : nat} () :<prf> ODD i =
make_natural {(2 * i) + 1} ()
prfn
addition {i, j : nat}
(i : NATURAL i,
let
prfun
add {k : nat | k <= j} .<j - k>.
(partial_sum : NATURAL (i + k),
shrinking : NATURAL (j - k)) :<prf>
NATURAL (i + j) =
case+ shrinking of
| ZERO () => partial_sum
| S (even_smaller) =>
add {k + 1} (S partial_sum, even_smaller)
prval
prval j = add {0, j} {0} (ZERO ())▼
prval sum = add {i, j} {0} i▼
in
end
prfn
addition_relation {i, j : nat} () :<prf>
let
prval i = make_natural {i} ()
prval j = make_natural {j} ()
in
(i, j, addition (i, j))
end
Line 270 ⟶ 302:
sum_of_evens {i, j : nat} () :<prf>
(EVEN i, EVEN j, EVEN (i + j)) =
(* or *)
prfn
sum_of_evens2 {i, j : nat} () :<prf>
(EVEN i, EVEN j, EVEN (i + j)) =
let
in
(i, j, addition (i, j))
end
(* 3.2 Prove addition is associative. *)
Line 278 ⟶ 322:
((NATURAL (i + j), NATURAL k, NATURAL (i + j + k)),
(NATURAL i, NATURAL (j + k), NATURAL (i + j + k))) =
(
(* 3.3 Prove addition is commutative. *)
Line 287 ⟶ 332:
((NATURAL i, NATURAL j, NATURAL (i + j)),
(NATURAL j, NATURAL i, NATURAL (i + j))) =
(
(* 3.4 Try to prove the sum of two evens is odd. *)
Line 297 ⟶ 342:
sum_of_evens_is_odd {i, j : nat} () :<prf>
(EVEN i, EVEN j, ODD (i + j)) =
(
#endif
Line 308 ⟶ 353:
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.
If suddenly a better approach occurs to me, I might substitute
it. *)
[k : nat | k mod 2 <> 1]
(EVEN i, EVEN j, NATURAL k) =
(* 4.2 Try to prove the sum of evens is not even. *)
Line 321 ⟶ 368:
[k : nat | k mod 2 <> 0]
(EVEN i, EVEN j, NATURAL k) =
#endif
| |||