Proof
Proof is a draft programming task. It is not yet considered ready to be promoted as a complete task, for reasons that should be found in its talk page.
This task only makes sense for dependently-typed languages and proof assistants, or for languages with a type system strong enough to emulate certain dependent types. It does not ask you to implement a theorem prover yourself.
In the following task the word "define" implies the need to build the system of Peano axioms using the language itself, that is a way to construct natural and even natural numbers in the canonical forms, as well as a definition of the rules of addition and a way to construct all other acceptable terms. The word "prove" means that some form of logical unification is used (i.e., it requires a type checker in the case of languages with dependent types and a verifying algorithm in the case of proof assistants). Thus, the metatheory of a language must be expressive enough to allow embedding of the Peano axioms and the opportunity to carry out constructive proofs. Examples of the trusted mathematical metatheories can be given: SystemF for Haskell, MLTT for Agda, CoC/CoIC for Coq.
Task:
- To illustrate the possibility of type formation and type introduction:
- Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}.
- Define a countably infinite set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers.
- Define a countably infinite set of odd natural numbers {1, 3, 5, 7, ...} within the previously defined set of natural numbers.
- To illustrate the possibility of type elimination:
- Define the addition on natural numbers.
- To demonstrate constructive proofs:
- Prove that the addition of any two even numbers is even.
- Prove that the addition is always associative.
- Prove that the addition is always commutative.
- Try to prove that the addition of any two even numbers is odd (it should be rejected).
- To demonstrate the ability of disproofs:
- Prove that the addition of any two even numbers cannot be odd.
- Try to prove that the addition of any two even numbers cannot be even (it should be rejected).
3. and 4. can't be done using a simple number enumeration since there is a countable many natural numbers which is quantified in propositions.
ACL2
3.1. using built-in natural numbers:
(thm (implies (and (evenp x) (evenp y))
(evenp (+ x y))))
Agda
module PeanoArithmetic where
-- 1.1. The natural numbers.
--
-- ℕ-formation: ℕ is set.
--
-- ℕ-introduction: zero ∈ ℕ,
-- a ∈ ℕ | (suc a) ∈ ℕ.
--
data ℕ : Set where
zero : ℕ
suc : (n : ℕ) → ℕ
-- 1.2. The even natural numbers.
--
data 2×ℕ : ℕ → Set where
zero₁ : 2×ℕ zero
2+_ : {m : ℕ} → 2×ℕ m → 2×ℕ (suc (suc m) )
-- 1.3. The odd natural numbers.
--
data 2×ℕ+1 : ℕ → Set where
one : 2×ℕ+1 (suc zero)
2+₁_ : {m : ℕ} → 2×ℕ+1 m → 2×ℕ+1 (suc (suc m) )
-- 2.1. The rule of addition.
--
-- via ℕ-elimination.
--
infixl 6 _+_
_+_ : (k : ℕ) → (n : ℕ) → ℕ
zero + n = n
(suc m) + n = suc (m + n)
-- 3.1. Sum of any two even numbers is even.
--
-- This function takes any two even numbers and returns their sum as an even
-- number, this is the type, i.e. logical proposition, algorithm itself is a
-- proof which builds a required term of a given (inhabited) type, and the
-- typechecker performs that proof (by unification, so that this is a form of
-- compile-time verification).
--
even+even≡even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ (m + n)
even+even≡even zero₁ n = n
even+even≡even (2+ m) n = 2+ (even+even≡even m n)
-- The identity type (for propositional equality).
--
infix 4 _≡_
data _≡_ {A : Set} (m : A) : A → Set where
refl : m ≡ m
sym : {A : Set} → {m n : A} → m ≡ n → n ≡ m
sym refl = refl
trans : {A : Set} → {m n p : A} → m ≡ n → n ≡ p → m ≡ p
trans refl n≡p = n≡p
-- refl, sym and trans forms an equivalence relation.
cong : {A B : Set} → (f : A → B) → {m n : A} → m ≡ n → f m ≡ f n
cong f refl = refl
-- 3.2.1. Direct proof of the associativity of addition using propositional
-- equality.
--
+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative zero _ _ = refl
+-associative (suc m) n p = cong suc (+-associative m n p)
-- Proof _of_ mathematical induction on the natural numbers.
--
-- P 0, ∀ x. P x → P (suc x) | ∀ x. P x.
--
ind : (P : ℕ → Set) → P zero → ((m : ℕ) → P m → P (suc m)) → (m : ℕ) → P m
ind _ P₀ _ zero = P₀
ind P P₀ next (suc n) = next n (ind P P₀ next n)
-- 3.2.2. The associativity of addition by induction (with propositional
-- equality, again).
--
+-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)
+-associative′ m n p = ind P P₀ is m
where
P : ℕ → Set
P m = m + n + p ≡ m + (n + p)
P₀ : P zero
P₀ = refl
is : (m : ℕ) → P m → P (suc m)
is _ Pi = cong suc Pi
-- Syntactic sugar for equational reasoning (we don't use preorders here).
infix 4 _≋_
data _≋_ (m n : ℕ) : Set where
refl₁ : m ≡ n → m ≋ n
infix 1 begin_
begin_ : {m n : ℕ} → m ≋ n → m ≡ n
begin (refl₁ m≡n) = m≡n
infixr 2 _~⟨_⟩_
_~⟨_⟩_ : (m : ℕ){n p : ℕ} → m ≡ n → n ≋ p → m ≋ p
_ ~⟨ m≡n ⟩ (refl₁ n≡p) = refl₁ (trans m≡n n≡p)
infix 3 _∎
_∎ : (m : ℕ) → m ≋ m
_∎ _ = refl₁ refl
-- Some helper proofs.
m+0≡m : (m : ℕ) → m + zero ≡ m
m+0≡m zero = refl
m+0≡m (suc m) = cong suc (m+0≡m m)
m+1+n≡1+m+n : (m n : ℕ) → m + (suc n) ≡ suc (m + n)
m+1+n≡1+m+n zero n = refl
m+1+n≡1+m+n (suc m) n = cong suc (m+1+n≡1+m+n m n)
-- 3.3. The commutativity of addition using equational reasoning.
--
+-commutative : (m n : ℕ) → m + n ≡ n + m
+-commutative zero n = sym (m+0≡m n)
+-commutative (suc m) n =
begin
suc m + n
~⟨ refl ⟩
suc (m + n)
~⟨ cong suc (+-commutative m n) ⟩
suc (n + m)
~⟨ sym (m+1+n≡1+m+n n m) ⟩
n + suc m
∎
-- 3.4.
--
even+even≡odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ+1 (m + n)
even+even≡odd zero₁ zero₁ = {!!}
even+even≡odd _ _ = {!!}
-- ^
-- That gives
--
-- ?0 : 2×ℕ+1 (zero + zero)
-- ?1 : 2×ℕ+1 (m + n)
--
-- but 2×ℕ+1 (zero + zero) = 2×ℕ+1 0 which is uninhabited, so that this proof
-- can not be writen.
--
-- The absurd (obviously uninhabited) type.
--
-- ⊥-introduction is empty.
--
data ⊥ : Set where
-- The negation of a proposition.
--
infix 6 ¬_
¬_ : Set → Set
¬ A = A → ⊥
-- 4.1. Disproof or proof by contradiction.
--
-- To disprove even+even≡odd we assume that even+even≡odd and derive
-- absurdity, i.e. uninhabited type.
--
even+even≢odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ+1 (m + n)
even+even≢odd zero₁ zero₁ ()
even+even≢odd zero₁ (2+ n) (2+₁ m+n) = even+even≢odd zero₁ n m+n
even+even≢odd (2+ m) n (2+₁ m+n) = even+even≢odd m n m+n
-- 4.2.
--
-- even+even≢even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)
-- even+even≢even zero zero ()
-- ^
-- rejected with the following message:
--
-- 2×ℕ zero should be empty, but the following constructor patterns
-- are valid:
-- zero
-- when checking that the clause even+even≢even zero zero () has type
-- {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)
--
ATS
An unusual use of ATS
The following seems similar, at least, to a completion of the task. The main problem I can see in it is it mostly consists of letting ATS do math it already knows on the recursion indices of the definition of addition. These happen to correspond to the natural numbers abstractly represented by the "prop" NATURAL.
Nevertheless, one can see that ATS is capable of some "abstract" reasoning. In fact, the prelude includes a recursive definition of multiplication, and in the ATS entry for the greatest common divisor task I present practical (not "first principles") definitions of the gcd both by way of axioms and by recursive prop.
And the following does show, by total functions, how to construct a particular number (by counting up to it) and how to add (again by counting). That proofs of such things as "evens add up to evens" are then trivialized is perhaps a point in favor of ATS, as a systems programming language.
(* Let us do a little quasi-math 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)
(* To construct a number. *)
prfn
make_natural {i : nat} () :<prf> NATURAL i =
let
prfun
loop {i, k : nat | k <= i} .<i - k>.
(partial_num : NATURAL k) :<prf>
NATURAL i =
sif k == i then
partial_num
else
loop (S partial_num)
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} ()
(* 2.1 Define addition. *)
prfn
addition {i, j : nat}
(i : NATURAL i,
j : NATURAL j) :<prf> NATURAL (i + j) =
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 sum = add {0} (i, j)
in
sum
end
prfn
addition_relation {i, j : nat} () :<prf>
(NATURAL i, NATURAL j, NATURAL (i + j)) =
let
prval i = make_natural {i} ()
prval j = make_natural {j} ()
in
(i, j, addition (i, j))
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_relation {2 * i, 2 * j} ()
(* or *)
prfn
sum_of_evens2 {i, j : nat} () :<prf>
(EVEN i, EVEN j, EVEN (i + j)) =
let
prval i = make_even {i} ()
prval j = make_even {j} ()
in
(i, j, addition (i, j))
end
(* 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_relation {i + j, k} (),
addition_relation {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_relation {i, j} (),
addition_relation {j, i} ())
(* 3.4 Try to prove the 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_relation {i, j} (),
addition_relation {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.
If suddenly a better approach occurs to me, I might substitute
it. *)
[k : nat | k mod 2 <> 1]
(EVEN i, EVEN j, NATURAL k) =
addition_relation {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_relation {2 * i, 2 * j} ()
#endif
(* A little main program, for your enjoyment. *)
implement
main0 () =
println! ("Success!")- Output:
$ patscc proof-primitively.dats && ./a.out Success!
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.
Another thing to note is that ATS contains multiple sublanguages, and that proofs are not done in the same sublanguage as executable code. There are dependent types of a practical kind, but not at all in the way some other languages have dependent types as first-class objects of the full language.
(* 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!")- Output:
$ patscc proof.dats && ./a.out Success!
Coq
(* 1.1 Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}. *)
Inductive nat : Set :=
| O : nat
| S : nat -> nat.
(* 2.1 Define the addition on natural numbers. *)
Fixpoint plus (n m:nat) {struct n} : nat :=
match n with
| O => m
| S p => S (p + m)
end
where "n + m" := (plus n m) : nat_scope.
(* 1.2 Define a countably infinite set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers. *)
Inductive even : nat -> Prop :=
| even_O : even O
| even_SSn : forall n:nat,
even n -> even (S (S n)).
(* 1.3 Define a countably infinite set of odd natural numbers {1, 3, 5, 7, ...} within the previously defined set of natural numbers. *)
Inductive odd : nat -> Prop :=
| odd_1 : odd (S O)
| odd_SSn : forall n:nat,
odd n -> odd (S (S n)).
(* 3.1 Prove that the addition of any two even numbers is even. *)
Theorem even_plus_even : forall n m:nat,
even n -> even m -> even (n + m).
Proof.
intros n m H H0.
elim H.
trivial.
intros.
simpl.
case even_SSn.
intros.
apply even_SSn; assumption.
assumption.
Qed.
(* 3.2 Prove that the addition is always associative. *)
Lemma plus_assoc : forall a b c, a + (b + c) = (a + b) + c.
Proof.
induction a; [ solve [ auto ] | ].
intros. simpl. rewrite IHa. reflexivity.
Qed.
(* 3.3 Prove that the addition is always commutative. *)
Lemma plus_comm : forall a b, a + b = b + a.
Proof.
induction a.
- induction b; [ solve [ auto ] | ].
simpl. rewrite <- IHb. simpl. reflexivity.
- induction b.
+ simpl. rewrite IHa. reflexivity.
+ simpl. rewrite <- IHb. rewrite IHa. simpl. rewrite IHa. reflexivity.
Qed.
Fixpoint even_n_odd_Sn {n} (p : even n) : odd (S n) :=
match p with
| even_O => odd_1
| even_SSn _ p' => odd_SSn _ (even_n_odd_Sn p')
end.
Fixpoint odd_n_even_Sn {n} (p : odd n) : even (S n) :=
match p with
| odd_1 => even_SSn O even_O
| odd_SSn _ p' => even_SSn _ (odd_n_even_Sn p')
end.
Lemma even_Sn_odd_n : forall n, even (S n) -> odd n.
Proof.
destruct n.
- intros. inversion H.
- intros. inversion H. subst. apply even_n_odd_Sn. assumption.
Qed.
Lemma odd_Sn_even_n : forall n, odd (S n) -> even n.
Proof.
destruct n.
- constructor.
- intros. inversion H. subst. apply odd_n_even_Sn. assumption.
Qed.
Lemma not_even_and_odd : forall n, even n -> odd n -> False.
Proof.
induction n.
- intros. inversion H0.
- intros. apply IHn.
+ apply (odd_Sn_even_n _ H0).
+ apply (even_Sn_odd_n _ H).
Qed.
(* 3.4 Try to prove that the addition of any two even numbers is odd (it should be rejected). *)
Goal forall n m, even n -> even m -> odd (n + m) -> False.
Proof.
intros ? ? en em onpm.
assert (enpm := even_plus_even _ _ en em).
exact (not_even_and_odd _ enpm onpm).
Qed.
(* 4.1 Prove that the addition of any two even numbers cannot be odd. *)
Goal forall n m, even n -> even m -> odd (n + m) -> False.
Proof.
intros. assert (Hx := even_plus_even _ _ H H0).
apply (not_even_and_odd _ Hx H1).
Qed.
(* 4.2 Try to prove that the addition of any two even numbers cannot be even (it should be rejected). *)
Goal forall n m, even n -> even m -> ~even (n + m) -> False.
Proof.
intros. apply H1. apply (even_plus_even _ _ H H0).
Qed.
FreeBASIC
Type Axioma
r As String
s As String
End Type
Dim Shared axiomas(1 To 6) As Axioma
axiomas(1).r = "even+1": axiomas(1).s = "odd"
axiomas(2).r = "even": axiomas(2).s = "2*int"
axiomas(3).r = "2*int+2*int": axiomas(3).s = "2*(int+int)"
axiomas(4).r = "(int+int)": axiomas(4).s = "int"
axiomas(5).r = "2*int": axiomas(5).s = "even"
axiomas(6).r = "odd": axiomas(6).s = "2*int+1"
Sub Proof(a As String, b As String)
'-- try to convert a into b using only the above axiomas
Dim As String w = a
Dim As String seen() ' -- (avoid infinite loops)
Dim As Integer i, k, hit
Do
Print Using """&"""; w
Redim Preserve seen(Lbound(seen) To Ubound(seen) + 1)
seen(Ubound(seen)) = w
If w = b Then Exit Do
hit = 0
For i = Lbound(axiomas) To Ubound(axiomas)
k = Instr(w, axiomas(i).r)
If k > 0 Then
w = Left(w, k - 1) & axiomas(i).s & Mid(w, k + Len(axiomas(i).r))
hit = i
Exit For
End If
Next i
Print " == ";
Loop Until hit = 0
Print Using "{""&"", ""&"", &}"; a; b; Iif(w = b, "true", "false")
End Sub
Proof("even+even", "even")
Proof("even+1", "odd")
'--bad proofs:
Proof("int", "even")
Sleep
- Output:
"even+even"
== "2*int+even"
== "2*int+2*int"
== "2*(int+int)"
== "2*int"
== "even"
{"even+even", "even", true}
"even+1"
== "odd"
{"even+1", "odd", true}
"int"
{"int", "even", false}
Go
Go lacks the infrastructure for theorem proving and so there's a limit to what can be done here. Rather than give up altogether, I've therefore just done what I can.
It's not difficult (though extremely inefficient) to program a Peano representation of the natural numbers (including addition thereon) in a non-rigorous way and I've based this on the code here which was written by the Go authors themselves to test heavy recursion (part 1.1 and 2).
Even numbers of the form (2 * x) and odd numbers of the form (2 * x + 1) can then be easily constructed by creating types with only one field, the natural number 'x' (parts 1.2 and 1.3).
We can then define addition for the even number type by simply adding the fields 'x' of the operands. Given the method of construction it is obvious that 3.1 must be true and 3.4, 4.1 and 4.2 must be false. If it were otherwise the 'addEven' function would simply not compile in a strongly-typed language such as Go.
However, there is no obvious way to show that 3.2 and 3.3 must always be true (though you could argue that addition must be commutative because the 'addEven' function is symmetric in relation to its arguments). So all I've been able to do here is write functions to test these assertions for given even numbers whilst accepting that this doesn't constitute a proof for all such cases.
package main
import "fmt"
// Represents a natural number.
type Number struct {
pred *Number
}
// Represents an even natural number: 2 * half.
type EvenNumber struct {
half *Number
}
// Represents an odd natural number: 2 * half + 1.
type OddNumber struct {
half *Number
}
// Returns the natural number zero by a nil pointer.
func zero() *Number { return nil }
// Tests whether a natural number is zero.
func isZero(x *Number) bool { return x == nil }
// Increments a natural number.
func add1(x *Number) *Number {
y := new(Number)
y.pred = x
return y
}
// Decrements a natural number.
func sub1(x *Number) *Number { return x.pred }
// Adds two natural numbers.
func add(x, y *Number) *Number {
if isZero(y) {
return x
}
return add(add1(x), sub1(y))
}
// Adds two even natural numbers.
func addEven(x, y *EvenNumber) *EvenNumber {
if isZero(y.half) {
return x
}
return genEven(add(x.half, y.half))
}
// Adds two odd natural numbers.
func addOdd(x, y *OddNumber) *EvenNumber {
z := add(x.half, y.half)
return genEven(add1(z))
}
// Generate a natural number from a uint.
func gen(n uint) *Number {
if n > 0 {
return add1(gen(n - 1))
}
return zero()
}
// Generate an even natural number: 2 * half.
func genEven(half *Number) *EvenNumber {
return &EvenNumber{half}
}
// Generate an odd natural number: 2 * half + 1.
func genOdd(half *Number) *OddNumber {
return &OddNumber{half}
}
// Counts a natural number i.e returns its integer representation.
func count(x *Number) uint {
if isZero(x) {
return 0
}
return count(sub1(x)) + 1
}
// Counts an even natural number i.e returns its integer representation.
func countEven(x *EvenNumber) uint {
return count(x.half) * 2
}
// Counts an odd natural number i.e returns its integer representation.
func countOdd(x *OddNumber) uint {
return count(x.half)*2 + 1
}
// Test if even number addition is commutative for given numbers.
func testCommutative(e1, e2 *EvenNumber) {
c1, c2 := countEven(e1), countEven(e2)
passed := countEven(addEven(e1, e2)) == countEven(addEven(e2, e1))
symbol := "=="
if !passed {
symbol = "!="
}
fmt.Printf("\n%d + %d %s %d + %d\n", c1, c2, symbol, c2, c1)
}
// Test if even number arithmetic is associative for given numbers.
func testAssociative(e1, e2, e3 *EvenNumber) {
c1, c2, c3 := countEven(e1), countEven(e2), countEven(e3)
passed := countEven(addEven(addEven(e1, e2), e3)) == countEven(addEven(e1, addEven(e2, e3)))
symbol := "=="
if !passed {
symbol = "!="
}
fmt.Printf("\n(%d + %d) + %d %s %d + (%d + %d)\n", c1, c2, c3, symbol, c1, c2, c3)
}
func main() {
numbers := [10]*Number{}
fmt.Println("The first 10 natural numbers are:")
for i := uint(0); i < 10; i++ {
numbers[i] = gen(i)
fmt.Printf("%d ", count(numbers[i]))
}
fmt.Println("\n")
fmt.Println("The first 10 even natural numbers are:")
for i := uint(0); i < 10; i++ {
e := genEven(numbers[i])
fmt.Printf("%d ", countEven(e))
}
fmt.Println("\n")
fmt.Println("The first 10 odd natural numbers are:")
for i := uint(0); i < 10; i++ {
o := genOdd(numbers[i])
fmt.Printf("%d ", countOdd(o))
}
fmt.Println("\n")
fmt.Print("The sum of the first 10 natural numbers is: ")
sum := numbers[0]
for i := 1; i < 10; i++ {
sum = add(sum, numbers[i])
}
fmt.Println(count(sum))
fmt.Print("\nThe sum of the first 10 even natural numbers (increasing order) is: ")
sumEven := genEven(numbers[0])
for i := 1; i < 10; i++ {
sumEven = addEven(sumEven, genEven(numbers[i]))
}
fmt.Println(countEven(sumEven))
fmt.Print("\nThe sum of the first 10 even natural numbers (decreasing order) is: ")
sumEven = genEven(numbers[9])
for i := 8; i >= 0; i-- {
sumEven = addEven(sumEven, genEven(numbers[i]))
}
fmt.Println(countEven(sumEven))
testCommutative(genEven(numbers[8]), genEven(numbers[9]))
testAssociative(genEven(numbers[7]), genEven(numbers[8]), genEven(numbers[9]))
}
- Output:
The first 10 natural numbers are: 0 1 2 3 4 5 6 7 8 9 The first 10 even natural numbers are: 0 2 4 6 8 10 12 14 16 18 The first 10 odd natural numbers are: 1 3 5 7 9 11 13 15 17 19 The sum of the first 10 natural numbers is: 45 The sum of the first 10 even natural numbers (increasing order) is: 90 The sum of the first 10 even natural numbers (decreasing order) is: 90 16 + 18 == 18 + 16 (14 + 16) + 18 == 14 + (16 + 18)
Haskell
Using GADTs and type families it is possible to write a partial adaptation of the Agda version:
{-# LANGUAGE TypeOperators, TypeFamilies, GADTs #-}
module PeanoArithmetic where
-- 1.1. Natural numbers.
data Z = Z
data S m = S m
-- 2.1. Addition.
infixl 6 :+
type family x :+ y
type instance Z :+ n = n
type instance S m :+ n = S (m :+ n)
-- 1.2. Even natural numbers.
data En :: * -> * where
Ez :: En Z
Es :: En m -> En (S (S m))
-- 1.3. Odd natural numbers.
data On :: * -> * where
Oo :: On (S Z)
Os :: On m -> On (S (S m))
-- 3.1. Sum of any two even numbers is even.
sum_of_even_is_even :: En m -> En n -> En (m :+ n)
sum_of_even_is_even Ez n = n
sum_of_even_is_even (Es m) n = Es $ sum_of_even_is_even m n
-- The identity type for natural numbers.
infix 4 :=
data (:=) m :: * -> * where
Refl :: m := m
sym :: m := n -> n := m
sym Refl = Refl
trans :: m := n -> n := p -> m := p
trans Refl np = np
cong :: m := n -> S m := S n
cong Refl = Refl
-- 3.2. Associativity of addition (via propositional equality).
class AssocAdd m where
proof :: m -> n -> p -> (m :+ n) :+ p := m :+ (n :+ p)
instance AssocAdd Z where
proof Z _ _ = Refl
instance AssocAdd m => AssocAdd (S m) where
proof (S m) n p = cong $ proof m n p
-- Induction, associativity of addition by induction, equational reasoning and
-- commutativity of addition is too tricky.
-- 3.4. Bad proof.
sum_of_even_is_odd :: En m -> En n -> On (m :+ n)
-- ^
-- Сan not be written totally:
--
sum_of_even_is_odd Ez Ez = undefined
-- ^
-- then, in GHCi:
--
-- *PeanoArithmetic> :t sum_of_even_is_odd Ez Ez
-- sum_of_even_is_odd Ez Ez :: On (Z :+ Z)
-- *PeanoArithmetic> :t undefined :: On (Z :+ Z)
-- undefined :: On (Z :+ Z) :: On Z
-- *PeanoArithmetic> :t sum_of_even_is_odd Ez Ez :: On Z
-- sum_of_even_is_odd Ez Ez :: On Z :: On Z
-- *PeanoArithmetic> :t Oo
-- Oo :: On (S Z)
-- *PeanoArithmetic> :t Os Oo
-- Os Oo :: On (S (S (S Z)))
-- *PeanoArithmetic> :t Os (Os Oo)
-- Os (Os Oo) :: On (S (S (S (S (S Z)))))
--
-- so that sum_of_even_is_odd Ez Ez :: On Z, but On Z is empty, it is impossible
-- to write such a proof.
--
-- Uninhabited type.
data Bot
-- Negation.
type Not a = a -> Bot
-- 4.1. Disproof.
sum_of_even_is_not_odd :: En m -> En n -> Not (On (m :+ n))
sum_of_even_is_not_odd Ez (Es n) (Os mn) = sum_of_even_is_not_odd Ez n mn
sum_of_even_is_not_odd (Es m) n (Os mn) = sum_of_even_is_not_odd m n mn
sum_of_even_is_not_odd Ez Ez _ =
error "impossible happened in sum_of_even_is_not_odd!"
-- ^
-- partial, however, we know that Ez :: En Z, Z + Z = Z and On Z is
-- uninhabited, so that this clause is unreachable.
--
-- Also, GHC complains:
--
-- Warning: Pattern match(es) are non-exhaustive
-- In an equation for `sum_of_even_is_not_odd':
-- Patterns not matched:
-- Ez (Es _) Oo
-- (Es _) _ Oo
--
-- and can't find that this clauses is unreachable too, since this isn't type check:
--
-- sum_of_even_is_not_odd Ez (Es _) Oo = undefined
-- sum_of_even_is_not_odd (Es _) _ Oo = undefined
--
-- 4.2. Bad disproof.
sum_of_even_is_not_even :: En m -> En n -> Not (En (m :+ n))
--
-- Starting from a partial definition:
--
sum_of_even_is_not_even Ez Ez _ = undefined
--
-- we can show that it can not be rewritten totally:
--
-- *PeanoArithmetic> :t sum_of_even_is_not_even Ez Ez
-- sum_of_even_is_not_even Ez Ez :: Not (En (Z :+ Z))
-- *PeanoArithmetic> :t sum_of_even_is_not_even Ez Ez :: Not (En Z)
-- sum_of_even_is_not_even Ez Ez :: Not (En Z) :: Not (En Z)
-- *PeanoArithmetic> :t sum_of_even_is_not_even Ez Ez :: En Z -> Bot
-- sum_of_even_is_not_even Ez Ez :: En Z -> Bot :: En Z -> Bot
-- *PeanoArithmetic> :t Ez
-- Ez :: En Z
-- *PeanoArithmetic> :t (sum_of_even_is_not_even Ez Ez :: En Z -> Bot) Ez
-- (sum_of_even_is_not_even Ez Ez :: En Z -> Bot) Ez :: Bot
--
-- since we have a "citizen" of an uninhabited type here (contradiction!).
--
See also Proof/Haskell for implementation of a small theorem prover.
Idris
Idris supports two types of proofs: using tactics, like Coq, or just write functions like Agda. These ways can be combined.
module Proof
-- Enable terminator checker by default
%default total
-- 1.1 Natural numbers
%elim
data MyNat
= Z
| S MyNat
-- 1.2 Even naturals
%elim
data EvNat : MyNat -> Type where
EvO : EvNat Z
EvSS : EvNat x -> EvNat (S (S x))
-- 1.3 Odd naturals
%elim
data OddNat : MyNat -> Type where
Odd1 : OddNat (S Z)
OddSS : OddNat x -> OddNat (S (S x))
-- 2.1 addition
infixl 4 :+
(:+) : MyNat -> MyNat -> MyNat
(:+) Z b = b
(:+) (S a) b = S (a :+ b)
-- 3.1, Prove that the addition of any two even numbers is even.
evensPlus1 : {a : MyNat} -> {b : MyNat} -> (EvNat a) -> (EvNat b) -> (EvNat (a :+ b))
evensPlus1 ea eb = ?proof31
congS : {a : MyNat} -> {b : MyNat} -> (a = b) -> (S a = S b)
congS refl = refl
evensPlus2 : {a : MyNat} -> {b : MyNat} -> (EvNat a) ->(EvNat b) -> (EvNat (a :+ b))
evensPlus2 EvO eb = eb
evensPlus2 {a=(S (S a))} (EvSS ea) eb = EvSS (evensPlus2 ea eb)
-- 3.2 Prove that the addition is always associative.
plusAssoc : (a : MyNat) -> (b : MyNat) -> (c : MyNat) -> (a :+ b) :+ c = a :+ (b :+ c)
plusAssoc Z b c = refl
plusAssoc (S a) b c = congS (plusAssoc a b c)
-- 3.3 Prove that the addition is always commutative.
plus0_r : (a : MyNat) -> a :+ Z = a
plus0_r Z = refl
plus0_r (S a) = congS (plus0_r a)
plusS_r : (a : MyNat) -> (b : MyNat) -> a :+ S b = S (a :+ b)
plusS_r Z b = refl
plusS_r (S a) b = congS (plusS_r a b)
plusComm : (a : MyNat) -> (b : MyNat) -> a :+ b = b :+ a
plusComm a b = ?proof33
-- 4.1 Prove that the addition of any two even numbers cannot be odd.
evenNotOdd : (ea : EvNat a) -> (oa : OddNat a) -> _|_
evenNotOdd (EvSS e) (OddSS o) = evenNotOdd e o
evensPlusNotOdd : (ea : EvNat a) -> (eb : EvNat b) -> (OddNat (a :+ b)) -> _|_
evensPlusNotOdd EvO (EvSS eb) (OddSS ob) = evenNotOdd eb ob
evensPlusNotOdd (EvSS y) EvO oab = ?epno_so
evensPlusNotOdd (EvSS y) (EvSS z) oab = ?epno_ss
---------- Proofs ----------
Proof.proof31 = proof
intro a
intro b
intro ea
intro eb
induction ea
compute
exact eb
intro x
intro ex
intro exh
exact (EvSS exh)
Proof.proof33 = proof
intros
induction a
compute
rewrite sym (plus0_r b)
trivial
intro a'
intro ha'
compute
rewrite sym (plusS_r b a')
exact (congS ha')
Proof.epno_ss = proof
intro x
intro ex
intro y
intro ey
compute
rewrite sym ( plusS_r x (S y))
rewrite sym ( plusS_r x y)
intro os4xy
let es4xy = EvSS(EvSS (evensPlus1 ex ey))
exact evenNotOdd es4xy os4xy
Proof.epno_so = proof
intro x
intro ex
rewrite sym (plus0_r x)
compute
rewrite sym (plus0_r x)
intro ossx
exact evenNotOdd (EvSS ex) ossx
Isabelle
theory Proof
imports Main
begin
section‹Using the Standard Library›
text‹
All natural numbers:
The \<^const>‹UNIV› with the type annotation \<^typ>‹nat set› represents all natural numbers.
In general, \<^term>‹UNIV :: 'a set› is the set of all elements of type \<^typ>‹'a›.
›
lemma "{0, 1, 2, 3, 4} ⊆ (UNIV :: nat set)" by simp
text‹The set of all even numbers.›
lemma "{0, 2, 4, 6, 8} ⊆ {n. even n}" by simp
lemma "3 ∉ {n. even n}" by simp
text‹The set of all odd numbers.›
lemma "{1, 3, 5, 7, 9} ⊆ {n. odd n}" by simp
lemma "2 ∉ {n. odd n}" by simp
lemma "2+2 = 4" by simp
text‹Prove that the addition of any two even numbers is even.›
lemma "even n ⟹ even m ⟹ even (n+m)" by simp
text‹Prove that the addition is always associative.›
lemma fixes a::nat shows "(a+b)+c = a+(b+c)" by simp
text‹Prove that the addition is always commutative.›
lemma fixes a::nat shows "a+b = b+a" by simp
text‹Try to prove that the addition of any two even numbers is odd (it should be rejected).›
lemma "even n ⟹ even m ⟹ odd (n+m) ⟹ False" by simp
section‹Implementing our Own Natural Numbers›
datatype mynat = Z | S mynat
fun add :: "mynat ⇒ mynat ⇒ mynat" where
"add a Z = a"
| "add a (S b) = S (add a b)"
inductive myeven :: "mynat ⇒ bool" where
"myeven Z"
| "myeven a ⟹ myeven (S (S a))"
text‹All \<^typ>‹mynat›s. Since \<^const>‹S› and \<^const>‹Z› are unique, we don't need a type annotation.›
lemma "{Z, S Z, S (S Z), S (S (S Z)), S (S (S (S Z)))} ⊆ UNIV" by simp
text‹The set of all even numbers.›
lemma "{Z, S (S Z), S (S (S (S Z))), S (S (S (S (S (S Z)))))} ⊆ {n. myeven n}" by (auto intro: myeven.intros)
lemma "S (S (S Z)) ∉ {n. myeven n}" using myeven.cases by auto
text‹The set of all odd numbers.›
lemma "{S Z, S (S (S Z)), S (S (S (S (S Z)))), S (S (S (S (S (S (S Z))))))} ⊆ {n. ¬myeven n}"
apply (auto intro: myeven.intros)
by (metis myeven.cases mynat.distinct(1) mynat.inject)+
lemma "S (S Z) ∉ {n. ¬myeven n}" by (auto intro: myeven.intros)
lemma "add (S (S Z)) (S (S Z)) = S (S (S (S Z)))" by simp
text‹Prove that the addition of any two even numbers is even.›
lemma "myeven m ⟹ myeven n ⟹ myeven (add n m)"
apply(induction m rule: myeven.induct)
apply(simp)
by (auto intro: myeven.intros)
text‹Prove that the addition is always associative.›
lemma "add (add a b) c = add a (add b c)" by(induction c) (simp)+
text‹Prove that the addition is always commutative.›
lemma add_zero[simp]: "add Z b = b" by(induction b) (simp)+
lemma add_fst: "add (S a) b = S (add a b)" by(induction b) (simp)+
lemma "add a b = add b a"
apply(induction a arbitrary:b )
apply(simp)
apply(simp add: add_fst)
done
text‹Try to prove that the addition of any two even numbers is odd (it should be rejected).›
lemma "myeven n ⟹ myeven m ⟹ ¬myeven (add n m) ⟹ False"
apply(induction n rule: myeven.induct)
apply(simp)
apply(simp add: add_fst)
by(auto intro: myeven.intros)
end
J
A Peano number needs a zero, a mechanism for distinguishing equality from its absence, a way of getting a successor to a number, and a system of induction.
We know that a computer can never fully implement peano numbers because a computer can only represent a finite number of distinct values (if necessary, Ackerman's function can be used to illustrate the existence of this limitation). So our implementation of Peano Numbers will represent these mechanisms rather than be a complete implementation of these mechanisms.
So, these can be our definitions:
context=:3 :0
if. 0 = L. y do. context (,: ; ]) y return. end.
kernel=. > {: y
symbols=. (#$kernel) {. > {. y
order=. /: symbols
(symbols /: order); order |: kernel
)
symbols=: >@{.
kernel=: >@{:
zero=: context0x
monadic=: (1 :'[:context u@symbols; u&kernel')( :[:)
dyadic=: (1 :'[:context ,&symbols; u&kernel')([: :)
successor=: +&1x monadic
equals=: -:&kernel
all=: i. >. %: kernel successor@$: ::] zero
is_member_of=: e.&(-. -.&all)&,&kernel ([: :)
exists_in=: 1&e.@e.&kernel ([: :)
not=: -. :[:
induction=:4 :0
3 :'(y)=:context ?~#all'&.>;:x
assert (#all) > #;._1 LF,y
assert 0 = # y -.&;: LF,defined,x
assert 0!:3 y
)
addition=: +/ dyadic
isN=: ([ assert@is_member_of&(context all))
even=: [: context kernel@addition~"0@,@kernel :[: @isN
odd=: successor@even
defined=: '(zero not exists_in odd successor equals is_member_of addition even)'
Here, even is a function which, given a natural number, produces a corresponding even natural number. odd is a similar function which gives us odd numbers.
And, induction is a verb where the left argument lists values which represent any natural number and the right argument represents an expression to be considered. If induction succeeds, the expression is true for all natural numbers.
Meanwhile -. is J's implementation of "logical negation" -- a function which has been grafted onto boolean algebra as a convenience for people working with logical systems. ("Grafted on" here means: [a] logical negation was not originally a part of the definition of boolean algebra, and [b] logical negation cannot be a valid part of an infinite set of systems that were valid boolean algebras before someone decided that logical negation should be a part of boolean algebra.)
Also is_member_of represents universal set membership, exists_in represents the existential quantifier.
Note that we do not have to prove that our definitions are correct -- they are our axioms that we use in our proof.
Thus, this is proof that
- all natural numbers are even, and
- addition is associative, and
- addition is commutative, and
- the sum of two even numbers can never be odd.
'A B C' induction 0 :0
((even A) addition (even B)) is_member_of (even C)
((A addition B) addition C) equals (A addition (B addition C))
(A addition B) equals (B addition A)
not ((even A) addition (even B)) exists_in (odd C)
)
Meanwhile, here is how the invalid proofs fail:
'A B C' induction '((even A) addition (even B)) is_member_of (odd C)'
|assertion failure: assert
and
'A B C' induction 'not ((even A) addition (even B)) is_member_of (even C)'
|assertion failure: assert
As an aside, note that peano numbers show us that numbers can represent recursive processes.
Nim
We use the Go method which means that this Nim version has the same limits. When translating, we did some adjustments: for instance, we use overloading of operators which allows a more natural way to express the operations.
import strformat, sugar
type
# Natural number.
Number = ref object
pred: Number
# Even natural number: 2 × half.
EvenNumber = ref object
half: Number
# Odd natural number: 2 × half + 1.
OddNumber = ref object
half: Number
const Zero: Number = nil
# Contructors.
func newNumber(pred: Number): auto = Number(pred: pred)
func newEvenNumber(half: Number): auto = EvenNumber(half: half)
func newOddNumber(half: Number): auto = OddNumber(half: half)
func isZero(n: Number): bool =
## Test whether a natural number is zero.
n.isNil
func inc(n: Number): Number =
## Increment a natural number.
newNumber(n)
func dec(n: Number): Number =
## Decrement a natural number.
n.pred
func `+`(x, y: Number): Number =
## Add two natural numbers.
if y.isZero: x else: x.inc + y.dec
func `+`(x, y: EvenNumber): EvenNumber =
## Add two even natural numbers.
if y.half.isZero: x else: newEvenNumber(x.half + y.half)
func `+`(x, y: OddNumber): EvenNumber =
## Add two odd natural numbers.
newEvenNumber(inc(x.half + y.half))
func newNumber(n: Natural): Number =
## Build a natural number from a Nim Natural.
if n > 0: inc(newNumber(n - 1)) else: Zero
func count(n: Number): Natural =
## Return the integer representation of a natural number.
if n.isZero: 0 else: count(dec(n)) + 1
func count(n: EvenNumber): Natural =
## Return the integer representation of an even natural number.
n.half.count * 2
func count(n: OddNumber): Natural =
## Return the integer representation of an odd natural number.
n.half.count * 2 + 1
proc testCommutative(e1, e2: EvenNumber) =
## Test if even number addition is commutative for given numbers.
let c1 = e1.count
let c2 = e2.count
let passed = count(e1 + e2) == count(e2 + e1)
let symbol = if passed: "==" else: "!="
echo &"\n{c1} + {c2} {symbol} {c2} + {c1}"
proc testAssociative(e1, e2, e3: EvenNumber) =
## Test if even number arithmetic is associative.
let c1 = e1.count
let c2 = e2.count
let c3 = e3.count
let passed = count((e1 + e2) + e3) == count(e1 + (e2 + e3))
let symbol = if passed: "==" else: "!="
echo &"\n({c1} + {c2}) + {c3} {symbol} {c1} + ({c2} + {c3})"
let numbers = collect(newSeq, for i in 0..9: newNumber(i))
echo "The first 10 even natural numbers are:"
for i, n in numbers:
stdout.write n.count, if i == 9: '\n' else: ' '
echo "\nThe first 10 even natural numbers are:"
for i, n in numbers:
stdout.write newEvenNumber(n).count, if i == 9: '\n' else: ' '
echo "\nThe first 10 odd natural numbers are:"
for i, n in numbers:
stdout.write newOddNumber(n).count, if i == 9: '\n' else: ' '
var sum = Zero
for n in numbers: sum = sum + n
echo &"\nThe sum of the first 10 natural numbers is: {sum.count}"
var evenSum = newEvenNumber(Zero)
for n in numbers: evenSum = evenSum + newEvenNumber(n)
echo &"\nThe sum of the first 10 even natural numbers (increasing order) is: {evenSum.count}"
evenSum = newEvenNumber(Zero)
for i in countdown(9, 0): evenSum = evenSum + newEvenNumber(numbers[i])
echo &"\nThe sum of the first 10 even natural numbers (decreasing order) is: {evenSum.count}"
testCommutative(newEvenNumber(numbers[8]), newEvenNumber(numbers[9]))
testAssociative(newEvenNumber(numbers[7]), newEvenNumber(numbers[8]), newEvenNumber(numbers[9]))
- Output:
The first 10 even natural numbers are: 0 1 2 3 4 5 6 7 8 9 The first 10 even natural numbers are: 0 2 4 6 8 10 12 14 16 18 The first 10 odd natural numbers are: 1 3 5 7 9 11 13 15 17 19 The sum of the first 10 natural numbers is: 45 The sum of the first 10 even natural numbers (increasing order) is: 90 The sum of the first 10 even natural numbers (decreasing order) is: 90 16 + 18 == 18 + 16 (14 + 16) + 18 == 14 + (16 + 18)
OCaml
Using GADT, we can port the Coq version to OCaml.
type zero = Zero
type 'a succ = Succ
(* 1.1 *)
type _ nat =
| Zero : zero nat
| Succ : 'a nat -> 'a succ nat
(* 1.2 *)
type _ even =
| Even_zero : zero even
| Even_ss : 'a even -> 'a succ succ even
(* 2.1: define the addition relation *)
type (_, _, _) plus =
| Plus_zero : ('a, zero, 'a) plus
| Plus_succ : ('a, 'b, 'c) plus -> ('a, 'b succ, 'c succ) plus
(* 3.1 *)
(* Define the property: there exists a number 'sum that is the sum of 'a and 'b and is even. *)
type ('a, 'b) exists_plus_even = Exists_plus_even : ('a, 'b, 'sum) plus * 'sum even -> ('a, 'b) exists_plus_even
(* The proof that if a and b are even, there exists sum that is the sum of a and b that is even.
This is a valid proof since it terminated, and it is total (no assert false, and the exhaustiveness
test of pattern matching doesn't generate a warning) *)
let rec even_plus_even : type a b. a even -> b even -> (a, b) exists_plus_even =
fun a_even b_even ->
match b_even with
| Even_zero ->
Exists_plus_even (Plus_zero, a_even)
| Even_ss b_even' ->
let Exists_plus_even (plus, even) = even_plus_even a_even b_even' in
Exists_plus_even (Plus_succ (Plus_succ plus), Even_ss even)
(* 3.3 *)
(* 0 + n = n *)
let rec plus_zero : type a. a nat -> (zero, a, a) plus = function
| Zero -> Plus_zero
| Succ a -> Plus_succ (plus_zero a)
(* a + b = n => (a + 1) + b = (n + 1) *)
let rec plus_succ_left : type a b sum. (a, b, sum) plus -> (a succ, b, sum succ) plus =
function
| Plus_zero -> Plus_zero
| Plus_succ plus -> Plus_succ (plus_succ_left plus)
(* a + b = n => b + a = n *)
let rec plus_commutative : type a b sum. a nat -> (a, b, sum) plus -> (b, a, sum) plus =
fun a plus ->
match plus with
| Plus_zero -> plus_zero a
| Plus_succ plus' ->
plus_succ_left (plus_commutative a plus')
Omega
data Even :: Nat ~> *0 where
EZ:: Even Z
ES:: Even n -> Even (S (S n))
plus:: Nat ~> Nat ~> Nat
{plus Z m} = m
{plus (S n) m} = S {plus n m}
even_plus:: Even m -> Even n -> Even {plus m n}
even_plus EZ en = en
even_plus (ES em) en = ES (even_plus em en)Phix
Silly text-based version, just for fun.
Obviously 1.1/1.2/1.3 are (loosely) eumlated by the strings "int"/"even"/"odd", and addition by axioms[4].
Clearly 3.2 and 3.3 are not attempted, and I'm not sure which of 3.4/4.1/4.2 the last axiom is
closest to, or for that matter what the difference between them is supposed to be.
with javascript_semantics constant axioms = {{"even+1","odd"}, {"even","2*int"}, {"2*int+2*int","2*(int+int)"}, {"(int+int)","int"}, {"2*int","even"}, {"odd","2*int+1"}} procedure proof(string a, b) -- try to convert a into b using only the above axioms string w = a sequence seen = {} -- (avoid infinite loops) while not find(w,seen) do seen = append(seen,w) ?w if w=b then exit end if integer hit = 0 for i=1 to length(axioms) do string {r,s} = axioms[i] integer k = match(r,w) if k then w[k..k+length(r)-1] = s hit = i exit end if end for if hit=0 then exit end if puts(1,"== ") end while ?{a,b,iff(w=b?"true","false")} end procedure proof("even+even","even") proof("even+1","odd") --bad proofs: proof("int","even") proof("even+even","odd")
- Output:
"even+even"
== "2*int+even"
== "2*int+2*int"
== "2*(int+int)"
== "2*int"
== "even"
{"even+even","even","true"}
"even+1"
== "odd"
{"even+1","odd","true"}
"int"
{"int","even","false"}
"even+even"
== "2*int+even"
== "2*int+2*int"
== "2*(int+int)"
== "2*int"
== "even"
== {"even+even","odd","false"}
Racket
Via #lang cur.
#lang cur
(require rackunit
cur/stdlib/equality
cur/stdlib/sugar
cur/ntac/base
cur/ntac/standard
cur/ntac/rewrite)
;; Task 1.1
(data nat : 0 Type
[O : nat]
[S : (-> nat nat)])
(define-syntax #%datum
(syntax-parser
[(_ . n:exact-nonnegative-integer)
#:when (zero? (syntax-e #'n))
#'O]
[(_ . n:exact-nonnegative-integer)
#`(S (#%datum . #,(- (syntax-e #'n) 1)))]))
(check-equal? (S (S (S (S O)))) 4)
;; Task 1.2
(data even : 0 (-> nat Type)
[even-O : (even 0)]
[even-SS : (forall [n : nat] (-> (even n) (even (S (S n)))))])
;; Task 1.3
(data odd : 0 (-> nat Type)
[odd-O : (odd 1)]
[odd-SS : (forall [n : nat] (-> (odd n) (odd (S (S n)))))])
;; Task 2.1
(define/rec/match + : nat [m : nat] -> nat
[O => m]
[(S n-1) => (S (+ n-1 m))])
(check-equal? (+ 2 3) 5)
;; Task 3.1
(define-theorem even-plus-even-is-even
(∀ [n : nat] [m : nat] (-> (even n) (even m) (even (+ n m))))
(by-intros n m Hn Hm)
(by-induction Hn #:as [() (n* IHn)])
;; subgoal 1
simpl
by-assumption
;; subgoal 2
(by-apply even-SS)
by-assumption)
;; Task 3.2
(define-theorem addition-assoc
(∀ [a : nat] [b : nat] [c : nat] (== nat (+ (+ a b) c) (+ a (+ b c))))
(by-intros a b c)
(by-induction a #:as [() (a-1 IHa)])
;; subgoal 1
reflexivity
;; subgoal 2
display-focus ; show how the context and goal are before rewrite
(by-rewrite IHa)
display-focus ; show how the context and goal are after rewrite
reflexivity)
- Output:
b : nat c : nat a-1 : nat IHa : (== nat (+ (+ a-1 b) c) (+ a-1 (+ b c))) -------------------------------- (== nat (S (+ (+ a-1 b) c)) (S (+ a-1 (+ b c)))) b : nat c : nat a-1 : nat IHa : (== nat (+ (+ a-1 b) c) (+ a-1 (+ b c))) -------------------------------- (== nat (S (+ a-1 (+ b c))) (S (+ a-1 (+ b c))))
The fact that there's no error indicates that all proofs are verified.
Raku
Partial attempt only.
# 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)
- Output:
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
Salmon
Note that the only current implementation of Salmon is an interpreter that ignores proofs and doesn't try to check them, but in the future when there is an implementation that checks proofs, it should be able to check the proof in this Salmon code.
pure function even(x) returns boolean ((x in [0...+oo)) && ((x % 2) == 0));
theorem(forall(x : even, y : even) ((x + y) in even))
proof
{
forall (x : even, y : even)
{
L1:
x in even;
L2:
((x in [0...+oo)) && ((x % 2) == 0)) because type_definition(L1);
L3:
((x % 2) == 0) because simplification(L2);
L4:
y in even;
L5:
((y in [0...+oo)) && ((y % 2) == 0)) because type_definition(L4);
L6:
((y % 2) == 0) because simplification(L5);
L7:
(((x + y) % 2) == (x % 2) + (y % 2)); // axiom of % and +
L8:
(((x + y) % 2) == 0 + (y % 2)) because substitution(L3, L7);
L9:
(((x + y) % 2) == 0 + 0) because substitution(L6, L8);
L10:
(((x + y) % 2) == 0) because simplification(L9);
(x + y) in even because type_definition(even, L10);
};
};Tcl
Using the datatype package from the Pattern Matching task...
package require datatype
datatype define Int = Zero | Succ val
datatype define EO = Even | Odd
proc evenOdd val {
global environment
datatype match $val {
case Zero -> { Even }
case [Succ [Succ x]] -> { evenOdd $x }
case t -> {
set term [list evenOdd $t]
if {[info exists environment($term)]} {
return $environment($term)
} elseif {[info exists environment($t)]} {
return [evenOdd $environment($t)]
} else {
return $term
}
}
}
}
proc add {a b} {
global environment
datatype match $a {
case Zero -> { return $b }
case [Succ x] -> { Succ [add $x $b] }
case t -> {
datatype match $b {
case Zero -> { return $t }
case [Succ x] -> { Succ [add $t $x] }
case t2 -> {
set term [list add $t $t2]
if {[info exists environment($term)]} {
return $environment($term)
} elseif {[info exists environment($t)]} {
return [add $environment($t) $t2]
} elseif {[info exists environment($t2)]} {
return [add $t $environment($t2)]
} else {
return $term
}
}
}
}
}
}
puts "BASE CASE"
puts "evenOdd Zero = [evenOdd Zero]"
puts "evenOdd \[add Zero Zero\] = [evenOdd [add Zero Zero]]"
puts "\nITERATIVE CASE"
set environment([list evenOdd p]) Even
puts "if evenOdd p = Even..."
puts "\tevenOdd \[Succ \[Succ p\]\] = [evenOdd [Succ [Succ p]]]"
unset environment
puts "if evenOdd \[add p q\] = Even..."
set environment([list evenOdd [add p q]]) Even
foreach {a b} {
p q
{Succ {Succ p}} q
p {Succ {Succ q}}
{Succ {Succ p}} {Succ {Succ q}}
} {
puts "\tevenOdd \[[list add $a $b]\] = [evenOdd [add $a $b]]"
}
Output:
BASE CASE
evenOdd Zero = Even
evenOdd [add Zero Zero] = Even
ITERATIVE CASE
if evenOdd p = Even...
evenOdd [Succ [Succ p]] = Even
if evenOdd [add p q] = Even...
evenOdd [add p q] = Even
evenOdd [add {Succ {Succ p}} q] = Even
evenOdd [add p {Succ {Succ q}}] = Even
evenOdd [add {Succ {Succ p}} {Succ {Succ q}}] = Even
It is up to the caller to take the output of this program and interpret it as a proof.
Twelf
nat : type.
z : nat.
s : nat -> nat.
plus : nat -> nat -> nat -> type.
plus-z : plus z N2 N2.
plus-s : plus (s N1) N2 (s N3)
<- plus N1 N2 N3.
%% declare totality assertion
%mode plus +N1 +N2 -N3.
%worlds () (plus _ _ _).
%% check totality assertion
%total N1 (plus N1 _ _).
even : nat -> type.
even-z : even z.
even-s : even (s (s N))
<- even N.
sum-evens : even N1 -> even N2 -> plus N1 N2 N3 -> even N3 -> type.
%mode sum-evens +D1 +D2 +Dplus -D3.
sez : sum-evens
even-z
(DevenN2 : even N2)
(plus-z : plus z N2 N2)
DevenN2.
ses : sum-evens
( (even-s DevenN1') : even (s (s N1')))
(DevenN2 : even N2)
( (plus-s (plus-s Dplus)) : plus (s (s N1')) N2 (s (s N3')))
(even-s DevenN3')
<- sum-evens DevenN1' DevenN2 Dplus DevenN3'.
%worlds () (sum-evens _ _ _ _).
%total D (sum-evens D _ _ _).Wren
Most of what was said in the preamble to the Go entry applies equally to Wren though, as Wren is dynamically typed, we have to rely on runtime type checks.
import "./fmt" for Fmt
// Represents a natural number.
class Number {
// Returns a Number with a null predecessor representing the natural number 0.
static zero { Number.new() }
// Generates a natural number from a non-negative integer.
static gen(n) {
if (n.type != Num || !n.isInteger || n < 0) Fiber.abort("Argument must be a non-negative integer.")
if (n > 0) return add1(gen(n-1))
return zero
}
// Increments a natural number.
static add1(x) {
if (x.type != Number) Fiber.abort("Argument must be a Number.")
var y = Number.new()
y.pred = x
return y
}
// Decrements a natural number.
static sub1(x) {
if (x.type != Number) Fiber.abort("Argument must be a Number.")
return x.pred
}
// Counts a natural number i.e returns its integer representation.
static count(x) {
if (x.type != Number) Fiber.abort("Argument must be a Number.")
if (x.isZero) return 0
return count(sub1(x)) + 1
}
// Constructs a new Number object with a null predecessor.
construct new() { _pred = null }
// Get or set predecessor.
pred { _pred }
pred=(p) {
if (p.type != Number) Fiber.abort("Argument must be a Number.")
_pred = p
}
// Tests whether the current instance is zero.
isZero { _pred == null }
// Add another Number.
+(other) {
if (other.type != Number) Fiber.abort("Argument must be a Number.")
if (other.isZero) return this
return Number.add1(this) + Number.sub1(other)
}
}
// Represents an even natural number: 2 * half.
class EvenNumber {
// Counts an even natural number i.e returns its integer representation.
static count(x) {
if (x.type != EvenNumber) Fiber.abort("Argument must be an EvenNumber.")
return Number.count(x.half) * 2
}
// Constructs a new EvenNumber object : 2 * half.
construct new(half) {
if (half.type != Number) Fiber.abort("Argument must be a Number.")
_half = half
}
// gets 'half' field
half { _half }
// Add another EvenNumber.
+(other) {
if (other.type != EvenNumber) Fiber.abort("Argument must be an EvenNumber.")
if (other.half.isZero) return this
return EvenNumber.new(this.half + other.half)
}
}
// Represents an odd natural number: 2 * half + 1.
class OddNumber {
// Counts an odd natural number i.e returns its integer representation.
static count(x) {
if (x.type != OddNumber) Fiber.abort("Argument must be an OddNumber.")
return Number.count(x.half) * 2 + 1
}
// Constructs a new OddNumber object : 2 * half + 1.
construct new(half) {
if (half.type != Number) Fiber.abort("Argument must be a Number.")
_half = half
}
// gets 'half' field
half { _half }
// Add another OddNumber. Note that it returns an EvenNumber.
+(other) {
if (other.type != OddNumber) Fiber.abort("Argument must be an OddNumber.")
var z = this.half + other.half
return EvenNumber.new(Number.add1(z))
}
}
// Tests if even number addition is commutative for given numbers.
var testCommutative = Fn.new { |e1, e2|
if (e1.type != EvenNumber || e2.type != EvenNumber) Fiber.abort("Arguments must be EvenNumbers.")
var c1 = EvenNumber.count(e1)
var c2 = EvenNumber.count(e2)
var passed = EvenNumber.count(e1 + e2) == EvenNumber.count(e2 + e1)
var symbol = passed ? "==" : "!="
Fmt.print("\n$d + $d $s $d + $d", c1, c2, symbol, c2, c1)
}
// Tests if even number arithmetic is associative for given numbers.
var testAssociative = Fn.new { |e1, e2, e3|
if (e1.type != EvenNumber || e2.type != EvenNumber || e3.type != EvenNumber) {
Fiber.abort("Arguments must be EvenNumbers.")
}
var c1 = EvenNumber.count(e1)
var c2 = EvenNumber.count(e2)
var c3 = EvenNumber.count(e3)
var passed = EvenNumber.count((e1 + e2) + e3) == EvenNumber.count(e1 + (e2 + e3))
var symbol = passed ? "==" : "!="
Fmt.lprint("\n($d + $d) + $d $s $d + ($d + $d)", [c1, c2, c3, symbol, c1, c2, c3])
}
var numbers = List.filled(10, null)
System.print("The first 10 natural numbers are:")
for (i in 0..9) {
numbers[i] = Number.gen(i)
Fmt.write("$d ", Number.count(numbers[i]))
}
System.print("\n\nThe first 10 even natural numbers are:")
for (i in 0..9) {
var e = EvenNumber.new(numbers[i])
Fmt.write("$d ", EvenNumber.count(e))
}
System.print("\n\nThe first 10 odd natural numbers are:")
for (i in 0..9) {
var o = OddNumber.new(numbers[i])
Fmt.write("$d ", OddNumber.count(o))
}
System.write("\n\nThe sum of the first 10 natural numbers is: ")
var sum = numbers[0]
for (i in 1..9) {
sum = sum + numbers[i]
}
System.print(Number.count(sum))
System.write("\nThe sum of the first 10 even natural numbers (increasing order) is: ")
var sumEven = EvenNumber.new(numbers[0])
for (i in 1..9) {
sumEven = sumEven + EvenNumber.new(numbers[i])
}
System.print(EvenNumber.count(sumEven))
System.write("\nThe sum of the first 10 even natural numbers (decreasing order) is: ")
sumEven = EvenNumber.new(numbers[9])
for (i in 8..0) {
sumEven = sumEven + EvenNumber.new(numbers[i])
}
System.print(EvenNumber.count(sumEven))
testCommutative.call(EvenNumber.new(numbers[8]), EvenNumber.new(numbers[9]))
testAssociative.call(EvenNumber.new(numbers[7]), EvenNumber.new(numbers[8]), EvenNumber.new(numbers[9]))
- Output:
The first 10 natural numbers are: 0 1 2 3 4 5 6 7 8 9 The first 10 even natural numbers are: 0 2 4 6 8 10 12 14 16 18 The first 10 odd natural numbers are: 1 3 5 7 9 11 13 15 17 19 The sum of the first 10 natural numbers is: 45 The sum of the first 10 even natural numbers (increasing order) is: 90 The sum of the first 10 even natural numbers (decreasing order) is: 90 16 + 18 == 18 + 16 (14 + 16) + 18 == 14 + (16 + 18)
Categories:
- Draft Programming Tasks
- Logic
- ACL2
- Agda
- ATS
- Coq
- FreeBASIC
- Go
- Haskell
- Idris
- Isabelle
- J
- Nim
- OCaml
- Omega
- Phix
- Racket
- Raku
- Salmon
- Tcl
- Twelf
- Wren
- Wren-fmt
- ALGOL 68/Omit
- AWK/Omit
- C/Omit
- C++/Omit
- D/Omit
- E/Omit
- Fortran/Omit
- GUISS/Omit
- Java/Omit
- JavaScript/Omit
- M4/Omit
- Metafont/Omit
- MUMPS/Omit
- Objective-C/Omit
- Processing/Omit
- PureBasic/Omit
- Python/Omit
- Ruby/Omit
- Smalltalk/Omit