Yves Bertot (Jan 28 2022 at 12:58): 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 *)
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: Apr 20 2024 at 13:01 UTC