How to use deriving to prove that a subtype of a choiceType which is not a finType is a finType?

[zunction]

I roughly understand from the surface (from here) that it throws an error if it does not satisfy the requirements for finType.

So i have a type that I have managed to successfully use deriving to prove it to be a choiceType. Using the record subtype functionality in mathcomp, I want to prove that this subtype is a finType using the following record type,

Record mysubtype (s : seq cT) := {val:> cT ; _ : contains s val == true}.

which says that I have a sequence of the choiceType, and it is subtype to mysubtype it is in s : seq cT. I understand that from choiceType onwards, the mixin for solely dependent on fK : cancel f f' as input to CanChoiceMixin or PcanChoiceMixin. I was thinking could my problem be solved by taking the fK proofs (that deriving has proven) and use it to derive the mixins for mysubtype to make it a finType.

Many thanks in advance!

[arthuraa]

I am not sure I fully understand your idea, but Math Comp has a generic seq_sub s of elements that belong to some sequence s. This type carries a canonical finType structure, so you can write code like this:

From mathcomp Require Import all_ssreflect.
From void Require Import void.
From deriving Require Import deriving.

(* Potentially infinite type *)
Inductive tree T :=
| Leaf : T -> tree T
| Node : tree T -> tree T -> tree T.

Definition tree_indMixin T := [indMixin for tree_rect T].
Canonical tree_indType T := IndType _ (tree T) (tree_indMixin T).
Definition tree_eqMixin (T : eqType) :=
  [derive eqMixin for tree T].
Canonical tree_eqType (T : eqType) :=
  EqType (tree T) (tree_eqMixin T).
Definition tree_choiceMixin (T : choiceType) :=
  [derive choiceMixin for tree T].
Canonical tree_choiceType (T : choiceType) :=
  ChoiceType (tree T) (tree_choiceMixin T).
Definition tree_countMixin (T : countType) :=
  [derive countMixin for tree T].
Canonical tree_countType (T : countType) :=
  CountType (tree T) (tree_countMixin T).

(* Some finite subtype of it *)
Check fun (T : choiceType) (x : T) =>
  [finType of seq_sub [:: Leaf _ x]].

The cancellation proof that you obtain from deriving wouldn't be of much use in a case like this, because the encoding is done in terms of the GenTree.tree type in choice, which is infinite.

[zunction]

seq_sub seems like a good suggestion. But from what I read from here it will construct the sequence of terms to belong to another type.

And yes, I also realised that the cancellation proofs are not helpful for proving of finTypes.

Sorry for asking questions that are not related to deriving, but how does this approach differ from the usual finType?

[arthuraa]

Yes, sub_seq does create another type. Its purpose is not to show that a finite type is indeed finite, but to restrict a potentially infinite type (e.g. the tree type above) to a finite number of elements, so that this restriction can be shown to be a finType.

If you have an inductive type without type dependency or recursion, then Deriving should be able to construct a finType instance. In this case, seq_sub is not necessary.

If you still have questions related to this, I suggest you go to the Coq mailing list or ask a question on Stack Overflow, as more people will be able to help you. If you provide a link to your development, it'll be easier to understand what your problem is.