Hello,

 

I have written the below proof as an exercise.

 

I want to explicitly annotate the proof with type variables…..but I cant get a line to work…

 

> {-# LANGUAGE DataKinds #-}

> {-# LANGUAGE ExplicitForAll #-}

> {-# LANGUAGE FlexibleContexts #-}

> {-# LANGUAGE FlexibleInstances #-}

> {-# LANGUAGE GADTs #-}

> {-# LANGUAGE MultiParamTypeClasses #-}

> {-# LANGUAGE PolyKinds #-}

> {-# LANGUAGE StandaloneDeriving #-}

> {-# LANGUAGE TypeFamilies #-}

> {-# LANGUAGE TypeOperators #-}

> {-# LANGUAGE UndecidableInstances #-}

> {-# LANGUAGE ScopedTypeVariables #-}

 

> import Prelude hiding (head, tail, (++), (+), replicate)

> import qualified Prelude as P

 

> data Nat where

>   Z :: Nat

>   S :: Nat -> Nat

 

> data SNat (a :: Nat) where

>   SZ :: SNat 'Z

>   SS :: SNat a -> SNat ('S a)

 

here a nice plus

 

> type family   (n :: Nat) :+ (m :: Nat) :: Nat

> type instance Z     :+ m = m

> type instance (S n) :+ m = S (n :+ m)

 

lets try to do

 

> data val1 :== val2 where

>   Refl :: val :== val

 

If I prove its abelian then we get it...

 

the "proof" works if we remove the type annotation

but I want the annotation to convince myself I know whats going on.

 

 

> theoremPlusAbelian :: SNat a -> SNat b -> (a :+ b) :== (b :+ a)

> theoremPlusAbelian (SZ :: SNat a) (SZ :: SNat b) =

> -- forall 0 and 0

>   (Refl :: (a :+ b) :== (b :+ a))

> theoremPlusAbelian ((SS a) :: SNat a) (SZ :: SNat b) =

> -- forall a + 1 and 0

>   case theoremPlusAbelian (a :: (a ~ 'S a1) => SNat a1) (SZ :: SNat b) of

>     (Refl :: (a1 :+ b) :== (b :+ a1)) ->

>       (Refl :: (a :+ b) :== (b :+ a))

> theoremPlusAbelian (SZ :: SNat a) ((SS a) :: SNat b) =

> -- forall 0 and a + 1

>   case theoremPlusAbelian (SZ :: SNat a) (a :: (b ~ 'S b1) => SNat b1) of

>     (Refl :: (a :+ b1) :== (b1 :+ a)) ->

>       (Refl :: (a :+ b) :== (b :+ a))

> -- cant seem to prove this...

> theoremPlusAbelian ((SS a) :: (SNat a)) ((SS b) :: (SNat b))      =

> -- forall a+1 and b+1

> -- 1st prove (a + 1) + b =  b + (a + 1)...from above

>   case theoremPlusAbelian ((SS a) :: (SNat a)) (b :: (b ~ 'S b1) => SNat b1) of

 

THE COMMENTED LINE FAILS.

 

Could not deduce ((b1 :+ 'S a1) ~ (a2 :+ 'S a1))

    from the context (a ~ 'S a1)

      bound by a pattern with constructor

                 SS :: forall (a :: Nat). SNat a -> SNat ('S a),

               in an equation for ‘theoremPlusAbelian’

      at Cafe2.lhs:57:24-27

    or from (b ~ 'S a2)

      bound by a pattern with constructor

                 SS :: forall (a :: Nat). SNat a -> SNat ('S a),

               in an equation for ‘theoremPlusAbelian’

      at Cafe2.lhs:57:45-48

    NB: ‘:+’ is a type function, and may not be injective

    The type variable ‘b1’ is ambiguous

    Expected type: (a :+ a2) :== (a2 :+ a)

      Actual type: (a :+ b1) :== (b1 :+ a)

    Relevant bindings include

      b :: SNat a2 (bound at Cafe2.lhs:57:48)

      a :: SNat a1 (bound at Cafe2.lhs:57:27)

    In the pattern: Refl :: (a :+ b1) :== (b1 :+ a)

    In a case alternative:

        (Refl :: (a :+ b1) :== (b1 :+ a))

          -> case theoremPlusAbelian a (SS b) of {

               Refl -> case theoremPlusAbelian a b of { Refl -> Refl } }

    In the expression:

      case

          theoremPlusAbelian ((SS a) :: SNat a) (b :: b ~ S b1 => SNat b1)

      of {

        (Refl :: (a :+ b1) :== (b1 :+ a))

          -> case theoremPlusAbelian a (SS b) of {

               Refl -> case theoremPlusAbelian a b of { Refl -> ... } } }

 

 

 

>     -- (Refl :: (a :+ b1) :== (b1 :+ a)) ->

>     Refl ->

> -- now prove a + (b + 1) =  (b + 1) + a...from above

>       case theoremPlusAbelian a (SS b) of

>         Refl ->

> -- now prove a + b = b + a

>           case theoremPlusAbelian a b of

> -- which seems to have proved a + b = b + a

>             Refl -> Refl