The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  you need an additional instance to solve the [subrelation (eq ==> R) 
(pointwise_relation A R)] 
constraint indeed, which you can declare like so:

Instance eq_sub A (R : relation A) B (R' : relation B) : 
  Reflexive R -> subrelation (R ==> R')%signature
                             (pointwise_relation A R')%signature.
Proof. intros Rrefl x y HR u; now apply HR. Defined.

  Not all « reasonable » instances like this are defined in the standard 
library, for lack of a 
general theory of which ones are « canonical » and behave well during proof 
search.

Best,
— Matthieu

Le 18 août 2014 à 21:51, Jason Gross 
<jasongross9 AT gmail.com>
 a écrit :

> Hi,
> I am trying to rewrite with [H : (R ==> S)%signature f g], and Coq doesn't 
> seem to want to do this.  It seems to be trying to prove that this is a 
> subrelation of [pointwise_relation _ S], and failing (regardless of whether 
> or not [R] is [Reflexive], or even [eq]).  How do I get Coq to allow me to 
> rewrite with such things (and why can't it do so already?).
> 
> Here is the relevant code:
> Require Import Coq.Setoids.Setoid Coq.Classes.Morphisms.
> Section foo.
>   Context A B (f g : A -> B) (R : relation B) (R' : relation A)
>           (H : (@eq _ ==> R)%signature f g)
>           (H' : (pointwise_relation _ R) f g)
>           (H'' : (R' ==> R)%signature f g)
>           `{@Reflexive _ R}
>           `{@Transitive _ R}
>           `{@Reflexive _ R'}.
>   Goal forall x, R (f x) (g x).
>   Proof.
>     intros.
>     Fail setoid_rewrite H. (* Error:
>    Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting 
> constraints.
>    Unable to satisfy the following constraints:
>    EVARS:
>     ?19==[A B f g R H H' H0 H1 x |- ProperProxy ?17 (g x)]
>            (internal placeholder)
>     ?18==[A B f g R H H' H0 H1 x (do_subrelation:=do_subrelation)
>            |- Proper (?14 ==> ?17 ==> Basics.flip Basics.impl) R]
>            (internal placeholder)
>     ?17==[A B f g R H H' H0 H1 x |- relation B] (internal placeholder)
>     ?15==[A B f g R H H' H0 H1 x
>            |- subrelation (eq ==> R) (pointwise_relation A ?14)]
>            (internal placeholder)
>     ?14==[A B f g R H H' H0 H1 x |- relation B] (internal placeholder) *)
>     setoid_rewrite H'.
>     Undo.
>     setoid_rewrite H''. (* Toplevel input, characters 0-18:
> Error:
> Tactic failure:setoid rewrite failed: Unable to satisfy the rewriting 
> constraints.
> Unable to satisfy the following constraints:
> EVARS:
>  ?34==[A B f g R R' H H' H'' H0 H1 H2 x |- ProperProxy ?32 (g x)]
>         (internal placeholder)
>  ?33==[A B f g R R' H H' H'' H0 H1 H2 x (do_subrelation:=do_subrelation)
>         |- Proper (?29 ==> ?32 ==> Basics.flip Basics.impl) R]
>         (internal placeholder)
>  ?32==[A B f g R R' H H' H'' H0 H1 H2 x |- relation B] (internal 
> placeholder)
>  ?30==[A B f g R R' H H' H'' H0 H1 H2 x
>         |- subrelation (R' ==> R) (pointwise_relation A ?29)]
>         (internal placeholder)
>  ?29==[A B f g R R' H H' H'' H0 H1 H2 x |- relation B] (internal 
> placeholder) *)
> 
> 
> Thanks,
> Jason