The Coq mailing list

[Adam Koprowski <adam.koprowski AT gmail.com>]

(*
   Dear all,

  I'm trying to define a setoid equality on vectors given a setoid

equality on vector elements. However, I'm having troubles properly
declaring morphisms for vector operations. It seems to me that the

problem has to do with declaring morphisms on dependently typed 
functions, however I'd appreciate a comment on whether I'm doing 

something wrong or just hitting a setoid limitation and if so, whether
there is a work-around. Let me illustrate what I have in mind on a 

simple example.
*)

(* Small setup *)
Require Import Bvector Setoid SetoidClass.

Set Implicit Arguments.
Implicit Arguments Vnil [A].

(* Few required functions; let's make them axioms to make it shorter *)

 (* Vnth [v_1,...v_n] i = v_i *)
Axiom Vnth : forall A n, vector A n -> forall i (ip : i < n), A.

 (* Vforall2 P vl vr <-> P vl_1 vr_1 /\ ... /\ P vl_n vr_n *)
Axiom Vforall2 : forall A n, (A -> A -> Prop) -> relation (vector A n).

(* Definition of setoid equality on vectors *)
Section eq_vec.

  Variables (A : Type) (eqA : Setoid A) (n : nat).


  (* ... as a point-wise equality on its elements *)
  Definition eq_vec : relation (vector A n) := @Vforall2 A n equiv.

  Axiom eq_vec_refl : Reflexive eq_vec.
  Axiom eq_vec_sym : Symmetric eq_vec.

  Axiom eq_vec_trans : Transitive eq_vec.

End eq_vec.

(* Let's declare this equality as a relation *)
Add Parametric Relation n A eqA : (vector A n) (@eq_vec A eqA n)

  reflexivity proved by (@eq_vec_refl A eqA n)
  symmetry proved by (@eq_vec_sym A eqA n)

  transitivity proved by (@eq_vec_trans A eqA n)
    as eq_vec_morphA.

(* Setoid equality on [A] yields a setoid on [vector A] *)
(* [?] Do we need to declare both the relation and a type-class instance?

       If I omit this declaration then the constraints for the following 
       parametric morhism fail... *)

Program Instance vec_equality `(eqA : Setoid A) : Setoid (vector A n) :=
  { equiv := @eq_vec A eqA n; setoid_equiv := _ }.

Next Obligation.
Proof.

  constructor. 
  apply eq_vec_refl.

  apply eq_vec_sym.
  apply eq_vec_trans.

Defined.

(* Now, let's declare [Vnth] as a morphism *)

Add Parametric Morphism A (eqA : Setoid A) n i (ip : i < n) : (fun v => Vnth v ip)
  with signature equiv ==> equiv

    as Vnth_morph.
Proof. Admitted.

(* and test it *)
Lemma test n x y i (ip : i < n) : x == y -> Vnth x ip == Vnth y ip.

Proof.
  intros. 

   (* Why does [rewrite H] fail here?... *)
  (*rewrite H. *)

   (* even though it's a morphism instance? *)
  apply Vnth_morph. assumption.

Qed.

(* If we swap arguments of [Vnth] as follows: *)

Axiom Vnth' : forall A n i (ip : i < n), vector A n -> A.

(* and declare appropriate morphism *)
Add Parametric Morphism A (eqA : Setoid A) n i (ip : i < n) : (Vnth' ip)
  with signature equiv ==> equiv

    as Vnth'_morph.
Proof. Admitted.

(* then everything works just fine... *)
Lemma test' n x y i (ip : i < n) : x == y -> Vnth' ip x == Vnth' ip y.

Proof.
  intros. rewrite H. reflexivity.

Qed.

(* 
   Thank you for help. 
    Cheers,

     Adam
*)

-- 
=====================================================

Adam.Koprowski AT gmail.com, http://www.cs.ru.nl/~Adam.Koprowski

The difference between impossible and possible
lies in determination (Tommy Lasorda)

=====================================================