The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Jason,

 

I attached a minimal example.

 

It contains the definition of a dependently defined cyclic type with two implementations for add.

 

The second (more efficient) definition actually uses the information that the inputs are within bounds to derive that the result is in bounds. But because this way the proofs of the inputs are parameters of the proof for the result, the (expanded) proof term grows exponentially with computation depth. The first definition of add, which doesn’t use the boundedness of the inputs, does not have this problem.

 

The idea of opaquify is to make the proof term opaque, since its inner structure should never be of interest. Automation would likely profit from this in terms of performance.

 

@all: is there a smarter way to define add' which would avoid this issue?

 

Best regards,

 

Michael

 

Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928

Attachment: Opaquify.v
Description: Opaquify.v