Stream: math-comp users

Topic: create finType from unique seq


view this post on Zulip Andrey Klaus (Oct 14 2021 at 13:48):

Hello. I would like to create finType from construction undup xs where xs : seq eqType. Do I understand right that I need map xs to 'I_(size xs) and back? Is there another ('standard') way?

view this post on Zulip Ana de Almeida Borges (Oct 14 2021 at 14:52):

Is this what you are looking for?

seq_sub s == the subType of all x \in s, where s : seq T for some
                       eqType T; seq_sub s has a canonical finType instance
                       when T is a choiceType.

view this post on Zulip Andrey Klaus (Oct 14 2021 at 15:40):

Thank you. It looks similar to what I need, but i'm not sure I understand how to use it. What I would like to have in result is finite function from seq nat to bool.

view this post on Zulip Karl Palmskog (Oct 14 2021 at 15:42):

this is in fact a question about MathComp, not ssreflect specifically. Please use the #math-comp users stream for these kinds of questions.

view this post on Zulip Karl Palmskog (Oct 14 2021 at 15:42):

ping @Théo Zimmermann to move this question.

view this post on Zulip Andrey Klaus (Oct 14 2021 at 15:42):

Thank you very much Karl. I missed this stream.

view this post on Zulip Notification Bot (Oct 14 2021 at 15:42):

This topic was moved here from #Coq users > [ssreflect] create finType from unique seq by Théo Zimmermann

view this post on Zulip Karl Palmskog (Oct 14 2021 at 15:54):

@Andrey Klaus maybe you're looking for UniqFinMixin? https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fintype.v#L25

view this post on Zulip Andrey Klaus (Oct 14 2021 at 15:54):

so, I need to use Finite.Mixin. for it I need Finite.axiom, which is

fun (T : eqType) (e : seq T) => forall x : T, count_mem x e = 1
     : forall T : eqType, seq T -> Prop

So, speaking roughly, it is what undup provides.

view this post on Zulip Andrey Klaus (Oct 14 2021 at 15:57):

@Karl Palmskog, thanks again. I saw it, but i'm not sure I see how to use it.

view this post on Zulip Karl Palmskog (Oct 14 2021 at 15:59):

one interpretation of the documentation is that to generate a finType from a list e, you need to prove uniq e and e =i xpredT. The lemma undup_uniq probably helps with the former.

view this post on Zulip Andrey Klaus (Oct 14 2021 at 16:01):

yes, thank you

view this post on Zulip Karl Palmskog (Oct 14 2021 at 16:01):

see page 146 in the MathComp book: https://zenodo.org/record/4457887

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 16:01):

As Ana pointed seq_sub will give you the right fintype.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 16:02):

Definition colors := seq_sub [:: 0; 1; 2].
Definition color_set := {set colors}.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 16:03):

colors is here a type, you can trigger its resolution for the fintype with the usual [finType of colors] if you gonna need it [you shouldn't tho]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 16:06):

Proofs are as usual tho sometimes you wanna do some low-level stuff:

view this post on Zulip Emilio Jesús Gallego Arias (Oct 14 2021 at 16:06):

Definition colors := seq_sub [:: 0; 1; 2].

Lemma foo (x : colors) : [|| val x == 0, val x == 1 | val x == 2].
Proof. by case: x => //= x; rewrite !inE. Qed.

view this post on Zulip Andrey Klaus (Oct 15 2021 at 06:40):

@Karl Palmskog, UniqFinMixin works great. What I was confused with is

Definition fmx := (@UniqFinMixin _ (undup xs) (undup_uniq xs) _).
Error:
The following term contains unresolved implicit arguments:
  (UniqFinMixin (undup_uniq xs) ?eT)
More precisely:
- ?eT: Cannot infer this placeholder of type "undup xs =i nat_countType".

but this one just magically works...

Definition fmx := (UniqFinMixin (undup_uniq xs)).

So, thanks again.

view this post on Zulip Andrey Klaus (Oct 15 2021 at 06:57):

@Ana de Almeida Borges , @Emilio Jesús Gallego Arias , thank you very much. seq_sub works for me too.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2021 at 08:00):

@Andrey Klaus that's the low level construction, you can just use the seq_sub construction which will take care of that for you.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2021 at 08:00):

And should be a tad more resilient

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:07):

@Emilio Jesús Gallego Arias, thank you for your comment. Yes, I can see that UniqFinMixin is a bit low lowel.

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:08):

It looks like seq_sub works for me.

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:09):

but it looks like I understand something in wrong way

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:09):

Definition ftxs := [finType of subxs].
Definition ftype := {ffun ftxs -> bool}.
Definition onef := [ffun v => false] : ftype.

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:09):

now I would like to call onef

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:10):

Eval compute in (onef 1).

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:10):

Error: The term "1" has type "nat" while it is expected to have type "Equality.sort ftxs".

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:11):

(deleted)

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:13):

(deleted)

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:14):

supposing Definition xs := [::1]

view this post on Zulip Andrey Klaus (Oct 15 2021 at 08:39):

I think a bit better version is

Definition xs := [::1] : seq nat.
Definition subxs := seq_sub (undup xs).
Definition ftype := {ffun subxs -> bool}.
Definition onef := [ffun v => false] : ftype.

so, the question : how to call onef (head xs) ?

view this post on Zulip Ana de Almeida Borges (Oct 15 2021 at 10:01):

Error: The term "1" has type "nat" while it is expected to have type "Equality.sort ftxs".

We can agree that 1 : nat. The confusion here is that onef expects an input of type subxs (using the terminology of your latter example), not an input of type nat. In order to obtain an element of type subxs, you need both a "raw" term (in this case 1) and a proof that this term is a member of xs. So if you have inxs1 : 1 \in xs, you can write SubSeq inxs1 : subxs. This is similar to what happens with 'I_n, where the expression 0 : 'I_1 is not correct, but if you have lt01 : 0 < 1, you can write Ordinal lt01 : 'I_1.

view this post on Zulip Ana de Almeida Borges (Oct 15 2021 at 10:03):

Unfortunately, Eval compute in (onef (SeqSub inxs1)). doesn't give me anything interesting. I don't think sub_seq was defined with computation as a goal.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2021 at 10:08):

[minor comment, no need to use undup xs , seq_sub will take care of that]

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2021 at 10:09):

Indeed, there are two use cases, depending on whether you want to compute or not; recall that a bit the idea in math-comp is that you can work with the plain seq representation as a base level, and recover for example the ffun structure when you need it for a proof.

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2021 at 10:10):

That being said, an element of subxs is a proof of x \in xs as @Ana de Almeida Borges pointed out, so the usual way to build such objects easily is to have a cast

view this post on Zulip Emilio Jesús Gallego Arias (Oct 15 2021 at 10:13):

Definition xs := [::1] : seq nat.
Definition subxs := seq_sub xs.
Definition x0 : subxs := @SeqSub _ xs 1 erefl.
Definition ftype := {ffun subxs -> bool}.
Definition onef := [ffun v => false] : ftype.
Lemma ex : onef (insubd x0 1) = false.
Proof. by rewrite ffunE. Qed.

view this post on Zulip Andrey Klaus (Oct 15 2021 at 10:27):

@Ana de Almeida Borges, @Emilio Jesús Gallego Arias thank you very much for the answers.


Last updated: Oct 13 2024 at 01:02 UTC