## Stream: math-comp users

### Topic: create finType from unique seq

#### 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?

#### 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.


#### 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.

#### 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.

#### Karl Palmskog (Oct 14 2021 at 15:42):

ping @Théo Zimmermann to move this question.

#### Andrey Klaus (Oct 14 2021 at 15:42):

Thank you very much Karl. I missed this stream.

#### 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

#### 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

#### 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.

#### 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.

#### 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.

yes, thank you

#### Karl Palmskog (Oct 14 2021 at 16:01):

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

#### Emilio Jesús Gallego Arias (Oct 14 2021 at 16:01):

As Ana pointed seq_sub will give you the right fintype.

#### Emilio Jesús Gallego Arias (Oct 14 2021 at 16:02):

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


#### 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]

#### Emilio Jesús Gallego Arias (Oct 14 2021 at 16:06):

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

#### 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.


#### 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.

#### 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.

#### 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.

#### Emilio Jesús Gallego Arias (Oct 15 2021 at 08:00):

And should be a tad more resilient

#### 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.

#### Andrey Klaus (Oct 15 2021 at 08:08):

It looks like seq_sub works for me.

#### Andrey Klaus (Oct 15 2021 at 08:09):

but it looks like I understand something in wrong way

#### Andrey Klaus (Oct 15 2021 at 08:09):

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


#### Andrey Klaus (Oct 15 2021 at 08:09):

now I would like to call onef

#### Andrey Klaus (Oct 15 2021 at 08:10):

Eval compute in (onef 1).

#### 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".

(deleted)

(deleted)

#### Andrey Klaus (Oct 15 2021 at 08:14):

supposing Definition xs := [::1]

#### 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) ?

#### 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.

#### 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.

#### 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]

#### 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.

#### 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

#### 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.


#### 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: Feb 08 2023 at 04:04 UTC