## Stream: math-comp users

### Topic: finType and card

#### Shengyi Wang (Oct 24 2022 at 14:48):

I'm a newbie in mathcomp. I followed the Section 8.5 of the Mathematical Components book, defined an inductive type and linked it to the theory of finType via `PcanXXXMixin` family of lemmas like this:

``````Inductive traficlight: predArgType := Red | Yellow | Green.

Definition trafic2ord (t: traficlight): 'I_3 :=
match t with
| Red => inord O | Yellow => inord 1 | Green => inord 2
end.

Definition ord2trafic (o: 'I_3): option traficlight :=
match val o with
| O => Some Red | 1 => Some Yellow | 2 => Some Green
| _ => None
end.

Lemma pcan_trafic_ord: pcancel trafic2ord ord2trafic.
Proof. by case; rewrite /ord2trafic /= inordK. Qed.

Definition traficlight_eqMixin := PcanEqMixin pcan_trafic_ord.
Canonical traficlight_eqType := EqType traficlight traficlight_eqMixin.
Definition traficlight_choiceMixin := PcanChoiceMixin pcan_trafic_ord.
Canonical traficlight_choiceType := ChoiceType traficlight traficlight_choiceMixin.
Definition traficlight_countMixin := PcanCountMixin pcan_trafic_ord.
Canonical traficlight_countType := CountType traficlight traficlight_countMixin.
Definition traficlight_finMixin := PcanFinMixin pcan_trafic_ord.
Canonical traficlight_finType := FinType traficlight traficlight_finMixin.

Check (Red != Yellow) && (Red \in traficlight) && (#| traficlight | == 3).
``````

Everything looks fine until I tried to prove some simple fact: `Goal #| traficlight | == 3.` The tactic like `by rewrite cardT enumT unlock.` does not work. Any suggestions? Thank you very much.

#### Karl Palmskog (Oct 24 2022 at 14:54):

sorry for a probably-not-what-you-want solution, but all these canonical instances should be generatable from only the inductive type by Deriving: https://github.com/arthuraa/deriving

.. which may also make solving the goal easier.

#### Shengyi Wang (Oct 24 2022 at 15:02):

I see. Thank you. From the README of Deriving, it seems that I still need to write a bunch of XXX_xxMixin and XXX_xxType. But I don't need to write the 1-to-1 mapping functions, right?

#### Karl Palmskog (Oct 24 2022 at 15:03):

right, you can skip that boilerplate. I think the other boilerplate can be lessened somewhat by using Hierarchy builder

#### Shengyi Wang (Oct 24 2022 at 15:09):

Thank you again! There are so many excellent math-comp related packages to learn. I definitely will put them in my TODO list. Let me try to get familiar with the basis of math-comp first, like proving this first simple fact.

#### Ana de Almeida Borges (Oct 24 2022 at 15:54):

I've been trying to prove your lemma and I also can't figure it out. My solution is to define the fin mixin in a different way:

``````Lemma traficlight_fin : Finite.axiom [:: Red; Yellow; Green].
Proof. by case. Qed.

Definition traficlight_finMixin := FinMixin traficlight_fin.
Canonical traficlight_finType := FinType traficlight traficlight_finMixin.

Goal #|traficlight| == 3.
Proof. by rewrite cardT enumT unlock. Qed.
``````

I'm sure there must be a way of doing it with your encoding though.

PS: It's spelled "traffic", with two f.

#### Shengyi Wang (Oct 24 2022 at 16:03):

Thank you very much! Sorry for the typo :smile: .

#### Shengyi Wang (Oct 24 2022 at 16:19):

Hi @Ana de Almeida Borges , I tried you code but I can not even go through the second line `by case.` Did you also define eq mixin in a different way?

#### Ana de Almeida Borges (Oct 24 2022 at 16:26):

Oh, sorry, yes I did. I was trying alternative encodings and forgot I hadn't changed it back. Here is the one I used:

``````Definition trafic2ord (t: traficlight): 'I_3 :=
match t with
| Red => @Ordinal 3 0 isT
| Yellow => @Ordinal 3 1 isT
| Green => @Ordinal 3 2 isT
end.

Definition ord2trafic (o: 'I_3): traficlight :=
match val o with
| O => Red | 1 => Yellow | 2 => Green
| _ => Red
end.

Lemma pcan_trafic_ord: cancel trafic2ord ord2trafic.
Proof. by case. Qed.
``````

#### Ana de Almeida Borges (Oct 24 2022 at 16:28):

And then since I used `cancel` instead of `pcancel`, I also changed `PcanXMixin` to `CanXMixin`

#### Shengyi Wang (Oct 24 2022 at 16:31):

Thank you so much! Now I'm considering define all those kind of Mixin and xxType directly by the naive way. Just like bool etc in the library of ssreflect.

#### Ana de Almeida Borges (Oct 24 2022 at 16:33):

You can also prove it with your encoding, it just needs a little more work:

``````Lemma traficlight_fin : Finite.axiom [:: Red; Yellow; Green].
Proof. by case=> /=; do 3!case: eqP. Qed.
``````

#### Ana de Almeida Borges (Oct 24 2022 at 16:34):

That seems strictly worse than defining everything up to `countType` your way and then defining `finType` manually (I mean, you already have it, so no extra work).

#### Ana de Almeida Borges (Oct 24 2022 at 16:35):

Still, maybe someone more knowledgeable will show up and answer your original question.

#### Shengyi Wang (Oct 24 2022 at 16:41):

Great! Thank you very much for all the help!

Last updated: Jan 29 2023 at 18:03 UTC