Rewriting with Morphisms

Sets.v

Require Export Setoid.
Require Export Relation_Definitions.

Section ASet.

Declare Scope aset_scope.
Delimit Scope aset_scope with aset. (* so that we can write term%aset *)

Open Scope aset_scope.

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.

Lemma eq_set_refl (s : nat -> Prop) : s ≡ s.
Proof.
    unfold eq_set. tauto.
Qed.

Lemma eq_set_sym (s1 s2 : nat -> Prop) : s1 ≡ s2 -> s2 ≡ s1.
Proof.
    unfold eq_set. intros. specialize (H i). split; tauto.
Qed.

Lemma eq_set_trans (s1 s2 s3 : nat -> Prop) : 
    s1 ≡ s2 -> s2 ≡ s3 -> s1 ≡ s3.
Proof.
    unfold eq_set. intros. specialize (H i). specialize (H0 i). tauto.
Qed.

(*
    This enables rewriting with the relation ≡
    For example,

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

*)

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

Sets2.v

Require Export Setoid.
Require Export Relation_Definitions.
Require Import Coq.Program.Basics.


Declare Scope aset_scope.
Delimit Scope aset_scope with aset. (* so that we can write term%aset *)

Open Scope aset_scope.

Definition In_set (i : nat) (s : nat -> Prop) : Prop :=
    s i.

Definition not_In_set (i : nat) (s : nat -> Prop) : Prop :=
    ~ In_set i s.

Notation "i ∈ s" := (In_set i s) (at level 70) : aset_scope.
Notation "i ∉ s" := (not_In_set i s) (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.

Lemma eq_set_refl (s : nat -> Prop) : s ≡ s.
Proof.
    unfold eq_set. tauto.
Qed.

Lemma eq_set_sym (s1 s2 : nat -> Prop) : s1 ≡ s2 -> s2 ≡ s1.
Proof.
    unfold eq_set. intros. specialize (H i). split; tauto.
Qed.

Lemma eq_set_trans (s1 s2 s3 : nat -> Prop) : 
    s1 ≡ s2 -> s2 ≡ s3 -> s1 ≡ s3.
Proof.
    unfold eq_set. intros. specialize (H i). specialize (H0 i). tauto.
Qed.

#[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_set)
    with signature eq ==> eq_set ==> iff
    as eq_set_morph.
Proof.
    unfold eq_set, In_set. firstorder.
Qed.

#[global] Add Morphism (not_In_set)
    with signature eq ==> eq_set ==> iff
    as not_In_set_morph.
Proof.
    unfold not_In_set, In_set. firstorder.
Qed.

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

Notation "s1 ⊆ s2" := (subset s1 s2) (at level 70) : aset_scope.

#[global] Add Morphism (In_set)
    with signature eq ==> subset ==> impl
    as In_set_subset.
Proof.
    unfold subset, In_set. firstorder.
Qed.

#[global] Add Morphism (not_In_set)
    with signature eq ==> subset --> impl
    as not_In_set_subset.
Proof.
    unfold subset, not_In_set, In_set. firstorder.
Qed.

Goal forall (a : nat) (s1 s2 : nat -> Prop),
    a ∈ s1 -> s1 ⊆ s2 -> a ∈ s2.
Proof.
    intros. now apply H0.
Qed.

Goal forall (a : nat) (s1 s2 : nat -> Prop),
    a ∉ s2 -> s1 ⊆ s2 -> a ∉ s1.
Proof.
    intros. Fail now apply H0.
Abort.