# 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) == a*a - b*b;
*/

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