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?

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

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`

.

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

ping @Théo Zimmermann to move this question.

Thank you very much Karl. I missed this stream.

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

@Andrey Klaus maybe you're looking for `UniqFinMixin`

? https://github.com/math-comp/math-comp/blob/master/mathcomp/ssreflect/fintype.v#L25

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.

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

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

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

As Ana pointed `seq_sub`

will give you the right fintype.

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

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

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

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

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

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

@Andrey Klaus that's the low level construction, you can just use the `seq_sub`

construction which will take care of that for you.

And should be a tad more resilient

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

It looks like seq_sub works for me.

but it looks like I understand something in wrong way

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

now I would like to call `onef`

`Eval compute in (onef 1).`

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

(deleted)

(deleted)

supposing `Definition xs := [::1]`

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)`

?

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

.

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.

[minor comment, no need to use `undup xs`

, seq_sub will take care of that]

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.

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

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

@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