{-# LANGUAGE Safe #-}

-- | Utility functions to help write proof tactics.

module Copilot.Theorem.Tactics
  ( instantiate, assume, admit
  ) where

import Copilot.Theorem.Prove

import Control.Monad.Writer

-- | Instantiate a universal proof into an existential proof.
instantiate :: Proof Universal -> Proof Existential
instantiate :: Proof Universal -> Proof Existential
instantiate (Proof Writer [Action] ()
p) = forall b a. Writer [Action] b -> ProofScheme a b
Proof Writer [Action] ()
p

-- | Assume that a property, given by reference, holds.
assume :: PropRef Universal -> Proof a
assume :: forall a. PropRef Universal -> Proof a
assume (PropRef PropId
p) = forall b a. Writer [Action] b -> ProofScheme a b
Proof forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [PropId -> Action
Assume PropId
p]

-- | Assume that the current goal holds.
admit :: Proof a
admit :: forall a. Proof a
admit = forall b a. Writer [Action] b -> ProofScheme a b
Proof forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [Action
Admit]