-
Notifications
You must be signed in to change notification settings - Fork 62
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Specification of term simplification #122
Comments
I implemented that, here is the definition:
If I understand well, you suggest to replace these two cases:
by I have to admit that I did not look at what simplification was about when I wrote this. A quick |
@rafoo Yes, that's one way.
|
Basic redux simplification and pretty-printing
I have played around with the simplify terms feature in a branch of mine. I implemented basic simplification for Redux, with the following rewriting:
0 + x = x
,0 * x = 0
,1 * x = x
,not (a < b) = b <= a
,not (not x) = x
, modulo associativity of+
and*
, constant folding. I also extended Pretty-printing to make use of associavity and precedence to minimize the number of parentheses.If people are interested, I can clean this code and turn it into a PR, however I have a few questions about the intended behavior of simplify.
Incorrect UI state
There is a mistake in the IDE:
So by default the UI shows that simplify will happen while it is not the case and one needs to toggle it twice to actually enable simplification.
Combiner simplification
The prover combiner as a slightly suprising behavior for simplification.
The simplification function returns an option (to notify the IDE that simplification succeded as far as I understand).
The combiner is an higher-order prover: it takes two provers, and its terms are terms of one of the provers (
Left prover1_term
orRight prover2_term
) or terms of each (Both (term1, term2)
).The simplification function of the combiner keeps the terms that were successfully simplified by their respective prover. So if one prover doesn't implement simplification, terms are simply dropped.
For instance, using Redux+Z3v4.5, consider the assumption:
<(0 < x); (< 0 x)>
, because Redux doesn't implement simplification the left side is simply dropped during printing:<; (< 0 x)>
.Shouldn't simplification amount to being identity in those cases? (and the
option
could be dropped).Looking forward
I would like to go beyond basic simplification:
0 < x && 0 < y
into two assumptions0 < x
;0 < y
) to bring more duplicate filtering opportunitiessubst
tactic of Coq), e.g when there is an assumption of the forma == b
(a, b being variables), rewrite all occurrences ofb
bya
in other assumptionslet
to represent structural sharing (as suggested in Avoid term pretty-printing exponential blowup #117), maybe the sharing should go beyond a single assertion? (introduce let bindings as separate entries in the assumption list, reuse them in different assertions)If that sounds right to you, I can look at that (in my spare time so I can't guarantee any delivery time, don't wait for me to implement similar features :)).
The text was updated successfully, but these errors were encountered: