0002100: readability of coq(?) names - Frama-C Bug Tracking System

View Issue Details [ Jump to Notes ]

[ Issue History ] [ Print ]

Project

Category

View Status

Date Submitted

Last Update

0002100

Frama-C

Plug-in > wp

public

2015-03-31 17:15

2017-10-09 17:19

Reporter

jens

Assigned To

correnson

Priority

normal

Severity

minor

Reproducibility

always

Status

acknowledged

Resolution

open

Platform

OS Version

Product Version

Frama-C Sodium

Target Version

Fixed in Version

Summary

0002100: readability of coq(?) names

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

Tags

No tags attached.

Attached Files

lemma.c [^] (70 bytes) 2015-03-31 17:15 [Show Content] [Hide Content]

/*@
    lemma X : \forall integer a, b; (a+b)*(a-b) == a*a - b*b;
*/

Relationships

related to

0002153

acknowledged

correnson

bound variable names in Coq file depend on unrelated function later in C source code

Notes
(0005837) jens (reporter) 2015-03-31 17:21	I wonder whether this is related to my previous request for "better" coq names... https://bts.frama-c.com/view.php?id=1630 [^]

(0005877) jens (reporter) 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?

(0005879) correnson (manager) 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...

(0005961) correnson (manager) 2015-06-29 17:16	We plan de completely rewrite the Coq output of goals to make them more readable.

(0006465) Jochen (reporter) 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 0002329 for details.

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