Okay, I think that should cover everything you mentioned?

**sarahzrf**
(8f98c736)
*
at
18 Jun 19:12
*

Minor style tweaks

`simpl`

doesn't expand `filter`

properly here; `cbn`

does (well, it's `fmap`

that `simpl`

mangles in the second use of `cbn`

). Maybe there's a flag I should be using?

I've added an instance `sig_finite`

along with a couple of minor things used to define/prove it. This is a `Finite`

instance for `sig`

s over `Finite`

types whose predicates are decidable and proof irrelevant:

```
(* Not a direct excerpt. *)
Context `{Finite A} (P : A → Prop) `{∀ x, Decision (P x)} `{∀ x, ProofIrrel (P x)}.
Global Instance sig_finite : Finite (sig P).
```

**sarahzrf**
(8962812c)
*
at
12 Jun 18:39
*

Added sig_finite (and elem_of_list_fmap_inj, proj1_inj_pi)

Also, would another alternative be to just define separate versions of `flip`

, etc, in stdpp? There's enough core stuff that uses definitions like those that fiddling with their evaluation and transparency behavior seems pretty questionable in general—is there a good reason to not just make your own overrides? I suppose it would create a ton of work to migrate every usage...

If the infrastructure is unreliable for you, it may be because of this exact issue :)

I don't have extensive experience with it myself, so I may be wrong, but—how much of you saying so is informed by projects that are working under this breakage?

The setoid rewriting mechanism uses a bunch of typeclass machinery to infer `Proper`

instances for the contexts being rewritten in, and it uses `flip`

to talk about contravariance. stdpp breaks its ability to infer lots of cases it ordinarily can, because it makes `flip`

typeclass transparent when the setoid rewriting mechanism is built with the assumption that it is typeclass opaque! In `base.v`

, we have:

`Typeclasses Transparent id compose flip const.`

This nullifies the effect of the very first non-comment non-import line of `Classes/Init.v`

in the Coq stdlib:

`Typeclasses Opaque id const flip compose arrow impl iff not all.`

Here's a minimal demonstration of the problems this causes:

```
From Coq Require Import ssreflect ssrfun ssrbool.
Require Import Morphisms.
Require Import PeanoNat.
Instance plus_proper_le : Proper (le ++> le ++> le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
Require Import stdpp.base.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
Fail setoid_rewrite <- H1 in H2 at 1.
Abort.
Section FlippedInstance.
(* Thus seemingly necessitating: *)
Local Instance plus_proper_le' : Proper (le --> le --> flip le) plus.
Proof. move=> n n' Le1 m m' Le2; by apply: Nat.add_le_mono. Qed.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
End FlippedInstance.
(* But alternatively: *)
Typeclasses Opaque flip.
Goal forall (n m o : nat), n <= m -> m + m <= o -> n + m <= o.
Proof.
move=> n m o H1 H2.
by setoid_rewrite <- H1 in H2 at 1.
Qed.
```