The Coq mailing list

[Dan Dougherty <dougherty.dan AT gmail.com>]

I should have said more in my original post.  I have tried
(essentially) what Pierre suggested, and several other things that
ought to work in the sense that they made sense semantically.  And
having proved various compatibility lemmas, I can _apply_ them and get
the results I need.  But when I want to declare a parametric morphism
and _rewrite_ then I get the infamous setoid rewrite error.

My impression that my problem is to find a way to fit a natural
compatibility result and ensuing morphism declaration into a format
that generalized rewriting will accept.

thanks in advance for any help.

Dan

On Fri, Mar 15, 2019 at 5:10 AM Pierre Courtieu
<pierre.courtieu AT gmail.com>
 wrote:
>
> I guess you need to define a relation for the list of terms. Something like:
>
> C1: eqv x x’ -> like x::l == x’::l
> C2:l ==l’ -> x::l ==x::l’
> Ctrans: ...
>
> P
>
> Le ven. 15 mars 2019 à 07:59, Dan Dougherty 
> <dougherty.dan AT gmail.com>
>  a écrit :
>>
>> (* Hi all,
>>
>> I'm having trouble setting up a generalized (setoid) rewriting
>> mechanism.  A simplified version of my setting is as follows.
>>
>> I'm working with first order terms and an inductive relation defining
>> provable equality based on some axioms, and I want to be able to
>> rewrite modulo that relation.  All is straightforward if I define
>> terms using the function symbols as constructors (see the second
>> snippet) but I'd prefer to define terms more generally using the first
>> "term" definition below.
>>
>> My question is, how can I define a parametric morphism, analogous to
>> what is done for A' and Lemma ok in the latter snippet, that allows
>> rewriting to succeed in Lemma not_ok?
>>
>> thanks in advance,
>> Dan
>> *)
>> Require Export List.
>> Export ListNotations.
>> Require Export Setoid.
>> Require Export SetoidClass.
>> Require Export Morphisms.
>>
>> Inductive FunSym : Type := A | M.
>>
>> Inductive term: Type :=
>> | V : nat -> term
>> | T : FunSym -> list term -> term .
>>
>> Inductive eqv : term -> term -> Prop :=
>>  (* some equations ...*)
>>
>> | eqv_ref:   forall x,  eqv x x
>> | eqv_sym:   forall x y,  eqv x y -> eqv y x
>> | eqv_trans: forall x y z,  eqv x y -> eqv y z -> eqv x z
>>
>> | A_compat : forall x x' ,
>>     eqv x x' -> forall y y' ,
>>     eqv y y' -> eqv (T A [x ; y] ) (T A [x' ;  y']).
>> Hint Constructors eqv.
>>
>> Add Parametric Relation  : term eqv
>>     reflexivity proved by @eqv_ref
>>     symmetry proved by @eqv_sym
>>     transitivity proved by @eqv_trans
>>       as eqv_rel.
>>
>> (* MY QUESTION: how to add some parametric morphism so that rewrites
>> like the following succeed? *)
>>
>> Lemma not_ok : forall x x' y,
>>   eqv x x' ->
>>   eqv (T A [x;y]) (T A [x'; y]).
>> Proof.
>>   intros x x' y H.
>>   try rewrite H.
>> Abort.
>>
>> (* ********* below works fine ****************** *)
>>
>> Inductive term' : Type :=
>> | V' : nat -> term'
>> | A'  :  term' -> term' -> term' .
>>
>> Inductive eqv' : term' -> term' -> Prop :=
>>  (* some equations ...*)
>>
>> | eqv'_ref:   forall x,  eqv' x x
>> | eqv'_sym:   forall x y,  eqv' x y -> eqv' y x
>> | eqv'_trans: forall x y z,  eqv' x y -> eqv' y z -> eqv' x z
>>
>> | A'_compat : forall x x' ,
>>     eqv' x x' -> forall y y' ,
>>     eqv' y y' -> eqv' (A' x y) (A' x' y').
>> Hint Constructors eqv'.
>>
>> Add Parametric Relation  : term' eqv'
>>     reflexivity proved by @eqv'_ref
>>     symmetry proved by @eqv'_sym
>>     transitivity proved by @eqv'_trans
>>       as eqv'_rel.
>>
>> Add Parametric Morphism : A' with
>>       signature eqv' ==> eqv' ==> eqv' as A'_mor.
>>   exact A'_compat.
>> Qed.
>>
>> Lemma ok : forall x x' y,
>>   eqv' x x' ->
>>   eqv' (A' x y) (A' x' y).
>> Proof.
>>   intros x x' y H.
>>   now rewrite H.
>> Qed.
>>
>>
>> --
>> Dan Dougherty
>> 231 Fuller Labs
>> Worcester Polytechnic Institute
>>
>> WPI Department of Computer Science:
>>     http://web.cs.wpi.edu/~dd/
>> Ombuds:
>>     http://www.wpi.edu/offices/ombuds/



-- 
Dan Dougherty
231 Fuller Labs
Worcester Polytechnic Institute

WPI Department of Computer Science:
    http://web.cs.wpi.edu/~dd/
Ombuds:
    http://www.wpi.edu/offices/ombuds/