From c77129cc8867ee7f614135df7a4c9a1fa41d77f5 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 7 Feb 2022 15:32:57 -0800
Subject: [PATCH 1/4] Add a `goal_exact` tactic that proves a goal by directly
 providing a proof term.  This is similar to the `core_thm` operator, but in
 the context of a `ProofScript` instead of at top-level.

---
 src/SAWScript/Builtins.hs    |  5 +++++
 src/SAWScript/Interpreter.hs |  8 ++++++++
 src/SAWScript/Proof.hs       | 15 +++++++++++++++
 3 files changed, 28 insertions(+)

diff --git a/src/SAWScript/Builtins.hs b/src/SAWScript/Builtins.hs
index cb687716e5..d9c2244a42 100644
--- a/src/SAWScript/Builtins.hs
+++ b/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
diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 3553afac37..76cfdda7dc 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/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
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 4eec6901a1..7b6591b395 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -68,6 +68,7 @@ module SAWScript.Proof
   , tacticId
   , tacticChange
   , tacticSolve
+  , tacticExact
 
   , Quantification(..)
   , predicateToProp
@@ -1132,6 +1133,20 @@ tacticTrivial _sc = Tactic \goal ->
   else
     fail "trivial tactic: not a trivial goal"
 
+
+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 False 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.
 tacticId :: Monad m => (ProofGoal -> m ()) -> Tactic m ()

From 7e61b9131e80c6ce5faf4e6c2f872a2b280f098c Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 7 Feb 2022 16:09:06 -0800
Subject: [PATCH 2/4] Enhance the `trivial` tactic so that it can prove
 instances of reflexivity that it can deduce from conversion.

---
 src/SAWScript/Interpreter.hs |  8 +++--
 src/SAWScript/Proof.hs       | 57 ++++++++++++++++++------------------
 2 files changed, 34 insertions(+), 31 deletions(-)

diff --git a/src/SAWScript/Interpreter.hs b/src/SAWScript/Interpreter.hs
index 76cfdda7dc..d948beef22 100644
--- a/src/SAWScript/Interpreter.hs
+++ b/src/SAWScript/Interpreter.hs
@@ -1393,7 +1393,7 @@ primitives = Map.fromList
     , "rule, this will result in zero or more new subgoals."
     ]
 
-  , prim "goal_exact" "Term -> ProofScript ()"
+  , prim "goal_exact"          "Term -> ProofScript ()"
     (pureVal goal_exact)
     Experimental
     [ "Prove the current goal by giving an explicit proof term."
@@ -1666,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)
diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 7b6591b395..56cd99b590 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -24,7 +24,6 @@ module SAWScript.Proof
   , termToProp
   , propToTerm
   , propToRewriteRule
-  , propIsTrivial
   , propSize
   , prettyProp
   , ppProp
@@ -254,16 +253,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
@@ -397,10 +401,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.
@@ -715,7 +715,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
@@ -758,13 +758,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
@@ -1127,18 +1120,24 @@ 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 False gp ty
+     ok <- liftIO $ scConvertible sc True gp ty
      unless ok $ fail $ unlines
          [ "Proof term does not prove the required proposition"
          , showTerm gp

From f502ddb679072338531c098d56f2b667ecb808d7 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 7 Feb 2022 16:31:09 -0800
Subject: [PATCH 3/4] Tweak the error message for `termToProp` to provide a
 hint to the user if the leading term is a lambda. The hint suggests to change
 the lambdas to Pis.

---
 src/SAWScript/Proof.hs | 10 +++++++++-
 1 file changed, 9 insertions(+), 1 deletion(-)

diff --git a/src/SAWScript/Proof.hs b/src/SAWScript/Proof.hs
index 56cd99b590..906c92ddee 100644
--- a/src/SAWScript/Proof.hs
+++ b/src/SAWScript/Proof.hs
@@ -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

From c6d17896d2b0890649e21461aa223b15a5b91879 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Mon, 7 Feb 2022 16:36:22 -0800
Subject: [PATCH 4/4] Update manual

---
 doc/manual/manual.md | 11 +++++++++--
 1 file changed, 9 insertions(+), 2 deletions(-)

diff --git a/doc/manual/manual.md b/doc/manual/manual.md
index f06f234ad6..fc50d60a4b 100644
--- a/doc/manual/manual.md
+++ b/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`.