Rewriting/Applying unidirectional morphisms in Coq

Question

Link to Code Gist

I have the following definition

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

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

I want Coq to notice that a ∈ s1 -> s1 ⊆ s2 -> a ∈ s2 and a ∉ s2 -> s1 ⊆ s2 -> a ∉ s1. To do this, I introduce the following morphisms:

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

However, while Coq recognizes the first chain of reasoning, it doesn't recognize the second one.

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.

What is the right way to do this kind of reasoning with tactics and morphsims? (other than using the names of the actual lemmas manually)

Answer 1

Morphisms only affect rewrite, not apply.

The following does work, and makes use of the not_In_set_subset morphism:

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

The fact that apply works in the first example is just a coincidence, having nothing to do with the Morphism. In fact you could delete all the Morphisms and apply would still work in the first example.