The Coq mailing list

[Matthieu Sozeau <mattam AT mattam.org>]

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