Stream: math-comp users

Topic: ✔ wrong display of list membership


view this post on Zulip 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.

view this post on Zulip 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 *)

view this post on Zulip Enrico Tassi (Jan 28 2022 at 13:43):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Enrico Tassi (Jan 29 2022 at 17:25):

So when is the lemla I found needed?

view this post on Zulip Notification Bot (Feb 10 2022 at 10:04):

Yves Bertot has marked this topic as resolved.


Last updated: Jan 29 2023 at 18:03 UTC