How do I enable this kind of rewriting?

Question

Link to Code Gist

Given two extensionally equal sets, s1 ≡ s2, I want to be able to obtain a ∈ s2 from a ∈ s1 using rewriting.

I want to enable an extensionality-style rewriting for unary predicates.

Notation "i ∈ s" := (s i) (at level 70) : aset_scope.

Definition eq_set (s1 s2 : nat -> Prop) : Prop :=
    forall i, i ∈ s1 <-> i ∈ s2.

Notation "s1 ≡ s2" := (eq_set s1 s2) (at level 70) : aset_scope.

#[global] Add Parametric Relation : (nat -> Prop) eq_set
    reflexivity proved by eq_set_refl
    symmetry proved by eq_set_sym
    transitivity proved by eq_set_trans
    as eq_set_rel.

#[global] Add Parametric Morphism : (fun i s => i ∈ s)
    with signature eq ==> eq_set ==> iff
    as eq_set_morph.
Proof.
    unfold eq_set. intros. 
    specialize (H y). assumption.
Qed.

This allows rewritings such as the following:

Goal forall s1 s2 s3 : nat -> Prop,
    s1 ≡ s2 -> s2 ≡ s3 -> s1 ≡ s3.
Proof.
        intros. rewrite H, H0. reflexivity.
Qed.

However, I can't seem to be able to perform rewrites like the following:

Goal forall (a : nat) (s1 s2 : nat -> Prop),
    a ∈ s1 -> s1 ≡ s2 -> a ∈ s2.
Proof.
    intros. Fail (rewrite H0 in H). Fail (setoid_rewrite H0 in H).
Abort.

How do I enable this? Is there a module in the Standard Library which already has these definitions?

Answer 1

In order to add a Morphism, your function needs a name. It can't just be an anonymous function. Below is a minimal working example.

From Coq Require Import Setoid Utf8 Ensembles.

Declare Scope aset_scope.
Open Scope aset_scope.

Notation "i ∈ s" := (In nat s i) (at level 70) : aset_scope.

Definition eq_set (s1 s2 : nat -> Prop) : Prop :=
    forall i, i ∈ s1 <-> i ∈ s2.

Notation "s1 ≡ s2" := (eq_set s1 s2) (at level 70) : aset_scope.

Theorem eq_set_refl : ∀ a : nat → Prop, a ≡ a.
Proof.
Admitted.

Theorem eq_set_sym : ∀ a b : nat → Prop, a ≡ b → b ≡ a.
Proof.
Admitted.

Theorem eq_set_trans : ∀ a b c : nat → Prop, a ≡ b → b ≡ c → a ≡ c.
Proof.
Admitted.

#[global] Add Parametric Relation : (nat -> Prop) eq_set
    reflexivity proved by eq_set_refl
    symmetry proved by eq_set_sym
    transitivity proved by eq_set_trans
    as eq_set_rel.

#[global] Add Morphism (In nat)
    with signature eq_set ==> eq ==> iff
    as eq_set_morph.
Proof.
    unfold eq_set. intros. 
    specialize (H y0). assumption.
Qed.

Goal forall s1 s2 s3 : nat -> Prop,
    s1 ≡ s2 -> s2 ≡ s3 -> s1 ≡ s3.
Proof.
        intros. rewrite H, H0. reflexivity.
Qed.

Goal forall (a : nat) (s1 s2 : nat -> Prop),
    a ∈ s1 -> s1 ≡ s2 -> a ∈ s2.
Proof.
  intros.
  now rewrite H0 in H.
Qed.