readability of coq(?) names
ID0002100: This issue was created automatically from Mantis Issue 2100. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002100 | Frama-C | Plug-in > wp | public | 2015-03-31 | 2019-10-17 |
| Reporter | jens | Assigned To | correnson | Resolution | won't fix |
| Priority | normal | Severity | minor | Reproducibility | always |
| Platform | - | OS | - | OS Version | - |
| Product Version | Frama-C Sodium | Target Version | - | Fixed in Version | - |
Description :
Consider the following ACSL lemma:
/@ lemma X : \forall integer a, b; (a+b)(a-b) == aa - bb; */
which is automatically discharged by alt-ergo. When I open the proof obligation in Coq, the lemma looks like follows:
Goal forall (i_1 i : Z), (((i_1 * i_1) = ((i * i) + ((i + i_1) * (i_1 - i))))%Z)%Z.
Under Neon the proof coq representation preserves the original names much better
Goal forall (a_0 b_0 : Z), (((a_0 * a_0) = ((b_0 * b_0) + ((a_0 + b_0) * (a_0 - b_0))))%Z)%Z.
The problem gets worse with more parameters.
Steps To Reproduce :
frama-c-gui -wp lemma.c