{-# LANGUAGE CPP #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE UndecidableInstances #-}
#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800
{-# LANGUAGE ConstrainedClassMethods, TypeFamilyDependencies #-}
#endif
module Proof.Equational
( (:~:) (..),
(:=:),
sym,
trans,
Equality (..),
Preorder (..),
reflexivity',
(:\/:),
(:/\:),
(=<=),
(=>=),
(=~=),
Leibniz (..),
Reason (..),
because,
by,
(===),
start,
byDefinition,
admitted,
Proxy (..),
cong,
cong',
Proposition (..),
HVec (..),
FromBool (..),
applyNAry,
applyNAry',
fromBool',
fromRefl,
fromLeibniz,
reflToLeibniz,
leibnizToRefl,
coerce,
coerceInner,
coerce',
withRefl,
module Data.Proxy,
)
where
import Data.Kind (Type)
import Data.Proxy
import Data.Type.Equality hiding (apply)
import Unsafe.Coerce
infix 4 :=:
type a :\/: b = Either a b
infixr 2 :\/:
type a :/\: b = (a, b)
infixr 3 :/\:
type (:=:) = (:~:)
data Leibniz a b = Leibniz {Leibniz a b -> forall (f :: k -> *). f a -> f b
apply :: forall f. f a -> f b}
leibnizToRefl :: Leibniz a b -> a :=: b
leibnizToRefl :: Leibniz a b -> a :=: b
leibnizToRefl Leibniz a b
eq = Leibniz a b -> (a :~: a) -> a :=: b
forall k (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply Leibniz a b
eq a :~: a
forall k (a :: k). a :~: a
Refl
fromLeibniz :: (Preorder eq) => Leibniz a b -> eq a b
fromLeibniz :: Leibniz a b -> eq a b
fromLeibniz Leibniz a b
eq = Leibniz a b -> eq a a -> eq a b
forall k (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply Leibniz a b
eq (Proxy a -> eq a a
forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity Proxy a
forall k (t :: k). Proxy t
Proxy)
fromRefl :: (Preorder eq) => a :=: b -> eq a b
fromRefl :: (a :=: b) -> eq a b
fromRefl a :=: b
Refl = eq a b
forall k (r :: k -> k -> *) (x :: k). Preorder r => r x x
reflexivity'
reflToLeibniz :: a :=: b -> Leibniz a b
reflToLeibniz :: (a :=: b) -> Leibniz a b
reflToLeibniz a :=: b
Refl = (forall (f :: k -> *). f a -> f b) -> Leibniz a b
forall k (a :: k) (b :: k).
(forall (f :: k -> *). f a -> f b) -> Leibniz a b
Leibniz forall a. a -> a
forall (f :: k -> *). f a -> f b
id
class Preorder (eq :: k -> k -> Type) where
reflexivity :: proxy a -> eq a a
transitivity :: eq a b -> eq b c -> eq a c
class Preorder eq => Equality (eq :: k -> k -> Type) where
symmetry :: eq a b -> eq b a
instance Preorder (:=:) where
{-# SPECIALIZE instance Preorder (:=:) #-}
transitivity :: (a :=: b) -> (b :=: c) -> a :=: c
transitivity a :=: b
Refl b :=: c
Refl = a :=: c
forall k (a :: k). a :~: a
Refl
{-# INLINE [1] transitivity #-}
reflexivity :: proxy a -> a :=: a
reflexivity proxy a
_ = a :=: a
forall k (a :: k). a :~: a
Refl
{-# INLINE [1] reflexivity #-}
instance Equality (:=:) where
{-# SPECIALIZE instance Equality (:~:) #-}
symmetry :: (a :=: b) -> b :=: a
symmetry a :=: b
Refl = b :=: a
forall k (a :: k). a :~: a
Refl
{-# INLINE [1] symmetry #-}
instance Preorder (->) where
reflexivity :: proxy a -> a -> a
reflexivity proxy a
_ = a -> a
forall a. a -> a
id
transitivity :: (a -> b) -> (b -> c) -> a -> c
transitivity = ((b -> c) -> (a -> b) -> a -> c) -> (a -> b) -> (b -> c) -> a -> c
forall a b c. (a -> b -> c) -> b -> a -> c
flip (b -> c) -> (a -> b) -> a -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.)
leibniz_refl :: Leibniz a a
leibniz_refl :: Leibniz a a
leibniz_refl = (forall (f :: k -> *). f a -> f a) -> Leibniz a a
forall k (a :: k) (b :: k).
(forall (f :: k -> *). f a -> f b) -> Leibniz a b
Leibniz forall a. a -> a
forall (f :: k -> *). f a -> f a
id
instance Preorder Leibniz where
reflexivity :: proxy a -> Leibniz a a
reflexivity proxy a
_ = Leibniz a a
forall k (a :: k). Leibniz a a
leibniz_refl
transitivity :: Leibniz a b -> Leibniz b c -> Leibniz a c
transitivity (Leibniz forall (f :: k -> *). f a -> f b
aEqb) (Leibniz forall (f :: k -> *). f b -> f c
bEqc) = (forall (f :: k -> *). f a -> f c) -> Leibniz a c
forall k (a :: k) (b :: k).
(forall (f :: k -> *). f a -> f b) -> Leibniz a b
Leibniz ((forall (f :: k -> *). f a -> f c) -> Leibniz a c)
-> (forall (f :: k -> *). f a -> f c) -> Leibniz a c
forall a b. (a -> b) -> a -> b
$ f b -> f c
forall (f :: k -> *). f b -> f c
bEqc (f b -> f c) -> (f a -> f b) -> f a -> f c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. f a -> f b
forall (f :: k -> *). f a -> f b
aEqb
instance Equality Leibniz where
symmetry :: Leibniz a b -> Leibniz b a
symmetry Leibniz a b
eq = Flip Leibniz a b -> Leibniz b a
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
Flip f a b -> f b a
unFlip (Flip Leibniz a b -> Leibniz b a)
-> Flip Leibniz a b -> Leibniz b a
forall a b. (a -> b) -> a -> b
$ Leibniz a b -> forall (f :: k -> *). f a -> f b
forall k (a :: k) (b :: k).
Leibniz a b -> forall (f :: k -> *). f a -> f b
apply Leibniz a b
eq (Flip Leibniz a a -> Flip Leibniz a b)
-> Flip Leibniz a a -> Flip Leibniz a b
forall a b. (a -> b) -> a -> b
$ Leibniz a a -> Flip Leibniz a a
forall k k (f :: k -> k -> *) (a :: k) (b :: k).
f b a -> Flip f a b
Flip Leibniz a a
forall k (a :: k). Leibniz a a
leibniz_refl
newtype Flip f a b = Flip {Flip f a b -> f b a
unFlip :: f b a}
data Reason eq x y where
Because :: proxy y -> eq x y -> Reason eq x y
reflexivity' :: (Preorder r) => r x x
reflexivity' :: r x x
reflexivity' = Proxy x -> r x x
forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity Proxy x
forall k (t :: k). Proxy t
Proxy
by, because :: proxy y -> eq x y -> Reason eq x y
because :: proxy y -> eq x y -> Reason eq x y
because = proxy y -> eq x y -> Reason eq x y
forall k k (proxy :: k -> *) (y :: k) (eq :: k -> k -> *) (x :: k).
proxy y -> eq x y -> Reason eq x y
Because
by :: proxy y -> eq x y -> Reason eq x y
by = proxy y -> eq x y -> Reason eq x y
forall k k (proxy :: k -> *) (y :: k) (eq :: k -> k -> *) (x :: k).
proxy y -> eq x y -> Reason eq x y
Because
infixl 4 ===, =<=, =~=, =>=
infix 5 `Because`
infix 5 `because`
(=<=) :: Preorder r => r x y -> Reason r y z -> r x z
r x y
eq =<= :: r x y -> Reason r y z -> r x z
=<= (proxy z
_ `Because` r y z
eq') = r x y -> r y z -> r x z
forall k (eq :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Preorder eq =>
eq a b -> eq b c -> eq a c
transitivity r x y
eq r y z
eq'
{-# SPECIALIZE INLINE [1] (=<=) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
(=>=) :: Preorder r => r y z -> Reason r x y -> r x z
r y z
eq =>= :: r y z -> Reason r x y -> r x z
=>= (proxy y
_ `Because` r x y
eq') = r x y -> r y z -> r x z
forall k (eq :: k -> k -> *) (a :: k) (b :: k) (c :: k).
Preorder eq =>
eq a b -> eq b c -> eq a c
transitivity r x y
eq' r y z
eq
{-# SPECIALIZE INLINE [1] (=>=) :: y :~: z -> Reason (:~:) x y -> x :~: z #-}
(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z
=== :: eq x y -> Reason eq y z -> eq x z
(===) = eq x y -> Reason eq y z -> eq x z
forall k (r :: k -> k -> *) (x :: k) (y :: k) (z :: k).
Preorder r =>
r x y -> Reason r y z -> r x z
(=<=)
{-# SPECIALIZE INLINE [1] (===) :: x :~: y -> Reason (:~:) y z -> x :~: z #-}
(=~=) :: r x y -> proxy y -> r x y
r x y
eq =~= :: r x y -> proxy y -> r x y
=~= proxy y
_ = r x y
eq
start :: Preorder eq => proxy a -> eq a a
start :: proxy a -> eq a a
start = proxy a -> eq a a
forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity
byDefinition :: (Preorder eq) => eq a a
byDefinition :: eq a a
byDefinition = Proxy a -> eq a a
forall k (eq :: k -> k -> *) (proxy :: k -> *) (a :: k).
Preorder eq =>
proxy a -> eq a a
reflexivity Proxy a
forall k (t :: k). Proxy t
Proxy
admitted :: Reason eq x y
admitted :: Reason eq x y
admitted = Reason eq x y
forall a. HasCallStack => a
undefined
{-# WARNING admitted "There are some goals left yet unproven." #-}
cong :: forall f a b. Proxy f -> a :=: b -> f a :=: f b
cong :: Proxy f -> (a :=: b) -> f a :=: f b
cong Proxy f
Proxy a :=: b
Refl = f a :=: f b
forall k (a :: k). a :~: a
Refl
cong' :: (pxy m -> pxy (f m)) -> a :=: b -> f a :=: f b
cong' :: (pxy m -> pxy (f m)) -> (a :=: b) -> f a :=: f b
cong' pxy m -> pxy (f m)
_ a :=: b
Refl = f a :=: f b
forall k (a :: k). a :~: a
Refl
coerceInner, coerce :: (a :=: b) -> f a -> f b
{-# DEPRECATED coerce "Use coerceInner instead" #-}
coerce :: (a :=: b) -> f a -> f b
coerce = (a :=: b) -> f a -> f b
forall k (a :: k) (b :: k) (f :: k -> *). (a :=: b) -> f a -> f b
coerceInner
{-# INLINE coerce #-}
coerceInner :: (a :=: b) -> f a -> f b
coerceInner a :=: b
_ = f a -> f b
forall a b. a -> b
unsafeCoerce
{-# INLINE [1] coerceInner #-}
coerce' :: a :=: b -> a -> b
coerce' :: (a :=: b) -> a -> b
coerce' a :=: b
_ = a -> b
forall a b. a -> b
unsafeCoerce
{-# INLINE [1] coerce' #-}
{-# RULES
"coerce/unsafeCoerce" [~1] forall xs.
coerceInner xs =
unsafeCoerce
"coerce'/unsafeCoerce" [~1] forall xs.
coerce' xs =
unsafeCoerce
#-}
withRefl :: forall a b r. a :~: b -> (a ~ b => r) -> r
withRefl :: (a :~: b) -> ((a ~ b) => r) -> r
withRefl a :~: b
_ = (a :~: b) -> ((a ~ b) => r) -> r
forall k (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith ((() :~: ()) -> a :~: b
forall a b. a -> b
unsafeCoerce (() :~: ()
forall k (a :: k). a :~: a
Refl :: () :~: ()) :: a :~: b)
class Proposition (f :: k -> Type) where
type OriginalProp (f :: k -> Type) (n :: k) :: Type
unWrap :: f n -> OriginalProp f n
wrap :: OriginalProp f n -> f n
data HVec (xs :: [Type]) where
HNil :: HVec '[]
(:-) :: x -> HVec xs -> HVec (x ': xs)
infixr 9 :-
type family (xs :: [Type]) :~> (a :: Type) :: Type where
'[] :~> a = a
(x ': xs) :~> a = x -> (xs :~> a)
infixr 1 :~>
data HVecView (xs :: [Type]) :: Type where
HNilView :: HVecView '[]
HConsView :: Proxy t -> HVecView ts -> HVecView (t ': ts)
deriving instance Show (HVecView xs)
class KnownTypeList (xs :: [Type]) where
viewHVec' :: HVecView xs
instance KnownTypeList '[] where
viewHVec' :: HVecView '[]
viewHVec' = HVecView '[]
HNilView
instance KnownTypeList ts => KnownTypeList (t ': ts) where
viewHVec' :: HVecView (t : ts)
viewHVec' = Proxy t -> HVecView ts -> HVecView (t : ts)
forall t (ts :: [*]). Proxy t -> HVecView ts -> HVecView (t : ts)
HConsView Proxy t
forall k (t :: k). Proxy t
Proxy HVecView ts
forall (xs :: [*]). KnownTypeList xs => HVecView xs
viewHVec'
newtype Magic (xs :: [Type]) a = Magic {Magic xs a -> KnownTypeList xs => a
_viewHVec' :: KnownTypeList xs => a}
withKnownTypeList :: forall a xs. HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList :: HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList HVecView xs
xs KnownTypeList xs => a
f = (Magic xs a -> HVecView xs -> a
forall a b. a -> b
unsafeCoerce ((KnownTypeList xs => a) -> Magic xs a
forall (xs :: [*]) a. (KnownTypeList xs => a) -> Magic xs a
Magic KnownTypeList xs => a
f :: Magic xs a) :: HVecView xs -> a) HVecView xs
xs
apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' :: HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' HVecView ts
HNilView HVec ts -> c
f = HVec ts -> c
f HVec ts
HVec '[]
HNil
apply' (HConsView Proxy t
Proxy HVecView ts
ts) HVec ts -> c
f = \t
a ->
HVecView ts -> (KnownTypeList ts => ts :~> c) -> ts :~> c
forall a (xs :: [*]). HVecView xs -> (KnownTypeList xs => a) -> a
withKnownTypeList HVecView ts
ts ((KnownTypeList ts => ts :~> c) -> ts :~> c)
-> (KnownTypeList ts => ts :~> c) -> ts :~> c
forall a b. (a -> b) -> a -> b
$
HVecView ts -> (HVec ts -> c) -> ts :~> c
forall (ts :: [*]) c. HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' HVecView ts
ts (\HVec ts
ts' -> HVec ts -> c
f (HVec ts -> c) -> HVec ts -> c
forall a b. (a -> b) -> a -> b
$ t
a t -> HVec ts -> HVec (t : ts)
forall x (xs :: [*]). x -> HVec xs -> HVec (x : xs)
:- HVec ts
ts')
applyNAry :: forall ts c. KnownTypeList ts => (HVec ts -> c) -> ts :~> c
applyNAry :: (HVec ts -> c) -> ts :~> c
applyNAry = HVecView ts -> (HVec ts -> c) -> ts :~> c
forall (ts :: [*]) c. HVecView ts -> (HVec ts -> c) -> ts :~> c
apply' (HVecView ts
forall (xs :: [*]). KnownTypeList xs => HVecView xs
viewHVec' :: HVecView ts)
applyNAry' :: KnownTypeList ts => proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' :: proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' proxy ts
_ proxy' c
_ = (HVec ts -> c) -> ts :~> c
forall (ts :: [*]) c.
KnownTypeList ts =>
(HVec ts -> c) -> ts :~> c
applyNAry
class FromBool (c :: Type) where
type Predicate c :: Bool
type Args c :: [Type]
fromBool :: Predicate c ~ 'True => HVec (Args c) -> c
fromBool' :: forall proxy c. (KnownTypeList (Args c), FromBool c, Predicate c ~ 'True) => proxy c -> Args c :~> c
fromBool' :: proxy c -> Args c :~> c
fromBool' proxy c
pxyc = Proxy (Args c) -> proxy c -> (HVec (Args c) -> c) -> Args c :~> c
forall (ts :: [*]) (proxy :: [*] -> *) (proxy' :: * -> *) c.
KnownTypeList ts =>
proxy ts -> proxy' c -> (HVec ts -> c) -> ts :~> c
applyNAry' (Proxy (Args c)
forall k (t :: k). Proxy t
Proxy :: Proxy (Args c)) proxy c
pxyc HVec (Args c) -> c
forall c. (FromBool c, Predicate c ~ 'True) => HVec (Args c) -> c
fromBool