coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: "Mark Dickinson" <dickinsm AT gmail.com>
- To: "Matthieu Sozeau" <sozeau AT lri.fr>
- Cc: "Coq Club" <coq-club AT pauillac.inria.fr>
- Subject: Re: [Coq-Club] setoid_rewrite and constant unfolding
- Date: Sun, 9 Nov 2008 20:28:41 +0000
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=message-id:date:from:to:subject:cc:in-reply-to:mime-version :content-type:content-transfer-encoding:content-disposition :references; b=n8VlJ6bSCLHBZFYofW+BdX0E0oZhJDSNnZoArxOBBbwYI5arV6IBRucj/aS2LVd8yH FN8aj0fxedaY6ULqPeBll+phhizZUS+7mOjGwym9fN/GjB37TAlXU9/wLs3mSchzc7v1 A4o2z1K8aj3FDHrrGhj+bj4IwPDA7OSfA17W0=
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
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
- [Coq-Club] setoid_rewrite and constant unfolding, Mark Dickinson
- Re: [Coq-Club] setoid_rewrite and constant unfolding,
Matthieu Sozeau
- Re: [Coq-Club] setoid_rewrite and constant unfolding, Mark Dickinson
- Re: [Coq-Club] setoid_rewrite and constant unfolding,
Matthieu Sozeau
Archive powered by MhonArc 2.6.16.