2021-03-03 04:05 CET

View Issue Details Jump to Notes ]
IDProjectCategoryView StatusLast Update
0002100Frama-CPlug-in > wppublic2019-10-17 18:03
Assigned Tocorrenson 
StatusclosedResolutionwon't fix 
Product VersionFrama-C Sodium 
Target VersionFixed in Version 
Summary0002100: readability of coq(?) names
DescriptionConsider 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:

  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

  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 Reproduceframa-c-gui -wp lemma.c
TagsNo tags attached.
Attached Files
  • c file icon lemma.c (70 bytes) 2015-03-31 17:15 -
        lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b;
    c file icon lemma.c (70 bytes) 2015-03-31 17:15 +

related to 0002153acknowledgedcorrenson bound variable names in Coq file depend on unrelated function later in C source code 



jens (reporter)

I wonder whether this is related to my previous request for "better" coq names...



jens (reporter)

The "obfuscated" names generated by WP make it quite hard to work on coq proofs for functions with several arguments.

Would it be possible to return to the naming scheme of Neon?


correnson (manager)

No it is not that easy. We need to find a solution to keep user names while still preserving our new very efficient locally-nameless implementation of binders in Qed...


correnson (manager)

We plan de completely rewrite the Coq output of goals to make them more readable.


Jochen (reporter)

I suspect that the (different) renaming (in lemmas and goals) even may lead to a worse verification rate, cf. issue 0002329 for details.


correnson (manager)

Coq output is now deprecated and will be abandoned in future releases.

-Issue History
Date Modified Username Field Change
2015-03-31 17:15 jens New Issue
2015-03-31 17:15 jens Status new => assigned
2015-03-31 17:15 jens Assigned To => correnson
2015-03-31 17:15 jens File Added: lemma.c
2015-03-31 17:21 jens Note Added: 0005837
2015-04-10 10:39 jens Note Added: 0005877
2015-04-10 11:16 correnson Note Added: 0005879
2015-06-29 17:16 correnson Note Added: 0005961
2015-06-29 17:16 correnson Status assigned => acknowledged
2015-09-01 12:03 correnson Relationship added related to 0002153
2017-10-09 17:19 Jochen Note Added: 0006465
2019-10-17 17:36 correnson Note Added: 0006913
2019-10-17 17:36 correnson Status acknowledged => resolved
2019-10-17 17:36 correnson Resolution open => won't fix
2019-10-17 18:03 signoles Status resolved => closed
+Issue History