Frama-C Bug Tracking System - Frama-C
View Issue Details
0002100Frama-CPlug-in > wppublic2015-03-31 17:152017-10-09 17:19
Frama-C Sodium 
0002100: readability of coq(?) names
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.
frama-c-gui -wp lemma.c
No tags attached.
related to 0002153acknowledged correnson bound variable names in Coq file depend on unrelated function later in C source code 
c lemma.c (70) 2015-03-31 17:15
Issue History
2015-03-31 17:15jensNew Issue
2015-03-31 17:15jensStatusnew => assigned
2015-03-31 17:15jensAssigned To => correnson
2015-03-31 17:15jensFile Added: lemma.c
2015-03-31 17:21jensNote Added: 0005837
2015-04-10 10:39jensNote Added: 0005877
2015-04-10 11:16corrensonNote Added: 0005879
2015-06-29 17:16corrensonNote Added: 0005961
2015-06-29 17:16corrensonStatusassigned => acknowledged
2015-09-01 12:03corrensonRelationship addedrelated to 0002153
2017-10-09 17:19JochenNote Added: 0006465

2015-03-31 17:21   
I wonder whether this is related to my previous request for "better" coq names...
2015-04-10 10:39   
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?
2015-04-10 11:16   
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...
2015-06-29 17:16   
We plan de completely rewrite the Coq output of goals to make them more readable.
2017-10-09 17:19   
I suspect that the (different) renaming (in lemmas and goals) even may lead to a worse verification rate, cf. issue #2329 for details.