1
$\begingroup$

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?

$\endgroup$

1 Answer 1

3
$\begingroup$

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.
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.