Better than Unit Tests? Idris Proofs

namespace Numbers  data Nat : Type where
Zero : Numbers.Nat
Successor : Numbers.Nat -> Numbers.Nat
decr : Numbers.Nat -> Numbers.Nat
decr Zero = Zero
decr (Successor x) = x
incr : Numbers.Nat -> Numbers.Nat
incr Zero = Successor Zero
incr (Successor x) = Successor (Successor x)
One : Numbers.Nat
One = Successor Zero
Two : Numbers.Nat
Two = Successor One
Three : Numbers.Nat
Three = Successor Two
proofIncrementOne : incr One = Two
proofIncrementOne = Refl
proofDecrementOne : decr One = Zero
proofDecrementOne = Refl
proofDecrementZero : decr Zero = Zero
proofDecrementZero = Refl
plus : Numbers.Nat -> Numbers.Nat -> Numbers.Nat
plus Zero b = b
plus (Successor a) b = Successor(plus a b)
syntax [x] "+" [y] = Numbers.plus x y
proofTwoPlusOne : (Two + One) = Three
proofTwoPlusOne = Refl
proofZeroPlusN : (n : Numbers.Nat) -> (Zero + n) = n
proofZeroPlusN n = Refl
  • prove a base case (in this instance n = Zero) some property (p)holds true. In this instance the property is n + 0 = n.
  • prove for some successor to the base case (in this instance n = Successor k) the property (p) also holds true; said another way if p(n) holds true then p(Successor n) also holds true.
  • conclude the property holds true for all
proofNPlusZero : (n : Numbers.Nat) -> (n + Zero) = n
proofNPlusZero Zero = Refl
proofNPlusZero (Successor k) =
let inductiveNPlusZero = proofNPlusZero k in
rewrite inductiveNPlusZero in Refl
lemmaPlusCommutesZeroM : (m: Numbers.Nat) -> m = plus m Zero
lemmaPlusCommutesZeroM (Successor k) =
let inductiveCummativeM = lemmaPlusCommutesZeroM k in
rewrite inductiveCummativeM in Refl
lemmaPlusCommutesZeroKM : (k, m: Numbers.Nat) ->
Successor (plus m k) = plus m (Successor k)
lemmaPlusCommutesZeroKM k Zero = Refl
lemmaPlusCommutesZeroKM k (Successor j) =
rewrite lemmaPlusCommutesZeroKM k j in Refl
proofPlusCommutative : (n, m : Numbers.Nat) -> (n + m) = (m + n)
proofPlusCommutative Zero Zero = Refl
proofPlusCommutative Zero m = lemmaPlusCommutesZeroM m
proofPlusCommutative (Successor n) m =
rewrite proofPlusCommutative n m in lemmaPlusCommutesZeroKM n m

--

--

--

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

Love podcasts or audiobooks? Learn on the go with our new app.

Recommended from Medium

#Day14 | #100DaysOfGADS

DevOps: The Infinite Mindset

Daily Stand-Up as you like it

Java Date Formatting and Utilization

How booting work in operating system?

Array Order and Permute() in MATLAB

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store
Todd Brown

Todd Brown

A 25 year software industry veteran with a passion for functional programming, architecture, mentoring / team development, xp/agile and doing the right thing.

More from Medium

My vision about outside-in testing as a Backend Developer

DB-Lock-Issues with Transactional REQUIRES_NEW — More Spring/Java transaction handling pitfalls

How bad models ruin an API

4 Things I’ve learned as a Software Engineer at ServiceRocket