Proof

From Rosetta Code

Proof
You are encouraged to solve this task according to the task description, using any language you may know.

Define a type for natural numbers (0, 1, 2, 3, ...) representable by a computer, and addition on them. Define a type of even numbers (0, 2, 4, 6, ...) within the previously defined range of natural numbers. Prove that the addition of any two even numbers is even, if the result is a member of the type.

[edit] Agda2

module Arith where


data Nat : Set where
  zero : Nat
  suc  : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero  + n = n
suc m + n = suc (m + n)


data Even : Nat -> Set where
  even_zero    : Even zero
  even_suc_suc : {n : Nat} -> Even n -> Even (suc (suc n))

_even+_ : {m n : Nat} -> Even m -> Even n -> Even (m + n)
even_zero       even+ en = en
even_suc_suc em even+ en = even_suc_suc (em even+ en)

[edit] 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.

[edit] Haskell

See Proof/Haskell.

[edit] 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)

[edit] Tcl

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

Works with: Tcl version 8.5

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.

[edit] 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 _ _ _).