Proof: Difference between revisions
→{{header|Coq}}
m (→{{header|Phix}}: syntax coloured) |
|||
Line 217:
-- {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)
-- </lang>
=={{header|ATS}}==
<lang ATS>(* ATS does not contain a full-fledged proof language, but does
contain enough to do a considerable amount of *informal* proof
about a program.
Incidentally, the reductio proofs below are not really reductio
proofs, because ATS already knows to reject the absurd branches.
But I have used the method for proofs where it actually did
some useful work. *)
// 1.1
stadef is_natural (i : int) : bool = 0 <= i
sortdef natural = {i : int | is_natural i}
// 1.2
stadef is_even (i : int) : bool = i mod 2 == 0
sortdef even = {i : natural | is_even i}
// 1.3
stadef is_odd (i : int) : bool = i mod 2 == 1
sortdef odd = {i : natural | is_odd i}
// 2.1
// Addition of integers is primitive in ATS. Integers are not
// represented as chains of ones, or as anything like that. The
// facilities are specialized to be aids for system programming,
// rather than for doing formal logic.
// 3.1
// Proof is by definition of a total function. In this case, ATS
// already knows enough to verify the proof.
prfn
lemma_sum_of_evens
{i, j : even}
() :<prf> [is_even (i + j)] void = ()
// 3.2
// ATS usually can do association of addition itself (though it needs
// help for association of multiplication), but it is possible to
// write a proof function.
prfn
addition_is_associative
{i, j, k : int}
() :<prf> [(i + j) + k == i + (j + k)] void = ()
// 3.3
// ATS usually automatically commutes addition (though not
// multiplication). But here is a proof function.
prfn
addition_is_commutative
{i, j : int}
() :<prf> [i + j == j + i] void = ()
// 3.4
#if 0 // Change to 1 to make typechecking fail.
#then
prfn
sum_of_evens_is_odd
{i, j : even}
() :<prf> [is_odd (i + j)] void = ()
#endif
// Or:
prfn
sum_of_evens_is_not_odd__by_reductio_ad_absurdum
{i, j : even}
() :<prf> [~is_odd (i + j)] void =
sif is_odd (i + j) then
case+ 0 of
| 0 =/=>
{
(* ATS already knows i + j is not odd. Thus the contradiction
is proven. *)
prval () = prop_verify {~is_odd (i + j)} ()
}
else
()
// 4.1
prfn
sum_of_evens_is_not_odd
{i, j : even}
() :<prf> [~is_odd (i + j)] void = ()
// 4.2
#if 0 // Change to 1 to make typechecking fail.
#then
prfn
sum_of_evens_is_not_even
{i, j : even}
() :<prf> [~is_even (i + j)] void = ()
#endif
// Or:
prfn
sum_of_evens_is_even__by_reductio_ad_absurdum
{i, j : even}
() :<prf> [is_even (i + j)] void =
sif ~is_even (i + j) then
case+ 0 of
| 0 =/=>
{
(* ATS already knows i + j is even. Thus the contradiction is
proven. *)
prval () = prop_verify {is_even (i + j)} ()
}
else
()
implement
main0 () =
println! ("Success!")</lang>
{{out}}
<pre>$ patscc proof.dats && ./a.out
Success!</pre>
=={{header|Coq}}==
| |||