Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Confusing error rewriting by impl with result in propositional with parameter

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





Archive powered by MhonArc 2.6.16.

Top of Page