hout (empty) → 0.1.0.0

raw patch · 11 files changed

+617/−0 lines, 11 filesdep +basedep +do-notationdep +houtsetup-changed

Dependencies added: base, do-notation, hout, indexed

Files

ChangeLog.md +5/−0
LICENSE +30/−0
README.md +93/−0
Setup.hs +2/−0
examples/Examples.hs +4/−0
examples/Hout/Examples.hs +51/−0
hout.cabal +54/−0
src/Hout/Logic/FirstOrder.hs +92/−0
src/Hout/Logic/Intuitionistic.hs +90/−0
src/Hout/Prover/Proofs.hs +54/−0
src/Hout/Prover/Tactics.hs +142/−0

+ ChangeLog.md view

@@ -0,0 +1,5 @@+# Changelog for hout++## 2020-04-11 -- 0.1.0.0++First release.

+ LICENSE view

@@ -0,0 +1,30 @@+Copyright Isaac van Bakel (c) 2020++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 Isaac van Bakel 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.

+ README.md view

@@ -0,0 +1,93 @@+# hout - a non-interactive proof assistant for first-order logic, in Haskell++hout is an in-Haskell non-interactive proof assistant for intuitionistic first-order logic.++Alternatively, hout provides a monad that allows you to write functions in the style of proof-assistant proofs, which are then computable Haskell terms.++This is possible thanks to the Curry-Howard isomorphism.++## Examples++Have a look at `examples/Hout/Examples.hs` for some examples.++## What?++If you know about the CHI and intuitionistic logic, skip this section.++### The Curry-Howard isomorphism++The Curry-Howard isomorphism (or correspondence) is a pattern between intuitionistic logic and type theory, which says that propositions correspond to types, and proofs correspond to terms.++The basis of this correspondence is that an *inhabitant* of a type is a proof that the type is inhabited. For example, the term `3 :: Int` is a proof that you can construct some terminating value of type `Int`.++What about types with no inhabitant? Taking some type known to have no inhabitants, like `Void`, you can show that a type `a` is uninhabited by producing a terminating term of type `a -> Void`. Why? Because `a -> Void` is inhabited only if `a` is uninhabited, and a term of type `a -> Void` is a *proof that `a -> Void` is inhabited*!++This also has implications for function types - a term with type `a -> b` is a function from terms of type `a` to terms of type `b`. You can equally consider it as a function from proofs of the proposition `a` to proofs of the proposition `b` - in other words, the function itself is a proof that `a` implies `b`, because if you have a proof that `a` is true, you can obtain a proof that `b` is true.++Other logical connectives also have equivalents in Haskell types. `False` is `Void`, because you can't construct a proof for it; `a /\ b` is the tuple (or product) `(a, b)`; `a \/ b` is (the sum) `Either a b`; and `Not a` - the claim that `a` is uninhabited - is precisely `a -> False`. `True` can be any inhabited type, but it's helpful to have a type with a canonical construction, so `True` is normally `()`, the empty tuple, which has the unique constructor `()`.++You can see the correspondence in these types - `(a, b)` is inhabited if and only if both `a` and `b` are inhabited. Similarly, `Either a b` is inhabited if and only if at least one of `a`, `b` is inhabited. Phrasing it in terms of proofs, if you have a proof of `a` and a proof of `b`, you can construct a proof of `a /\ b` (and vice-versa) - and with a proof of `a`, you can construct a proof of `a \/ b`. With a proof of `a \/ b`, you can *destruct* the proof to get either a proof for `a` (`Left a`) or a proof for `b` (`Right b`).++For notation's sake, we write `a <-> b` for the type `(a -> b) /\ (b -> a)`.++### Intuistionistic logic++Intuistionistic (or constructive) logic is a subset of classical logic (the kind of logic you normally learn in a CS or Maths course). It behaves exactly like classical logic, but with one caveat - *you can only _construct_ proofs of a proposition*.++To see what that means, consider the type of the law of the excluded middle - `forall a. a \/ Not a`. For every type `a`, one of these two terms must be constructable - either `a` is inhabited, so you can construct a value of type `a`, or `a` is uninhabited, so you can construct a function of type `a -> Void`.++But you can't write a terminating Haskell function with type `forall a. a \/ Not a` - because it would require you to somehow decide if `a` is inhabited, and then get a value of type `a` if it was. In other words, you have to construct either a `Left a` or a `Right (Not a)`, and you have no way to do either of those things.++There are lots of other consequences of this caveat: the following implications do *not* hold in intuitionistic logic - and similarly, you cannot write a terminating Haskell term for their type.++  * `Not (Not a) -> a`+  * `(a -> b) -> (Not a \/ b)`+  * `Not (Not a /\ Not b) -> a \/ b`++## Proofs and the Tactic monad++The `Tactic` monad is an indexed monad for which the monad state is the current proof goal, and the type argument is an additional hypothesis introduced at that proof step. Looking at its definition+```+data Tactic from to a = Tactic ((a -> to) -> from)+```+A `Tactic` term represents a valid goal transformation - you are allowed to change a proof of `from` into a proof of `to`, and introduce the additional hypothesis `a`, if you can use a proof of `a -> to` to prove `from`.++For example, the `apply` function has the signature+```+apply :: (a -> b) -> Tactic b a ()+```+Given a function `a -> b`, it allows you to transform the goal from proving `b` to proving `a` - because once you prove `a`, it will be possible to use the given function to produce a proof of `b`.++Some tactics introduce additional hypotheses - such as `intro`+```+intro :: Tactic (a -> b) b a+```+`intro` allows you to transform a goal of `a -> b` to a goal of `b`, giving you the hypothesis of type `a` to bind into a variable. If you can use the proof of `a` to construct a proof of `b`, then the resulting function term is indeed a proof of `a -> b`.++### Available tactics++hout provides some tactics based on those used in `Coq` - for example, you can `apply` hypotheses to a goal; you can `split` the proof a conjunction into proofs of its conjuncts; you can `intro` a variable; you can `exists` the witness of an existential goal; you can `rewrite` propositions with equality; you can even `assert` hypothesis and produce subgoals.++The full list of tactics is given in `Hout.Prover.Tactics`, and it is possible to write your own using the type signature of the `Tactic` monad.++### Proofs in do notation++Because `Tactic` is an indexed monad, you can use the `do-notation` package to write proofs in do notation, which end up looking quite similar to proofs in interactive proof assistants. Some advice for doing this is:++  * use pattern-matching in binds, particularly when working with existential types. GHC has some unfortunate behaviour when trying to use `let` in do notation when working with existential type arguments.+  * Enable block arguments, and use do notation for subgoals+  * If your final statement is a tactic that introduces a hypothesis, but the new goal is trivial `()`, use `qed` to end your proof.++### Limitations++The use of `Forall` is limited by Haskell's lack of support for impredicative polymorphism - the instantiation of type variables with higher-ranked types. This makes it basically impossible to prove a `Forall` using the `Tactic` monad, since under the hood `Forall` is just a Haskell type-level `forall`.++## Computations written in the proof style++hout also has the nice property of intuitionistic proof assistants that proofs are themselves terms, and can be run as Haskell code. This gives hout the alternative use of writing functions in a proof-y syntax using the `Tactic` monad. For example, the `identity` function can be written as+```+identity :: a -> a+identity :: runProof $ Proof do+  a <- intro+  exact a+```

+ Setup.hs view

@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain

+ examples/Examples.hs view

@@ -0,0 +1,4 @@+module Main where++main :: IO ()+main = return ()

+ examples/Hout/Examples.hs view

@@ -0,0 +1,51 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE RebindableSyntax #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE KindSignatures, PolyKinds #-}++module Hout.Examples where++import Prelude hiding (True, False, Monad (..), pure)+import Prelude (fail)++import Control.Monad.Indexed+import Language.Haskell.DoNotation++import Hout.Logic.Intuitionistic+import Hout.Logic.FirstOrder+import Hout.Prover.Proofs+import Hout.Prover.Tactics++orComm :: Lemma ((a \/ b) -> (b \/ a))+orComm = Proof do+  a_or_b <- intro+  case a_or_b of+    Left a -> do+      right+      exact a+    Right b -> do+      left+      exact b+  qed++data Implies1 (p :: k -> *) (q :: k -> *) (a :: k) = I1 (p a -> q a)++composition :: Definition ((a -> b) -> (b -> c) -> (a -> c))+composition = Proof do+  a_impl_b <- intro+  b_impl_c <- intro+  a <- intro+  apply b_impl_c+  apply a_impl_b+  exact a++runComposition :: (a -> b) -> (b -> c) -> (a -> c)+runComposition = runProof composition++exists_and_forall_implies_exists :: Theorem (Exists k p -> Forall k (Implies1 p q) -> Exists k q)+exists_and_forall_implies_exists = Proof do+  (Exists witness p_witness) <- intro+  (Forall (I1 forall_implies)) <- intro+  exists witness+  apply forall_implies+  exact p_witness

+ hout.cabal view

@@ -0,0 +1,54 @@+name:                hout+version:             0.1.0.0+synopsis:            Non-interactive proof assistant monad for first-order logic.+description:         Hout is an in-Haskell non-interactive proof assistant for+                     intuitionistic first-order logic, using Haskell's type+                     system. If a proof written in Hout compiles, it is correct.+                     .+                     Alternatively, Hout provides an indexed monad which,+                     combined with Haskell's do notation, allows for writing+                     Haskell code in the style of proof assistants.+                     .+                     The main part of Hout's value is found in+                     "Hout.Prover.Tactics", which defines the @Tactic@ monad+                     and several proof tactics similar to those found in Coq.+                     Other useful defintions for using Hout can be found in+                     "Hout.Prover.Proofs".++homepage:            https://github.com/ivanbakel/hout-prover#readme+license:             BSD3+license-file:        LICENSE+author:              Isaac van Bakel+maintainer:          ivb@vanbakel.io+copyright:           2020 Isaac van Bakel+category:            Type System, Logic+build-type:          Simple+extra-source-files:  README.md, ChangeLog.md+cabal-version:       >=1.10++library+  hs-source-dirs:      src+  exposed-modules:     Hout.Logic.Intuitionistic+                     , Hout.Logic.FirstOrder+                     , Hout.Prover.Tactics+                     , Hout.Prover.Proofs+  build-depends:       base >= 4.7 && < 5+                     , indexed+  default-language:    Haskell2010++test-suite examples+  type: exitcode-stdio-1.0+  main-is: Examples.hs+  hs-source-dirs:+    examples+  build-depends:       base >= 4.7 && < 5+                     , indexed+                     , do-notation+                     , hout+  other-modules:       Hout.Examples+  default-language:    Haskell2010+  ++source-repository head+  type:     git+  location: https://github.com/ivanbakel/hout-prover

+ src/Hout/Logic/FirstOrder.hs view

@@ -0,0 +1,92 @@+{-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE ExistentialQuantification #-}+{-# LANGUAGE Rank2Types #-}++{-|+Module      : Hout.Logic.FirstOrder+Description : Constructs of first-order intuitionistic logic in Haskell types+Copyright   : (c) Isaac van Bakel, 2020+License     : BSD-3+Maintainer  : ivb@vanbakel.io+Stability   : experimental+Portability : POSIX++This module contains type aliases for first-order logic constructions which are+expressed as Haskell types, based on those in "Hout.Logic.Intuitionistic". This+gives definitions for++  * the universal quantifier+  * the existential quantifier+  * first-order equality++It also gives the natural deduction rules for these constructions, though they+are not very useful to the programmer.+-}+module Hout.Logic.FirstOrder where++import Data.Kind++-- Types++-- | A witness of a kind inhabitant. 'Witness'es can be constructed for the+-- 'Type' kind, 'Constraint' kind, or any data kind.+data Witness (a :: k) where+  -- | Because Type is the only kind of habitats, it is the only constructor for+  -- which we can demand an inhabitant+  Witness :: (a :: Type) -> Witness a+  ConstraintWitness :: Witness (a :: Constraint)+  DataKindWitness :: Witness (a :: (k :: Type))++-- | The existential quantifier, parameterised by a kind. The predicate itself+-- is required to return a 'Type', since 'Exists' carries the proof term. If+-- @k@ is 'Type', then 'Exists' also carries the witness term in a 'Witness'.+data Exists k (p :: k -> *) where+  Exists :: Witness (a :: k) -> p a -> Exists k p++-- | The forall quantifier. As with 'Exists', the predicate is required to+-- return a 'Type'. Despite @forall@ being a Haskell built-in, the lack of+-- support for impredicative types means that a newtype is declared for+-- usability. +data Forall k (p :: k -> *) = Forall (forall (a :: k). p a)++-- | Type level equality, parameterised by a kind.+data Equal (a :: k) (b :: k) where+  -- | The unique equality constructor - pattern matching on 'Refl' allows the+  -- compiler to deduce that @a@ and @b@ must unify.+  Refl :: Equal a a++-- Natural deduction (FO)++existsIntro :: Witness (a :: k) -> p a -> Exists k p+existsIntro witness proof = Exists witness proof++-- | Exists elimination, as a continuation.+--+-- Note that this has to be expressed in this continuation style because+-- existential types are not allowed in the return type+existsElim :: (forall (a :: k). Witness a -> p a -> b) -> Exists k p -> b+existsElim f (Exists witness proof) = f witness proof++forallIntro :: (forall (a :: k). p a) -> Forall k p+forallIntro forall = Forall forall++forallElim :: Forall k p -> p (a :: k)+forallElim (Forall forall) = forall++eqRefl :: Equal a a+eqRefl = Refl++eqSym :: Equal a b -> Equal b a+eqSym Refl = Refl++eqTrans :: Equal a b -> Equal b c -> Equal a c+eqTrans Refl Refl = Refl++-- | Rewrite by equality.+--+-- This could be expressed as an @<->@, but @->@ is easier to use. The power+-- of the rule is not affected.+eqRewrite :: Equal a b -> p a -> p b+eqRewrite Refl proof = proof

+ src/Hout/Logic/Intuitionistic.hs view

@@ -0,0 +1,90 @@+-- For ex falso+{-# LANGUAGE EmptyCase #-}+-- For nice-looking type aliases+{-# LANGUAGE TypeOperators #-}+-- To allow us to redefine True & False as types instead of constructors+{-# LANGUAGE NoImplicitPrelude #-}++{-|+Module      : Hout.Logic.Intuitionistic+Description : Constructs of intuitionistic logic in Haskell types+Copyright   : (c) Isaac van Bakel, 2020+License     : BSD-3+Maintainer  : ivb@vanbakel.io+Stability   : experimental+Portability : POSIX++This module contains type aliases for intuitionistic logic constructions which are+expressed as Haskell types.++It also gives the natural deduction rules for those aliases, except when they+are aliases of arrow types. For example, implies-introduction and elimination+are both Haskell arrow constructions (function abstraction and application,+respectively) so no rule is given.+-}+module Hout.Logic.Intuitionistic where++import Prelude hiding (True, False)++import Data.Void++-- Types++-- | The trivially-inhabited type. 'True' is defined as '()' to give it a+-- canonical construction, so that all proofs of 'True' are identical.+type True = ()++-- | The uninhabited type.+type False = Void++type (a /\ b) = (a, b)++type (a \/ b) = Either a b++-- | Negation of a type. Because this is an arrow type alias, not-introduction+-- and elimination are not part of this module.+type Not a = a -> False++-- | Iff. Some derived rules are defined for iff for the sake of completeness.+type (a <-> b) = (a -> b) /\ (b -> a)++-- Natural deduction ++andIntro :: a -> b -> a /\ b+andIntro a b = (a, b)++andElimLeft :: a /\ b -> a+andElimLeft ((a, _)) = a++andElimRight :: a /\ b -> b+andElimRight ((_, b)) = b++orIntroLeft :: a -> a \/ b+orIntroLeft a = Left a++orIntroRight :: b -> a \/ b+orIntroRight b = Right b++orElim :: (a -> c) -> (b -> c) -> (a \/ b) -> c+orElim fromA fromB (Left a) = fromA a+orElim fromA fromB (Right b) = fromB b++trueIntro :: True+trueIntro = ()++-- | Ex Falso Quod Libet - it is recommended when writing functions of this+-- form to use the 'EmptyCase' extension, to make the compiler check that+-- the type is uninhabited.+exFalso :: False -> a+exFalso false = case false of++-- Derived rules++iffIntro :: (a -> b) -> (b -> a) -> (a <-> b)+iffIntro verse converse = (verse, converse)++iffElimLeft :: (a <-> b) -> a -> b+iffElimLeft (verse, _) a = verse a++iffElimRight :: (a <-> b) -> b -> a+iffElimRight (_, converse) b = converse b

+ src/Hout/Prover/Proofs.hs view

@@ -0,0 +1,54 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE EmptyCase #-}+{-# LANGUAGE RebindableSyntax #-}++{-|+Module      : Hout.Prover.Proofs+Description : Definition of the theorem construction.+Copyright   : (c) Isaac van Bakel, 2020+License     : BSD-3+Maintainer  : ivb@vanbakel.io+Stability   : experimental+Portability : POSIX++This module contains some helpers for declaring proofs, and running them as+code.+-}+module Hout.Prover.Proofs where++import Control.Monad.Indexed+import Prelude hiding (True, False, Monad (..))++import Hout.Prover.Tactics++-- | Run a theorem to its Haskell term. If the proof of the theorem uses only+-- terminating values, then the resulting Haskell term can be run as usual+-- without errors.+runProof :: Theorem a -> a+runProof (Proof (Tactic f)) = f \() -> ()++-- | A proven theorem.+--+-- As described in "Hout.Prover.Tactics", proof of @a@ is equivalent to reducing+-- the proof goal @a@ to the trival proof goal @()@.+data Theorem a = Proof (Tactic a () ())++-- Some possible type synonyms+type Lemma a = Theorem a+type Corollary a = Theorem a+type Example a = Theorem a+type Definition a = Theorem a++-- | An unprovable axiom.+data Axiom a++-- | Admit an axiom, without proof. Note that this is not a terminating term,+-- so using it will not yield computable Haskell.+admitted :: Axiom a+admitted = admitted++-- | Use an axiom, with the understood caveat that the result will not be a+-- computable term. It is impossible to construct an 'Axiom', so using one+-- cannot give runnable Haskell.+noncomputable :: Axiom a -> a+noncomputable axiom = case axiom of

+ src/Hout/Prover/Tactics.hs view

@@ -0,0 +1,142 @@+{-# LANGUAGE BlockArguments #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE KindSignatures, PolyKinds #-}++{-|+Module      : Hout.Prover.Tactics+Description : Definition of the proof-transformation monad 'Tactic'.+Copyright   : (c) Isaac van Bakel, 2020+License     : BSD-3+Maintainer  : ivb@vanbakel.io+Stability   : experimental+Portability : POSIX++The module forms the basis of hout as a non-interactive proof assistant. It+contains the definition of 'Tactic', the monad which allows for proof-goal+manipulations in do-notation, and defines some useful 'Tactic' functions to+mimic the syntax of actual proof assistants.+-}+module Hout.Prover.Tactics where++import Control.Monad.Indexed+import Prelude hiding (True, False)++import Hout.Logic.Intuitionistic+import Hout.Logic.FirstOrder++-- Basics of theorem proving++-- | The proof-transformation monad. 'Tactic' is an indexed monad for which+-- the type state is the current proof goal.+--+-- The aim of most 'Tactic' uses is to produce a term with type+-- @Tactic a () ()@ for the proof goal @a@ - this represents a proof of @a@,+-- since it involves reducing the proof goal @a@ to the trivial proof goal @()@.+--+-- A 'Tactic' term is a valid manipulation which takes a proof of @a -> to@+-- and gives a proof of @from@ - allowing for the proof-goal to be transformed+-- from @from@ into @to@, giving the additional hypothesis @a@.+data Tactic from to a = Tactic ((a -> to) -> from)++-- | Bind a term as a hypothesis name.+name :: a -> Tactic b b a+name a = Tactic \f -> f a++-- | Apply a proof transformation to the hypothesis.+applyH :: (a -> b) -> Tactic m n a -> Tactic m n b+applyH proof (Tactic g) = Tactic \f -> g (f . proof)++-- | Combine two hypotheses together.+combineH :: Tactic m n (a -> b) -> Tactic n o a -> Tactic m o b+combineH (Tactic g) (Tactic h) = Tactic \f -> g (\a_b -> h (f . a_b))++-- | Apply an intermediate proof to the hypothesis.+bindH :: (a -> Tactic n o b) -> Tactic m n a -> Tactic m o b+bindH a_tactic (Tactic g) = Tactic \b_o -> g (\a -> let Tactic h = a_tactic a in h b_o)++instance IxFunctor Tactic where+  imap = applyH++instance IxPointed Tactic where+  ireturn = name++instance IxApplicative Tactic where+  iap = combineH++instance IxMonad Tactic where+  ibind = bindH++-- | Apply a proof transformation to the goal. This simplifies the goal of @b@+-- to a goal of @a@.+apply :: (a -> b) -> Tactic b a ()+apply f = Tactic \unit_a -> f (unit_a ())++-- | Apply a forall to the goal. This solves the goal immediately.+applyF :: Forall k p -> Tactic (p a) () ()+applyF (Forall f) = Tactic (\nil -> f)++-- | Transform a disjunction goal into the goal of the left side.+left :: Tactic (a \/ b) a ()+left = Tactic (\f -> Left (f ()))++-- | Transform a disjunction goal into the goal of the right side.+right :: Tactic (a \/ b) b ()+right = Tactic (\f -> Right (f ()))++-- | Give a name to the hypothesis of an @->@.+intro :: Tactic (a -> b) b a+intro = Tactic (\this -> this)++-- | Solve a goal by giving its exact proof.+exact :: a -> Tactic a () ()+exact a = Tactic (\_ -> a)++-- | Split a conjuction goal into two subgoals.+split :: Tactic a () () -> Tactic b () () -> Tactic (a /\ b) () ()+split (Tactic f) (Tactic g) = Tactic (\nil -> (f nil, g nil))++-- | Assert a statement, giving a proof of it. The statement can then be bound+-- as a hypothesis+assert :: Tactic a () () -> Tactic m m a+assert (Tactic f) = Tactic (\a_m -> a_m (f (\() -> ())))++-- | Assert a statement, giving a proof that it solves the goal. The goal then+-- becomes proving the statement.+enough :: (a -> Tactic b () ()) -> Tactic b a ()+enough transform = Tactic \f -> let Tactic g = transform (f ()) in g \() -> ()++-- | Give the witness for an existential goal. The goal then becomes proving+-- the statement for that witness.+exists :: Witness (a :: k) -> Tactic (Exists k p) (p a) ()+exists a = Tactic (\proof_of_p_a -> Exists a (proof_of_p_a ()))++-- | Transform a goal for a specific value to a general 'Forall' goal+generalize :: Tactic (p a) (Forall k p) ()+generalize = Tactic \f -> let Forall forall = f () in forall++-- | Solve a reflexive goal.+reflexivity :: Tactic (Equal a a) () ()+reflexivity = Tactic (\id -> Refl)++-- | Transform an equality goal by symmetry.+symmetry :: Tactic (Equal a b) (Equal b a) ()+symmetry = Tactic (\f -> eqSym (f ()))++-- | Split an equality goal into two subgoals, by transitivity. +transitivity :: Tactic (Equal a b) () () -> Tactic (Equal b c) () () -> Tactic (Equal a c) () ()+transitivity (Tactic f) (Tactic g) = Tactic (\nil -> eqTrans (f nil) (g nil))++-- | Rewrite a goal by equality, left-to-right.+rewrite :: Equal a b -> Tactic (p a) (p b) ()+rewrite equality = apply (eqRewrite (eqSym equality))++-- | Rewrite a goal by equality, right-to-left.+rewriteRev :: Equal a b -> Tactic (p b) (p a) ()+rewriteRev equality = apply (eqRewrite equality)++-- | A helper for the end of proofs. Assert to the type system that the proof+-- is complete, and act as an ending statement if the final 'Tactic' otherwise+-- introduces a hypothesis.+qed :: Tactic () () ()+qed = Tactic (\unit -> ())