Hello, in the following example, I end up with a goal that does not have the right form:

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section sandbox.
Variables (E : eqType) (r : rel E) (p : pred E) (f : E -> E).
Lemma question s c :
{in rcons s c & &, transitive r} ->
sorted r [seq i <- s | p i].
Proof.
intros e_trans.
apply : (sorted_filter_in e_trans).
apply/allP=> x xin.
change (x \in rcons s c).
```

The last lines shows that the goal just before is convertible with what I would like to see, but I would like to know which tactic would have the same effect without requiring me to type the contents of the goal.

I never really mastered *mem*, so maybe this is not the way... but seems to work.

```
From mathcomp Require Import all_ssreflect.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Section sandbox.
Variables (E : eqType) (r : rel E) (p : pred E) (f : E -> E).
(* NEW: x \in [mem s] === (pred_of_seq s) x via app_predE *)
Canonical xxx (T : eqType) (s : seq T) :=
@RegisteredApplicativePred _ [mem s] (pred_of_seq s) (erefl _).
Lemma question s c :
{in rcons s c & &, transitive r} ->
sorted r [seq i <- s | p i].
Proof.
intros e_trans.
apply : (sorted_filter_in e_trans).
apply/allP=> x xin.
rewrite app_predE. (* ap x = x \in p for registered_applicative_predicate p *)
```

I mean, since this CS is not there, I suspect there is another, simpler, way.

Maybe `rewrite topredE`

? The file ssrbool.v has the following comment:

Users should take care not to inadvertently "strip" (mem A) down to the

coerced A, since this will expose the internal toP coercion: Coq could then

display terms A x that cannot be typed as such. The topredE lemma can be used

to restore the x \in A syntax in this case.

YAMAMOTO Mitsuharu said:

Maybe

`rewrite topredE`

? The file ssrbool.v has the following comment:Users should take care not to inadvertently "strip" (mem A) down to the

coerced A, since this will expose the internal toP coercion: Coq could then

display terms A x that cannot be typed as such. The topredE lemma can be used

to restore the x \in A syntax in this case.

Indeed, `rewrite /= topredE`

to be precise.

So when is the lemla I found needed?

Yves Bertot has marked this topic as resolved.

Last updated: Sep 25 2023 at 12:01 UTC