Merge pull request #1568 from GaloisInc/tactic-tweaks

Tactic tweaks

doc/manual/manual.md

@@ -1304,8 +1304,10 @@ development, or as a way to provide some evidence for the validity of a
 specification believed to be true but difficult or infeasible to prove.
 
 * `trivial : ProofScript ()` states that the current goal should
-be trivially true (i.e., the constant `True` or a function that
-immediately returns `True`). It fails if that is not the case.
+be trivially true. This tactic recognizes instances of equality
+that can be demonstrated by conversion alone. In particular
+it is able to prove `EqTrue x` goals where `x` reduces to
+the constant value `True`. It fails if this is not the case.
 
 ## Multiple Goals
 
@@ -1331,6 +1333,11 @@ variable in the current proof goal, returning the variable as a `Term`.
 * `goal_when : String -> ProofScript () -> ProofScript ()` will run the
 given proof script only when the goal name contains the given string.
 
+* `goal_exact : Term -> ProofScript ()` will attempt to use the given
+term as an exact proof for the current goal. This tactic will succeed
+whever the type of the given term exactly matches the current goal,
+and will fail otherwise.
+
 * `split_goal : ProofScript ()` will split a goal of the form
 `Prelude.and prop1 prop2` into two separate goals `prop1` and `prop2`.
 

src/SAWScript/Builtins.hs

@@ -629,6 +629,11 @@ goal_apply thm =
   do sc <- SV.scriptTopLevel getSharedContext
      execTactic (tacticApply sc thm)
 
+goal_exact :: TypedTerm -> ProofScript ()
+goal_exact tm =
+  do sc <- SV.scriptTopLevel getSharedContext
+     execTactic (tacticExact sc (ttTerm tm))
+
 goal_assume :: ProofScript Theorem
 goal_assume =
   do sc <- SV.scriptTopLevel getSharedContext

src/SAWScript/Interpreter.hs

@@ -1392,6 +1392,14 @@ primitives = Map.fromList
     [ "Apply an introduction rule to the current goal. Depending on the"
     , "rule, this will result in zero or more new subgoals."
     ]
+
+  , prim "goal_exact"          "Term -> ProofScript ()"
+    (pureVal goal_exact)
+    Experimental
+    [ "Prove the current goal by giving an explicit proof term."
+    , "This will succeed if the type of the given term matches the current goal."
+    ]
+
   , prim "goal_assume"         "ProofScript Theorem"
     (pureVal goal_assume)
     Experimental
@@ -1658,7 +1666,11 @@ primitives = Map.fromList
   , prim "trivial"             "ProofScript ()"
     (pureVal trivial)
     Current
-    [ "Succeed only if the proof goal is a literal 'True'." ]
+    [ "Succeeds if the goal is trivial. This tactic recognizes goals"
+    , "that are instances of reflexivity, possibly with quantified variables."
+    , "In particular, it will prove goals of the form 'EqTrue x' when 'x' reduces"
+    , "to the constant value 'True'."
+    ]
 
   , prim "w4"                  "ProofScript ()"
     (pureVal w4_z3)

src/SAWScript/Proof.hs

@@ -24,7 +24,6 @@ module SAWScript.Proof
   , termToProp
   , propToTerm
   , propToRewriteRule
-  , propIsTrivial
   , propSize
   , prettyProp
   , ppProp
@@ -68,6 +67,7 @@ module SAWScript.Proof
   , tacticId
   , tacticChange
   , tacticSolve
+  , tacticExact
 
   , Quantification(..)
   , predicateToProp
@@ -145,7 +145,15 @@ termToProp sc tm =
       ty <- scTypeOf sc tm
       case evalSharedTerm mmap mempty mempty ty of
         TValue (VSort s) | s == propSort -> return (Prop tm)
-        _ -> fail $ unlines [ "termToProp: Term is not a proposition", showTerm tm, showTerm ty ]
+        _ ->
+          case asLambda tm of
+            Just _ ->
+              fail $ unlines [ "termToProp: Term is not a proposition."
+                             , "Note: the given term is a lambda; try using Pi terms instead."
+                             , showTerm tm, showTerm ty
+                             ]
+            Nothing ->
+              fail $ unlines [ "termToProp: Term is not a proposition", showTerm tm, showTerm ty ]
 
 
 -- | Turn a boolean-valued saw-core term into a proposition by asserting
@@ -253,16 +261,21 @@ falseProp sc = Prop <$> (scEqTrue sc =<< scApplyPrelude_False sc)
 propSize :: Prop -> Integer
 propSize (Prop tm) = scSharedSize tm
 
--- | Test if the given proposition is trivially true.  This holds
---   just when the proposition is a (possibly empty) sequence of
---   Pi-types followed by an @EqTrue@ proposition for a
---   concretely-true boolean value.
-propIsTrivial :: Prop -> Bool
-propIsTrivial (Prop tm) = checkTrue tm
+trivialProofTerm :: SharedContext -> Prop -> IO (Either String Term)
+trivialProofTerm sc (Prop p) = runExceptT (loop =<< lift (scWhnf sc p))
   where
-    checkTrue :: Term -> Bool
-    checkTrue (asPiList -> (_, asEqTrue -> Just (asBool -> Just True))) = True
-    checkTrue _ = False
+    loop (asPi -> Just (nm, tp, tm)) =
+      do pf <- loop =<< lift (scWhnf sc tm)
+         lift $ scLambda sc nm tp pf
+
+    loop (asEq -> Just (tp, x, _y)) =
+      lift $ scCtorApp sc "Prelude.Refl" [tp, x]
+
+    loop _ = throwError $ unlines
+               [ "The trivial tactic can only prove quantified equalities, but"
+               , "the given goal is not in the correct form."
+               , showTerm p
+               ]
 
 -- | Pretty print the given proposition as a string.
 prettyProp :: PPOpts -> Prop -> String
@@ -396,10 +409,6 @@ data Evidence
     --   user's direction.
   | Admitted Text Pos Prop
 
-    -- | This type of evidence is produced when a given proposition is trivially
-    --   true.
-  | TrivialEvidence
-
     -- | This type of evidence is produced when a proposition can be deconstructed
     --   along a conjunction into two subgoals, each of which is supported by
     --   the included evidence.
@@ -714,7 +723,7 @@ checkEvidence sc db = \e p -> do hyps <- Map.keysSet <$> readIORef (theoremMap d
     check hyps e p@(Prop ptm) = case e of
       ProofTerm tm ->
         do ty <- scTypeCheckError sc tm
-           ok <- scConvertible sc False ptm ty
+           ok <- scConvertible sc True ptm ty
            unless ok $ fail $ unlines
                [ "Proof term does not prove the required proposition"
                , showTerm ptm
@@ -757,13 +766,6 @@ checkEvidence sc db = \e p -> do hyps <- Map.keysSet <$> readIORef (theoremMap d
                ]
            return (mempty, TestedTheorem n)
 
-      TrivialEvidence ->
-        do unless (propIsTrivial p) $ fail $ unlines
-             [ "Proposition is not trivial"
-             , showTerm ptm
-             ]
-           return mempty
-
       SplitEvidence e1 e2 ->
         splitProp sc p >>= \case
           Nothing -> fail $ unlines
@@ -1126,11 +1128,31 @@ tacticSplit sc = Tactic \(ProofGoal num ty name prop) ->
 
 -- | Attempt to solve a goal by recognizing it as a trivially true proposition.
 tacticTrivial :: (F.MonadFail m, MonadIO m) => SharedContext -> Tactic m ()
-tacticTrivial _sc = Tactic \goal ->
-  if (propIsTrivial (goalProp goal)) then
-    return ((), mempty, [], leafEvidence TrivialEvidence)
-  else
-    fail "trivial tactic: not a trivial goal"
+tacticTrivial sc = Tactic \goal ->
+  liftIO (trivialProofTerm sc (goalProp goal)) >>= \case
+    Left err -> fail err
+    Right pf ->
+       do let gp = unProp (goalProp goal)
+          ty <- liftIO $ scTypeCheckError sc pf
+          ok <- liftIO $ scConvertible sc True gp ty
+          unless ok $ fail $ unlines
+            [ "The trivial tactic cannot prove this equality"
+            , showTerm gp
+            ]
+          return ((), mempty, [], leafEvidence (ProofTerm pf))
+
+tacticExact :: (F.MonadFail m, MonadIO m) => SharedContext -> Term -> Tactic m ()
+tacticExact sc tm = Tactic \goal ->
+  do let gp = unProp (goalProp goal)
+     ty <- liftIO $ scTypeCheckError sc tm
+     ok <- liftIO $ scConvertible sc True gp ty
+     unless ok $ fail $ unlines
+         [ "Proof term does not prove the required proposition"
+         , showTerm gp
+         , showTerm tm
+         ]
+     return ((), mempty, [], leafEvidence (ProofTerm tm))
+
 
 -- | Examine the given proof goal and potentially do some work with it,
 --   but do not alter the proof state.