Chu construction, third attempt

Chu.idr

module Chu

-- Examining Chu construction again, this time in Idris.

data Prop : Type where
  Unit : Prop
  Counit : Prop
  AC : Prop -> Prop -> Prop
  AD : Prop -> Prop -> Prop
  MC : Prop -> Prop -> Prop
  MD : Prop -> Prop -> Prop

mutual
  prof : Prop -> Type
  prof Unit = ()
  prof Counit = Void
  prof (AC x y) = (prof x, prof y)
  prof (AD x y) = Either (prof x) (prof y)
  prof (MC x y) = (prof x, prof y)
  prof (MD x y) = (refu x -> prof y, refu y -> prof x)

  refu : Prop -> Type
  refu Unit = Void
  refu Counit = ()
  refu (AC x y) = Either (refu x) (refu y)
  refu (AD x y) = (refu x, refu y)
  refu (MC x y) = (prof x -> refu y, prof y -> refu x)
  refu (MD x y) = (refu x, refu y)

conflict : (p:Prop) -> prof p -> refu p -> Void
conflict Unit x y = y
conflict Counit x y = x
conflict (AC z w) (a, b) (Left l) = conflict z a l
conflict (AC z w) (a, b) (Right r) = conflict w b r
conflict (AD z w) (Left l) (a, b) = conflict z l a
conflict (AD z w) (Right r) (a, b) = conflict w r b
conflict (MC z w) (a, b) (f, g) = conflict z a (g b)
conflict (MD z w) (a, b) (c, d) = conflict w (a c) d

dual : Prop -> Prop
dual Unit = Counit
dual Counit = Unit
dual (AC x y) = AD (dual x) (dual y)
dual (AD x y) = AC (dual x) (dual y)
dual (MC x y) = MD (dual x) (dual y)
dual (MD x y) = MC (dual x) (dual y)

mutual
  refu_dual : (a:Prop) -> prof a -> refu (dual a)
  refu_dual Unit x = x
  refu_dual Counit x = x
  refu_dual (AC y z) (a, b) = (refu_dual y a, refu_dual z b)
  refu_dual (AD y z) (Left a) = Left (refu_dual y a)
  refu_dual (AD y z) (Right b) = Right (refu_dual z b)
  refu_dual (MC y z) (a, b) = (refu_dual y a, refu_dual z b)
  refu_dual (MD y z) (f, g) = (refu_dual z . f . dual_refu y, refu_dual y . g . dual_refu z)

  dual_refu : (a:Prop) -> prof (dual a) -> refu a
  dual_refu Unit x = x
  dual_refu Counit x = x
  dual_refu (AC y z) (Left a) = Left (dual_refu y a)
  dual_refu (AC y z) (Right b) = Right (dual_refu z b)
  dual_refu (AD y z) (a, b) = (dual_refu y a, dual_refu z b)
  dual_refu (MC y z) (f, g) = (dual_refu z . f . refu_dual y, dual_refu y . g . refu_dual z)
  dual_refu (MD y z) (a, b) = (dual_refu y a, dual_refu z b)

-- mutual
--   prof_dual : (a:Prop) -> refu a -> prof (dual a)
--   dual_prof : (a:Prop) -> refu (dual a) -> prof a

data Rule : Prop -> Prop -> Type where
  Proof : (prof x -> prof y) -> (refu y -> refu x) -> Rule x y

id : Rule x x
id = Proof (\a => a) (\a => a)

interface Com (op : Prop -> Prop -> Prop) where
  com : Rule (op a b) (op b a)

interface Asl (op : Prop -> Prop -> Prop) where
  asl : Rule (op (op a b) c) (op a (op b c))

--Com AC where
--  com = Proof (\x => (?aaa1, ?aaa2)) (\y => Left ?aaaa1)

srl_prof : prof (MC a (MD b c)) -> prof (MD (MC a b) c)
srl_prof (a, (f,g)) = ((\(h,i) => f (h a)), (\rc => (a, g rc)))

srl_refu : refu (MD (MC a b) c) -> refu (MC a (MD b c))
srl_refu ((f,g), b) = ((\a => (f a, b)), (\(h,i) => g (i b)))

srl : Rule (MC a (MD b c)) (MD (MC a b) c)
srl = Proof srl_prof srl_refu

ax_prof : prof Unit -> prof (MD a (dual a))

ax_refu : refu (MD a (dual a)) -> refu Unit

ax : Rule Unit (MD a (dual a))
ax = Proof ax_prof ax_refu

cut_prof : (a:Prop) -> prof (MC a (dual a)) -> prof Counit
cut_prof a (x, y) = conflict a x (dual_refu a y)

cut_refu : (a:Prop) -> refu Counit -> refu (MC a (dual a))
cut_refu a () = (\x => refu_dual a x, \x => dual_refu a x)

cut : {auto a:Prop} -> Rule (MC a (dual a)) Counit
cut {a} = Proof (cut_prof a) (cut_refu a)