The Coq mailing list

[Freek Wiedijk <freek AT cs.kun.nl>]

Dear Benjamin,

>In John Harrison's terminology, this would mean introducing
>a little piece of declarative proof-style, in coq's
>overhelmingly procedural style

Exactly!  Thank you for pointing this out.  My way to look at
proof checking happens to be very declarative, I don't know
why (the "Step" tactic we use here for equational reasoning
also is the declarative way to do that.)  Unfortunately for
me, almost all major systems that I know of seem to be
procedural :-)

>Then, the next step is probably to have the search in the
>environment being done modulo some isomorphisms over the
>type/proposition, in the style of the searchiso facility.

I don't think I need anything like this for the application
that I had in mind.

>All this obviously raises questions of efficiency

That was my original question.  I don't think I need
convertibility, if that helps.  But looking at the parameters
and definitions would be real nice.  However, if that's too
hard, with a sufficient number of "lets" (or "Cuts", in a
procedural situation :-)) I can pull them into the local
context of my expression, so even that is not _really_
necessary.

>So I would advocate to be careful and propose a feature
>as modest as possible, if it appears necessary.

Ah.  I think hardly _anything_ in life is really necessary :-)
But having this feature might make the stuff I do quite a bit
more readable.  (And maybe it would make it much slower too.)

Freek