The Coq mailing list

[Fabian Kunze <kunze AT ps.uni-saarland.de>]

Hello Michael,

Do you have an example where performance is degenerating because of this (except for printing)? It seems to me that the approach proposed by Maximilian will lead to coq never looking into the proof during unification. And I was under the impression that sharing will be used by coq to only evaluate the proof term once, even when repeated multiple times.

Best,

Fabian

Soegtrop, Michael <michael.soegtrop AT intel.com> schrieb am Mi., 16. Mai 2018 um 12:05 Uhr:

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