%if False > {-# OPTIONS_GHC -F -pgmF she #-} > {-# LANGUAGE TypeOperators, TypeSynonymInstances, GADTs, FlexibleInstances, > PatternGuards, TupleSections #-} > module Tactics.ProblemSimplify where > import Prelude hiding (any, foldl, elem) > import Control.Applicative > import Control.Monad.Reader > import Data.Foldable > import Data.Traversable > import Kit.BwdFwd > import Kit.MissingLibrary > import Kit.Trace > import Evidences.Tm > import Evidences.Utilities > import Evidences.Eval > import Evidences.Operators > import Evidences.DefinitionalEquality > import Evidences.Mangler > import ProofState.Edition.ProofState > import ProofState.Edition.GetSet > import ProofState.Edition.Navigation > import ProofState.Edition.Scope > import ProofState.Interface.ProofKit > import ProofState.Interface.Definition > import ProofState.Interface.Parameter > import ProofState.Interface.Solving > import ProofState.Interface.Lifting > import Tactics.Elimination > import Tactics.PropositionSimplify %endif \section{Problem Simplification} Now that we have considered how to simplify propositions, we wish to use this technology to simplify programming problems. Suppose we have a goal of type $\Delta \rightarrow T$, where $\Delta$ is some telescope of hypotheses. There are various things we can do to simplify the problem, such as: \begin{itemize} \item splitting up $\Sigma$-types into their components; \item simplifying propositions in the hypotheses and goal; \item discarding uninformative hypotheses; and \item solving the problem completely if it is trivial (for example, if it depends on a proof of false). \end{itemize} The |problemSimplify| command performs these simplifications. It works by repeatedly transforming the proof state into a simpler version, one step at a time. It will fail if no simplification is possible. The real work is done in |simplifyGoal| below. > problemSimplify :: ProofState (EXTM :=>: VAL) > problemSimplify = do > simpTrace "problemSimplify" > getHoleGoal >>= simplifyGoal True . valueOf >> getCurrentDefinition We say simplification is \emph{at the top level} if we are simplifying exactly the current goal in the proof state. If this is not the case, we can still make some simplifications but others require us to quote the type being simplified and make a new goal so we are back at the top level. The |Bool| parameter to the following functions indicates whether simplification is at the top level. When simplifying at the top level, we should |give| the simplified form once we have computed it. The |topWrap| command makes this easy. > topWrap :: Bool -> INTM :=>: VAL -> ProofState (INTM :=>: VAL) > topWrap True tt = give (termOf tt) >> return tt > topWrap False tt = return tt Once we have simplified the goal slightly, we use |trySimplifyGoal| to attempt to continue, but give back the current result if no more simplification is possible. If not at the top level, this has to create a new goal. > trySimplifyGoal :: Bool -> TY -> ProofState (INTM :=>: VAL) > trySimplifyGoal True g = simplifyGoal True g <|> > (neutralise =<< getCurrentDefinition) > trySimplifyGoal False g = simplifyGoal False g <|> (do > g' <- bquoteHere g > es <- getEntriesAbove > cursorAboveLambdas > make ("tsg" :<: liftType es g') > goIn > let rs = paramREFs es > traverse (lambdaParam . refNameAdvice) rs > x :=>: xv <- getCurrentDefinition > goOut > let z = x $## map NP rs > return$ N z :=>: evTm z > ) We implement the simplification steps in |simplifyGoal|. This takes a boolean parameter indicating whether simplification is at the top level, and a type being simplified. It will return a term and value of that type (which might be the current hole). > simplifyGoal :: Bool -> TY -> ProofState (INTM :=>: VAL) Functions from the unit type are simply constants, so we simplify them as such. > simplifyGoal b (PI UNIT t) = do > simpTrace "PI UNIT" > x :=>: xv <- trySimplifyGoal False (t $$A VOID) > topWrap b  LK x :=>: LK xv Given a function from a \Sigma-type, we can split it into its components. \adam{we should not automatically split if this parameter belongs to the user (i.e. appears in a programming problem).} > simplifyGoal b (PI (SIGMA d r) t) = do > simpTrace "PI SIGMA" > let mt = PI d . L  (fortran r) :. [.a. > PI (r - [NV a]) . L  (fortran t) :. [.b. > t - [PAIR (NV a) (NV b)] ] ] > x :=>: xv <- simplifyGoal False mt > ex <- annotate x mt > let body = N (ex : A (N (V 0 : Fst)) : A (N (V 0 : Snd))) > topWrap b  L ("ps" :. body) :=>: L ("ps" :. body) Similarly, if we have a function from an enumeration, we can split it into its branches. \adam{we should not do this automatically at all, but we need to modify the induction principles generated for data types first. For the moment, we check the enumeration is completely canonical, thereby avoiding the worst problems with this simplification step.} > simplifyGoal b (PI (ENUMT e) t) | checkTags e = do > simpTrace "PI ENUMT" > x :=>: xv <- trySimplifyGoal False (branchesOp @@ [e, t]) > e' <- bquoteHere e > t' <- bquoteHere t > let body = N (switchOp :@ [e', NV 0, t', x]) > topWrap b  L ("pe" :. body) :=>: L ("pe" :. body) > where > checkTags :: VAL -> Bool > checkTags NILE = True > checkTags (CONSE _ e) = checkTags e > checkTags _ = False If we have a function from a proof, we call on propositional simplification to help out. If the proposition is absurd we win, and if it simplifies into a conjunction we abstract over each conjunct individually. If the proposition cannot be simplified, we check to see if it is an equation with a variable on one side, and if so, eliminate it by |substEq|. Otherwise, we just put it in the context and carry on. Note that this assumes we are at the top level. > simplifyGoal True (PI (PRF p) t) = do > simpTrace "PI PRF" > pSimp <- runPropSimplify p > maybe (elimEquation p t <|> passHypothesis t) (simplifyProp p t) pSimp > where > elimEquation :: VAL -> VAL -> ProofState (INTM :=>: VAL) > elimEquation (EQBLUE (_X :>: x) (_Y :>: NP y@(yn := DECL :<: _))) t = do > guard =<< (withNSupply  equal (SET :>: (_X, _Y))) > t' <- bquoteHere t > guard  y elem t' > simpTrace  "elimSimp: " ++ show yn > q <- lambdaParam "qe" > _X' <- bquoteHere _X > x' <- bquoteHere x > let ety = PI (ARR _X SET)  L  "P" :. [._P. > ARR (N (V _P : A x')) (N (V _P : A (NP y))) > ] > ex = P substEq : A _X' : A x' : A (NP y) : A (NP q) > elimSimplify (ety :>: ex) > neutralise =<< getCurrentDefinition > elimEquation (EQBLUE (_Y :>: NP y@(yn := DECL :<: _)) (_X :>: x)) t = do > guard =<< (withNSupply  equal (SET :>: (_X, _Y))) > t' <- bquoteHere t > guard  y elem t' > simpTrace  "elimSimp: " ++ show yn > q <- lambdaParam "qe" > _X' <- bquoteHere _X > x' <- bquoteHere x > let ety = PI (ARR _X SET)  L  "P" :. [._P. > ARR (N (V _P : A x')) (N (V _P : A (NP y))) > ] > ex = P substEq : A _X' : A x' : A (NP y) : A > (N (P symEq : A _X' : A (NP y) : A x' : A (NP q))) > elimSimplify (ety :>: ex) > neutralise =<< getCurrentDefinition > elimEquation _ _ = (|) > > simplifyProp :: VAL -> VAL -> Simplify -> ProofState (INTM :=>: VAL) > simplifyProp p t (SimplyAbsurd prf) = do > r <- lambdaParam (fortran t) > t' <- bquoteHere t > t'' <- annotate t' (ARR (PRF p) SET) > neutralise =<< give (N (nEOp :@ [prf (P r), N (t'' : A (NP r))])) > simplifyProp p t (SimplyTrivial prf) = do > x :=>: xv <- trySimplifyGoal False (t$$ A (evTm prf)) > neutralise =<< give (LK x) > > simplifyProp p t (SimplyOne (qr :<: qst) g h) = do > t' <- bquoteHere t > t'' <- annotate t' (ARR (PRF p) SET) > let q = PIV (fortran t) qst (N (t'' :$A ((B0 :< qr) -|| h))) > x :=>: xv <- trySimplifyGoal False (evTm q) > let y = x ?? q > r <- lambdaParam (fortran t) > neutralise =<< give (N (y :$ A (g (P r)))) > > simplifyProp p t (Simply qs gs h) = do > t' <- bquoteHere t > t'' <- annotate t' (ARR (PRF p) SET) > let q = dischargePi qs (N (t'' :$A h)) > x :=>: xv <- trySimplifyGoal False (evTm q) > let y = x ?? q > r <- lambdaParam (fortran t) > let gs' = fmap ($ (P r)) gs > neutralise =<< give (N (y $## gs')) Otherwise, we simplify$\Pi$-types by introducing a hypothesis, provided we are at the top level. > simplifyGoal True (PI s t) = do > simpTrace "PI top" > passHypothesis t To simplify a$\Pi$-type when not at the top level, we have to create a subgoal. > simplifyGoal False g@(PI _ _) = do > simpTrace "PI not" > g' <- bquoteHere g > es <- getEntriesAbove > cursorAboveLambdas > make ("pig" :<: liftType es g') > goIn > let rs = paramREFs es > traverse (lambdaParam . refNameAdvice) rs > _ :=>: ty <- getHoleGoal > simplifyGoal True ty > x :=>: xv <- getCurrentDefinition > goOut > let z = x$## map NP rs > return $N z :=>: evTm z When the goal is a proof of a proposition, and we are at the top level, we can just invoke propositional simplification... > simplifyGoal True (PRF p) = do > simpTrace "PRF top" > propSimplifyHere > getCurrentDefinition >>= neutralise ...and if we are not at the top level, we create a subgoal. > simplifyGoal False g@(PRF _) = do > simpTrace "PRF not" > g' <- bquoteHere g > make ("prg" :<: g') > goIn > x :=>: xv <- simplifyGoal True g > goOut > return$ x :=>: xv If the goal is a programming problem to produce a proof, and the proposition is trivial, then we win. However, we cannot simplify non-trivial propositions as the user might not want us to. Similarly, we cannot simplify inside |LABEL| unless we know we are going to solve the goal completely. > simplifyGoal b (LABEL _ (PRF p)) = do > pSimp <- runPropSimplify p > case pSimp of > Just (SimplyTrivial prf) -> do > topWrap b $LRET prf :=>: LRET (evTm prf) > _ -> (|) If the goal is a$\Sigma\$-type, we might as well split it into its components. > simplifyGoal b (SIGMA s t) = do > simpTrace "SIGMA" > stm :=>: sv <- trySimplifyGoal False s > ttm :=>: tv <- trySimplifyGoal False (t $$A sv) > topWrap b  PAIR stm ttm :=>: PAIR sv tv If we are really lucky, the goal is trivial and we win. > simplifyGoal b UNIT = topWrap b  VOID :=>: VOID > simplifyGoal b (LABEL _ UNIT) = topWrap b  LRET VOID :=>: LRET VOID Otherwise, we cannot simplify the problem. > simplifyGoal _ _ = throwError'  err "simplifyGoal: cannot simplify" When at the top level and simplifying a \Pi-type, |passHypothesis| introduces a hypothesis into the context and continues simplifying. Its argument is the codomain function of the \Pi-type. > passHypothesis :: VAL -> ProofState (INTM :=>: VAL) > passHypothesis t = do > ref <- lambdaParam (fortran t) > trySimplifyGoal True (t$$ A (NP ref)) The |elimSimplify| command invokes elimination with a motive, simplifies the methods, then returns to the original goal. > elimSimplify :: (TY :>: EXTM) -> ProofState () > elimSimplify tt = do > methods <- elim Nothing tt > simpTrace "Eliminated!" > toFirstMethod > replicateM_ (length methods) (optional problemSimplify >> goDown) > goOut > cursorAboveLambdas :: ProofState () > cursorAboveLambdas = do > es <- getEntriesAbove > case paramREFs es of > [] -> return () > _ -> cursorUp >> cursorAboveLambdas > import -> CochonTactics where > : nullaryCT "simplify" (problemSimplify >> optional seekGoal >> return "Simplified.") > "simplify - simplifies the current problem."