# How do I enable this kind of rewriting?

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?

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.

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

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

#[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.

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.