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: Oct 13 2024 at 01:02 UTC