The Coq mailing list

[Brandon Moore <brandon_m_moore AT yahoo.com>]

----- Original Message -----
> From: Matthieu Sozeau 
>Â <mattam AT mattam.org>
> To: 
>Â brandon_m_moore AT yahoo.com
> Cc: 
>Â coq-club AT inria.fr
> Sent: Tuesday, June 7, 2011 7:09 AM
> Subject: Re: [Coq-Club] Confusing error rewriting by impl with result in 
> propositional with parameter
> 
> 
> 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]).

Thanks for the quick fix.

What is wrong with making impl opaque? It seems to work
in small examples.

> 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.

I'm already proving all the lemmas I want to rewrite by,
so it should be easy to switch to this.

Brandon