The Coq mailing list

[Arthur Azevedo de Amorim <arthur.aa AT gmail.com>]

Ok, here are the basic definitions

Require Export Relation_Definitions.
Require Import Setoid.

Set Implicit Arguments.

Record Setoid : Type := {
  carrier :> Type;
  eq      :  relation carrier;

  IsEq    :  Equivalence eq
}.

Bind Scope Setoid_scope with Setoid.

Open Scope Setoid_scope.

Notation "A == B" := (eq _ A B) (at level 70, no associativity) : Setoid_scope.
Notation "A != B" := (~ A == B) (at level 70, no associativity) : Setoid_scope.

Hint Extern 0 (?X == ?X) => reflexivity.

Lemma reflS (S : Setoid) : Reflexive (eq S).
Proof. move => [? ? [? ? ?]]; auto. Qed.
Lemma symmS (S : Setoid) : Symmetric (eq S).
Proof. move => [? ? [? ? ?]]; auto. Qed.

Lemma trnsS (S : Setoid) : Transitive (eq S).
Proof. move => [? ? [? ? ?]]; auto. Qed.

Add Parametric Relation (S : Setoid) : S (eq S)
  reflexivity proved by (reflS S)
  symmetry proved by (symmS S)

  transitivity proved by (trnsS S)
  as eq_rel.

Require Import ssreflect.
Set Implicit Arguments.

(* Some important setoids *)

Section FunctionSetoid.

Variable S T : Setoid.

Definition preserves (F : S -> T) :=

  forall (s1 s2 : S), s1 == s2 -> F s1 == F s2.

Record SetoidMap := {
  Map      :> S -> T;
  Map_pres :  preserves Map
}.

Definition map_equal (f g : SetoidMap) :=
  forall s, f s == g s.

Definition map_equal_is_equivalence : Equivalence map_equal.
  split.
  - by move => f s.
  - by move => f g h s; rewrite (h s).
  - by move => f g h e1 e2 s; rewrite -(e2 s); apply e1.
Defined.

Canonical Structure SetoidMapSetoid : Setoid.
  apply (Build_Setoid map_equal_is_equivalence).
Defined.

End FunctionSetoid.

Notation "A =>> B" := (SetoidMapSetoid A B) (at level 55, right associativity) : Setoid_scope.

Set Printing Coercions.

Add Parametric Morphism (A B : Setoid) (M : A =>> B) :
  M with signature ((@eq A) ==> (@eq B))
  as setoid_mor.
  Proof. by move: M => [? ?]. Qed.

(* ... *)

Now, I want to proof this:

Lemma L : forall (A B C : Setoid) (f : A =>> B =>> C) a1 a2 b, a1 == a2 -> f a1 b == f a2 b.
Proof. intros. (* ... *)

Doing "rewrite e" does not work, but "apply (Map_pres f)" does.

On Fri, Apr 24, 2009 at 9:44 AM, Arnaud Spiwack <Arnaud.Spiwack AT lix.polytechnique.fr> wrote:

Hello,

If I understand your question correctly it should be possible. Maybe you should post some code to make it clearer what are the precise circumstances of your troubles.

Arthur Azevedo de Amorim a écrit :

Hello,

I am having a problem using the new rewriting system in Coq 8.2. First, I declared a basic setoid record
with a carrier, a relation and a proof that this relation is an equivalence relation. Then I declared a new type
for maps between setoids (A =>> B), that have a function and a proof that it preserves equality. I added the equality
and these maps as relations and morphisms, and then added a canonical structure for seeing a setoid morphism
with a setoid structure. So far so good. The problem appears when I try to curry this scheme: if I have F : A =>> B =>> C,
I can't proof that a1 == a2 -> F a1 b == F a2 b unless I destruct F explicitly and apply the preservation lemma
it carries. Is there a way of doing this with a regular rewrite?

--
Arthur Azevedo de Amorim

-- 
Arthur Azevedo de Amorim