Stream: math-comp users

Topic: ✔ wrong display of list membership

Yves Bertot (Jan 28 2022 at 12:58):

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.

Enrico Tassi (Jan 28 2022 at 13:41):

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 *)

Enrico Tassi (Jan 28 2022 at 13:43):

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

YAMAMOTO Mitsuharu (Jan 29 2022 at 05:42):

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.

Cyril Cohen (Jan 29 2022 at 15:30):

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.

Enrico Tassi (Jan 29 2022 at 17:25):

So when is the lemla I found needed?

Notification Bot (Feb 10 2022 at 10:04):

Yves Bertot has marked this topic as resolved.

Last updated: Oct 13 2024 at 01:02 UTC