Proof: Difference between revisions

=={{header|Idris}}==

Idris supports two types of proofs: using tactics, like Coq, or just write functions like Agda.

These ways can be combined.

<lang Idris>

module Proof

-- Enable terminator chercker by default

%default total

-- 1.1 Natural numbers

%elim

data MyNat

= Z

| S MyNat

-- 1.2 Even naturals

%elim

data EvNat : MyNat -> Type where

EvO : EvNat Z

EvSS : EvNat x -> EvNat (S (S x))

-- 1.3 Odd naturals

%elim

data OddNat : MyNat -> Type where

Odd1 : OddNat (S Z)

OddSS : OddNat x -> OddNat (S (S x))

-- 2.1 addition

infixl 4 :+

(:+) : MyNat -> MyNat -> MyNat

(:+) Z b = b

(:+) (S a) b = S (a :+ b)

-- 3.1, Prove that the addition of any two even numbers is even.

evensPlus1 : {a : MyNat} -> {b : MyNat} -> (EvNat a) -> (EvNat b) -> (EvNat (a :+ b))

evensPlus1 ea eb = ?proof31

congS : {a : MyNat} -> {b : MyNat} -> (a = b) -> (S a = S b)

congS refl = refl

evensPlus2 : {a : MyNat} -> {b : MyNat} -> (EvNat a) ->(EvNat b) -> (EvNat (a :+ b))

evensPlus2 EvO eb = eb

evensPlus2 {a=(S (S a))} (EvSS ea) eb = EvSS (evensPlus2 ea eb)

-- 3.2 Prove that the addition is always associative.

plusAssoc : (a : MyNat) -> (b : MyNat) -> (c : MyNat) -> (a :+ b) :+ c = a :+ (b :+ c)

plusAssoc Z b c = refl

plusAssoc (S a) b c = congS (plusAssoc a b c)

-- 3.3 Prove that the addition is always commutative.

plus0_r : (a : MyNat) -> a :+ Z = a

plus0_r Z = refl

plus0_r (S a) = congS (plus0_r a)

plusS_r : (a : MyNat) -> (b : MyNat) -> a :+ S b = S (a :+ b)

plusS_r Z b = refl

plusS_r (S a) b = congS (plusS_r a b)

plusComm : (a : MyNat) -> (b : MyNat) -> a :+ b = b :+ a

plusComm a b = ?proof33

-- 4.1 Prove that the addition of any two even numbers cannot be odd.

evenNotOdd : (ea : EvNat a) -> (oa : OddNat a) -> _|_

evenNotOdd (EvSS e) (OddSS o) = evenNotOdd e o

evensPlusNotOdd : (ea : EvNat a) -> (eb : EvNat b) -> (OddNat (a :+ b)) -> _|_

evensPlusNotOdd EvO (EvSS eb) (OddSS ob) = evenNotOdd eb ob

evensPlusNotOdd (EvSS y) EvO oab = ?epno_so

evensPlusNotOdd (EvSS y) (EvSS z) oab = ?epno_ss

---------- Proofs ----------

Proof.proof31 = proof

intro a

intro b

intro ea

intro eb

induction ea

compute

exact eb

intro x

intro ex

intro exh

exact (EvSS exh)

Proof.proof33 = proof

intros

induction a

compute

rewrite sym (plus0_r b)

trivial

intro a'

intro ha'

compute

rewrite sym (plusS_r b a')

exact (congS ha')

Proof.epno_ss = proof

intro x

intro ex

intro y

intro ey

compute

rewrite sym ( plusS_r x (S y))

rewrite sym ( plusS_r x y)

intro os4xy

let es4xy = EvSS(EvSS (evensPlus1 ex ey))

exact evenNotOdd es4xy os4xy

Proof.epno_so = proof

intro x

intro ex

rewrite sym (plus0_r x)

compute

rewrite sym (plus0_r x)

intro ossx

exact evenNotOdd (EvSS ex) ossx

</lang>