Inj.idr

module Inj

import Decidable.Equality
import Decidable.Order

-- These definitions would go in some stdlib

public export
interface Equivalence ty inj => Inj (ty : Type) (inj : ty -> ty -> Type) where
  useInj : {x, y: ty} -> inj x y -> x = y

mkInj : Inj ty inj => {x, y: ty} -> x = y -> inj x y
mkInj {x} Refl = reflexive x

-- Unsure if DecEq ty should be a superclass constraint
public export
interface Inj ty inj => DecInj (ty : Type) (inj : ty -> ty -> Type) where
  decInj : (x, y: ty) -> Dec (inj x y)

-- From this definition...
data Foo : Type where
  Zap : Foo
  Bar : Int -> Foo
  Quux : Foo -> Foo

-- We should be able to derive this datatype and all that follows
data FooInj : (a, b: Foo) -> Type where
  ZapInj : FooInj Zap Zap
  BarInj : (x1, x2: Int) -> x1 = x2 -> FooInj (Bar x1) (Bar x2)
  QuuxInj : (r1, r2: Foo) -> r1 = r2 -> FooInj (Quux r1) (Quux r2)

implementation Preorder Foo FooInj where
  transitive _ _ _ ZapInj ZapInj = ZapInj
  transitive _ _ _ (BarInj x x Refl) (BarInj x x Refl) = BarInj x x Refl
  transitive _ _ _ (QuuxInj r r Refl) (QuuxInj r r Refl) = QuuxInj r r Refl

  reflexive f =
    case f of
      Zap => ZapInj
      Bar x => BarInj x x Refl
      Quux r => QuuxInj r r Refl

implementation Equivalence Foo FooInj where
  symmetric _ _ ZapInj = ZapInj
  symmetric _ _ (BarInj x x Refl) = BarInj x x Refl
  symmetric _ _ (QuuxInj r r Refl) = QuuxInj r r Refl

implementation Inj Foo FooInj where
  useInj ZapInj = Refl
  useInj (BarInj x x Refl) = Refl
  useInj (QuuxInj r r Refl) = Refl