The Coq mailing list

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

(* 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/