Stream: math-comp users

Topic: [finmap] `fset_finpred` vs `fin_finpred`


view this post on Zulip Ana de Almeida Borges (Apr 06 2022 at 10:55):

I ran into one of those annoying cases where visually everything looks the same but after much digging it turns out it's different under the hood.

From mathcomp Require Import all_ssreflect finmap.

Section example.

Open Scope fset.

Variables (K : choiceType) (P : {fset K} -> Prop).

Lemma enum_fsetK (ks : {fset K}) :
  [fset k in enum_fset ks] = ks.
Proof.
  apply/fsetP => k; apply/imfsetP/idP => /=.
    by move=> [k' k'inks ->].
  by move=> kinks; exists k.
Qed.

Lemma fset_enum (ff : {fset K}) :
  P ff -> P [fset s in (enum_fset ff)].
Proof. by rewrite enum_fsetK. Qed.

(* So far so good. Now I want to use fset_enum in the wild... *)
Lemma Ps_seq (ff : {fset K}) :
  P ff -> exists (ss : seq K), P [fset s in ss].
Proof.
  move=> /fset_enum Pff.
  exists (enum_fset ff).
  Fail exact: Pff. (* ... but alas, this doesn't work *)
  set X := [fset _ in _] in Pff. (* X := [fset H in fset_finpred ff] : {fset K} *)
  set Y := [fset _ in _]. (* Y := [fset H in fin_finpred (pT:=seq_finpredType K) ff] : {fset K} *)
(* so indeed X and Y are different, although we can easily prove they are the same: *)
  suff <- : X = Y by [].
  by apply/fsetP => x; apply/imfsetP/imfsetP.
Qed.

End example.

Is there anything I can change in my definitions or my environment so that exact: Pff works?

view this post on Zulip Ana de Almeida Borges (Apr 06 2022 at 12:19):

For now I'm making do with

Lemma fin_fset_finpred (ff : {fset K}) :
  [fset f in fin_finpred (pT:=seq_finpredType K) ff]
    = [fset f in fset_finpred ff].
Proof. by apply/fsetP => f; apply/imfsetP/imfsetP. Qed.

every time this issue pops up, but it feels very hacky to me (because someone not in the know will just be puzzled about why I'm rewriting with it).


Last updated: Jan 29 2023 at 18:03 UTC