gdp 0.0.0.2 → 0.0.3.0

raw patch · 14 files changed

+446/−367 lines, 14 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• README.md +0/−2
• app/Main.hs +8/−4
• gdp.cabal +4/−2
• src/Data/Arguments.hs +1/−1
• src/Data/Refined.hs +6/−0
• src/GDP.hs +11/−9
• src/Logic/Classes.hs +20/−31
• src/Logic/Implicit.hs +54/−0
• src/Logic/NegClasses.hs +7/−11
• src/Logic/Proof.hs +17/−133
• src/Logic/Propositional.hs +145/−168
• src/Theory/Equality.hs +8/−5
• src/Theory/Lists.hs +151/−0
• src/Theory/Named.hs +14/−1

@@ -1,4 +1,2 @@ # gdp: Ghosts of Departed Proofs --

@@ -1,12 +1,13 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE GADTs         #-}+{-# LANGUAGE GADTs           #-}+{-# LANGUAGE RoleAnnotations #-}+{-# LANGUAGE TypeOperators   #-}  module Main where -import GDP+import           GDP -import Data.Ord import qualified Data.List as L+import           Data.Ord  -- An unsafe merge. This relies on the user remembering to -- sort both of the inputs using the same comparator passed@@ -25,6 +26,7 @@ -- Introduce a predicate `SortedBy comp`, indicating that -- the value has been sorted by the comparator named `comp`. newtype SortedBy comp name = SortedBy Defn+type role SortedBy nominal nominal  -- Sort a value using the comparator named `comp`. The -- resulting value will satisfy `SortedBy comp`.@@ -43,6 +45,7 @@ mergeBy (The comp) (The xs) (The ys) = assert (unsafeMergeBy comp xs ys)  newtype Opposite comp = Opposite Defn+type role Opposite nominal  -- A named version of the opposite ordering. opposite :: ((a -> a -> Ordering) ~~ comp)@@ -53,6 +56,7 @@   LT -> GT  newtype Reverse xs = Reverse Defn+type role Reverse nominal  -- A named version of Prelude's 'reverse'. rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)

@@ -1,5 +1,5 @@ name:                gdp-version:             0.0.0.2+version:             0.0.3.0 synopsis:            Reason about invariants and preconditions with ghosts of departed proofs. description:         Reason about invariants and preconditions with ghosts of departed proofs.                      The GDP library implements building blocks for creating and working with@@ -8,7 +8,7 @@                      so that they will be statically checked at compile-time.                      As a library user, you can use the `gdp` deduction rules to codify your                      proofs that you are using the library correctly.-homepage:            https://github.com/githubuser/gdp#readme+homepage:            https://github.com/matt-noonan/gdp#readme license:             BSD3 license-file:        LICENSE author:              Matt Noonan@@ -26,11 +26,13 @@                      , Data.Refined                      , Data.The                      , Logic.Classes+                     , Logic.Implicit                      , Logic.NegClasses                      , Logic.Propositional                      , Logic.Proof                      , Theory.Equality                      , Theory.Named+                     , Theory.Lists                         build-depends:       base >= 4.7 && < 5                      , lawful

@@ -23,7 +23,7 @@ --   This is entirely a type-level operation, there --   is nothing corresponding to a value access or update. class Argument (f :: k1) (n :: k2) where-  type GetArg f n   :: k1+  type GetArg f n   :: k   type SetArg f n x :: k1  -- | Position: the left-hand side of a type.

@@ -5,6 +5,7 @@ {-# LANGUAGE RankNTypes            #-} {-# LANGUAGE KindSignatures        #-} {-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE RoleAnnotations       #-}  {-|   Module      :  Data.Refined@@ -61,6 +62,7 @@ -} newtype a ::: p = SuchThat a infixr 1 :::+type role (:::) nominal nominal  instance The a' a => The (a' ::: p) a where   the (SuchThat x) = the x@@ -102,6 +104,7 @@     run-time space or time cost. -} newtype Satisfies (p :: * -> *) a = Satisfies a+type role Satisfies nominal nominal instance The (Satisfies p a) a  -- | An infix alias for 'Satisfies'.@@ -130,7 +133,10 @@  @ newtype NonEmpty xs = NonEmpty Defn+type role Nonempty nominal -- disallows coercion of Nonempty's argument.+ newtype Reverse  xs = Reverse  Defn+type role Reverse nominal  rev :: ([a] ~~ xs) -> ([a] ~~ Reverse xs) rev xs = defn (reverse (the xs))

@@ -11,6 +11,7 @@   , module Data.Refined   , module Data.The   , module Logic.Classes+  , module Logic.Implicit   , module Logic.NegClasses   , module Logic.Proof   , module Logic.Propositional@@ -18,12 +19,13 @@   , module Theory.Named   ) where -import Data.Arguments-import Data.Refined-import Data.The-import Logic.Classes-import Logic.NegClasses-import Logic.Proof-import Logic.Propositional-import Theory.Equality-import Theory.Named+import           Data.Arguments+import           Data.Refined+import           Data.The+import           Logic.Classes+import           Logic.Implicit+import           Logic.NegClasses+import           Logic.Proof+import           Logic.Propositional+import           Theory.Equality+import           Theory.Named

@@ -1,7 +1,6 @@ {-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE DefaultSignatures     #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE PolyKinds             #-}  {-|   Module      :  Logic.Classes@@ -30,7 +29,6 @@  import Logic.Proof import Theory.Equality-import Theory.Named  {--------------------------------------------------------   Special properties of predicates and functions@@ -46,13 +44,12 @@  @ -- Define a reflexive binary relation-newtype SameColor p q = SameColor Defn+data SameColor p q instance Reflexive SameColor @--}   +-} class Reflexive r where   refl :: Proof (r x x)-  default refl :: (Defining (r x x)) => Proof (r x x)   refl = axiom  {-| A binary relation R is /symmetric/ if, for all x and y,@@ -66,13 +63,12 @@  @ -- Define a symmetric binary relation-newtype NextTo p q = NextTo Defn+data NextTo p q instance Symmetric NextTo @--}   +-} class Symmetric c where-  symmetric :: c p q -> Proof (c q p)-  default symmetric :: (Defining (c p q)) => c p q -> Proof (c q p)+  symmetric :: Proof (c p q) -> Proof (c q p)   symmetric _ = axiom  {-| A binary relation R is /transitive/ if, for all x, y, z,@@ -86,17 +82,16 @@  @ -- Define a transitive binary relation-newtype CanReach p q = CanReach Defn+data CanReach p q instance Transitive CanReach @--}   +-} class Transitive c where-  transitive :: c p q -> c q r -> Proof (c p r)-  default transitive :: Defining (c p q) => c p q -> c q r -> Proof (c p r)+  transitive :: Proof (c p q) -> Proof (c q r) -> Proof (c p r)   transitive _ _ = axiom  -- | @transitive@, with the arguments flipped.-transitive' :: Transitive c => c q r -> c p q -> Proof (c p r)+transitive' :: Transitive c => Proof (c q r) -> Proof (c p q) -> Proof (c p r) transitive' = flip transitive  {-| A binary operation @#@ is idempotent if @x # x == x@ for all @x@.@@ -108,15 +103,14 @@  @ -- Define an idempotent binary operation-newtype Union x y = Union Defn+data Union x y instance Idempotent Union @ -} class Idempotent c where   idempotent :: Proof (c p p == p)-  default idempotent :: Defining (c p p) => Proof (c p p == p)   idempotent = axiom-  + {-| A binary operation @#@ is commutative if @x # y == y # x@ for all @x@ and @y@.     The @Commutative c@ typeclass provides a single method,     @commutative :: Proof (c x y == c y x)@.@@ -126,13 +120,12 @@  @ -- Define a commutative binary operation-newtype Union x y = Union Defn+data Union x y instance Commutative Union @ -} class Commutative c where   commutative :: Proof (c p q == c q p)-  default commutative :: Defining (c p q) => Proof (c p q == c q p)   commutative = axiom  {-| A binary operation @#@ is associative if @x # (y # z) == (x # y) # z@ for@@ -145,13 +138,12 @@  @ -- Define an associative binary operation-newtype Union x y = Union Defn+data Union x y instance Associative Union @ -} class Associative c where   associative :: Proof (c p (c q r) == c (c p q) r)-  default associative :: Defining (c p q) => Proof (c p (c q r) == c (c p q) r)   associative = axiom  {-| A binary operation @#@ distributes over @%@ on the left if@@ -165,14 +157,13 @@  @ -- x `Union` (y `Intersect` z) == (x `Union` y) `Intersect` (x `Union` z)-newtype Union     x y = Union     Defn-newtype Intersect x y = Intersect Defn+data Union     x y+data Intersect x y instance DistributiveL Union Intersect @ -} class DistributiveL c c' where   distributiveL :: Proof (c p (c' q r) == c' (c p q) (c p r))-  default distributiveL :: (Defining (c p q), Defining (c' p q)) => Proof (c p (c' q r) == c' (c p q) (c p r))   distributiveL = axiom  {-| A binary operation @#@ distributes over @%@ on the right if@@ -186,14 +177,13 @@  @ -- (x `Intersect` y) `Union` z == (x `Union` z) `Intersect` (y `Union` z)-newtype Union     x y = Union     Defn-newtype Intersect x y = Intersect Defn+data Union     x y+data Intersect x y instance DistributiveR Union Intersect @ -} class DistributiveR c c' where   distributiveR :: Proof (c (c' p q) r == c' (c p r) (c q r))-  default distributiveR :: (Defining (c p q), Defining (c' p q)) => Proof (c (c' p q) r == c' (c p r) (c q r))   distributiveR = axiom  {-| A function @f@ is /injective/ if @f x == f y@ implies @x == y@.@@ -205,13 +195,12 @@  @ -- {x} == {y} implies x == y.-newtype Singleton x = Singleton Defn+data Singleton x instance Injective Singleton @ -} class Injective f where-  elim_inj :: (f x == f y) -> Proof (x == y)-  default elim_inj :: (Defining (f x), Defining (f y)) => (f x == f y) -> Proof (x == y)+  elim_inj :: Proof (f x == f y) -> Proof (x == y)   elim_inj _ = axiom  

@@ -0,0 +1,54 @@+{-# LANGUAGE RankNTypes          #-}+{-# LANGUAGE RoleAnnotations     #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-}++module Logic.Implicit+    ( Fact+    , known+    , note+    , on+    ) where++import           Logic.Proof+import           Theory.Named++import           Unsafe.Coerce++-- | A @Fact p@ is an implicit proof of @p@, propagated by Haskell's constraint solver.+--   @Fact@s can be used to implicitly introduce or propagate proofs. However, there is+--   a small run-time cost associated with using @Fact@s: typeclass dictionaries for+--   @Fact@s are still passed around. In many cases they will be optimized away, but this+--   is not guaranteed.+class Fact p++-- | Recall a known @Fact@ from the implicit context.+known :: Fact p => Proof p+known = axiom++newtype WithFact p t = WithFact (Fact p => t)+type role WithFact nominal nominal++-- | Add a proof to the implicit context.+note :: forall p t. Proof p -> (Fact p => t) -> t+note _ k = unsafeCoerce (WithFact k :: WithFact p t) ()++{-| Apply an implication to a predicate in the implicit context. The @(a ~~ n)@+    parameter is not actually used; it's type is used to help select a specific+    fact from the context.++@+-- A safe 'head' function, using an implicitly-passed safety proof.+head :: Fact (IsCons xs) => ([a] ~~ xs) -> a+head xs = Prelude.head (the xs)++-- Reverse, and a lemma.+reverse :: ([a] ~~ xs) -> ([a] ~~ Reverse xs)+revConsLemma :: Proof (IsCons xs) -> Proof (IsCons (Reverse xs))++-- Implement a safe 'last' function.+last :: Fact (IsCons xs) => ([a] ~~ xs) -> a+last xs = note (revConsLemma `on` xs) $ head (reverse xs)+-}+on :: Fact (p n) => (Proof (p n) -> Proof q) -> (a ~~ n) -> Proof q+on impl _ = impl known

@@ -1,7 +1,5 @@-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE DefaultSignatures     #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE PolyKinds             #-}  {-|   Module      :  Logic.NegClasses@@ -17,10 +15,8 @@   , Antisymmetric(..)   ) where -import Logic.Proof-import Logic.Propositional (Not)-import Theory.Equality-import Theory.Named+import           Logic.Proof+import           Logic.Propositional (Not)  {--------------------------------------------------------   Special properties of predicates and functions@@ -37,12 +33,12 @@ @ -- Define an irreflexive binary relation newtype DifferentColor p q = DifferentColor Defn+type role DifferentColor nominal nominal instance Irreflexive DifferentColor @ -} class Irreflexive r where   irrefl :: Proof (Not (r x x))-  default irrefl :: (Defining (r x x)) => Proof (Not (r x x))   irrefl = axiom  @@ -58,10 +54,10 @@ @ -- Define an antisymmetric binary relation newtype AncestorOf p q = AncestorOf Defn+type role DifferentColor nominal nominal instance Antisymmetric AncestorOf @--}   +-} class Antisymmetric c where-  antisymmetric :: c p q -> Proof (Not (c q p))-  default antisymmetric :: Defining (c p q) => c p q -> Proof (Not (c q p))+  antisymmetric :: Proof (c p q) -> Proof (Not (c q p))   antisymmetric _ = axiom

@@ -1,4 +1,5 @@ {-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds      #-}  {-|   Module      :  Logic.Proof@@ -9,43 +10,35 @@ -}  module Logic.Proof-  ( -- * The `Proof` monad+  ( -- * The `Proof` type     Proof-  , (|.), (|$), (|/), (|\), ($$)-  , given   , axiom, sorry   ) where -import Data.Coerce-import Control.Monad ((>=>))- {---------------------------------------------------  The `Proof` monad+  The `Proof` type --------------------------------------------------} -{-| The @Proof@ monad is used as a domain-specific+{-| The @Proof@ type is used as a domain-specific     language for constructing proofs. A value of type     @Proof p@ represents a proof of the proposition @p@. -    For example, this function constructions a proof of-    "P or Q" from the assumption "P and Q":+    A @Proof@ as an argument to a function represents an+    assumption. For example, this function constructions a proof of "P+    or Q" from the assumption "P and Q": -> and2or :: (p && q) -> Proof (p || q)+> and2or :: Proof (p && q) -> Proof (p || q) >-> and2or pq = do->    p <- and_elimL pq    -- or: "p <- fst <$> and_elim pq"->    or_introL p+> and2or pq = introOrL $ elimAndL pq      If the body of the proof does not match the proposition     you claim to be proving, the compiler will raise a type     error. Here, we accidentally try to use @or_introR@     instead of @or_introL@: -> and2or :: (p && q) -> Proof (p || q)+> and2or :: Proof (p && q) -> Proof (p || q) >-> and2or pq = do->    p <- and_elimL pq->    or_introR p+> and2or pq = introOrR $ elimAndL pq  resulting in the error @@ -53,126 +46,17 @@     • Couldn't match type ‘p’ with ‘q’       ‘p’ is a rigid type variable bound by         the type signature for:-          and2or :: forall p q. (p && q) -> Proof (p || q)+          and2or :: forall p q. Proof (p && q) -> Proof (p || q)        ‘q’ is a rigid type variable bound by         the type signature for:-          and2or :: forall p q. (p && q) -> Proof (p || q)+          and2or :: forall p q. Proof (p && q) -> Proof (p || q)        Expected type: Proof (p || q)         Actual type: Proof (p || p) @ -}-data Proof (pf :: *) = QED--instance Functor Proof where-  fmap _ = const QED -- modus ponens (external?)--instance Applicative Proof where-  pure = const QED -- axiom-  pf1 <*> pf2 = QED -- modus ponens (internal?)--instance Monad Proof where-  pf >>= f = QED--{-| This operator is just a specialization of @(>>=)@, but-    can be used to create nicely delineated chains of-    derivations within a larger proof. The first statement-    in the chain should produce a formula; @(|$)@ then-    pipes this formula into the following derivation rule.--> and2or :: (p && q) -> Proof (p || q)->-> and2or pq =  and_elimL pq->           |$ or_introL--}--(|$) :: Proof p -> (p -> Proof q) -> Proof q-(|$) = (>>=)--infixr 7 |$----(|-) :: ((p -> Proof r) -> Proof r) -> (p -> Proof r) -> Proof r--{-| This operator is used to create nicely delineated chains of-    derivations within a larger proof. If X and Y are two-    deduction rules, each with a single premise and a single-    conclusion, and the premise of Y matches the conclusion of X,-    then @X |. Y@ represents the composition of the two-    deduction rules.--> and2or :: (p && q) -> Proof (p || q)->-> and2or =  and_elimL->        |. or_introL--}--(|.) :: (p -> Proof q) -> (q -> Proof r) -> p -> Proof r-(|.) = (>=>)--infixr 9 |.--{-| The @(|/)@ operator is used to feed the remainder of the proof in-    as a premise of the first argument.--    A common use-case is with the @Or@-elimination rules @or_elimL@ and-    @or_elimR@, when one case is trivial. For example, suppose we wanted-    to prove that @R && (P or (Q and (Q implies P)))@ implies @P@:--@-my_proof :: r && (p || (q && (q --> p))) -> Proof p--my_proof =-  do  and_elimR          -- Forget the irrelevant r.-   |. or_elimL given     -- The first case of the || is immediate;-   |/ and_elim           -- The rest of the proof handles the second case,-   |. uncurry impl_elim  --   by unpacking the && and feeding the q into-                         --   the implication (q --> p).-@--    The rising @/@ is meant to suggest the bottom half of the proof getting-    plugged in to the Or-elimination line.--}-(|/) :: (p -> (q -> Proof r) -> Proof r) -> (q -> Proof r) -> p -> Proof r-(|/) = flip-infixr 9 |/--{-| The @(|\\)@ operator is used to take the subproof so far and feed it-    into a rule that is expecting a subproof as a premise.--    A common use-case is with the @Not@-introduction rule @not_intro@,-    which has a type that fits the second argument of @(|\\)@. By way-    of example, here is a proof that "P implies Q" along with "Not Q"-    implies "Not P".--@-my_proof :: (p --> q) -> (Not p --> r) -> Not q -> Proof r--my_proof impl1 impl2 q' =-  do  modus_ponens impl1   -- This line, composed with the next,-   |. contradicts' q'      --   form a proof of FALSE from p.-   |\\ not_intro            -- Closing the subproof above, conclude not-p.-   |. modus_ponens impl2   -- Now apply the second implication to conclude r.-@--    The falling @\\@ is meant to suggest the upper half of the proof-    being closed off by the Not-introduction line.--}-(|\) :: (p -> Proof q) -> ((p -> Proof q) -> Proof r) -> Proof r-(|\) = flip ($)-infixl 8 |\---- | Take a proof of @p@ and feed it in as the first premise of---   an argument that expects a @p@ and a @q@.-($$) :: (p -> q -> Proof r) -> Proof p -> (q -> Proof r)-(f $$ pp) q = do { p <- pp; f p q }---- | @given@ creates a proof of P, given P as---   an assumption.------   @given@ is just a specialization of @pure@ / @return@.-given :: p -> Proof p-given _ = QED+data Proof (pf :: k) = QED  -- | @sorry@ can be used to provide a "proof" of --   any proposition, by simply assering it as@@ -183,6 +67,7 @@ -- _Completed proofs should never use @sorry@!_ sorry :: Proof p sorry = QED+{-# WARNING sorry "Completed proofs should never use sorry!" #-}  {-| @axiom@, like @sorry@, provides a "proof" of any     proposition. Unlike @sorry@, which is used to indicate@@ -194,10 +79,9 @@ data Reverse xs = Reverse Defn data Length  xs = Length  Defn -rev_length_lemma :: Proof (Length (Reverse xs) == Length xs)-rev_length_lemma = axiom+revLengthLemma :: Proof (Length (Reverse xs) == Length xs)+revLengthLemma = axiom @ -} axiom :: Proof p axiom = QED-

@@ -1,15 +1,8 @@-{-# LANGUAGE TypeOperators         #-}-{-# LANGUAGE ScopedTypeVariables   #-}-{-# LANGUAGE RankNTypes            #-}-{-# LANGUAGE KindSignatures        #-}-{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE ExplicitNamespaces    #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE DataKinds             #-}-{-# LANGUAGE DefaultSignatures     #-}-{-# LANGUAGE ConstraintKinds       #-}-{-# LANGUAGE FlexibleContexts      #-}-{-# LANGUAGE UndecidableSuperClasses #-}-{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE RankNTypes            #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE PolyKinds             #-}  {-|   Module      :  Logic.Propositional@@ -24,7 +17,7 @@    -- ** Logical symbols     TRUE, FALSE-  +   , And,     type (&&), type (∧), type (/\)   , Or,      type (||), type (∨), type (\/)   , Implies, type (-->)@@ -42,92 +35,97 @@    -- | Introduction rules give the elementary building blocks   --   for creating a formula from simpler ones.-  , and_intro-  , or_introL-  , or_introR-  , impl_intro-  , not_intro+  , introAnd+  , introAnd'++  , introOrL+  , introOrR++  , introImpl+  , introNot+   , contrapositive   , contradicts   , contradicts'-  , univ_intro-  , ex_intro+  , introUniv+  , introEx    -- *** Elimination rules    -- | Elimination rules give the elementary building blocks for   --   decomposing a complex formula into simpler ones.-  , and_elimL-  , and_elimR-  , and_elim-  , or_elim-  , or_elimL-  , or_elimR-  , impl_elim-  , modus_ponens-  , modus_tollens+  , elimAndL+  , elimAndR++  , elimOr+  , elimOrL+  , elimOrR++  , elimImpl+  , modusPonens+  , modusTollens   , absurd-  , univ_elim-  , ex_elim+  , elimUniv+  , elimEx    -- *** Classical logic and the Law of the Excluded Middle   , Classical   , classically   , lem   , contradiction-  , not_not_elim+  , elimNot+  , elimNotNot -   -- *** Mapping over conjunctions and disjunctions-  , and_mapL-  , and_mapR-  , and_map+  -- *** Mapping over conjunctions and disjunctions. -  , or_mapL-  , or_mapR-  , or_map+  -- | These function names mimic the ones for+  -- (@Functor@/@Bifunctor@/@Profunctor@).+  , firstAnd+  , secondAnd+  , bimapAnd -  , impl_mapL-  , impl_mapR-  , impl_map+  , firstOr+  , secondOr+  , bimapOr -  , not_map+  , lmapImpl+  , rmapImpl+  , dimapImpl +  , mapNot+   ) where -import Data.Arguments-import Data.Refined-import Data.The import Logic.Classes import Logic.Proof-import Theory.Named  {--------------------------------------------------   Logical constants --------------------------------------------------}  -- | The constant "true".-newtype TRUE  = TRUE Defn+data TRUE  -- | The constant "false".-newtype FALSE = FALSE Defn+data FALSE  -- | The conjunction of @p@ and @q@.-newtype And p q = And Defn+data And p q  -- | The disjunction of @p@ and @q@.-newtype Or p q  = Or  Defn+data Or p q  -- | The negation of @p@.-newtype Not p   = Not Defn+data Not p  -- | The implication "@p@ implies @q@".-newtype Implies p q = Implies Defn+data Implies p q  -- | Existential quantifiation.-newtype Exists x p = Exists Defn+data Exists x p  -- | Universal quantification.-newtype ForAll x p = ForAll Defn+data ForAll x p  -- | An infix alias for @Or@. type p || q   = p `Or` q@@ -168,54 +166,48 @@ --------------------------------------------------}  -- | Apply a derivation to the left side of a conjunction.-and_mapL :: (p -> Proof p') -> (p && q) -> Proof (p' && q)-and_mapL impl conj = do-  (lhs, rhs) <- and_elim conj-  lhs' <- impl lhs-  and_intro lhs' rhs+firstAnd :: (Proof p -> Proof p') -> Proof (p && q) -> Proof (p' && q)+firstAnd = flip bimapAnd id  -- | Apply a derivation to the right side of a conjunction.-and_mapR :: (q -> Proof q') -> (p && q) -> Proof (p && q')-and_mapR impl conj = do-  (lhs, rhs) <- and_elim conj-  rhs' <- impl rhs-  and_intro lhs rhs'+secondAnd :: (Proof q -> Proof q') -> Proof (p && q) -> Proof (p && q')+secondAnd = bimapAnd id  -- | Apply derivations to the left and right sides of a conjunction.-and_map :: (p -> Proof p') -> (q -> Proof q') -> (p && q) -> Proof (p' && q')-and_map implP implQ conj = do-  (lhs, rhs) <- and_elim conj-  lhs' <- implP lhs-  rhs' <- implQ rhs-  and_intro lhs' rhs'+bimapAnd :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p && q) -> Proof (p' && q')+bimapAnd implP implQ conj = let+  (lhs, rhs) = elimAnd conj+  lhs' = implP lhs+  rhs' = implQ rhs+  in introAnd lhs' rhs'  -- | Apply a derivation to the left side of a disjunction.-or_mapL :: (p -> Proof p') -> (p || q) -> Proof (p' || q)-or_mapL impl = or_elim (impl |. or_introL) or_introR+firstOr :: (Proof p -> Proof p') -> Proof (p || q) -> Proof (p' || q)+firstOr = flip bimapOr id  -- | Apply a derivation to the right side of a disjunction.-or_mapR :: (q -> Proof q') -> (p || q) -> Proof (p || q')-or_mapR impl = or_elim or_introL (impl |. or_introR)+secondOr :: (Proof q -> Proof q') -> Proof (p || q) -> Proof (p || q')+secondOr = bimapOr id  -- | Apply derivations to the left and right sides of a disjunction.-or_map :: (p -> Proof p') -> (q -> Proof q') -> (p || q) -> Proof (p' || q')-or_map implP implQ = or_elim (implP |. or_introL) (implQ |. or_introR)+bimapOr :: (Proof p -> Proof p') -> (Proof q -> Proof q') -> Proof (p || q) -> Proof (p' || q')+bimapOr implP implQ = elimOr (introOrL . implP) (introOrR . implQ)  -- | Apply a derivation to the left side of an implication.-impl_mapL :: (p' -> Proof p) -> (p --> q) -> Proof (p' --> q)-impl_mapL derv impl = impl_intro (derv |. modus_ponens impl)+lmapImpl :: (Proof p' -> Proof p) -> Proof (p --> q) -> Proof (p' --> q)+lmapImpl = flip dimapImpl id  -- | Apply a derivation to the right side of an implication.-impl_mapR :: (q -> Proof q') -> (p --> q) -> Proof (p --> q')-impl_mapR derv impl = impl_intro (modus_ponens impl |. derv)+rmapImpl :: (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p --> q')+rmapImpl = dimapImpl id  -- | Apply derivations to the left and right sides of an implication.-impl_map :: (p' -> Proof p) -> (q -> Proof q') -> (p --> q) -> Proof (p' --> q')-impl_map dervL dervR impl = impl_intro (dervL |. modus_ponens impl |. dervR)+dimapImpl :: (Proof p' -> Proof p) -> (Proof q -> Proof q') -> Proof (p --> q) -> Proof (p' --> q')+dimapImpl dervL dervR impl = introImpl (dervR . modusPonens impl . dervL)  -- | Apply a derivation inside of a negation.-not_map :: (p' -> Proof p) -> Not p -> Proof (Not p')-not_map impl notP = not_intro (impl |. contradicts' notP |. absurd)+mapNot :: (Proof p' -> Proof p) -> Proof (Not p) -> Proof (Not p')+mapNot impl notP = introNot (absurd . contradicts' notP . impl)  {--------------------------------------------------   Tautologies@@ -234,100 +226,97 @@ --------------------------------------------------}  -- | Prove "P and Q" from P and Q.-and_intro :: p -> q -> Proof (p && q)-and_intro _ _ = axiom+introAnd :: Proof p -> Proof q -> Proof (p && q)+introAnd _ _ = axiom  -- | Prove "P and Q" from Q and P.-and_intro' :: q -> p -> Proof (p && q)-and_intro' _ _ = axiom+introAnd' :: Proof q -> Proof p -> Proof (p && q)+introAnd' _ _ = axiom  -- | Prove "P or Q" from  P.-or_introL :: p -> Proof (p || q)-or_introL _ = axiom+introOrL :: Proof p -> Proof (p || q)+introOrL _ = axiom  -- | Prove "P or Q" from Q.-or_introR :: q -> Proof (p || q)-or_introR _ = axiom+introOrR :: Proof q -> Proof (p || q)+introOrR _ = axiom  -- | Prove "P implies Q" by demonstrating that, --   from the assumption P, you can prove Q.-impl_intro :: (p -> Proof q) -> Proof (p --> q)-impl_intro _ = axiom+introImpl :: (Proof p -> Proof q) -> Proof (p --> q)+introImpl _ = axiom  -- | Prove "not P" by demonstrating that, --   from the assumption P, you can derive a false conclusion.-not_intro :: (p -> Proof FALSE) -> Proof (Not p)-not_intro _ = axiom+introNot :: (Proof p -> Proof FALSE) -> Proof (Not p)+introNot _ = axiom --- | `contrapositive` is an alias for `not_intro`, with+-- | `contrapositive` is an alias for `introNot`, with --   a somewhat more suggestive name. Not-introduction --   corresponds to the proof technique "proof by contrapositive".-contrapositive :: (p -> Proof FALSE) -> Proof (Not p)-contrapositive = not_intro+contrapositive :: (Proof p -> Proof FALSE) -> Proof (Not p)+contrapositive = introNot  -- | Prove a contradiction from "P" and "not P".-contradicts :: p -> Not p -> Proof FALSE+contradicts :: Proof p -> Proof (Not p) -> Proof FALSE contradicts _ _ = axiom  -- | `contradicts'` is `contradicts` with the arguments --   flipped. It is useful when you want to partially --   apply `contradicts` to a negation.-contradicts' :: Not p -> p -> Proof FALSE+contradicts' :: Proof (Not p) -> Proof p -> Proof FALSE contradicts' = flip contradicts  -- | Prove "For all x, P(x)" from a proof of P(*c*) with --   *c* indeterminate.-univ_intro :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))-univ_intro _ = axiom+introUniv :: (forall c. Proof (p c)) -> Proof (ForAll x (p x))+introUniv _ = axiom  -- | Prove "There exists an x such that P(x)" from a specific --   instance of P(c).-ex_intro :: p c -> Proof (Exists x (p x))-ex_intro _ = axiom+introEx :: Proof (p c) -> Proof (Exists x (p x))+introEx _ = axiom  {--------------------------------------------------   Elimination rules --------------------------------------------------}  -- | From the assumption "P and Q", produce a proof of P.-and_elimL :: p && q -> Proof p-and_elimL _ = axiom+elimAndL :: Proof (p && q) -> Proof p+elimAndL _ = axiom  -- | From the assumption "P and Q", produce a proof of Q.-and_elimR :: p && q -> Proof q-and_elimR _ = axiom+elimAndR :: Proof (p && q) -> Proof q+elimAndR _ = axiom  -- | From the assumption "P and Q", produce both a proof --   of P, and a proof of Q.-and_elim :: p && q -> Proof (p, q)-and_elim c = (,) <$> and_elimL c <*> and_elimR c-  -{-| If you have a proof of R from P, and a proof of-     R from Q, then convert "P or Q" into a proof of R.--}-or_elim :: (p -> Proof r) -> (q -> Proof r) -> (p || q) -> Proof r-or_elim _ _ _ = axiom+elimAnd :: Proof (p && q) -> (Proof p, Proof q)+elimAnd c = (elimAndL c, elimAndR c) -{-| Eliminate the first alternative in a conjunction.--}-or_elimL :: (p -> Proof r) -> (p || q) -> (q -> Proof r) -> Proof r-or_elimL case1 disj case2 = or_elim case1 case2 disj+-- | If you have a proof of R from P, and a proof of R from Q, then+--   convert "P or Q" into a proof of R.+elimOr :: (Proof p -> Proof r) -> (Proof q -> Proof r) -> Proof (p || q) -> Proof r+elimOr _ _ _ = axiom -{-| Eliminate the second alternative in a conjunction.--}-or_elimR :: (q -> Proof r) -> (p || q) -> (p -> Proof r) -> Proof r-or_elimR case2 disj case1 = or_elim case1 case2 disj+-- | Eliminate the first alternative in a conjunction.+elimOrL :: (Proof p -> Proof r) -> Proof (p || q) -> (Proof q -> Proof r) -> Proof r+elimOrL case1 disj case2 = elimOr case1 case2 disj +-- | Eliminate the second alternative in a conjunction.+elimOrR :: (Proof q -> Proof r) -> Proof (p || q) -> (Proof p -> Proof r) -> Proof r+elimOrR case2 disj case1 = elimOr case1 case2 disj+ -- | Given "P imples Q" and P, produce a proof of Q. --   (modus ponens)-impl_elim :: p -> (p --> q) -> Proof q-impl_elim _ _ = axiom+elimImpl :: Proof p -> Proof (p --> q) -> Proof q+elimImpl _ _ = axiom --- | @modus_ponens@ is just @impl_elim@ with the arguments+-- | @modusPonens@ is just `elimImpl` with the arguments --   flipped. In this form, it is useful for partially --   applying an implication.-modus_ponens :: (p --> q) -> p -> Proof q-modus_ponens = flip impl_elim+modusPonens :: Proof (p --> q) -> Proof p -> Proof q+modusPonens = flip elimImpl  {-| Modus tollens lets you prove "Not P" from     "P implies Q" and "Not Q".@@ -339,46 +328,39 @@                                   -----         (assumption)                         p --> q,    p                        ---------------------    (modus ponens)-                 q,           Not q    +               Not q,            q               --------------------------        (contradicts')                       FALSE           ------------------------------------- (not-intro)                              Not p @ -We can encode this proof tree more-or-less directly as a @Proof@-to implement @modus_tollens@:+We can encode this proof tree as a @Proof@ to implement+@modus_tollens@:  @-modus_tollens :: (p --> q) -> Not q -> Proof (Not p)--modus_tollens impl q' =-  do  modus_ponens impl-   |. contradicts' q'-   |\\ not_intro+modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)+modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p) @ -} -modus_tollens :: (p --> q) -> Not q -> Proof (Not p)-modus_tollens impl q' =-  do  modus_ponens impl-   |. contradicts' q'-   |\ not_intro+modusTollens :: Proof (p --> q) -> Proof (Not q) -> Proof (Not p)+modusTollens impl q' = introNot $ \p -> contradicts' q' (modusPonens impl p)  -- | From a falsity, prove anything.-absurd :: FALSE -> Proof p+absurd :: Proof FALSE -> Proof p absurd _ = axiom  -- | Given "For all x, P(x)" and any c, prove the proposition --   "P(c)".-univ_elim :: ForAll x (p x) -> Proof (p c)-univ_elim _ = axiom+elimUniv :: Proof (ForAll x (p x)) -> Proof (p c)+elimUniv _ = axiom  -- | Given a proof of Q from P(c) with c generic, and the --   statement "There exists an x such that P(x)", produce --   a proof of Q.-ex_elim :: (forall c. p c -> Proof q) -> Exists x (p x) -> Proof q-ex_elim _ _ = axiom+elimEx :: (forall c. Proof (p c) -> Proof q) -> Proof (Exists x (p x)) -> Proof q+elimEx _ _ = axiom   {--------------------------------------------------@@ -409,7 +391,7 @@ {-| Proof by contradiction: this proof technique allows      you to prove P by showing that, from "Not P", you      can prove a falsehood.-  +      Proof by contradiction is not a theorem of      constructive logic, so it requires the @Classical@      constraint. But note that the similar technique@@ -417,8 +399,8 @@      valid in constructive logic! For comparison, the two types are:  @-contradiction  :: Classical => (Not p -> Proof FALSE) -> p-not_intro      ::              (p     -> Proof FALSE) -> Not p+contradiction  :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p+introNot       ::              (Proof      p  -> Proof FALSE) -> Proof (Not p) @  The derivation of proof by contradiction from the law of the excluded@@ -429,32 +411,28 @@ from which the desired conclusion is derived.  @-contradiction impl =-  do  lem             -- introduce p || Not p-   |$ or_elimL given  -- dispatch the first, straightforward case-   |/ impl            -- Now we're on the second case. Apply the implication..-   |. absurd          -- .. and, from falsity, conclude p.+contradiction impl = elimOr id (absurd . impl) lem @ -}-contradiction :: forall p. Classical => (Not p -> Proof FALSE) -> Proof p-contradiction impl =-  do  lem-   |$ or_elimL given-   |/ impl-   |. absurd-  +contradiction :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p+contradiction impl = elimOr id (absurd . impl) lem++-- | Alias for 'contradiction', to complete the patterns.+elimNot :: Classical => (Proof (Not p) -> Proof FALSE) -> Proof p+elimNot = contradiction+ {-| Double-negation elimination. This is another non-constructive     proof technique, so it requires the @Classical@ constraint.      The derivation of double-negation elimination follows from     proof by contradiction, since "Not (Not p)" contradicts "Not p". @-not_not_elim p'' = contradiction (contradicts' p'')+elimNotNot p'' = contradiction (contradicts' p'') @ -} -not_not_elim :: Classical => Not (Not p) -> Proof p-not_not_elim p'' = contradiction (contradicts' p'')+elimNotNot :: Classical => Proof (Not (Not p)) -> Proof p+elimNotNot p'' = contradiction (contradicts' p'')  {--------------------------------------------------   Algebraic properties@@ -475,4 +453,3 @@ instance DistributiveL And Or instance DistributiveL Or  And instance DistributiveL Or  Or-

@@ -1,10 +1,12 @@ {-# LANGUAGE TypeOperators         #-} {-# LANGUAGE RankNTypes            #-} {-# LANGUAGE DataKinds             #-}+{-# LANGUAGE PolyKinds             #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE TypeFamilies          #-} {-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE RoleAnnotations       #-}  {-|   Module      :  Theory.Equality@@ -49,6 +51,7 @@ --   Given an equality, you are then able to substitute one side of the equality --   for the other, anywhere you please. newtype Equals x y = Equals Defn+type role Equals nominal nominal  -- | An infix alias for 'Equals'. type x == y = x `Equals` y@@ -76,25 +79,25 @@  -- | Apply a function to both sides of an equality. apply :: forall f n x x'. (Argument f n, GetArg f n ~ x)-    => Arg n -> (x == x') -> Proof (f == SetArg f n x')+    => Arg n -> Proof (x == x') -> Proof (f == SetArg f n x') apply _ _ = axiom --- | Given a formula and an equality over ones of its arguments,+-- | Given a formula and an equality over one of its arguments, --   replace the left-hand side of the equality with the right-hand side. substitute :: (Argument f n, GetArg f n ~ x)-    => Arg n -> (x == x') -> f -> Proof (SetArg f n x')+    => Arg n -> Proof (x == x') -> f -> Proof (SetArg f n x') substitute _ _ _ = axiom  -- | Substitute @x'@ for @x@ under the function @f@, on the left-hand side --   of an equality. substituteL :: (Argument f n, GetArg f n ~ x)-    => Arg n -> (x == x') -> (f == g) -> Proof (SetArg f n x' == g)+    => Arg n -> Proof (x == x') -> Proof (f == g) -> Proof (SetArg f n x' == g) substituteL _ _ _ = axiom  -- | Substitute @x'@ for @x@ under the function @f@, on the right-hand side --   of an equality. substituteR :: (Argument f n, GetArg f n ~ x)-    => Arg n -> (x == x') -> (g == f) -> Proof (g == SetArg f n x')+    => Arg n -> Proof (x == x') -> Proof (g == f) -> Proof (g == SetArg f n x') substituteR _ _ _ = axiom  {--------------------------------------------------

@@ -0,0 +1,151 @@+{-# LANGUAGE FlexibleContexts    #-}+{-# LANGUAGE GADTs               #-}+{-# LANGUAGE LambdaCase          #-}+{-# LANGUAGE PatternSynonyms     #-}+{-# LANGUAGE RoleAnnotations     #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE TypeOperators       #-}+{-# LANGUAGE ViewPatterns        #-}++module Theory.Lists+    ( -- * Basic functions on lists+      head, tail, cons, nil+      -- ** Names for parts of a list+    , Head, Tail+      -- ** Names for basic list operations+    , Cons', Nil'+      -- * Reasoning about lists+      -- ** Predicates about list shapes+    , IsList, IsCons, IsNil+      -- ** Axioms about list shapes+    , consIsList, nilIsList, listIsList+    , listShapes, consIsCons, headOfCons, tailOfCons+      -- ** Induction principle+    , listInduction+      -- * Pattern-matching on lists+      -- ** Decompositions that use explicit evidence-passing+    , classify, ListCase (..)+      -- *** Pattern synonyms+    , pattern IsCons, pattern IsNil+      -- ** Decompositions that use implicit evidence-passing+    , classify', ListCase' (..)+      -- *** Pattern synonyms+    , pattern Cons, pattern Nil+    ) where++import           Prelude             hiding (cons, head, reverse, tail)+import qualified Prelude++import           Data.The+import           Logic.Implicit+import           Logic.Proof+import           Logic.Propositional+import           Theory.Equality+import           Theory.Named++-- | Predicates about the possible shapes of lists.+data IsList xs+data IsCons xs+data IsNil  xs++-- | Names for the parts of a list.+newtype Head xs = Head Defn+type role Head nominal+newtype Tail xs = Tail Defn+type role Tail nominal++-- | Possible shapes of a list, along with evidence that the list+--   has the given shape.+data ListCase a xs+  = IsCons_ (Proof (IsCons xs)) (a ~~ Head xs) ([a] ~~ Tail xs)+  | IsNil_  (Proof (IsNil  xs))++-- | Classify a named list by shape, producing evidence that the+--   list matches the corresponding case.+classify :: ([a] ~~ xs) -> ListCase a xs+classify xs = case the xs of+    (h:t) -> IsCons_ axiom (defn h) (defn t)+    []    -> IsNil_  axiom++pattern IsCons :: Proof (IsCons xs) -> (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ([a] ~~ xs)+pattern IsCons proof hd tl <- (classify -> IsCons_ proof hd tl)++pattern IsNil :: Proof (IsNil xs) -> ([a] ~~ xs)+pattern IsNil proof <- (classify -> IsNil_ proof)++-- | A variation on @ListCase@ that passes the shape facts implicitly. Pattern-matching on a+--   constructor of @ListCase'@ will bring a shape proof into the implicit context.+data ListCase' a xs where+    Cons_ :: Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ListCase' a xs+    Nil_  :: Fact (IsNil  xs) => ListCase' a xs++-- | Classify a named list by shape, producing /implicit/ evidence that the+--   list matches the corresponding case.+classify' :: forall a xs. ([a] ~~ xs) -> ListCase' a xs+classify' xs = case the xs of+    (h:t) -> note (axiom :: Proof (IsCons xs)) (Cons_ (defn h) (defn t))+    []    -> note (axiom :: Proof (IsNil  xs))  Nil_++pattern Cons :: () => Fact (IsCons xs) => (a ~~ Head xs) -> ([a] ~~ Tail xs) -> ([a] ~~ xs)+pattern Cons hd tl <- (classify' -> Cons_ hd tl)++pattern Nil :: () => Fact (IsNil xs) => ([a] ~~ xs)+pattern Nil <- (classify' -> Nil_)++-- | Extract the first element from a non-empty list.+head :: Fact (IsCons xs) => ([a] ~~ xs) -> (a ~~ Head xs)+head (The xs) = defn (Prelude.head xs)++-- | Extract all but the first element from a non-empty list.+tail :: Fact (IsCons xs) => ([a] ~~ xs) -> ([a] ~~ Tail xs)+tail (The xs) = defn (Prelude.tail xs)++-- | Construct a list from an element and another list.+cons :: (a ~~ x) -> ([a] ~~ xs) -> ([a] ~~ Cons' x xs)+cons (The x) (The xs) = defn (x:xs)++-- | The empty list, named @Nil'@.+nil :: ([a] ~~ Nil')+nil = defn []++-- | A name for referring to the result of a @cons@ operation.+newtype Cons' x xs = Cons' Defn+type role Cons' nominal nominal++-- | A name for referring to the empty list.+newtype Nil' = Nil' Defn++-- | Axiom: The @head@ of @cons x y@ is @x@.+headOfCons :: Proof (Head (Cons' x xs) == x)+headOfCons = axiom++-- | Axiom: The @tail@ of @cons x y@ is @y@.+tailOfCons :: Proof (Tail (Cons' x xs) == xs)+tailOfCons = axiom++-- | Axiom: The result of @cons x y@ satisfies @IsCons@.+consIsCons :: Proof (IsCons (Cons' x xs))+consIsCons = axiom++-- | Axiom: The empty list satisfies @IsNil@.+nilIsNil :: Proof (IsNil Nil')+nilIsNil = axiom++-- | Axiom: a list @xs@ satisfies exactly one of @IsCons xs@ or @IsNil xs@.+listShapes :: Proof (IsList xs) -> Proof ( (IsNil xs && Not (IsCons xs)) || (IsCons xs && Not (IsNil xs)) )+listShapes _ = axiom++-- | Induction principle: If a predicate @P@ is true for the empty list, and+--   @P@ is true for a list whenever it is true for the tail of the list,+--   then @P@ is true.+listInduction :: Proof (IsList xs) -> Proof (p Nil') -> Proof (ForAll ys ((IsList ys && p (Tail ys)) --> p ys)) -> Proof (p xs)+listInduction _ _ _ = axiom++consIsList :: Proof (IsCons xs) -> Proof (IsList xs)+consIsList _ = axiom++nilIsList :: Proof (IsNil xs) -> Proof (IsList xs)+nilIsList _ = axiom++listIsList :: ([a] ~~ xs) -> Proof (IsList xs)+listIsList _ = axiom

@@ -4,6 +4,8 @@ {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-} {-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE RoleAnnotations       #-}  {-|   Module      :  Theory.Named@@ -36,6 +38,7 @@ --   representation as a value of type @a@, with a --   phantom "name" attached. newtype Named name a = Named a+type role Named nominal nominal  -- | An infix alias for 'Named'. type a ~~ name = Named name a@@ -63,13 +66,23 @@ {-| Library authors can introduce new names in a controlled way     by creating @newtype@ wrappers of @Defn@. The constructor of     the @newtype@ should *not* be exported, so that the library-    can retain control of how the name is introduced.+    can retain control of how the name is introduced. If a newtype+    wrapper of @Defn@ contains phantom parameters, these parameters+    should be given the @nominal@ type role; otherwise, library users+    may be able to use coercions to manipulate library-specific names+    in a manner not blessed by the library author.  @ newtype Bob = Bob Defn  bob :: Int ~~ Bob bob = defn 42++newtype FooOf name = FooOf Defn+type role FooOf nominal -- disallow coerce :: FooOf name1 -> FooOf name2++fooOf :: (Int ~~ name) -> (Int ~~ FooOf name)+fooOf x = defn (the x) @ -} data Defn = Defn