brianhuffman
commented
3 years ago To implement this, we would need to modify function ruleOfProp from the Rewriter module in saw-core. (This function was most recently modified by GaloisInc/saw-core#112.)
To be able to take a proposition p and return the rewrite rule p = True, we need to be able to construct the term True for the right-hand side. Currently ruleOfProp only takes terms apart, never constructing new ones; that's why it can get away with the non-IO type Term -> Maybe RewriteRule and without a SharedContext argument. We should probably change the type to something like SharedContext -> Term -> IO (Maybe RewriteRule) or SharedContext -> Term -> IO [RewriteRule] to give us maximum flexibility in the future.
Another thing that bothers me about ruleOfProp is that it has the names of several equality operators like boolEq, bvEq, and vecEq hard-coded into it. It would be better if the SharedContext could refer to a set of rules/axioms for turning propositions into equations, and then ruleOfProp could work generically over this set. For example, there would be a rule like (n : Nat) -> (x y : Vec n Bool) -> EqTrue (bvEq n x y) -> Eq (Vec n Bool) x y for bvEq, and if ruleOfProp was given a theorem matching the pattern EqTrue (bvEq _ _ _) then it could be composed with this rule to produce an Eq theorem that could work directly as a rewrite rule.
If ruleOfProp was implemented this way, then we could easily extend ruleOfProp to handle new forms of theorems later, even at runtime.
It would be nice to be able to prove a theorem that is not an equality and interpret it as a rewrite rule that replaces instances of the theorem by
True.