Proof: Difference between revisions

3.1. using built-in natural numbers:

=={{header|Agda}}==

-- 1.1. The natural numbers.

-- when checking that the clause even+even≢even zero zero () has type

-- {m n : ℕ} → 2×ℕ m → 2×ℕ n → ¬ 2×ℕ (m + n)

=={{header|ATS}}==

intended use of the facilities. However, I DO consider the task a

good didactic exercise. *)

implement

main0 () =

{{out}}

contain enough to do a considerable amount of *informal* proof

about a program.

implement

main0 () =

{{out}}

=={{header|Coq}}==

Inductive nat : Set :=

| O : nat

intros. apply H1. apply (even_plus_even _ _ H H0).

Qed.

=={{header|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.

import "fmt"

testAssociative(genEven(numbers[7]), genEven(numbers[8]), genEven(numbers[9]))

{{out}}

Using [http://www.haskell.org/haskellwiki/GADT GADTs] and [http://www.haskell.org/haskellwiki/GHC/Type_families type families] it is possible to write a partial adaptation of the Agda version:

module PeanoArithmetic where

--

-- since we have a "citizen" of an uninhabited type here (contradiction!).

See also [[Proof/Haskell]] for implementation of a small theorem prover.

These ways can be combined.

module Proof

exact evenNotOdd (EvSS ex) ossx

=={{header|Isabelle}}==

imports Main

begin

by(auto intro: myeven.intros)

=={{header|J}}==

So, these can be our definitions:

if. 0 = L. y do. context (,: ; ]) y return. end.

kernel=. > {: y

odd=: successor@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.

# the sum of two even numbers can never be odd.

((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:

and

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.

type

testCommutative(newEvenNumber(numbers[8]), newEvenNumber(numbers[9]))

{{out}}

Using GADT, we can port the Coq version to OCaml.

type zero = Zero

type 'a succ = Succ

plus_succ_left (plus_commutative a plus')

=={{header|Omega}}==

EZ:: Even Z

ES:: Even n -> Even (S (S n))

even_plus EZ en = en

even_plus (ES em) en = ES (even_plus em en)

=={{header|Phix}}==

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.

<span style="color: #008080;">with</span> <span style="color: #008080;">javascript_semantics</span>

<span style="color: #008080;">constant</span> <span style="color: #000000;">axioms</span> <span style="color: #0000FF;">=</span> <span style="color: #0000FF;">{{</span><span style="color: #008000;">"even+1"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">},</span>

<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"int"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"even"</span><span style="color: #0000FF;">)</span>

<span style="color: #000000;">proof</span><span style="color: #0000FF;">(</span><span style="color: #008000;">"even+even"</span><span style="color: #0000FF;">,</span><span style="color: #008000;">"odd"</span><span style="color: #0000FF;">)</span>

{{out}}

<pre>

Via <code>#lang cur</code>.

(require rackunit

(by-rewrite IHa)

display-focus ; show how the context and goal are after rewrite

{{out}}

=={{header|Raku}}==

Partial attempt only.

sub check ($type, @testee) {

# 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)

{{out}}

<pre>Is 0 ∈ ℕ : True

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.

theorem(forall(x : even, y : even) ((x + y) in even))

proof

(x + y) in even because type_definition(even, L10);

};

=={{header|Tcl}}==

{{works with|Tcl|8.5}}

datatype define Int = Zero | Succ val

datatype define EO = Even | Odd

} {

puts "\tevenOdd \[[list add $a $b]\] = [evenOdd [add $a $b]]"

Output:

<pre>BASE CASE

=={{header|Twelf}}==

z : nat.

s : nat -> nat.

%worlds () (sum-evens _ _ _ _).

%total D (sum-evens D _ _ _).

=={{header|Wren}}==

{{libheader|Wren-fmt}}

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.

// Represents a natural number.

testCommutative.call(EvenNumber.new(numbers[8]), EvenNumber.new(numbers[9]))

{{out}}