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



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.