The Coq mailing list

["Mark Dickinson" <dickinsm AT gmail.com>]

On Sun, Nov 9, 2008 at 5:30 PM, Matthieu Sozeau 
<sozeau AT lri.fr>
 wrote:

> To quote 18.5.4: "It is useful when some constants prevent some
> unifications and make resolution fail." This is meant for the typeclass
> resolution process. [...]

So I was indeed misreading the manual.  :-)  Thank you for the
explanation.  It's taking me a while to absorb how everything
in Coq fits together.

> On the other hand, [setoid_rewrite] could indeed try a little harder at
> finding an applied homogeneous relation under definitions, like [rewrite]
> does when it tries to find a Leibniz equality. The [setoid_rewrite] tactic
> simply didn't try to reduce the type of the lemma at all if it failed,
> whereas
> [rewrite] did as much beta-delta-iota as needed to find the arity of the
> type
> and search for a relation there. I will fix this in the trunk and 8.2
> branches.
> Your initial proof script will then go through.

Thank you!  As is probably clear from the example script,
I'm trying to formalize some setoid-based abstract algebra
and category theory, so am making fairly heavy use of these
tactics;  for me, this would certainly be yet another small
step towards making proofs easier to write (and read).

Mark