{-# 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) = Writer [Action] () -> Proof Existential
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 :: PropRef Universal -> Proof a
assume (PropRef PropId
p) = Writer [Action] () -> Proof a
forall b a. Writer [Action] b -> ProofScheme a b
Proof (Writer [Action] () -> Proof a) -> Writer [Action] () -> Proof a
forall a b. (a -> b) -> a -> b
$ [Action] -> Writer [Action] ()
forall w (m :: * -> *). MonadWriter w m => w -> m ()
tell [PropId -> Action
Assume PropId
p]

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