problem with Qed's simplification power
ID0002278: This issue was created automatically from Mantis Issue 2278. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002278 | Frama-C | Plug-in > wp | public | 2017-02-06 | 2017-02-06 |
| Reporter | Jochen | Assigned To | correnson | Resolution | open |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | Silicon-20161101 | OS | Ubuntu 16.04.1 LTS | OS Version | - |
| Product Version | Frama-C 14-Silicon | Target Version | - | Fixed in Version | - |
Description :
Running "frama-c -wp -wp-out wp-out shift.c" on the attached file and inspecting the file "wp-out/typed/foo_post_Alt-Ergo.mlw" shows that lemma "ShiftAssociative" is simplified to "true" (see line 360) by Qed. (The postcondition of foo doesn't matter here, except that it is intentionally unprovable in order to demonstrate the lemma's simplification.)
This situation doesn't change even when all options to disable Qed functionality (i.e. "-wp-no-bits -wp-no-clean -wp-no-core -wp-no-filter -wp-no-init-summarize-array -wp-no-let -wp-no-pruning -wp-no-simpl -wp-no-simplify-forall -wp-no-simplify-is-cint -wp-no-simplify-type") are given. (In contrast, in the somewhat related issue #1751, providing option "-wp-no-bits" is sufficient to circumvent the problem.)
While Qed's simplification capabilities are appreciated in general, the disappearance of the lemma can be a problem:
- In many Coq proofs related to C address computation, a similar lemma has to be stated and proven again and again. There seems to be no easy way to make Coq see what is considered trivial by Qed.
- Considering the discussion at https://github.com/OCamlPro/alt-ergo/issues/19, if I understood the Alt-Ergo people right, Alt-Ergo isn't complete on linear arithmetic with arrays (except for quantifier-free formulas). Therefore it sometimes needs trivial lemmas. In the particular example, to make Alt-Ergo prove the goal "reverse", a kind of associtivity property (axiom "arith") is needed that Qed would simplify also to "true", and even Alt-Ergo would.
Generally speaking, Qed should be (configurable such that it is) no stronger than any of the external provers, such as Coq and Alt-Ergo. This would enable the user to provide appropriate prover hints that are not simplified away by Qed. Maybe a command line option to completely switch off Qed is sufficient. As an alternative, a command-line switch could reduce the capabilities of Qed when applied to lemmas, assuming that the user is responsible to give them in an optimal form.