coq-club AT inria.fr
Subject: The Coq mailing list
List archive
Re: [Coq-Club] Confusing error rewriting by impl with result in propositional with parameter
chronological Thread
- From: Matthieu Sozeau <mattam AT mattam.org>
- To: brandon_m_moore AT yahoo.com
- Cc: coq-club AT inria.fr
- Subject: Re: [Coq-Club] Confusing error rewriting by impl with result in propositional with parameter
- Date: Tue, 7 Jun 2011 14:09:59 +0200
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=nY4/LW31jk+vAOoDaVxWo2BQm4MQMpoGazi+mYJy9+yLK6p9bH5PweqXlWxvZBGCRn rflFK9TsDNCJqUu+JinFjJ3UlySnuyxZOynwStKCqgmHYMDJhK4Z2ZCsKDDaOQ1GGvCb eoo6f12nojyw8SRI3DAJKmZmFMSg+yOJson5U=
Le 2 juin 2011 à 23:04,
brandon_m_moore AT yahoo.com
a écrit :
> I'm trying to use setoid rewriting over impl to simplify hypotheses.
> It usually works fine, but if the conclusion of the implication is
> an equality or similarly defined inductive type, there are problems.
>
> rewriting in * |- always seems to fail, by encountering a fatal error
> when deciding whether the rule can be used to rewrite in a type
> like Z in a hypothesis like (p : Z).
Hello Brandon,
indeed the error should not be fatal for a [rewrite in * |-], it
was an overlook, now fixed in the trunk. One unpractical workaround
would be to make "impl" opaque before the rewrite (using [Opaque impl]).
Another one would be to use an inductive definition like:
Record implication (A B : Prop) : Prop := mkImpl { impl_proof : A -> B }.
Instance: subrelation implication impl.
Proof. intros x y [H]. assumption. Qed.
Parameter breaks : forall a b, implication (Zeq_bool a b = true) (a = b).
Lemma examples p q : Zeq_bool p q = true -> True.
Proof. intro H. rewrite breaks in *. constructor. Qed.
-- Matthieu
- [Coq-Club] Confusing error rewriting by impl with result in propositional with parameter, brandon_m_moore
- Re: [Coq-Club] Confusing error rewriting by impl with result in propositional with parameter, Matthieu Sozeau
Archive powered by MhonArc 2.6.16.