Skip to content

Instantly share code, notes, and snippets.

@madsbuch
Last active May 8, 2021
Embed
What would you like to do?
{-# 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.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment