Proof: Difference between revisions

3.1. using built-in natural numbers:

 

 

=={{header|Agda}}==

 

-- 1.1. The natural numbers.

-- ℕ-formation: ℕ is set.

data ℕ : Set where

zero : ℕ

 

-- 1.2. The even natural numbers.

data 2×ℕ : ℕ → Set where

 

-- 1.3. The odd natural numbers.

data 2×ℕ+1 : ℕ → Set where

 

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

-- 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 (2+ m) n = 2+ (even+even≡even m n)

 

infix 4 _≡_

refl : m ≡ m

 

sym refl = refl

 

trans refl n≡p = n≡p

 

-- refl, sym and trans forms an equivalence relation.

 

 

-- 3.2.1. Direct proof of the associativity of addition using propositional

-- equality.

+-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p)

 

-- Proof _of_ mathematical induction on the natural numbers.

 

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

P : ℕ → Set

P m = m + n + p ≡ m + (n + p)

P₀ = refl

 

-- Syntactic sugar for equational reasoning (we don't use preorders here).

infix 4 _≋_

data _≋_ (m n : ℕ) : Set where

 

infix 1 begin_

begin_ : {m n : ℕ} → m ≋ n → m ≡ n

 

infixr 2 _~⟨_⟩_

_~⟨_⟩_ : (m : ℕ){n p : ℕ} → m ≡ n → n ≋ p → m ≋ p

 

_∎ : (m : ℕ) → m ≋ m

 

-- Some helper proofs.

 

 

 

-- 3.3. The commutativity of addition using equational reasoning.

+-commutative : (m n : ℕ) → m + n ≡ n + m

 

-- 3.4.

even+even≡odd : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ+1 (m + n)

-- ^

-- That gives

-- ?0 : 2×ℕ+1 (zero + zero)

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

 

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

 

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

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

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

 

 

 

| O : nat

| S : nat -> nat.

Fixpoint plus (n m:nat) {struct n} : nat :=

match n with

| S p => S (p + m)

end

where "n + m" := (plus n m) : nat_scope.

| even_O : even O

| even_SSn : forall n:nat,

even n -> even (S (S n)).

 

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.

 

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

 

 

 

As an aside, note that peano numbers show us that numbers can represent recursive processes.

 

=={{header|OCaml}}==

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.

{{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 _ _ _).

 

{{omit from|ALGOL 68}} <!-- might be possible, but would require a complex library like Maple, not sure -->