{-# LANGUAGE GADTs                #-} -- Soft dependent types
{-# LANGUAGE PolyKinds            #-} -- Allow general specification of Refl
{-# LANGUAGE RankNTypes           #-} -- Explicit quantification and inline type context
{-# LANGUAGE DataKinds            #-} -- Lift data constructors to Kind level
{-# LANGUAGE TypeFamilies         #-} -- Equational reasoning about types
{-# LANGUAGE TypeOperators        #-} -- Allow types such as :~:

-- Starting the interactive shell:
-- 
-- ghci -XDataKinds -XTypeOperators -Wall -Werror Script.hs
-- 
-- Important interactive commands
-- 
-- :r  - reload file
-- :t  - type of a value
-- :k! - Get kind and reduce it (by !) 

module Proof where

-- Part 1: Prove De Morgans low `not (a /\ b) = not a \/ not b`

-- Booleans

-- Type level Booleans
data Boolean = 'Tru | 'Fls

data SBool (a :: Boolean) where
  STrue :: SBool 'Tru
  SFalse :: SBool 'Fls

-- Define operators
type family And a b where
  And 'Tru 'Tru = 'Tru
  And 'Fls 'Tru = 'Fls
  And 'Tru 'Fls = 'Fls
  And 'Fls 'Fls = 'Fls

-- See that we can use it for Typing
calculateAnd :: SBool (And 'Tru 'Fls)
calculateAnd = SFalse

-- Define Rest of Operators
type family Not (a :: Boolean) :: Boolean
type instance Not 'Tru = 'Fls
type instance Not 'Fls = 'Tru

type family Or (a :: Boolean) (b :: Boolean) :: Boolean
type instance Or 'Tru 'Tru = 'Tru
type instance Or 'Fls 'Tru = 'Tru
type instance Or 'Tru 'Fls = 'Tru
type instance Or 'Fls 'Fls = 'Fls

-- Equality
data a :~: b where
  Refl :: a :~: a

instance Show (a :~: b) where
  show Refl = "QED"

-- Besides reflexivity the equivalence relation needs transitivity and symmetry
-- We prove that easily!
transitivity :: a :~: b -> b :~: c -> a :~: c
transitivity Refl Refl = Refl

symmetry :: a :~: b -> b :~: a
symmetry Refl = Refl

-- De Morgen
proofDeMorgan :: SBool a -> SBool b -> (Not (And a b)) :~: Or (Not a) (Not b)
-- Compute by `:t proofDeMorgan STrue STrue` etc.
proofDeMorgan STrue STrue = Refl
proofDeMorgan STrue SFalse = Refl
proofDeMorgan SFalse STrue = Refl
proofDeMorgan SFalse SFalse = Refl

-- Needed for proof composition
gcastWith :: a :~: b -> (a ~ b => r) -> r
gcastWith Refl x = x

-- What does this do? It allows the type checker to draw in an existing proof
-- to model a new proposition. A trivial example would be

-- A test proof
lemma :: 'Tru :~: Not 'Fls
lemma = Refl

-- Kind of silly, but shows that we can use the lemma
theorem :: Not (Not 'Tru) :~: Not 'Fls
theorem = gcastWith lemma Refl

-- Part 2 Prove properties about Naturals

-- Define type level natural
data Nat = 'Z | 'S Nat

-- Define value level naturals
data SNat (n :: Nat) where
  SZ :: SNat 'Z
  SS :: SNat n -> SNat ('S n)

type family a + b where
  'Z + b = b              -- Rule 1
  'S a + b = 'S (a + b)   -- Rule 2

-- one plus one equals two
onePlusOneEqualTwo :: 'S 'Z + 'S 'Z :~: 'S ('S 'Z)
onePlusOneEqualTwo = Refl

plusZeroLeftId :: SNat b -> 'Z + b :~: b
plusZeroLeftId _ = Refl

plusZeroRightId :: SNat a -> a + 'Z :~: a
plusZeroRightId SZ = Refl
plusZeroRightId (SS a) = gcastWith (plusZeroRightId a) Refl

-- Undertandig gcastWith:
-- 1. plusZeroRightId a proves that:    a + 'Z :~: a
-- 2. Refl seeks to prove the goal, ie  ('S a) + 'Z :~: 'S a    
--
-- Then some automatic stuff happens:
-- ('S a) + 'Z :~: 'S a is rewritten to 'S (a + 'Z) :~: 'S a            (Rule 2)
-- 'S (a + 'Z) :~: 'S a is rewritten to 'S a :~: 'S a                   (Provided proof)
-- Refl inhabits 'S a :~: 'S a
-- Simple pimple!

plusIsAssociative :: SNat a -> SNat b -> SNat c -> ((a + b) + c) :~: (a + (b + c))
plusIsAssociative SZ _ _ = Refl
plusIsAssociative (SS a) b c = gcastWith (plusIsAssociative a b c) Refl

plusIsCommutative :: SNat a -> SNat b -> (a + b) :~: (b + a)
plusIsCommutative SZ b = gcastWith (plusZeroRightId b) Refl
plusIsCommutative (SS _) _ = error "For the reader"

-- The commutativity proof is rather long. Though it simply uses the tools
-- already defined. There are online resources on how to do it.