IndEven.hs

{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeInType #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unticked-promoted-constructors #-}
module IndEven where

import Data.Kind
import Data.Singletons.TH
import Data.Type.Equality

import Prelude hiding (sum, (+))

-----
-- IndEven
-----

$(singletons
  [d| data Peano :: Type where
        Z :: Peano
        S :: Peano -> Peano

      isEven :: Peano -> Bool
      isEven Z = True
      isEven (S Z) = False
      isEven (S (S n)) = isEven n

      (+) :: Peano -> Peano -> Peano
      Z   + b = b
      S a + b = S (a + b)
    |])

data Ev :: Peano -> Type where
  EZ  :: Ev Z
  ESS :: Peano -> Ev n -> Ev (S (S n))

data So :: Bool -> Type where
  Oh :: So True

test :: forall (n :: Peano). Ev (S (S n)) -> Ev n
test (ESS _ q) = q

thm1 :: Sing (n :: Peano) -> So (IsEven n) -> Ev n
thm1 SZ          Oh = EZ
thm1 (SS SZ)     oh = case oh of {}
thm1 (SS (SS n)) Oh = ESS (fromSing n) (thm1 n Oh)

thm2 :: forall (n :: Peano). Ev n -> So (IsEven n)
thm2 EZ         = Oh
thm2 (ESS _ pf) = thm2 pf

-----
-- IndPerm
-----

$(singletons
  [d| data List a = Nil | Cons a (List a)

      sum :: List Peano -> Peano
      sum Nil         = Z
      sum (Cons x xs) = x + sum xs
    |])

assoc :: forall a b c.
         Sing (a :: Peano) -> a :+ (b :+ c) :~: (a :+ b) :+ c
assoc SZ                 = Refl
assoc (SS (n :: Sing k)) = case assoc @k @b @c n of Refl -> Refl

rightZero :: Sing (n :: Peano) -> n :+ Z :~: n
rightZero SZ     = Refl
rightZero (SS n) = case rightZero n of Refl -> Refl

rightAdd1 :: forall a b. Sing (a :: Peano) -> a :+ S b :~: S (a :+ b)
rightAdd1 SZ                 = Refl
rightAdd1 (SS (n :: Sing k)) = case rightAdd1 @k @b n of Refl -> Refl

comm :: forall a b. Sing (a :: Peano) -> Sing (b :: Peano)
     -> a :+ b :~: b :+ a
comm SZ                 sb = sym (rightZero sb)
comm (SS (n :: Sing k)) sb =
  case comm n sb of
    Refl -> case rightAdd1 @b @k sb of
      Refl -> Refl

twiddle :: forall a b c.
           Sing (a :: Peano) -> Sing (b :: Peano) -> Sing (c :: Peano)
        -> a :+ (b :+ c) :~: b :+ (a :+ c)
twiddle sa sb sc =
  case comm sa (sb %:+ sc) of
    Refl -> case assoc @b @c @a sb of
      Refl -> case comm sc sa of
        Refl -> Refl

data Ins :: forall (a :: Type). a -> List a -> List a -> Type where
  Here  :: forall (m :: a) (ms :: List a).
           Ins m ms (Cons m ms)
  There :: forall (m :: a) (n :: a) (ns :: List a) (mns :: List a).
           Sing m -> Sing n -> Sing ns -> Sing mns
        -> Ins m ns mns -> Ins m (Cons n ns) (Cons n mns)

data Perm :: forall (a :: Type). List a -> List a -> Type where
  NilPerm  :: Perm Nil Nil
  ConsPerm :: forall (m :: a) (ms :: List a) (ns :: List a) (mns :: List a).
              Sing m -> Sing ms -> Sing ns -> Sing mns
           -> Ins m ns mns
           -> Perm ms ns
           -> Perm (Cons m ms) mns

lemma :: forall (m :: Peano) (ns :: List Peano) (mns :: List Peano).
         Sing m -> Sing ns -> Sing mns
      -> Ins m ns mns -> (m :+ Sum ns) :~: (Sum mns)
lemma _ _ _ Here = Refl
lemma _ _ _ (There sm sn sns smns pf) =
    case lemma sm sns smns pf of
      Refl -> case twiddle sn sm (sSum sns) of
        Refl -> Refl

theorem :: forall (ms :: List Peano) (ns :: List Peano).
           Sing ms -> Sing ns
        -> Perm ms ns
        -> Sum ms :~: Sum ns
theorem _ _ NilPerm = Refl
theorem _ _ (ConsPerm sm sms sns smns ins perm)
  = case lemma sm sns smns ins of
      Refl -> case theorem sms sns perm of
        Refl -> Refl

-----
-- IndStar
-----

type Rel a = a -> a -> Bool

data Star :: forall (a :: Type). Rel a -> a -> a -> Type where
  StarRefl :: forall (r :: Rel a) (x :: a).
              Star r x x
  StarStep :: forall (r :: Rel a) (x :: a) (y :: a) (z :: a).
              So (r x y)
           -> Star r y z
           -> Star r x z

thm :: Star r x y -> Star r y z -> Star r x z
thm StarRefl          yz = yz
thm (StarStep x1 x1y) yz = StarStep x1 (thm x1y yz)