-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | Reason about invariants and preconditions with ghosts of departed proofs.
--   
--   Reason about invariants and preconditions with ghosts of departed
--   proofs. The GDP library implements building blocks for creating and
--   working with APIs that may carry intricate preconditions for proper
--   use. As a library author, you can use <a>gdp</a> to encode your API's
--   preconditions and invariants, so that they will be statically checked
--   at compile-time. As a library user, you can use the <a>gdp</a>
--   deduction rules to codify your proofs that you are using the library
--   correctly.
@package gdp
@version 0.0.0.2


module Data.Arguments

-- | Get or modify a type within a larger type. 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 family GetArg f n :: k1;
    type family SetArg f n x :: k1;
}

-- | Position: the left-hand side of a type.
data LHS

-- | Position: the right-hand side of a type.
data RHS

-- | A specialized proxy for arguments.
data Arg n
Arg :: Arg n

-- | Inhabitant of the argument proxy.
arg :: Arg n
instance Data.Arguments.Argument (Data.Either.Either a b) Data.Arguments.RHS
instance Data.Arguments.Argument (Data.Either.Either a b) Data.Arguments.LHS


module Data.The

-- | A class for extracing "the" underlying value. <a>the</a> should
--   ideally be a coercion from some <tt>newtype</tt> wrap of <tt>a</tt>
--   back to <tt>a</tt>.
--   
--   For this common use case, in the module where <tt>newtype New a = New
--   a</tt> is defined, an instance of <tt>The</tt> can be created with an
--   empty definition:
--   
--   <pre>
--   newtype New a = New a
--   instance The (New a) a
--   </pre>
class The d a | d -> a
the :: The d a => d -> a
the :: (The d a, Coercible d a) => d -> a

-- | A view pattern for discarding the wrapper around a value.
--   
--   <pre>
--   f (The x) = expression x
--   </pre>
--   
--   is equivalent to
--   
--   <pre>
--   f x = let x' = the x in expression x'
--   </pre>


module Logic.Proof

-- | The <tt>Proof</tt> monad is used as a domain-specific language for
--   constructing proofs. A value of type <tt>Proof p</tt> represents a
--   proof of the proposition <tt>p</tt>.
--   
--   For example, this function constructions a proof of "P or Q" from the
--   assumption "P and Q":
--   
--   <pre>
--   and2or :: (p &amp;&amp; q) -&gt; Proof (p || q)
--   
--   and2or pq = do
--      p &lt;- and_elimL pq    -- or: "p &lt;- fst &lt;$&gt; and_elim pq"
--      or_introL p
--   </pre>
--   
--   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 <tt>or_introR</tt> instead of
--   <tt>or_introL</tt>:
--   
--   <pre>
--   and2or :: (p &amp;&amp; q) -&gt; Proof (p || q)
--   
--   and2or pq = do
--      p &lt;- and_elimL pq
--      or_introR p
--   </pre>
--   
--   resulting in the error
--   
--   <pre>
--   • Couldn't match type ‘p’ with ‘q’
--     ‘p’ is a rigid type variable bound by
--       the type signature for:
--         and2or :: forall p q. (p &amp;&amp; q) -&gt; Proof (p || q)
--   
--     ‘q’ is a rigid type variable bound by
--       the type signature for:
--         and2or :: forall p q. (p &amp;&amp; q) -&gt; Proof (p || q)
--   
--     Expected type: Proof (p || q)
--       Actual type: Proof (p || p)
--   </pre>
data Proof (pf :: *)

-- | 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 <tt>X |. Y</tt> represents the
--   composition of the two deduction rules.
--   
--   <pre>
--   and2or :: (p &amp;&amp; q) -&gt; Proof (p || q)
--   
--   and2or =  and_elimL
--          |. or_introL
--   </pre>
(|.) :: (p -> Proof q) -> (q -> Proof r) -> p -> Proof r
infixr 9 |.

-- | This operator is just a specialization of <tt>(&gt;&gt;=)</tt>, 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; <tt>(|$)</tt> then pipes this formula into the following
--   derivation rule.
--   
--   <pre>
--   and2or :: (p &amp;&amp; q) -&gt; Proof (p || q)
--   
--   and2or pq =  and_elimL pq
--             |$ or_introL
--   </pre>
(|$) :: Proof p -> (p -> Proof q) -> Proof q
infixr 7 |$

-- | The <tt>(|/)</tt> 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 <tt>Or</tt>-elimination rules
--   <tt>or_elimL</tt> and <tt>or_elimR</tt>, when one case is trivial. For
--   example, suppose we wanted to prove that <tt>R &amp;&amp; (P or (Q and
--   (Q implies P)))</tt> implies <tt>P</tt>:
--   
--   <pre>
--   my_proof :: r &amp;&amp; (p || (q &amp;&amp; (q --&gt; p))) -&gt; 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 &amp;&amp; and feeding the q into
--                            --   the implication (q --&gt; p).
--   </pre>
--   
--   The rising <tt>/</tt> 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
infixr 9 |/

-- | The <tt>(|\)</tt> 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 <tt>Not</tt>-introduction rule
--   <tt>not_intro</tt>, which has a type that fits the second argument of
--   <tt>(|\)</tt>. By way of example, here is a proof that "P implies Q"
--   along with "Not Q" implies "Not P".
--   
--   <pre>
--   my_proof :: (p --&gt; q) -&gt; (Not p --&gt; r) -&gt; Not q -&gt; 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.
--   </pre>
--   
--   The falling <tt>\</tt> 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
infixl 8 |\

-- | Take a proof of <tt>p</tt> and feed it in as the first premise of an
--   argument that expects a <tt>p</tt> and a <tt>q</tt>.
($$) :: (p -> q -> Proof r) -> Proof p -> (q -> Proof r)

-- | <tt>given</tt> creates a proof of P, given P as an assumption.
--   
--   <tt>given</tt> is just a specialization of <tt>pure</tt> /
--   <tt>return</tt>.
given :: p -> Proof p

-- | <tt>axiom</tt>, like <tt>sorry</tt>, provides a "proof" of any
--   proposition. Unlike <tt>sorry</tt>, which is used to indicate that a
--   proof is still in progress, <tt>axiom</tt> is meant to be used by
--   library authors to assert axioms about how their library works. For
--   example:
--   
--   <pre>
--   data Reverse xs = Reverse Defn
--   data Length  xs = Length  Defn
--   
--   rev_length_lemma :: Proof (Length (Reverse xs) == Length xs)
--   rev_length_lemma = axiom
--   </pre>
axiom :: Proof p

-- | <tt>sorry</tt> can be used to provide a "proof" of any proposition, by
--   simply assering it as true. This is useful for stubbing out portions
--   of a proof as you work on it, but subverts the entire proof system.
--   
--   _Completed proofs should never use <tt>sorry</tt>!_
sorry :: Proof p
instance GHC.Base.Functor Logic.Proof.Proof
instance GHC.Base.Applicative Logic.Proof.Proof
instance GHC.Base.Monad Logic.Proof.Proof


module Theory.Named

-- | A value of type <tt>a ~~ name</tt> has the same runtime representation
--   as a value of type <tt>a</tt>, with a phantom "name" attached.
data Named name a

-- | An infix alias for <a>Named</a>.
type a ~~ name = Named name a

-- | Introduce a name for the argument, and pass the named argument into
--   the given function.
name :: a -> (forall name. a ~~ name -> t) -> t

-- | Same as <a>name</a>, but names two values at once.
name2 :: a -> b -> (forall name1 name2. (a ~~ name1) -> (b ~~ name2) -> t) -> t

-- | Same as <a>name</a>, but names three values at once.
name3 :: a -> b -> c -> (forall name1 name2 name3. (a ~~ name1) -> (b ~~ name2) -> (c ~~ name3) -> t) -> t

-- | The <tt>Defining P</tt> constraint holds in any module where
--   <tt>P</tt> has been defined as a <tt>newtype</tt> wrapper of
--   <tt>Defn</tt>. It holds <i>only</i> in that module, if the constructor
--   of <tt>P</tt> is not exported.
type Defining p = (Coercible p Defn, Coercible Defn p)

-- | Library authors can introduce new names in a controlled way by
--   creating <tt>newtype</tt> wrappers of <tt>Defn</tt>. The constructor
--   of the <tt>newtype</tt> should *not* be exported, so that the library
--   can retain control of how the name is introduced.
--   
--   <pre>
--   newtype Bob = Bob Defn
--   
--   bob :: Int ~~ Bob
--   bob = defn 42
--   </pre>
data Defn

-- | In the module where the name <tt>f</tt> is defined, attach the name
--   <tt>f</tt> to a value.
defn :: Defining f => a -> (a ~~ f)
instance Data.The.The (Theory.Named.Named name a) a


module Theory.Equality

-- | The <tt>Equals</tt> relation is used to express equality between two
--   entities. Given an equality, you are then able to substitute one side
--   of the equality for the other, anywhere you please.
data Equals x y

-- | An infix alias for <a>Equals</a>.
type x == y = x `Equals` y

-- | Chain equalities, a la Liquid Haskell.
(==.) :: Proof (x == y) -> Proof (y == z) -> Proof (x == z)

-- | 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')

-- | Given a formula and an equality over ones 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')

-- | Substitute <tt>x'</tt> for <tt>x</tt> under the function <tt>f</tt>,
--   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)

-- | Substitute <tt>x'</tt> for <tt>x</tt> under the function <tt>f</tt>,
--   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')

-- | Test if the two named arguments are equal and, if so, produce a proof
--   of equality for the names.
same :: Lawful Eq a => (a ~~ x) -> (a ~~ y) -> Maybe (Proof (x == y))

-- | Reflect an equality between <tt>x</tt> and <tt>y</tt> into a
--   propositional equality between the <i>types</i> <tt>x</tt> and
--   <tt>y</tt>.
--   
--   <pre>
--   newtype Bob = Bob Defn
--   
--   bob :: Int ~~ Bob
--   bob = defn 42
--   
--   needsBob :: (Int ~~ Bob) -&gt; Int
--   needsBob x = the x + the x
--   
--   isBob :: (Int ~~ name) -&gt; Maybe (Proof (name == Bob))
--   isBob = same x bob
--   
--   f :: (Int ~~ name) -&gt; Int
--   f x = case reflectEq &lt;$&gt; isBob x of
--     Nothing   -&gt; 17
--     Just Refl -&gt; needsBob x x
--   </pre>
reflectEq :: Proof (x == y) -> (x :~: y)

-- | Convert a propositional equality between the types <tt>x</tt> and
--   <tt>y</tt> into a proof of <tt>x == y</tt>.
propEq :: (x :~: y) -> Proof (x == y)
instance Data.Arguments.Argument (Theory.Equality.Equals x y) 0
instance Data.Arguments.Argument (Theory.Equality.Equals x y) 1
instance Data.Arguments.Argument (Theory.Equality.Equals x y) Data.Arguments.LHS
instance Data.Arguments.Argument (Theory.Equality.Equals x y) Data.Arguments.RHS


module Logic.Classes

-- | A binary relation R is <i>reflexive</i> if, for all x, R(x, x) is
--   true. The <tt>Reflexive r</tt> typeclass provides a single method,
--   <tt>refl :: Proof (r x x)</tt>, proving R(x, x) for an arbitrary x.
--   
--   Within the module where the relation <tt>R</tt> is defined, you can
--   declare <tt>R</tt> to be reflexive with an empty instance:
--   
--   <pre>
--   -- Define a reflexive binary relation
--   newtype SameColor p q = SameColor Defn
--   instance Reflexive SameColor
--   </pre>
class Reflexive r
refl :: Reflexive r => Proof (r x x)
refl :: (Reflexive r, (Defining (r x x))) => Proof (r x x)

-- | A binary relation R is <i>symmetric</i> if, for all x and y, R(x, y)
--   is true if and only if R(y, x) is true. The <tt>Symmetric</tt>
--   typeclass provides a single method, <tt>symmetric :: r x y -&gt; Proof
--   (r y x)</tt>, proving the implication "R(x, y) implies R(y, x)".
--   
--   Within the module where <tt>R</tt> is defined, you can declare
--   <tt>R</tt> to be symmetric with an empty instance:
--   
--   <pre>
--   -- Define a symmetric binary relation
--   newtype NextTo p q = NextTo Defn
--   instance Symmetric NextTo
--   </pre>
class Symmetric c
symmetric :: Symmetric c => c p q -> Proof (c q p)
symmetric :: (Symmetric c, (Defining (c p q))) => c p q -> Proof (c q p)

-- | A binary relation R is <i>transitive</i> if, for all x, y, z, if R(x,
--   y) is true and R(y, z) is true, then R(x, z) is true. The
--   <tt>Transitive r</tt> typeclass provides a single method,
--   <tt>transitive :: r x y -&gt; r y z -&gt; Proof (r x z)</tt>, proving
--   R(x, z) from R(x, y) and R(y, z).
--   
--   Within the module where <tt>R</tt> is defined, you can declare
--   <tt>R</tt> to be transitive with an empty instance:
--   
--   <pre>
--   -- Define a transitive binary relation
--   newtype CanReach p q = CanReach Defn
--   instance Transitive CanReach
--   </pre>
class Transitive c
transitive :: Transitive c => c p q -> c q r -> Proof (c p r)
transitive :: (Transitive c, Defining (c p q)) => c p q -> c q r -> Proof (c p r)

-- | <tt>transitive</tt>, with the arguments flipped.
transitive' :: Transitive c => c q r -> c p q -> Proof (c p r)

-- | A binary operation <tt>#</tt> is idempotent if <tt>x # x == x</tt> for
--   all <tt>x</tt>. The <tt>Idempotent c</tt> typeclass provides a single
--   method, <tt>idempotent :: Proof (c p p == p)</tt>.
--   
--   Within the module where <tt>F</tt> is defined, you can declare
--   <tt>F</tt> to be idempotent with an empty instance:
--   
--   <pre>
--   -- Define an idempotent binary operation
--   newtype Union x y = Union Defn
--   instance Idempotent Union
--   </pre>
class Idempotent c
idempotent :: Idempotent c => Proof (c p p == p)
idempotent :: (Idempotent c, Defining (c p p)) => Proof (c p p == p)

-- | A binary operation <tt>#</tt> is commutative if <tt>x x</tt> for all
--   <tt>x</tt> and <tt>y</tt>. The <tt>Commutative c</tt> typeclass
--   provides a single method, <tt>commutative :: Proof (c x y == c y
--   x)</tt>.
--   
--   Within the module where <tt>F</tt> is defined, you can declare
--   <tt>F</tt> to be commutative with an empty instance:
--   
--   <pre>
--   -- Define a commutative binary operation
--   newtype Union x y = Union Defn
--   instance Commutative Union
--   </pre>
class Commutative c
commutative :: Commutative c => Proof (c p q == c q p)
commutative :: (Commutative c, Defining (c p q)) => Proof (c p q == c q p)

-- | A binary operation <tt>#</tt> is associative if <tt>x z) == (x z</tt>
--   for all <tt>x</tt>, <tt>y</tt>, and <tt>z</tt>. The <tt>Associative
--   c</tt> typeclass provides a single method, <tt>associative :: Proof (c
--   x (c y z) == c (c x y) z)</tt>.
--   
--   Within the module where <tt>F</tt> is defined, you can declare
--   <tt>F</tt> to be associative with an empty instance:
--   
--   <pre>
--   -- Define an associative binary operation
--   newtype Union x y = Union Defn
--   instance Associative Union
--   </pre>
class Associative c
associative :: Associative c => Proof (c p (c q r) == c (c p q) r)
associative :: (Associative c, Defining (c p q)) => Proof (c p (c q r) == c (c p q) r)

-- | A binary operation <tt>#</tt> distributes over <tt>%</tt> on the left
--   if <tt>x y) % (x # z)</tt> for all <tt>x</tt>, <tt>y</tt>, and
--   <tt>z</tt>. The <tt>DistributiveL c c'</tt> typeclass provides a
--   single method, <tt>distributiveL :: Proof (c x (c' y z) == c' (c x y)
--   (c x z))</tt>.
--   
--   Within the module where <tt>F</tt> and <tt>G</tt> are defined, you can
--   declare <tt>F</tt> to distribute over <tt>G</tt> on the left with an
--   empty instance:
--   
--   <pre>
--   -- x <tt>Union</tt> (y <tt>Intersect</tt> z) == (x <tt>Union</tt> y) <tt>Intersect</tt> (x <tt>Union</tt> z)
--   newtype Union     x y = Union     Defn
--   newtype Intersect x y = Intersect Defn
--   instance DistributiveL Union Intersect
--   </pre>
class DistributiveL c c'
distributiveL :: DistributiveL c c' => Proof (c p (c' q r) == c' (c p q) (c p r))
distributiveL :: (DistributiveL c c', Defining (c p q), Defining (c' p q)) => Proof (c p (c' q r) == c' (c p q) (c p r))

-- | A binary operation <tt>#</tt> distributes over <tt>%</tt> on the right
--   if <tt>(x % y) z) % (y # z)</tt> for all <tt>x</tt>, <tt>y</tt>, and
--   <tt>z</tt>. The <tt>DistributiveR c c'</tt> typeclass provides a
--   single method, <tt>distributiveR :: Proof (c (c' x y) z == c' (c x z)
--   (c y z))</tt>.
--   
--   Within the module where <tt>F</tt> and <tt>G</tt> are defined, you can
--   declare <tt>F</tt> to distribute over <tt>G</tt> on the left with an
--   empty instance:
--   
--   <pre>
--   -- (x <tt>Intersect</tt> y) <tt>Union</tt> z == (x <tt>Union</tt> z) <tt>Intersect</tt> (y <tt>Union</tt> z)
--   newtype Union     x y = Union     Defn
--   newtype Intersect x y = Intersect Defn
--   instance DistributiveR Union Intersect
--   </pre>
class DistributiveR c c'
distributiveR :: DistributiveR c c' => Proof (c (c' p q) r == c' (c p r) (c q r))
distributiveR :: (DistributiveR c c', Defining (c p q), Defining (c' p q)) => Proof (c (c' p q) r == c' (c p r) (c q r))

-- | A function <tt>f</tt> is <i>injective</i> if <tt>f x == f y</tt>
--   implies <tt>x == y</tt>. The <tt>Injective f</tt> typeclass provides a
--   single method, <tt>elim_inj :: (f x == f y) -&gt; Proof (x == y)</tt>.
--   
--   Within the module where <tt>F</tt> is defined, you can declare
--   <tt>F</tt> to be injective with an empty instance:
--   
--   <pre>
--   -- {x} == {y} implies x == y.
--   newtype Singleton x = Singleton Defn
--   instance Injective Singleton
--   </pre>
class Injective f
elim_inj :: Injective f => (f x == f y) -> Proof (x == y)
elim_inj :: (Injective f, Defining (f x), Defining (f y)) => (f x == f y) -> Proof (x == y)
instance Logic.Classes.Transitive Theory.Equality.Equals
instance Logic.Classes.Symmetric Theory.Equality.Equals
instance Logic.Classes.Reflexive Theory.Equality.Equals


module Data.Refined

-- | Given a type <tt>a</tt> and a proposition <tt>p</tt>, the type <tt>(a
--   ::: p)</tt> represents a value of type <tt>a</tt>, with an attached
--   "ghost proof" of <tt>p</tt>.
--   
--   Values of the type <tt>(a ::: p)</tt> have the same run-time
--   representation as values of the normal type <tt>a</tt>; the
--   proposition <tt>p</tt> does not carry a run-time space or time cost.
data a (:::) p

-- | Given a value and a proof, attach the proof as a ghost proof on the
--   value.
(...) :: a -> Proof p -> (a ::: p)

-- | Apply an implication to the ghost proof attached to a value, leaving
--   the value unchanged.
(...>) :: (a ::: p) -> (p -> Proof q) -> (a ::: q)

-- | Given a value and a proof, apply a function to the value but leave the
--   proof unchanged.
($:) :: (a -> b) -> (a ::: p) -> (b ::: p)

-- | Forget the ghost proof attached to a value.
exorcise :: (a ::: p) -> a

-- | Extract the ghost proof from a value.
conjure :: (a ::: p) -> Proof p

-- | Given a type <tt>a</tt> and a predicate <tt>p</tt>, the type <tt>a
--   ?p</tt> represents a <i>refinement type</i> for <tt>a</tt>. Values of
--   type <tt>a ?p</tt> should be values of type <tt>a</tt> that satisfy
--   the predicate <tt>p</tt>.
--   
--   Values of type <tt>a ?p</tt> have the same run-time representation as
--   values of type <tt>a</tt>; the proposition <tt>p</tt> does not carry a
--   run-time space or time cost.
data Satisfies (p :: * -> *) a

-- | An infix alias for <a>Satisfies</a>.
type a ? p = Satisfies p a

-- | For library authors: assert that a property holds.
assert :: Defining (p ()) => a -> (a ? p)

-- | Existential introduction for names: given a named value of type
--   <tt>a</tt> that satisfies a predicate <tt>p</tt>, coerce to a value of
--   type <tt>a ?p</tt>.
unname :: (a ~~ name ::: p name) -> (a ? p)

-- | Existential elimination for names: given a value of type <tt>a
--   ?p</tt>, re-introduce a new name to produce a value of type <tt>a ~~
--   name ::: p name</tt>.
rename :: (a ? p) -> (forall name. (a ~~ name ::: p name) -> t) -> t

-- | Take a simple function with one named argument and a named return,
--   plus an implication relating a precondition to a postcondition of the
--   function, and produce a function between refined input and output
--   types.
--   
--   <pre>
--   newtype NonEmpty xs = NonEmpty Defn
--   newtype Reverse  xs = Reverse  Defn
--   
--   rev :: ([a] ~~ xs) -&gt; ([a] ~~ Reverse xs)
--   rev xs = defn (reverse (the xs))
--   
--   rev_nonempty_lemma :: NonEmpty xs -&gt; Proof (NonEmpty (Reverse xs))
--   
--   rev' :: ([a] ?NonEmpty) -&gt; ([a] ?NonEmpty)
--   rev' = rev ...? rev_nonempty_lemma
--   </pre>
(...?) :: (forall name. (a ~~ name) -> (b ~~ f name)) -> (forall name. p name -> Proof (q (f name))) -> (a ? p) -> (b ? q)

-- | Traverse a collection of refined values, re-introducing names in the
--   body of the action.
traverseP :: (Traversable t, Applicative f) => (forall name. (a ~~ name ::: p name) -> f b) -> t (a ? p) -> f (t b)

-- | Same as <a>traverseP</a>, but ignores the action's return value.
traverseP_ :: (Foldable t, Applicative f) => (forall name. (a ~~ name ::: p name) -> f b) -> t (a ? p) -> f ()

-- | Same as <a>traverse</a>, with the argument order flipped.
forP :: (Traversable t, Applicative f) => t (a ? p) -> (forall name. (a ~~ name ::: p name) -> f b) -> f (t b)

-- | Same as <a>traverse_</a>, with the argument order flipped.
forP_ :: (Foldable t, Applicative f) => t (a ? p) -> (forall name. (a ~~ name ::: p name) -> f b) -> f ()
instance Data.The.The (Data.Refined.Satisfies p a) a
instance Data.The.The a' a => Data.The.The (a' Data.Refined.::: p) a


module Logic.Propositional

-- | The constant "true".
data TRUE

-- | The constant "false".
data FALSE

-- | The conjunction of <tt>p</tt> and <tt>q</tt>.
data And p q

-- | An infix alias for <tt>And</tt>.
type p && q = p `And` q

-- | An infix alias for <tt>And</tt>.
type p ∧ q = p `And` q

-- | An infix alias for <tt>And</tt>.
type p /\ q = p `And` q

-- | The disjunction of <tt>p</tt> and <tt>q</tt>.
data Or p q

-- | An infix alias for <tt>Or</tt>.
type p || q = p `Or` q

-- | An infix alias for <tt>Or</tt>.
type p ∨ q = p `Or` q

-- | An infix alias for <tt>Or</tt>.
type p \/ q = p `Or` q

-- | The implication "<tt>p</tt> implies <tt>q</tt>".
data Implies p q

-- | An infix alias for <tt>Implies</tt>.
type p --> q = p `Implies` q

-- | The negation of <tt>p</tt>.
data Not p

-- | Universal quantification.
data ForAll x p

-- | Existential quantifiation.
data Exists x p

-- | <tt>TRUE</tt> is always true, and can be introduced into a proof at
--   any time.
true :: Proof TRUE

-- | The Law of Noncontradiction: for any proposition P, "P and not-P" is
--   false.
noncontra :: Proof (Not (p && Not p))

-- | Prove "P and Q" from P and Q.
and_intro :: p -> q -> Proof (p && q)

-- | Prove "P or Q" from P.
or_introL :: p -> Proof (p || q)

-- | Prove "P or Q" from Q.
or_introR :: q -> Proof (p || q)

-- | Prove "P implies Q" by demonstrating that, from the assumption P, you
--   can prove Q.
impl_intro :: (p -> Proof q) -> Proof (p --> q)

-- | Prove "not P" by demonstrating that, from the assumption P, you can
--   derive a false conclusion.
not_intro :: (p -> Proof FALSE) -> Proof (Not p)

-- | <a>contrapositive</a> is an alias for <a>not_intro</a>, with a
--   somewhat more suggestive name. Not-introduction corresponds to the
--   proof technique "proof by contrapositive".
contrapositive :: (p -> Proof FALSE) -> Proof (Not p)

-- | Prove a contradiction from <a>P</a> and "not P".
contradicts :: p -> Not p -> Proof FALSE

-- | <a>contradicts'</a> is <a>contradicts</a> with the arguments flipped.
--   It is useful when you want to partially apply <a>contradicts</a> to a
--   negation.
contradicts' :: Not p -> p -> Proof FALSE

-- | 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))

-- | 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))

-- | From the assumption "P and Q", produce a proof of P.
and_elimL :: p && q -> Proof p

-- | From the assumption "P and Q", produce a proof of Q.
and_elimR :: p && q -> Proof q

-- | From the assumption "P and Q", produce both a proof of P, and a proof
--   of Q.
and_elim :: p && q -> Proof (p, q)

-- | 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

-- | Eliminate the first alternative in a conjunction.
or_elimL :: (p -> Proof r) -> (p || q) -> (q -> Proof r) -> Proof r

-- | Eliminate the second alternative in a conjunction.
or_elimR :: (q -> Proof r) -> (p || q) -> (p -> Proof r) -> Proof r

-- | Given "P imples Q" and P, produce a proof of Q. (modus ponens)
impl_elim :: p -> (p --> q) -> Proof q

-- | <tt>modus_ponens</tt> is just <tt>impl_elim</tt> with the arguments
--   flipped. In this form, it is useful for partially applying an
--   implication.
modus_ponens :: (p --> q) -> p -> Proof q

-- | Modus tollens lets you prove "Not P" from "P implies Q" and "Not Q".
--   
--   Modus tollens is not fundamental, and can be derived from other rules:
--   
--   <pre>
--                           -----         (assumption)
--                 p --&gt; q,    p
--                ---------------------    (modus ponens)
--          q,           Not q    
--       --------------------------        (contradicts')
--               FALSE
--   ------------------------------------- (not-intro)
--                      Not p
--   </pre>
--   
--   We can encode this proof tree more-or-less directly as a
--   <tt>Proof</tt> to implement <tt>modus_tollens</tt>:
--   
--   <pre>
--   modus_tollens :: (p --&gt; q) -&gt; Not q -&gt; Proof (Not p)
--   
--   modus_tollens impl q' =
--     do  modus_ponens impl
--      |. contradicts' q'
--      |\ not_intro
--   </pre>
modus_tollens :: (p --> q) -> Not q -> Proof (Not p)

-- | From a falsity, prove anything.
absurd :: FALSE -> Proof p

-- | Given "For all x, P(x)" and any c, prove the proposition "P(c)".
univ_elim :: ForAll x (p x) -> Proof (p c)

-- | 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

-- | The inference rules so far have all been valid in constructive logic.
--   Proofs in classical logic are also allowed, but will be constrained by
--   the <a>Classical</a> typeclass.
class Classical

-- | Discharge a <tt>Classical</tt> constraint, by saying "I am going to
--   allow a classical argument here."
--   
--   NOTE: The existence of this function means that a proof should only be
--   considered constructive if it does not have a <tt>Classical</tt>
--   constraint, *and* it does not invoke <tt>classically</tt>.
classically :: (Classical => Proof p) -> Proof p

-- | The Law of the Excluded Middle: for any proposition P, assert that
--   either P is true, or Not P is true.
lem :: Classical => Proof (p || Not p)

-- | 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 <tt>Classical</tt> constraint. But note that the similar
--   technique of proof by contrapositive (not-introduction) <i>is</i>
--   valid in constructive logic! For comparison, the two types are:
--   
--   <pre>
--   contradiction  :: Classical =&gt; (Not p -&gt; Proof FALSE) -&gt; p
--   not_intro      ::              (p     -&gt; Proof FALSE) -&gt; Not p
--   </pre>
--   
--   The derivation of proof by contradiction from the law of the excluded
--   middle goes like this: first, use the law of the excluded middle to
--   prove <tt>p || Not p</tt>. Then use or-elimination to prove <tt>p</tt>
--   for each alternative. The first alternative is immediate; for the
--   second alternative, use the provided implication to get a proof of
--   falsehood, from which the desired conclusion is derived.
--   
--   <pre>
--   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.
--   </pre>
contradiction :: forall p. Classical => (Not p -> Proof FALSE) -> Proof p

-- | Double-negation elimination. This is another non-constructive proof
--   technique, so it requires the <tt>Classical</tt> constraint.
--   
--   The derivation of double-negation elimination follows from proof by
--   contradiction, since "Not (Not p)" contradicts "Not p". <tt>
--   not_not_elim p'' = contradiction (contradicts' p'') </tt>
not_not_elim :: Classical => Not (Not p) -> Proof p

-- | Apply a derivation to the left side of a conjunction.
and_mapL :: (p -> Proof p') -> (p && q) -> Proof (p' && q)

-- | Apply a derivation to the right side of a conjunction.
and_mapR :: (q -> Proof q') -> (p && q) -> Proof (p && q')

-- | Apply derivations to the left and right sides of a conjunction.
and_map :: (p -> Proof p') -> (q -> Proof q') -> (p && q) -> Proof (p' && q')

-- | Apply a derivation to the left side of a disjunction.
or_mapL :: (p -> Proof p') -> (p || q) -> Proof (p' || q)

-- | Apply a derivation to the right side of a disjunction.
or_mapR :: (q -> Proof q') -> (p || q) -> Proof (p || q')

-- | Apply derivations to the left and right sides of a disjunction.
or_map :: (p -> Proof p') -> (q -> Proof q') -> (p || q) -> Proof (p' || q')

-- | Apply a derivation to the left side of an implication.
impl_mapL :: (p' -> Proof p) -> (p --> q) -> Proof (p' --> q)

-- | Apply a derivation to the right side of an implication.
impl_mapR :: (q -> Proof q') -> (p --> q) -> Proof (p --> q')

-- | Apply derivations to the left and right sides of an implication.
impl_map :: (p' -> Proof p) -> (q -> Proof q') -> (p --> q) -> Proof (p' --> q')

-- | Apply a derivation inside of a negation.
not_map :: (p' -> Proof p) -> Not p -> Proof (Not p')
instance Logic.Classes.Symmetric Logic.Propositional.Or
instance Logic.Classes.Associative Logic.Propositional.Or
instance Logic.Classes.DistributiveR Logic.Propositional.And Logic.Propositional.Or
instance Logic.Classes.DistributiveR Logic.Propositional.Or Logic.Propositional.And
instance Logic.Classes.DistributiveR Logic.Propositional.Or Logic.Propositional.Or
instance Logic.Classes.DistributiveL Logic.Propositional.And Logic.Propositional.Or
instance Logic.Classes.DistributiveL Logic.Propositional.Or Logic.Propositional.And
instance Logic.Classes.DistributiveL Logic.Propositional.Or Logic.Propositional.Or
instance Logic.Classes.Symmetric Logic.Propositional.And
instance Logic.Classes.Associative Logic.Propositional.And
instance Logic.Classes.DistributiveR Logic.Propositional.And Logic.Propositional.And
instance Logic.Classes.DistributiveL Logic.Propositional.And Logic.Propositional.And


module Logic.NegClasses

-- | A binary relation R is <i>irreflexive</i> if, for all x, R(x, x) is
--   false. The <tt>Irreflexive r</tt> typeclass provides a single method,
--   <tt>irrefl :: Proof (Not (r x x))</tt>, proving the negation of R(x,
--   x) for an arbitrary x.
--   
--   Within the module where the relation <tt>R</tt> is defined, you can
--   declare <tt>R</tt> to be irreflexive with an empty instance:
--   
--   <pre>
--   -- Define an irreflexive binary relation
--   newtype DifferentColor p q = DifferentColor Defn
--   instance Irreflexive DifferentColor
--   </pre>
class Irreflexive r
irrefl :: Irreflexive r => Proof (Not (r x x))
irrefl :: (Irreflexive r, (Defining (r x x))) => Proof (Not (r x x))

-- | A binary relation R is <i>antisymmetric</i> if, for all x and y, when
--   R(x, y) is true, then R(y, x) is false. The <tt>Antisymmetric</tt>
--   typeclass provides a single method, <tt>antisymmetric :: r x y -&gt;
--   Proof (Not (r y x))</tt>, proving the implication "R(x, y) implies the
--   negation of R(y, x)".
--   
--   Within the module where <tt>R</tt> is defined, you can declare
--   <tt>R</tt> to be antisymmetric with an empty instance:
--   
--   <pre>
--   -- Define an antisymmetric binary relation
--   newtype AncestorOf p q = AncestorOf Defn
--   instance Antisymmetric AncestorOf
--   </pre>
class Antisymmetric c
antisymmetric :: Antisymmetric c => c p q -> Proof (Not (c q p))
antisymmetric :: (Antisymmetric c, Defining (c p q)) => c p q -> Proof (Not (c q p))


module GDP
