The Coq mailing list

[Pierre Courtieu <pierre.courtieu AT gmail.com>]

You must declare enough morphisms so that you can rewrite under "T",
and also under "cons". In this case you need a relation on lists to be
able to do that.

The solution below 1) defines a relation eqvl on lists, 2) declares
cons as a morphis 3) declares T as amorphism. I think the proofs left
admitted should be straightforward.

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

Inductive eqvl : list term -> list term -> Prop :=
  eqvl1: eqvl nil nil
| eqqvl2: forall x x' l l', eqv x x' -> eqvl l l' -> eqvl (x::l) (x'::l').

Hint Constructors eqvl.


Add Parametric Relation  : term eqv
    reflexivity proved by @eqv_ref
    symmetry proved by @eqv_sym
    transitivity proved by @eqv_trans
      as eqv_rel.

Lemma eqvl_ref: reflexive _ eqvl.
Admitted.

Lemma eqvl_sym: symmetric _ eqvl.
Admitted.

Lemma eqvl_trans: transitive _ eqvl.
Admitted.


Add Parametric Relation  : (list term) eqvl
    reflexivity proved by @eqvl_ref
    symmetry proved by @eqvl_sym
    transitivity proved by @eqvl_trans
      as eqvl_rel.


Add Parametric Morphism : T with
      signature eq ==> eqvl ==> eqv as T_mor.
Admitted.

Add Parametric Morphism : cons with
      signature eqv ==> eqvl ==> eqvl as cons_mor.
Admitted.


(* 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.
  rewrite H.
Abort.

Le dim. 17 mars 2019 à 19:41, Dan Dougherty 
<dougherty.dan AT gmail.com>
 a écrit :
>
> 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/