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:

1. Define a countably infinite set of natural numbers {0, 1, 2, 3, ...}.
2. Define an addition on that numbers.
3. Define a countably infinite set of even natural numbers {0, 2, 4, 6, ...} within the previously defined set of natural numbers.
4. Prove that the addition of any two even numbers is even.
5. Prove that the addition is always associative.

4. and 5. can't be done using a simple number enumeration since there is a countable many natural numbers which is quantified in propositions.

ACL2

<lang Lisp>(thm (implies (and (evenp x) (evenp y))

             (evenp (+ x y))))</lang>

Agda

<lang agda>module Arith where

-- 1. Natural numbers. -- -- ℕ-formation: ℕ is set. -- -- ℕ-introduction: o ∈ ℕ, -- a ∈ ℕ | (1 + a) ∈ ℕ. -- data ℕ : Set where

 o : ℕ
 1+ : ℕ → ℕ

-- 2. Addition. -- -- via ℕ-elimination. -- infixl 6 _+_ _+_ : ℕ → ℕ → ℕ o + n = n 1+ m + n = 1+ (m + n)

-- 3. Even natural numbers. -- data 2×ℕ : ℕ → Set where

 o : 2×ℕ o
 2+ : {n : ℕ} → 2×ℕ n → 2×ℕ (1+ (1+ n))

-- 4. 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 a type, i.e. logical proposition, algorithm itself is a proof by unification -- which builds a required term of a given (inhabited) type, and the typechecker -- performs that proof (so that this is compile-time verification). -- even+even≡even : {m n : ℕ} → 2×ℕ m → 2×ℕ n → 2×ℕ (m + n) even+even≡even o n = n even+even≡even (2+ m) n = 2+ (even+even≡even m n)

-- The identity type for natural numbers. -- infix 4 _≡_ data _≡_ (n : ℕ) : ℕ → Set where

 refl : n ≡ n

cong : {m n : ℕ} → m ≡ n → 1+ m ≡ 1+ n cong refl = refl

-- 5.1. Direct proof of the associativity of addition. -- +-associative : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-associative o _ _ = refl +-associative (1+ m) n p = cong (+-associative m n p)

-- Proof _of_ mathematical induction on the natural numbers. -- -- P 0, ∀ x. P x → P (1 + x) | ∀ x. P x. -- ind : (P : ℕ → Set) → P o → (∀ n → P n → P (1+ n)) → ∀ n → P n ind _ P₀ _ o = P₀ ind P P₀ next (1+ n) = next n (ind P P₀ next n)

-- 5.2. Associativity of addition by induction. -- +-associative′ : (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-associative′ m n p = ind P P₀ is m

 where
   P : ℕ → Set
   P i = i + n + p ≡ i + (n + p)
   P₀ : P o
   P₀ = refl
   is : ∀ i → P i → P (1+ i)
   is i Pi = cong Pi

</lang>

Coq

<lang coq>Inductive nat : Set :=

 | O : nat
 | S : nat -> nat.

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.

Inductive even : nat -> Set :=

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

Haskell

Using GADTs and type families it is possible to write an adaptation of the Agda version:

<lang haskell>{-# LANGUAGE TypeOperators, TypeFamilies, GADTs #-}

module Arith where

-- 1. Natural numbers.

data Z = Z data S n = S n

-- 2. Addition.

infixl 6 :+ type family x :+ y type instance Z :+ n = n type instance (S m) :+ n = S (m :+ n)

-- 3. Even natural numbers.

data En :: * -> * where

 Ez :: En Z
 Es :: En n -> En (S (S n))

-- 4. 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 (:=) n :: * -> * where

 Refl :: n := n

cong :: m := n -> S m := S n cong Refl = Refl

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

</lang>

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

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:

<lang J>zero=: 0x successor=: +&1x equals=: -: all=: i. >. %: successor@$: ::] zero every=:3 :0"0&.;:

 if. 3 = nc y do.
   if. 0 0 -: }. (y`:6) b. 0 do.
     y,&.>'/' return.
   end.
 elseif. _1 = nc y do.
   (y)=: all
 end.
 y

) is_member_of=: [: :e.&(-. -.&all) induction=:4 :0

  erase x
  assert y <&# all
  assert _1 = nc y -.&;: defined
  assert 1 = do every y

)

addition=: [: :+ even=: addition~ :[:

defined=: '(zero successor equals is_member_of addition even)'</lang>

Here, even is a function which, given a natural number, produces a corresponding even natural number.

Induction is a verb where the left argument lists values which represent any natural number and the right argument lists values which represent an expression to be considered. If it succeeds, the expression is true for all natural numbers.

Note that we do not have to prove that our definitions are correct -- they are our axioms that we use in our proof.

Thus, proof that all natural numbers are even:

<lang J>'A B C' induction '((even A) addition (even B)) is_member_of (even C)'</lang>

And, proof that addition is associative:

<lang J>'A B C' induction '((A addition B) addition C) equals (A addition (B addition C))'</lang>

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

Omega

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

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.

<lang Salmon>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);
     };
 };</lang>

Tcl

Using the datatype package from the Pattern Matching task...

Works with: Tcl version 8.5

<lang tcl>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]]"

}</lang> 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

<lang 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 _ _ _). </lang>