Specification of term simplification

[let-def]

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:

• in the config state, simplify is disabled by default https://github.com/verifast/verifast/blob/master/src/vfide.ml#L170
• in the ui state, it is enabled by default https://github.com/verifast/verifast/blob/master/src/vfide.ml#L266
  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 or Right 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:

• as a proof-of-concept, I implemented removal of redundant assumptions in the window; for now it is as stupid as filtering duplicate strings, but thanks to the normalization done by simplification it proved quite useful in my tests
• split conjunctions (e.g turning 0 < x && 0 < y into two assumptions 0 < x; 0 < y) to bring more duplicate filtering opportunities
• substitutions of trivial equalities (the subst tactic of Coq), e.g when there is an assumption of the form a == b (a, b being variables), rewrite all occurrences of b by a in other assumptions
• introducing let 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 :)).

[rafoo]

The prover combiner as a slightly suprising behavior for simplification.

I implemented that, here is the definition:

method simplify = function
 | Left x ->
    begin match p1#simplify x with Some xx -> Some (Left xx) | None -> None end
 | Right y ->
    begin match p2#simplify y with Some yy -> Some (Right yy) | None -> None end
 | Both (x, y) ->
    begin match (p1#simplify x, p2#simplify y) with
    | (Some xx, Some yy) -> Some (Both (xx, yy))
    | (Some xx, None) -> Some (Left xx)
    | (None, Some yy) -> Some (Right yy)
    | (None, None) -> None
    end

If I understand well, you suggest to replace these two cases:

| (Some xx, None) -> Some (Left xx)
| (None, Some yy) -> Some (Right yy)

by Some (Both (xx, y)) and Some (Both (x, yy)) respectively.

I have to admit that I did not look at what simplification was about when I wrote this. A quick git grep taught me it was about the way terms are printed and if simplify t returns None, it makes no difference with the case where simplify t returns Some t; Verifast does not use the extra bit of information.

[let-def]

@rafoo Yes, that's one way.
Or just dropping the notion of option from the simplify method, behaving like the identity when nothing could be simplified.
Alternatively returning a list of terms which together are equivalent to the term being simplified:

• empty list when the term is a tautology
• one or more simpler elements when the term can be split (the conjunction case above).
  Simplification is not used in the rest of verifast as far as I can see, only for pretty-printing.