packages feed

equational-reasoning (empty) → 0.0.1.0

raw patch · 5 files changed

+222/−0 lines, 5 filesdep +basedep +singletonsdep +taggedsetup-changed

Dependencies added: base, singletons, tagged, void

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2012, Hiromi ISHII++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Hiromi ISHII nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Proof/Equational.hs view
@@ -0,0 +1,115 @@+{-# LANGUAGE DataKinds, FlexibleContexts, GADTs, PolyKinds, RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TypeFamilies     #-}+{-# LANGUAGE TypeOperators, TypeSynonymInstances                       #-}+module Proof.Equational ((:=:)(..), Equality(..), Preorder(..), reflexivity'+                        ,(:\/:), (:/\:), (=>=), (=~=), Leibniz(..)+                        , Reason(..), because, by, (===), start, byDefinition+                        , admitted, Proxy(..), cong, cong', fromRefl+                        , Proposition(..), (:~>), FromBool (..)+                          -- * Re-exported modules+                        , module Data.Singletons, module Data.Proxy+                        ) where+import Data.Proxy+import Data.Singletons++infix 4 :=:+type a :\/: b = Either a b+infixr 2 :\/:++type a :/\: b = (a, b)+infixr 3 :/\:++data a :=: b where+  Refl :: a :=: a++data Leibniz a b = Leibniz { apply :: forall f. f a -> f b }++fromRefl :: (Preorder eq, SingRep b) => a :=: b -> eq a b+fromRefl Refl = reflexivity'++deriving instance Show (a :=: b)++class Preorder (eq :: k -> k -> *) where+  reflexivity  :: Sing a -> eq a a+  transitivity :: eq a b  -> eq b c -> eq a c++class Preorder eq => Equality (eq :: k -> k -> *) where+  symmetry     :: eq a b  -> eq b a++instance Preorder (:=:) where+  transitivity Refl Refl = Refl+  reflexivity  _         = Refl++instance Equality (:=:) where+  symmetry     Refl      = Refl++instance Preorder (->) where+  reflexivity _ = id+  transitivity = flip (.)++leibniz_refl :: Leibniz a a+leibniz_refl = Leibniz id++instance Preorder Leibniz where+  reflexivity _ = leibniz_refl+  transitivity (Leibniz aEqb) (Leibniz bEqc) = Leibniz $ bEqc . aEqb++instance Equality Leibniz where+  symmetry eq  = unFlip $ apply eq $ Flip leibniz_refl++newtype Flip f a b = Flip { unFlip :: f b a }++data Reason eq x y where+  Because :: Sing y -> eq x y -> Reason eq x y++reflexivity' :: (SingRep x, Preorder r) => r x x+reflexivity' = reflexivity sing++by, because :: Sing y -> eq x y -> Reason eq x y+because = Because+by      = Because++infixl 4 ===, =>=, =~=+infix 5 `Because`+infix 5 `because`++(=>=) :: Preorder r => r x y -> Reason r y z -> r x z+eq =>= (_ `Because` eq') = transitivity eq eq'++(===) :: Equality eq => eq x y -> Reason eq y z -> eq x z+(===) = (=>=)++(=~=) :: Preorder r => r x y -> Sing y -> r x y+eq =~= _ = eq++start :: Preorder eq => Sing a -> eq a a+start = reflexivity++byDefinition :: (SingRep a, Preorder eq) => eq a a+byDefinition = reflexivity sing++admitted :: Reason eq x y+admitted = 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 Refl = Refl++cong' :: (Sing m -> Sing (f m)) -> a :=: b -> f a :=: f b+cong' _ Refl =  Refl++class Proposition f where+  type OriginalProp f n :: *+  unWrap :: f n -> OriginalProp f n+  wrap   :: OriginalProp f n -> f n++type family   (xs :: [*]) :~> (a :: *) :: *+type instance '[]       :~> a = a+type instance (x ': xs) :~> a = x -> (xs :~> a)++infixr 1 :~>++class FromBool (c :: *) where+  type Predicate c :: Bool+  type Args c :: [*]+  fromBool :: Predicate c ~ True => Args c :~> c
+ Proof/Propositional.hs view
@@ -0,0 +1,52 @@+{-# LANGUAGE TypeOperators #-}+-- | Provides type synonyms for logical connectives.+module Proof.Propositional ( type (/\), type (\/), Not, exfalso, orIntroL+                           , orIntroR, orElim, andIntro, andElimL+                           , andElimR, orAssocL, orAssocR+                           , andAssocL, andAssocR+                           ) where+import Data.Void++type a /\ b = (a, b)+type a \/ b = Either a b+type Not a  = a -> Void++infixr 2 \/+infixr 3 /\++exfalso :: a -> Not a -> b+exfalso a neg = absurd (neg a)++orIntroL :: a -> a \/ b+orIntroL = Left++orIntroR :: b -> a \/ b+orIntroR = Right++orElim :: a \/ b -> (a -> c) -> (b -> c) -> c+orElim aORb aTOc bTOc = either aTOc bTOc aORb++andIntro :: a -> b -> a /\ b+andIntro = (,)++andElimL :: a /\ b -> a+andElimL = fst++andElimR :: a /\ b -> b+andElimR = snd++andAssocL :: a /\ (b /\ c) -> (a /\ b) /\ c+andAssocL (a,(b,c)) = ((a,b), c)++andAssocR :: (a /\ b) /\ c -> a /\ (b /\ c)+andAssocR ((a,b),c) = (a,(b,c))++orAssocL :: a \/ (b \/ c) -> (a \/ b) \/ c+orAssocL (Left a)          = Left (Left a)+orAssocL (Right (Left b))  = Left (Right b)+orAssocL (Right (Right c)) = Right c++orAssocR :: (a \/ b) \/ c -> a \/ (b \/ c)+orAssocR (Left (Left a))  = Left a+orAssocR (Left (Right b)) = Right (Left b)+orAssocR (Right c)        = Right (Right c)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ equational-reasoning.cabal view
@@ -0,0 +1,23 @@+-- Initial equational-reasoning.cabal generated by cabal init.  For further+--  documentation, see http://haskell.org/cabal/users-guide/++name:                equational-reasoning+version:             0.0.1.0+synopsis:            Proof assistant for Haskell using DataKinds & PolyKinds+-- description:         +license:             BSD3+license-file:        LICENSE+author:              Hiromi ISHII+maintainer:          konn.jinro_at_gmail.com+-- copyright:           +category:            Math+build-type:          Simple+cabal-version:       >=1.8++library+  exposed-modules:     Proof.Equational, Proof.Propositional+  build-depends:       base       == 4.6.*+               ,       singletons == 0.8.*+               ,       tagged     == 0.6.*+               ,       void       == 0.6.*+