Use entire goal in proof strategy #1936
Conversation
…Rule in CommonProofState
| :: InternalVariable variable | ||
| => RHS variable | ||
| -> Pattern variable | ||
| rhsToPattern RHS { existentials, right, ensures } = |
There was a problem hiding this comment.
This transformation is not valid, it takes
\exists(X, \and(right, ensures))
and turns it into
\and(\exists(X, right), \exists(X, ensures))
The correct thing to do is construct a Pattern using right and ensures, convert that into a TermLike, and call mkExistsN on that TermLike.
There was a problem hiding this comment.
Yes, you're right, the second doesn't imply the first, so they're not equivalent. Thanks!
I noticed that there already is a rhsToTerm which only does some trivial simplification in the case the ensures is \top. Pattern.toTermLike also does this for \bottom. Changing rhsToTerm to use Pattern.fromTermLike made some unit tests fail. Is there any reason we don't use this there? In any case, I just implemented rhsToPattern without using rhsToTerm.
There was a problem hiding this comment.
I think the reason is only that, in some cases, we expect the \and structure of the Pattern to be preserved. Does that answer your question?
| :: InternalVariable variable | ||
| => RHS variable | ||
| -> Pattern variable | ||
| rhsToPattern RHS { existentials, right, ensures } = |
There was a problem hiding this comment.
I think the reason is only that, in some cases, we expect the \and structure of the Pattern to be preserved. Does that answer your question?
Fixes #1918
Reviewer checklist
stack test --coveragestack haddock