Proof: Difference between revisions

{{draft task|Logic}}

 

This task only makes sense for [[wp:dependently-typed language|dependently-typed languages]] and [[wp:proof assistant|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.

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|Haskell}}==

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.

 

=={{header|J}}==

So, these can be our definitions:

 

induction=:4 :0

assert (#all) > #;._1 LF,y

assert 0 = # y -.&;: LF,defined,x

assert 0!:3 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)

 

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

 

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

{{omit from|JavaScript}}