Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] setoid_rewrite and constant unfolding

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] setoid_rewrite and constant unfolding


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page