Idris: Using the properties of simple constructors for equality and inequality

data Bin = O Nat Bin | BNil
— Thanks:
O_injective : (O a v = O b w) -> (a = b, v = w)
O_injective Refl = (Refl, Refl)
total aNEBMeansNotEqual : (a : Nat) -> (b : Nat) -> (v : Bin) -> Dec (a = b) -> Dec (O a v = O b v)
aNEBMeansNotEqual a b v (Yes prf) = rewrite prf in Yes Refl
aNEBMeansNotEqual a b v (No contra) =
No $ \prf =>
let (ojAB, _) = O_injective prf in
contra ojAB
total vNEWMeansNotEqual : (v : Bin) -> (w : Bin) -> Dec (v = w) -> Dec (O Z v = O Z w)
vNEWMeansNotEqual v w (Yes prf) = rewrite prf in Yes Refl
vNEWMeansNotEqual v w (No contra) =
No $ \prf =>
let (_, ojVW) = O_injective prf in
contra ojVW
  • Simple constructors are implicitly injective because each unique set of argument values results in a unique outcome in the space of the constructor’s type. Despite having this code for a while, my experiences with more complex proofs suggested that idris would require me to rewrite these myself. I admittedly was weirdly blind to it for a while.
  • Not only simply injective, constructors are also bijective: each unique value of the constructor fully populated also represents a unique set of inputs, and idris also allows us to write this:
O_bijective : (a = b) -> (c = d) -> (O a c = O b d)
O_bijective Refl Refl = Refl




An old programmer learning new tricks.

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

Recommended from Medium

Working with GitHub and Git

Automatically sync your Guest WiFi users to Campaign Monitor

How to trigger a Blue Prism process using Outlook.


Day 27 of Game Dev: Immersing the Player with SFX in Unity!

Getting Preliminary Commits of a local Repository into a Remote Repository

Managing async code in Swift

Best FluentU Vs Pimsleur Review: Which App Is At #1?

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
art yerkes

art yerkes

An old programmer learning new tricks.

More from Medium

Two Ballet Birds

Toward a Mobility of Algorithms?

From Development or Conservation to Fat Bears and Big Trees

How to Debug Your Arguments and Clarify Your Thinking