The Coq mailing list

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

Dear Fabian,

 

> Do you have an example where performance is degenerating because of this … ?

 

the main issue I see is with “match goal” constructs with context. I make heavy use of automation and Ltac and use this frequently to decide if it makes sense to apply a certain lemma or not. I would think that any context search would go into the proof term and I don’t see how Maximilian’s approach would prevent this.

Of cause I can give Argument options to prevent cbn or simpl from ever expanding opaque, but the complete term is still there in the argument list of opaque, so a context search would go into it even without expanding opaque. Btw.: I am not sure how context search is influenced by implicit arguments – I need to check, but I guess not at all.

 

For unification I don’t know if I have issues, but I also don’t think that Maximilian’s proposal makes a difference here. It is good for controlling what is printed, but I think that’s it, and as far as I understood this is also what Maximilian claims his proposal does.

 

But in general my experience with automation is: if there is some path you don’t want automation to follow and if you are sure you don’t need this path, close the gate to this path.

 

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